1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006, Adam Chlipala
4 * This program is free software
; you can redistribute it
and/or
5 * modify it under the terms
of the GNU General Public License
6 * as published by the Free Software Foundation
; either version
2
7 * of the License
, or (at your option
) any later version
.
9 * This program is distributed
in the hope that it will be useful
,
10 * but WITHOUT ANY WARRANTY
; without even the implied warranty
of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE
. See the
12 * GNU General Public License for more details
.
14 * You should have received a copy
of the GNU General Public License
15 * along
with this program
; if not
, write to the Free Software
16 * Foundation
, Inc
., 51 Franklin Street
, Fifth Floor
, Boston
, MA
02110-1301, USA
.
19 (* Evaluation
of expressions until only externs are around
*)
21 structure Reduce
:> REDUCE
= struct
25 structure SM
= StringMap
31 | EList es
=> List.exists (freeIn x
) es
33 |
ELam (x
', _
, b
') => x
<> x
' andalso freeIn x b
'
35 |
EApp (e1
, e2
) => freeIn x e1
orelse freeIn x e2
38 |
ESet (_
, e
) => freeIn x e
39 |
EGet (x
', _
, b
') => x
<> x
' andalso freeIn x b
'
40 | ESeq es
=> List.exists (freeIn x
) es
41 |
ELocal (e1
, e2
) => freeIn x e1
orelse freeIn x e2
42 |
EWith (e1
, e2
) => freeIn x e1
orelse freeIn x e2
43 |
EALam (x
', _
, b
') => x
<> x
' andalso freeIn x b
'
46 val freshCount
= ref
0
57 fun subst x
e (bAll
as (b
, loc
)) =
61 | EList es
=> (EList (map (subst x e
) es
), loc
)
63 |
ELam (x
', to
, b
') =>
66 else if freeIn x
' e
then
70 (ELam (x
'', to
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
73 (ELam (x
', to
, subst x e b
'), loc
)
79 |
EApp (b1
, b2
) => (EApp (subst x e b1
, subst x e b2
), loc
)
82 |
ESet (v
, b
) => (ESet (v
, subst x e b
), loc
)
86 else if freeIn x
' e
then
90 (EGet (x
'', v
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
93 (EGet (x
', v
, subst x e b
'), loc
)
94 | ESeq es
=> (ESeq (map (subst x e
) es
), loc
)
95 |
ELocal (b1
, b2
) => (ELocal (subst x e b1
, subst x e b2
), loc
)
96 |
EWith (b1
, b2
) => (EWith (subst x e b1
, subst x e b2
), loc
)
97 |
EALam (x
', p
, b
') =>
100 else if freeIn x
' e
then
102 val x
'' = freshVar ()
104 (EALam (x
'', p
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
107 (EALam (x
', p
, subst x e b
'), loc
)
109 fun reduceExp
G (eAll
as (e
, loc
)) =
113 | EList es
=> (EList (map (reduceExp G
) es
), loc
)
118 NONE
=> (Tycheck
.newUnif (), loc
)
121 val G
' = bindVal
G (x
, to
', NONE
)
123 (ELam (x
, to
, reduceExp G
' e
), loc
)
126 (case lookupEquation G x
of
128 | SOME e
=> reduceExp G e
)
131 val e1
' = reduceExp G e1
132 val e2
' = reduceExp G e2
135 (ELam (x
, _
, b
), _
) => reduceExp
G (subst x e2
' b
)
136 | _
=> (EApp (e1
', e2
'), loc
)
140 |
ESet (v
, b
) => (ESet (v
, reduceExp G b
), loc
)
141 |
EGet (x
, v
, b
) => (EGet (x
, v
, reduceExp G b
), loc
)
142 | ESeq es
=> (ESeq (map (reduceExp G
) es
), loc
)
143 |
ELocal (e1
, e2
) => (ELocal (reduceExp G e1
, reduceExp G e2
), loc
)
146 val e1
' = reduceExp G e1
147 val e2
' = reduceExp G e2
150 (EALam (x
, _
, b
), _
) => reduceExp
G (subst x e2
' b
)
151 | _
=> (EWith (e1
', e2
'), loc
)
155 val G
' = bindVal
G (x
, (TAction (p
, SM
.empty
, SM
.empty
), loc
), NONE
)
157 (EALam (x
, p
, reduceExp G
' e
), loc
)