add6f172 |
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. |
ae3a5b8c |
17 | *) |
add6f172 |
18 | |
19 | (* Evaluation of expressions until only externs are around *) |
20 | |
21 | structure Reduce :> REDUCE = struct |
22 | |
23 | open Ast Print Env |
24 | |
bf9b0bc3 |
25 | structure SM = StringMap |
26 | |
add6f172 |
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 |
28cf1be3 |
39 | | EGet (x', _, _, b') => x <> x' andalso freeIn x b' |
add6f172 |
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 |
bf9b0bc3 |
43 | | EALam (x', _, b') => x <> x' andalso freeIn x b' |
add6f172 |
44 | |
254f7f93 |
45 | | EIf (e1, e2, e3) => freeIn x e1 orelse freeIn x e2 orelse freeIn x e3 |
46 | |
add6f172 |
47 | local |
48 | val freshCount = ref 0 |
49 | in |
50 | fun freshVar () = |
51 | let |
52 | val v = !freshCount |
53 | in |
54 | freshCount := v + 1; |
55 | Int.toString v ^ "v" |
56 | end |
57 | end |
58 | |
59 | fun subst x e (bAll as (b, loc)) = |
60 | case b of |
61 | EInt _ => bAll |
62 | | EString _ => bAll |
63 | | EList es => (EList (map (subst x e) es), loc) |
64 | |
65 | | ELam (x', to, b') => |
66 | if x = x' then |
67 | bAll |
68 | else if freeIn x' e then |
69 | let |
70 | val x'' = freshVar () |
71 | in |
72 | (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc) |
73 | end |
74 | else |
75 | (ELam (x', to, subst x e b'), loc) |
76 | | EVar x' => |
77 | if x = x' then |
78 | e |
79 | else |
80 | bAll |
81 | | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc) |
82 | |
83 | | ESkip => bAll |
84 | | ESet (v, b) => (ESet (v, subst x e b), loc) |
28cf1be3 |
85 | | EGet (x', topt, v, b') => |
add6f172 |
86 | if x = x' then |
87 | bAll |
88 | else if freeIn x' e then |
89 | let |
90 | val x'' = freshVar () |
91 | in |
28cf1be3 |
92 | (EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc) |
add6f172 |
93 | end |
94 | else |
28cf1be3 |
95 | (EGet (x', topt, v, subst x e b'), loc) |
add6f172 |
96 | | ESeq es => (ESeq (map (subst x e) es), loc) |
97 | | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc) |
98 | | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc) |
bf9b0bc3 |
99 | | EALam (x', p, b') => |
100 | if x = x' then |
101 | bAll |
102 | else if freeIn x' e then |
103 | let |
104 | val x'' = freshVar () |
105 | in |
106 | (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc) |
107 | end |
108 | else |
109 | (EALam (x', p, subst x e b'), loc) |
add6f172 |
110 | |
254f7f93 |
111 | | EIf (b1, b2, b3) => (EIf (subst x e b1, subst x e b2, subst x e b3), loc) |
112 | |
1fbe6533 |
113 | fun findPrim (e, _) = |
114 | case e of |
115 | EApp (f, x) => |
116 | (case findPrim f of |
117 | NONE => NONE |
118 | | SOME (f, xs) => SOME (f, xs @ [x])) |
119 | | EVar x => SOME (x, []) |
120 | | _ => NONE |
121 | |
add6f172 |
122 | fun reduceExp G (eAll as (e, loc)) = |
123 | case e of |
124 | EInt _ => eAll |
125 | | EString _ => eAll |
126 | | EList es => (EList (map (reduceExp G) es), loc) |
127 | |
128 | | ELam (x, to, e) => |
129 | let |
130 | val to' = case to of |
131 | NONE => (Tycheck.newUnif (), loc) |
132 | | SOME to => to |
133 | |
134 | val G' = bindVal G (x, to', NONE) |
135 | in |
136 | (ELam (x, to, reduceExp G' e), loc) |
137 | end |
138 | | EVar x => |
139 | (case lookupEquation G x of |
3901a942 |
140 | NONE => |
141 | (case function x of |
142 | NONE => eAll |
143 | | SOME f => case f [] of |
144 | NONE => eAll |
145 | | SOME e' => reduceExp G e') |
add6f172 |
146 | | SOME e => reduceExp G e) |
147 | | EApp (e1, e2) => |
148 | let |
149 | val e1' = reduceExp G e1 |
150 | val e2' = reduceExp G e2 |
151 | in |
152 | case e1' of |
153 | (ELam (x, _, b), _) => reduceExp G (subst x e2' b) |
1fbe6533 |
154 | | _ => |
155 | case findPrim eAll of |
156 | NONE => (EApp (e1', e2'), loc) |
157 | | SOME (f, args) => |
158 | case function f of |
159 | NONE => (EApp (e1', e2'), loc) |
160 | | SOME f => case f (map (reduceExp G) args) of |
161 | NONE => (EApp (e1', e2'), loc) |
162 | | SOME e' => reduceExp G e' |
add6f172 |
163 | end |
164 | |
165 | | ESkip => eAll |
166 | | ESet (v, b) => (ESet (v, reduceExp G b), loc) |
28cf1be3 |
167 | | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc) |
add6f172 |
168 | | ESeq es => (ESeq (map (reduceExp G) es), loc) |
169 | | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc) |
bf9b0bc3 |
170 | | EWith (e1, e2) => |
171 | let |
172 | val e1' = reduceExp G e1 |
173 | val e2' = reduceExp G e2 |
174 | in |
175 | case e1' of |
176 | (EALam (x, _, b), _) => reduceExp G (subst x e2' b) |
177 | | _ => (EWith (e1', e2'), loc) |
178 | end |
179 | | EALam (x, p, e) => |
180 | let |
181 | val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE) |
182 | in |
183 | (EALam (x, p, reduceExp G' e), loc) |
184 | end |
add6f172 |
185 | |
254f7f93 |
186 | | EIf (e1, e2, e3) => |
187 | let |
188 | val e1' = reduceExp G e1 |
189 | fun e2' () = reduceExp G e2 |
190 | fun e3' () = reduceExp G e3 |
191 | in |
192 | case e1' of |
193 | (EVar "true", _) => e2' () |
194 | | (EVar "false", _) => e3' () |
195 | | _ => (EIf (e1', e2' (), e3' ()), loc) |
196 | end |
197 | |
add6f172 |
198 | end |