Mercurial > urweb

comparison src/mono_reduce.sml @ 398:ab3177746c78

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