Commit | Line | Data |
---|---|---|
492c1cff AC |
1 | (* HCoop Domtool (http://hcoop.sourceforge.net/) |
2 | * Copyright (c) 2006, Adam Chlipala | |
3 | * | |
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. | |
8 | * | |
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. | |
13 | * | |
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. | |
dac62e84 | 17 | *) |
492c1cff AC |
18 | |
19 | (* Evaluation of expressions until only externs are around *) | |
20 | ||
21 | structure Reduce :> REDUCE = struct | |
22 | ||
23 | open Ast Print Env | |
24 | ||
6bb366c5 AC |
25 | structure SM = StringMap |
26 | ||
492c1cff AC |
27 | fun freeIn x (b, _) = |
28 | case b of | |
29 | EInt _ => false | |
30 | | EString _ => false | |
31 | | EList es => List.exists (freeIn x) es | |
32 | ||
33 | | ELam (x', _, b') => x <> x' andalso freeIn x b' | |
34 | | EVar x' => x = x' | |
35 | | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2 | |
36 | ||
37 | | ESkip => false | |
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 | |
6bb366c5 | 43 | | EALam (x', _, b') => x <> x' andalso freeIn x b' |
492c1cff AC |
44 | |
45 | local | |
46 | val freshCount = ref 0 | |
47 | in | |
48 | fun freshVar () = | |
49 | let | |
50 | val v = !freshCount | |
51 | in | |
52 | freshCount := v + 1; | |
53 | Int.toString v ^ "v" | |
54 | end | |
55 | end | |
56 | ||
57 | fun subst x e (bAll as (b, loc)) = | |
58 | case b of | |
59 | EInt _ => bAll | |
60 | | EString _ => bAll | |
61 | | EList es => (EList (map (subst x e) es), loc) | |
62 | ||
63 | | ELam (x', to, b') => | |
64 | if x = x' then | |
65 | bAll | |
66 | else if freeIn x' e then | |
67 | let | |
68 | val x'' = freshVar () | |
69 | in | |
70 | (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc) | |
71 | end | |
72 | else | |
73 | (ELam (x', to, subst x e b'), loc) | |
74 | | EVar x' => | |
75 | if x = x' then | |
76 | e | |
77 | else | |
78 | bAll | |
79 | | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc) | |
80 | ||
81 | | ESkip => bAll | |
82 | | ESet (v, b) => (ESet (v, subst x e b), loc) | |
83 | | EGet (x', v, b') => | |
84 | if x = x' then | |
85 | bAll | |
86 | else if freeIn x' e then | |
87 | let | |
88 | val x'' = freshVar () | |
89 | in | |
90 | (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc) | |
91 | end | |
92 | else | |
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) | |
6bb366c5 AC |
97 | | EALam (x', p, b') => |
98 | if x = x' then | |
99 | bAll | |
100 | else if freeIn x' e then | |
101 | let | |
102 | val x'' = freshVar () | |
103 | in | |
104 | (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc) | |
105 | end | |
106 | else | |
107 | (EALam (x', p, subst x e b'), loc) | |
492c1cff AC |
108 | |
109 | fun reduceExp G (eAll as (e, loc)) = | |
110 | case e of | |
111 | EInt _ => eAll | |
112 | | EString _ => eAll | |
113 | | EList es => (EList (map (reduceExp G) es), loc) | |
114 | ||
115 | | ELam (x, to, e) => | |
116 | let | |
117 | val to' = case to of | |
118 | NONE => (Tycheck.newUnif (), loc) | |
119 | | SOME to => to | |
120 | ||
121 | val G' = bindVal G (x, to', NONE) | |
122 | in | |
123 | (ELam (x, to, reduceExp G' e), loc) | |
124 | end | |
125 | | EVar x => | |
126 | (case lookupEquation G x of | |
127 | NONE => eAll | |
128 | | SOME e => reduceExp G e) | |
129 | | EApp (e1, e2) => | |
130 | let | |
131 | val e1' = reduceExp G e1 | |
132 | val e2' = reduceExp G e2 | |
133 | in | |
134 | case e1' of | |
135 | (ELam (x, _, b), _) => reduceExp G (subst x e2' b) | |
136 | | _ => (EApp (e1', e2'), loc) | |
137 | end | |
138 | ||
139 | | ESkip => eAll | |
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) | |
6bb366c5 AC |
144 | | EWith (e1, e2) => |
145 | let | |
146 | val e1' = reduceExp G e1 | |
147 | val e2' = reduceExp G e2 | |
148 | in | |
149 | case e1' of | |
150 | (EALam (x, _, b), _) => reduceExp G (subst x e2' b) | |
151 | | _ => (EWith (e1', e2'), loc) | |
152 | end | |
153 | | EALam (x, p, e) => | |
154 | let | |
155 | val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE) | |
156 | in | |
157 | (EALam (x, p, reduceExp G' e), loc) | |
158 | end | |
492c1cff AC |
159 | |
160 | end |