Mercurial > urweb
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)) => |