Mercurial > urweb
comparison src/reduce.sml @ 510:c644ec94866d
Fix environments for repeat visits for exp reduction
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 26 Nov 2008 14:51:52 -0500 |
parents | 140c68046598 |
children | 6d6222e045b0 |
comparison
equal
deleted
inserted
replaced
509:140c68046598 | 510:c644ec94866d |
---|---|
42 | 42 |
43 | Lift of int * int | 43 | Lift of int * int |
44 | 44 |
45 type env = env_item list | 45 type env = env_item list |
46 | 46 |
47 fun ei2s ei = | |
48 case ei of | |
49 UnknownC => "UC" | |
50 | KnownC _ => "KC" | |
51 | UnknownE => "UE" | |
52 | KnownE _ => "KE" | |
53 | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" | |
54 | |
55 fun e2s env = String.concatWith " " (map ei2s env) | |
56 | |
57 val deKnown = List.filter (fn KnownC _ => false | |
58 | KnownE _ => false | |
59 | _ => true) | |
60 | |
47 fun conAndExp (namedC, namedE) = | 61 fun conAndExp (namedC, namedE) = |
48 let | 62 let |
49 fun con env (all as (c, loc)) = | 63 fun con env (all as (c, loc)) = |
64 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) | |
50 case c of | 65 case c of |
51 TFun (c1, c2) => (TFun (con env c1, con env c2), loc) | 66 TFun (c1, c2) => (TFun (con env c1, con env c2), loc) |
52 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) | 67 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) |
53 | TRecord c => (TRecord (con env c), loc) | 68 | TRecord c => (TRecord (con env c), loc) |
54 | 69 |
55 | CRel n => | 70 | CRel n => |
56 let | 71 let |
57 fun find (n', env, lift) = | 72 fun find (n', env, nudge, lift) = |
58 if n' = 0 then | 73 case env of |
59 case env of | 74 [] => raise Fail "Reduce.con: CRel" |
60 UnknownC :: _ => (CRel (n + lift), loc) | 75 | UnknownE :: rest => find (n', rest, nudge, lift) |
61 | KnownC c :: _ => con (Lift (lift, 0) :: env) c | 76 | KnownE _ :: rest => find (n', rest, nudge, lift) |
62 | Lift (lift', _) :: rest => find (0, rest, lift + lift') | 77 | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift') |
63 | _ => raise Fail "Reduce.con: CRel [1]" | 78 | UnknownC :: rest => |
64 else | 79 if n' = 0 then |
65 case env of | 80 (CRel (n + nudge), loc) |
66 UnknownC :: rest => find (n' - 1, rest, lift + 1) | 81 else |
67 | KnownC _ :: rest => find (n' - 1, rest, lift) | 82 find (n' - 1, rest, nudge, lift + 1) |
68 | UnknownE :: rest => find (n' - 1, rest, lift) | 83 | KnownC c :: rest => |
69 | KnownE _ :: rest => find (n' - 1, rest, lift) | 84 if n' = 0 then |
70 | Lift (lift', _) :: rest => find (n', rest, lift + lift') | 85 con (Lift (lift, 0) :: rest) c |
71 | [] => raise Fail "Reduce.con: CRel [2]" | 86 else |
72 in | 87 find (n' - 1, rest, nudge - 1, lift) |
73 find (n, env, 0) | 88 in |
89 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) | |
90 find (n, env, 0, 0) | |
74 end | 91 end |
75 | CNamed n => | 92 | CNamed n => |
76 (case IM.find (namedC, n) of | 93 (case IM.find (namedC, n) of |
77 NONE => all | 94 NONE => all |
78 | SOME c => c) | 95 | SOME c => c) |
82 val c1 = con env c1 | 99 val c1 = con env c1 |
83 val c2 = con env c2 | 100 val c2 = con env c2 |
84 in | 101 in |
85 case #1 c1 of | 102 case #1 c1 of |
86 CAbs (_, _, b) => | 103 CAbs (_, _, b) => |
87 con (KnownC c2 :: env) b | 104 con (KnownC c2 :: deKnown env) b |
88 | 105 |
89 | CApp ((CApp (fold as (CFold _, _), f), _), i) => | 106 | CApp ((CApp (fold as (CFold _, _), f), _), i) => |
90 (case #1 c2 of | 107 (case #1 c2 of |
91 CRecord (_, []) => i | 108 CRecord (_, []) => i |
92 | CRecord (k, (x, c) :: rest) => | 109 | CRecord (k, (x, c) :: rest) => |
93 con env (CApp ((CApp ((CApp (f, x), loc), c), loc), | 110 con (deKnown env) |
94 (CApp ((CApp ((CApp (fold, f), loc), i), loc), | 111 (CApp ((CApp ((CApp (f, x), loc), c), loc), |
95 (CRecord (k, rest), loc)), loc)), loc) | 112 (CApp ((CApp ((CApp (fold, f), loc), i), loc), |
113 (CRecord (k, rest), loc)), loc)), loc) | |
96 | _ => (CApp (c1, c2), loc)) | 114 | _ => (CApp (c1, c2), loc)) |
97 | 115 |
98 | _ => (CApp (c1, c2), loc) | 116 | _ => (CApp (c1, c2), loc) |
99 end | 117 end |
100 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) | 118 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) |
122 val c = con env c | 140 val c = con env c |
123 in | 141 in |
124 case #1 c of | 142 case #1 c of |
125 CTuple cs => List.nth (cs, n - 1) | 143 CTuple cs => List.nth (cs, n - 1) |
126 | _ => (CProj (c, n), loc) | 144 | _ => (CProj (c, n), loc) |
127 end | 145 end) |
128 | 146 |
129 fun patCon pc = | 147 fun patCon pc = |
130 case pc of | 148 case pc of |
131 PConVar _ => pc | 149 PConVar _ => pc |
132 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => | 150 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => |
139 fun doPart e (this as (x, t), rest) = | 157 fun doPart e (this as (x, t), rest) = |
140 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), | 158 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), |
141 this :: rest) | 159 this :: rest) |
142 | 160 |
143 fun exp env (all as (e, loc)) = | 161 fun exp env (all as (e, loc)) = |
162 ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), | |
163 ("env", Print.PD.string (e2s env))];*) | |
144 case e of | 164 case e of |
145 EPrim _ => all | 165 EPrim _ => all |
146 | ERel n => | 166 | ERel n => |
147 let | 167 let |
148 fun find (n', env, liftC, liftE) = | 168 fun find (n', env, nudge, liftC, liftE) = |
149 if n' = 0 then | 169 case env of |
150 case env of | 170 [] => raise Fail "Reduce.exp: ERel" |
151 UnknownE :: _ => (ERel (n + liftE), loc) | 171 | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) |
152 | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e | 172 | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) |
153 | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE') | 173 | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', |
154 | _ => raise Fail "Reduce.exp: ERel [1]" | 174 liftC + liftC', liftE + liftE') |
155 else | 175 | UnknownE :: rest => |
156 case env of | 176 if n' = 0 then |
157 UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE) | 177 (ERel (n + nudge), loc) |
158 | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE) | 178 else |
159 | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1) | 179 find (n' - 1, rest, nudge, liftC, liftE + 1) |
160 | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE) | 180 | KnownE e :: rest => |
161 | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE') | 181 if n' = 0 then |
162 | [] => raise Fail "Reduce.exp: ERel [2]" | 182 ((*print "SUBSTITUTING\n";*) |
163 in | 183 exp (Lift (liftC, liftE) :: rest) e) |
164 find (n, env, 0, 0) | 184 else |
185 find (n' - 1, rest, nudge - 1, liftC, liftE) | |
186 in | |
187 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) | |
188 find (n, env, 0, 0, 0) | |
165 end | 189 end |
166 | ENamed n => | 190 | ENamed n => |
167 (case IM.find (namedE, n) of | 191 (case IM.find (namedE, n) of |
168 NONE => all | 192 NONE => all |
169 | SOME e => e) | 193 | SOME e => e) |
176 let | 200 let |
177 val e1 = exp env e1 | 201 val e1 = exp env e1 |
178 val e2 = exp env e2 | 202 val e2 = exp env e2 |
179 in | 203 in |
180 case #1 e1 of | 204 case #1 e1 of |
181 EAbs (_, _, _, b) => exp (KnownE e2 :: env) b | 205 EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b |
182 | _ => (EApp (e1, e2), loc) | 206 | _ => (EApp (e1, e2), loc) |
183 end | 207 end |
184 | 208 |
185 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) | 209 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) |
186 | 210 |
188 let | 212 let |
189 val e = exp env e | 213 val e = exp env e |
190 val c = con env c | 214 val c = con env c |
191 in | 215 in |
192 case #1 e of | 216 case #1 e of |
193 ECAbs (_, _, b) => exp (KnownC c :: env) b | 217 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b |
194 | _ => (ECApp (e, c), loc) | 218 | _ => (ECApp (e, c), loc) |
195 end | 219 end |
196 | 220 |
197 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) | 221 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) |
198 | 222 |
228 (CRecord (k, xcs1), CRecord (_, xcs2)) => | 252 (CRecord (k, xcs1), CRecord (_, xcs2)) => |
229 let | 253 let |
230 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 | 254 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 |
231 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 | 255 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 |
232 in | 256 in |
233 exp env (ERecord (xes1 @ xes2), loc) | 257 exp (deKnown env) (ERecord (xes1 @ xes2), loc) |
234 end | 258 end |
235 | _ => (EConcat (e1, c1, e2, c2), loc) | 259 | _ => (EConcat (e1, c1, e2, c2), loc) |
236 end | 260 end |
237 end | 261 end |
238 | 262 |
248 case #1 rest of | 272 case #1 rest of |
249 CRecord (k, xcs) => | 273 CRecord (k, xcs) => |
250 let | 274 let |
251 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs | 275 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs |
252 in | 276 in |
253 exp env (ERecord xes, loc) | 277 exp (deKnown env) (ERecord xes, loc) |
254 end | 278 end |
255 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) | 279 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) |
256 end | 280 end |
257 in | 281 in |
258 case (#1 e, #1 c) of | 282 case (#1 e, #1 c) of |
277 case #1 rest of | 301 case #1 rest of |
278 CRecord (k, xcs) => | 302 CRecord (k, xcs) => |
279 let | 303 let |
280 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs | 304 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs |
281 in | 305 in |
282 exp env (ERecord xes, loc) | 306 exp (deKnown env) (ERecord xes, loc) |
283 end | 307 end |
284 | _ => (ECutMulti (e, c, {rest = rest}), loc) | 308 | _ => (ECutMulti (e, c, {rest = rest}), loc) |
285 end | 309 end |
286 in | 310 in |
287 case (#1 e, #1 c) of | 311 case (#1 e, #1 c) of |
326 end | 350 end |
327 | 351 |
328 | EWrite e => (EWrite (exp env e), loc) | 352 | EWrite e => (EWrite (exp env e), loc) |
329 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) | 353 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) |
330 | 354 |
331 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) | 355 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)) |
332 in | 356 in |
333 {con = con, exp = exp} | 357 {con = con, exp = exp} |
334 end | 358 end |
335 | 359 |
336 fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c | 360 fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c |