Mercurial > urweb

comparison src/reduce.sml @ 510:c644ec94866d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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