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
)
83 |
EGet (x
', topt
, v
, b
') =>
86 else if freeIn x
' e
then
90 (EGet (x
'', topt
, v
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
93 (EGet (x
', topt
, 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 findPrim (e
, _
) =
114 |
SOME (f
, xs
) => SOME (f
, xs @
[x
]))
115 | EVar x
=> SOME (x
, [])
118 fun reduceExp
G (eAll
as (e
, loc
)) =
122 | EList es
=> (EList (map (reduceExp G
) es
), loc
)
127 NONE
=> (Tycheck
.newUnif (), loc
)
130 val G
' = bindVal
G (x
, to
', NONE
)
132 (ELam (x
, to
, reduceExp G
' e
), loc
)
135 (case lookupEquation G x
of
139 | SOME f
=> case f
[] of
141 | SOME e
' => reduceExp G e
')
142 | SOME e
=> reduceExp G e
)
145 val e1
' = reduceExp G e1
146 val e2
' = reduceExp G e2
149 (ELam (x
, _
, b
), _
) => reduceExp
G (subst x e2
' b
)
151 case findPrim eAll
of
152 NONE
=> (EApp (e1
', e2
'), loc
)
155 NONE
=> (EApp (e1
', e2
'), loc
)
156 | SOME f
=> case f (map (reduceExp G
) args
) of
157 NONE
=> (EApp (e1
', e2
'), loc
)
158 | SOME e
' => reduceExp G e
'
162 |
ESet (v
, b
) => (ESet (v
, reduceExp G b
), loc
)
163 |
EGet (x
, topt
, v
, b
) => (EGet (x
, topt
, v
, reduceExp G b
), loc
)
164 | ESeq es
=> (ESeq (map (reduceExp G
) es
), loc
)
165 |
ELocal (e1
, e2
) => (ELocal (reduceExp G e1
, reduceExp G e2
), loc
)
168 val e1
' = reduceExp G e1
169 val e2
' = reduceExp G e2
172 (EALam (x
, _
, b
), _
) => reduceExp
G (subst x e2
' b
)
173 | _
=> (EWith (e1
', e2
'), loc
)
177 val G
' = bindVal
G (x
, (TAction (p
, SM
.empty
, SM
.empty
), loc
), NONE
)
179 (EALam (x
, p
, reduceExp G
' e
), loc
)