comparison src/monoize.sml @ 251:326fb4686f60

Monoize transaction identifiers; improve disjointness prover on irreducible folds; change 'query' type
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 10:36:54 -0400
parents 5c50b17f5e4a
children 7e9bd70ad3ce
comparison
equal deleted inserted replaced
250:98f551ddd54b 251:326fb4686f60
68 | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "xml"), _), _), _), _), _), _) => 68 | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "xml"), _), _), _), _), _), _) =>
69 (L'.TFfi ("Basis", "string"), loc) 69 (L'.TFfi ("Basis", "string"), loc)
70 | L.CApp ((L.CApp ((L.CFfi ("Basis", "xhtml"), _), _), _), _) => 70 | L.CApp ((L.CApp ((L.CFfi ("Basis", "xhtml"), _), _), _), _) =>
71 (L'.TFfi ("Basis", "string"), loc) 71 (L'.TFfi ("Basis", "string"), loc)
72 72
73 | L.CApp ((L.CFfi ("Basis", "transaction"), _), t) =>
74 (L'.TFun (mt env dtmap t, (L'.TRecord [], loc)), loc)
75
73 | L.CRel _ => poly () 76 | L.CRel _ => poly ()
74 | L.CNamed n => 77 | L.CNamed n =>
75 (case IM.find (dtmap, n) of 78 (case IM.find (dtmap, n) of
76 SOME r => (L'.TDatatype (n, r), loc) 79 SOME r => (L'.TDatatype (n, r), loc)
77 | NONE => 80 | NONE =>
374 | L.EFfiApp (m, x, es) => 377 | L.EFfiApp (m, x, es) =>
375 let 378 let
376 val (es, fm) = ListUtil.foldlMap (fn (e, fm) => monoExp (env, st, fm) e) fm es 379 val (es, fm) = ListUtil.foldlMap (fn (e, fm) => monoExp (env, st, fm) e) fm es
377 in 380 in
378 ((L'.EFfiApp (m, x, es), loc), fm) 381 ((L'.EFfiApp (m, x, es), loc), fm)
382 end
383
384 | L.ECApp ((L.EFfi ("Basis", "return"), _), t) =>
385 ((L'.EAbs ("x", monoType env t, (L'.TRecord [], loc), (L'.ERel 0, loc)), loc), fm)
386 | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), t1), _), t2) =>
387 let
388 val t1 = monoType env t1
389 val t2 = monoType env t2
390 val un = (L'.TRecord [], loc)
391 val mt1 = (L'.TFun (t1, un), loc)
392 val mt2 = (L'.TFun (t2, un), loc)
393 in
394 ((L'.EAbs ("m1", mt1, (L'.TFun (mt1, (L'.TFun (mt2, un), loc)), loc),
395 (L'.EAbs ("m2", mt2, un,
396 (L'.ELet ("r", t1, (L'.ERel 1, loc),
397 (L'.EApp ((L'.ERel 1, loc), (L'.ERel 0, loc)),
398 loc)), loc)), loc)), loc),
399 fm)
379 end 400 end
380 401
381 | L.EApp ( 402 | L.EApp (
382 (L.ECApp ( 403 (L.ECApp (
383 (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _), 404 (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _),
807 828
808 val ts = map (monoType env) (unwind t) 829 val ts = map (monoType env) (unwind t)
809 in 830 in
810 SOME (env, fm, (L'.DExport (ek, s, n, ts), loc)) 831 SOME (env, fm, (L'.DExport (ek, s, n, ts), loc))
811 end 832 end
812 | L.DTable _ => raise Fail "Monoize DTable" 833 | L.DTable (x, n, _, s) =>
834 let
835 val t = (L.CFfi ("Basis", "string"), loc)
836 val t' = (L'.TFfi ("Basis", "string"), loc)
837 val e = (L'.EPrim (Prim.String s), loc)
838 in
839 SOME (Env.pushENamed env x n t NONE s,
840 fm,
841 (L'.DVal (x, n, t', e, s), loc))
842 end
813 end 843 end
814 844
815 fun monoize env ds = 845 fun monoize env ds =
816 let 846 let
817 val (_, _, ds) = List.foldl (fn (d, (env, fm, ds)) => 847 val (_, _, ds) = List.foldl (fn (d, (env, fm, ds)) =>