Mercurial > urweb
comparison src/mono_reduce.sml @ 398:ab3177746c78
Simple listShop working
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 21 Oct 2008 13:24:54 -0400 |
parents | 7abb28e9d51f |
children | 9095a95a1bf9 |
comparison
equal
deleted
inserted
replaced
397:4d519baf357c | 398:ab3177746c78 |
---|---|
273 | 273 |
274 | EDml e => summarize d e @ [WriteDb] | 274 | EDml e => summarize d e @ [WriteDb] |
275 | ENextval e => summarize d e @ [WriteDb] | 275 | ENextval e => summarize d e @ [WriteDb] |
276 | 276 |
277 fun exp env e = | 277 fun exp env e = |
278 case e of | 278 let |
279 ERel n => | 279 (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*) |
280 (case E.lookupERel env n of | 280 |
281 (_, _, SOME e') => #1 e' | 281 val r = |
282 | _ => e) | 282 case e of |
283 | ENamed n => | 283 ERel n => |
284 (case E.lookupENamed env n of | 284 (case E.lookupERel env n of |
285 (_, _, SOME e', _) => #1 e' | 285 (_, _, SOME e') => #1 e' |
286 | _ => e) | 286 | _ => e) |
287 | 287 | ENamed n => |
288 | EApp ((EAbs (x, t, _, e1), loc), e2) => | 288 (case E.lookupENamed env n of |
289 ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp env e1), | 289 (_, _, SOME e', _) => ((*Print.prefaces "Switch" [("n", Print.PD.string (Int.toString n)), |
290 ("e2", MonoPrint.p_exp env e2)];*) | 290 ("e'", MonoPrint.p_exp env e')];*) |
291 if impure e2 then | 291 #1 e') |
292 #1 (reduceExp env (ELet (x, t, e2, e1), loc)) | 292 | _ => e) |
293 else | 293 |
294 #1 (reduceExp env (subExpInExp (0, e2) e1))) | 294 | EApp ((EAbs (x, t, _, e1), loc), e2) => |
295 | 295 ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1), |
296 | ECase (e', pes, {disc, result}) => | 296 ("e2", MonoPrint.p_exp env e2), |
297 let | 297 ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*) |
298 fun push () = | 298 if impure e2 then |
299 case result of | 299 #1 (reduceExp env (ELet (x, t, e2, e1), loc)) |
300 (TFun (dom, result), loc) => | 300 else |
301 if List.all (fn (_, (EAbs _, _)) => true | _ => false) pes then | 301 #1 (reduceExp env (subExpInExp (0, e2) e1))) |
302 EAbs ("_", dom, result, | 302 |
303 (ECase (liftExpInExp 0 e', | 303 | ECase (e', pes, {disc, result}) => |
304 map (fn (p, (EAbs (_, _, _, e), _)) => | 304 let |
305 (p, swapExpVarsPat (0, patBinds p) e) | 305 fun push () = |
306 | _ => raise Fail "MonoReduce ECase") pes, | 306 case result of |
307 {disc = disc, result = result}), loc)) | 307 (TFun (dom, result), loc) => |
308 else | 308 if List.all (fn (_, (EAbs _, _)) => true | _ => false) pes then |
309 e | 309 EAbs ("_", dom, result, |
310 | _ => e | 310 (ECase (liftExpInExp 0 e', |
311 | 311 map (fn (p, (EAbs (_, _, _, e), _)) => |
312 fun search pes = | 312 (p, swapExpVarsPat (0, patBinds p) e) |
313 case pes of | 313 | _ => raise Fail "MonoReduce ECase") pes, |
314 [] => push () | 314 {disc = disc, result = result}), loc)) |
315 | (p, body) :: pes => | |
316 case match (env, p, e') of | |
317 No => search pes | |
318 | Maybe => push () | |
319 | Yes env => #1 (reduceExp env body) | |
320 in | |
321 search pes | |
322 end | |
323 | |
324 | EField ((ERecord xes, _), x) => | |
325 (case List.find (fn (x', _, _) => x' = x) xes of | |
326 SOME (_, e, _) => #1 e | |
327 | NONE => e) | |
328 | |
329 | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) => | |
330 let | |
331 val e' = (ELet (x2, t2, e1, | |
332 (ELet (x1, t1, b1, | |
333 liftExpInExp 1 b2), loc)), loc) | |
334 in | |
335 (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)), | |
336 ("e'", MonoPrint.p_exp env e')];*) | |
337 #1 (reduceExp env e') | |
338 end | |
339 | EApp ((ELet (x, t, e, b), loc), e') => | |
340 #1 (reduceExp env (ELet (x, t, e, | |
341 (EApp (b, liftExpInExp 0 e'), loc)), loc)) | |
342 | |
343 | ELet (x, t, e, (EAbs (x', t' as (TRecord [], _), ran, e'), loc)) => | |
344 EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e, swapExpVars 0 e'), loc)) | |
345 | |
346 | ELet (x, t, e', b) => | |
347 if impure e' then | |
348 let | |
349 val effs_e' = summarize 0 e' | |
350 val effs_b = summarize 0 b | |
351 | |
352 fun does eff = List.exists (fn eff' => eff' = eff) effs_e' | |
353 val writesPage = does WritePage | |
354 val readsDb = does ReadDb | |
355 val writesDb = does WriteDb | |
356 | |
357 fun verifyUnused eff = | |
358 case eff of | |
359 UseRel r => r <> 0 | |
360 | Unsure => false | |
361 | _ => true | |
362 | |
363 fun verifyCompatible effs = | |
364 case effs of | |
365 [] => false | |
366 | eff :: effs => | |
367 case eff of | |
368 Unsure => false | |
369 | UseRel r => | |
370 if r = 0 then | |
371 List.all verifyUnused effs | |
372 else | 315 else |
373 verifyCompatible effs | 316 e |
374 | WritePage => not writesPage andalso verifyCompatible effs | 317 | _ => e |
375 | ReadDb => not writesDb andalso verifyCompatible effs | 318 |
376 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs | 319 fun search pes = |
377 in | 320 case pes of |
378 (*Print.prefaces "verifyCompatible" | 321 [] => push () |
379 [("e'", MonoPrint.p_exp env e'), | 322 | (p, body) :: pes => |
380 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), | 323 case match (env, p, e') of |
381 ("effs_e'", Print.p_list p_event effs_e'), | 324 No => search pes |
382 ("effs_b", Print.p_list p_event effs_b)];*) | 325 | Maybe => push () |
383 if verifyCompatible effs_b then | 326 | Yes env => #1 (reduceExp env body) |
327 in | |
328 search pes | |
329 end | |
330 | |
331 | EField ((ERecord xes, _), x) => | |
332 (case List.find (fn (x', _, _) => x' = x) xes of | |
333 SOME (_, e, _) => #1 e | |
334 | NONE => e) | |
335 | |
336 | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) => | |
337 let | |
338 val e' = (ELet (x2, t2, e1, | |
339 (ELet (x1, t1, b1, | |
340 liftExpInExp 1 b2), loc)), loc) | |
341 in | |
342 (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)), | |
343 ("e'", MonoPrint.p_exp env e')];*) | |
344 #1 (reduceExp env e') | |
345 end | |
346 | EApp ((ELet (x, t, e, b), loc), e') => | |
347 #1 (reduceExp env (ELet (x, t, e, | |
348 (EApp (b, liftExpInExp 0 e'), loc)), loc)) | |
349 | |
350 | ELet (x, t, e, (EAbs (x', t' as (TRecord [], _), ran, e'), loc)) => | |
351 EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e, swapExpVars 0 e'), loc)) | |
352 | |
353 | ELet (x, t, e', b) => | |
354 if impure e' then | |
355 let | |
356 val effs_e' = summarize 0 e' | |
357 val effs_b = summarize 0 b | |
358 | |
359 fun does eff = List.exists (fn eff' => eff' = eff) effs_e' | |
360 val writesPage = does WritePage | |
361 val readsDb = does ReadDb | |
362 val writesDb = does WriteDb | |
363 | |
364 fun verifyUnused eff = | |
365 case eff of | |
366 UseRel r => r <> 0 | |
367 | Unsure => false | |
368 | _ => true | |
369 | |
370 fun verifyCompatible effs = | |
371 case effs of | |
372 [] => false | |
373 | eff :: effs => | |
374 case eff of | |
375 Unsure => false | |
376 | UseRel r => | |
377 if r = 0 then | |
378 List.all verifyUnused effs | |
379 else | |
380 verifyCompatible effs | |
381 | WritePage => not writesPage andalso verifyCompatible effs | |
382 | ReadDb => not writesDb andalso verifyCompatible effs | |
383 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs | |
384 in | |
385 (*Print.prefaces "verifyCompatible" | |
386 [("e'", MonoPrint.p_exp env e'), | |
387 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), | |
388 ("effs_e'", Print.p_list p_event effs_e'), | |
389 ("effs_b", Print.p_list p_event effs_b)];*) | |
390 if verifyCompatible effs_b then | |
391 #1 (reduceExp env (subExpInExp (0, e') b)) | |
392 else | |
393 e | |
394 end | |
395 else | |
384 #1 (reduceExp env (subExpInExp (0, e') b)) | 396 #1 (reduceExp env (subExpInExp (0, e') b)) |
385 else | 397 |
386 e | 398 | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) => |
387 end | 399 EPrim (Prim.String (s1 ^ s2)) |
388 else | 400 |
389 #1 (reduceExp env (subExpInExp (0, e') b)) | 401 | _ => e |
390 | 402 in |
391 | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) => | 403 (*Print.prefaces "exp'" [("r", MonoPrint.p_exp env (r, ErrorMsg.dummySpan))];*) |
392 EPrim (Prim.String (s1 ^ s2)) | 404 r |
393 | 405 end |
394 | _ => e | |
395 | 406 |
396 and bind (env, b) = | 407 and bind (env, b) = |
397 case b of | 408 case b of |
398 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs | 409 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs |
399 | U.Decl.RelE (x, t) => E.pushERel env x t NONE | 410 | U.Decl.RelE (x, t) => E.pushERel env x t NONE |