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
29 | EList es
=> List.exists (freeIn x
) es
31 |
ELam (x
', _
, b
') => x
<> x
' andalso freeIn x b
'
33 |
EApp (e1
, e2
) => freeIn x e1
orelse freeIn x e2
36 |
ESet (_
, e
) => freeIn x e
37 |
EGet (x
', _
, b
') => x
<> x
' andalso freeIn x b
'
38 | ESeq es
=> List.exists (freeIn x
) es
39 |
ELocal (e1
, e2
) => freeIn x e1
orelse freeIn x e2
40 |
EWith (e1
, e2
) => freeIn x e1
orelse freeIn x e2
43 val freshCount
= ref
0
54 fun subst x
e (bAll
as (b
, loc
)) =
58 | EList es
=> (EList (map (subst x e
) es
), loc
)
60 |
ELam (x
', to
, b
') =>
63 else if freeIn x
' e
then
67 (ELam (x
'', to
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
70 (ELam (x
', to
, subst x e b
'), loc
)
76 |
EApp (b1
, b2
) => (EApp (subst x e b1
, subst x e b2
), loc
)
79 |
ESet (v
, b
) => (ESet (v
, subst x e b
), loc
)
83 else if freeIn x
' e
then
87 (EGet (x
'', v
, subst x
e (subst x
' (EVar x
'', loc
) b
')), loc
)
90 (EGet (x
', v
, subst x e b
'), loc
)
91 | ESeq es
=> (ESeq (map (subst x e
) es
), loc
)
92 |
ELocal (b1
, b2
) => (ELocal (subst x e b1
, subst x e b2
), loc
)
93 |
EWith (b1
, b2
) => (EWith (subst x e b1
, subst x e b2
), loc
)
95 fun reduceExp
G (eAll
as (e
, loc
)) =
99 | EList es
=> (EList (map (reduceExp G
) es
), loc
)
104 NONE
=> (Tycheck
.newUnif (), loc
)
107 val G
' = bindVal
G (x
, to
', NONE
)
109 (ELam (x
, to
, reduceExp G
' e
), loc
)
112 (case lookupEquation G x
of
114 | SOME e
=> reduceExp G e
)
117 val e1
' = reduceExp G e1
118 val e2
' = reduceExp G e2
121 (ELam (x
, _
, b
), _
) => reduceExp
G (subst x e2
' b
)
122 | _
=> (EApp (e1
', e2
'), loc
)
126 |
ESet (v
, b
) => (ESet (v
, reduceExp G b
), loc
)
127 |
EGet (x
, v
, b
) => (EGet (x
, v
, reduceExp G b
), loc
)
128 | ESeq es
=> (ESeq (map (reduceExp G
) es
), loc
)
129 |
ELocal (e1
, e2
) => (ELocal (reduceExp G e1
, reduceExp G e2
), loc
)
130 |
EWith (e1
, e2
) => (EWith (reduceExp G e1
, reduceExp G e2
), loc
)