Mercurial > urweb
changeset 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 | 98f551ddd54b |
| children | 7e9bd70ad3ce |
| files | lib/basis.urs src/cjrize.sml src/corify.sml src/disjoint.sml src/mono.sml src/mono_print.sml src/mono_util.sml src/monoize.sml tests/query.ur |
| diffstat | 9 files changed, 115 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.urs Sun Aug 31 09:52:52 2008 -0400 +++ b/lib/basis.urs Sun Aug 31 10:36:54 2008 -0400 @@ -155,11 +155,10 @@ -> transaction t1 -> (t1 -> transaction t2) -> transaction t2 -val query : tables ::: {{Type}} -> exps ::: {Type} +val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps -> sql_query tables exps -> state ::: Type - -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) - -> $exps + -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) -> state -> transaction state) -> state
--- a/src/cjrize.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/cjrize.sml Sun Aug 31 10:36:54 2008 -0400 @@ -275,6 +275,8 @@ ((L'.ESeq (e1, e2), loc), sm) end + | L.ELet _ => raise Fail "Cjrize ELet" + | L.EClosure _ => (ErrorMsg.errorAt loc "Nested closure remains in code generation"; (dummye, sm))
--- a/src/corify.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/corify.sml Sun Aug 31 10:36:54 2008 -0400 @@ -817,6 +817,7 @@ val ef = (L.EModProj (basis, [], "bind"), loc) val ef = (L.ECApp (ef, ran'), loc) + val ef = (L.ECApp (ef, ran), loc) val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc) val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
--- a/src/disjoint.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/disjoint.sml Sun Aug 31 10:36:54 2008 -0400 @@ -104,7 +104,9 @@ type env = PS.set PM.map -type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con +structure E = ElabEnv + +type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con val empty = PM.empty @@ -151,6 +153,8 @@ fun decomposeRow (env, denv) c = let + val loc = #2 c + fun decomposeProj c = let val (c, gs) = hnormCon (env, denv) c @@ -179,21 +183,59 @@ (acc, gs' @ gs) end - fun decomposeRow (c, (acc, gs)) = + fun decomposeRow' (c, (acc, gs)) = let - val (cAll as (c, _), ns, gs') = decomposeProj c - val gs = gs' @ gs + fun default () = + let + val (cAll as (c, _), ns, gs') = decomposeProj c + val gs = gs' @ gs + in + case c of + CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs + | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs))) + | CRel n => (Piece (RowR n, ns) :: acc, gs) + | CNamed n => (Piece (RowN n, ns) :: acc, gs) + | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) + | _ => (Unknown cAll :: acc, gs) + end in - case c of - CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs - | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs))) - | CRel n => (Piece (RowR n, ns) :: acc, gs) - | CNamed n => (Piece (RowN n, ns) :: acc, gs) - | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) - | _ => (Unknown cAll :: acc, gs) + case #1 (#1 (hnormCon (env, denv) c)) of + CApp ( + (CApp ( + (CApp ((CFold (dom, ran), _), f), _), + i), _), + r) => + let + val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE + val (env', v) = E.pushCNamed env' "v" dom NONE + val (env', st) = E.pushCNamed env' "st" ran NONE + + val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc), + (CUnit, loc))]), loc), + (CNamed st, loc)) + + val c' = (CApp (f, (CNamed nm, loc)), loc) + val c' = (CApp (c', (CNamed v, loc)), loc) + val c' = (CApp (c', (CNamed st, loc)), loc) + val (ps, gs'') = decomposeRow (env', denv') c' + + fun covered p = + case p of + Unknown _ => false + | Piece p => + case p of + (NameN n, []) => n = nm + | (RowN n, []) => n = st + | _ => false + + val ps = List.filter (not o covered) ps + in + decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs))) + end + | _ => default () end in - decomposeRow (c, ([], [])) + decomposeRow' (c, ([], [])) end and assert env denv (c1, c2) =
--- a/src/mono.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/mono.sml Sun Aug 31 10:36:54 2008 -0400 @@ -71,6 +71,7 @@ | EWrite of exp | ESeq of exp * exp + | ELet of string * typ * exp * exp | EClosure of int * exp list
--- a/src/mono_print.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/mono_print.sml Sun Aug 31 10:36:54 2008 -0400 @@ -185,6 +185,21 @@ string ";", space, p_exp env e2] + | ELet (x, t, e1, e2) => box [string "let", + space, + string x, + space, + string ":", + space, + p_typ env t, + space, + string "=", + space, + p_exp env e1, + space, + string "in", + space, + p_exp (E.pushERel env x t NONE) e2] | EClosure (n, es) => box [string "CLOSURE(", p_enamed env n,
--- a/src/mono_util.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/mono_util.sml Sun Aug 31 10:36:54 2008 -0400 @@ -213,6 +213,14 @@ S.map2 (mfe ctx e2, fn e2' => (ESeq (e1', e2'), loc))) + | ELet (x, t, e1, e2) => + S.bind2 (mft t, + fn t' => + S.bind2 (mfe ctx e1, + fn e1' => + S.map2 (mfe (bind (ctx, RelE (x, t))) e2, + fn e2' => + (ELet (x, t', e1', e2'), loc)))) | EClosure (n, es) => S.map2 (ListUtil.mapfold (mfe ctx) es,
--- a/src/monoize.sml Sun Aug 31 09:52:52 2008 -0400 +++ b/src/monoize.sml Sun Aug 31 10:36:54 2008 -0400 @@ -70,6 +70,9 @@ | L.CApp ((L.CApp ((L.CFfi ("Basis", "xhtml"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CFfi ("Basis", "transaction"), _), t) => + (L'.TFun (mt env dtmap t, (L'.TRecord [], loc)), loc) + | L.CRel _ => poly () | L.CNamed n => (case IM.find (dtmap, n) of @@ -378,6 +381,24 @@ ((L'.EFfiApp (m, x, es), loc), fm) end + | L.ECApp ((L.EFfi ("Basis", "return"), _), t) => + ((L'.EAbs ("x", monoType env t, (L'.TRecord [], loc), (L'.ERel 0, loc)), loc), fm) + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), t1), _), t2) => + let + val t1 = monoType env t1 + val t2 = monoType env t2 + val un = (L'.TRecord [], loc) + val mt1 = (L'.TFun (t1, un), loc) + val mt2 = (L'.TFun (t2, un), loc) + in + ((L'.EAbs ("m1", mt1, (L'.TFun (mt1, (L'.TFun (mt2, un), loc)), loc), + (L'.EAbs ("m2", mt2, un, + (L'.ELet ("r", t1, (L'.ERel 1, loc), + (L'.EApp ((L'.ERel 1, loc), (L'.ERel 0, loc)), + loc)), loc)), loc)), loc), + fm) + end + | L.EApp ( (L.ECApp ( (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _), @@ -809,7 +830,16 @@ in SOME (env, fm, (L'.DExport (ek, s, n, ts), loc)) end - | L.DTable _ => raise Fail "Monoize DTable" + | L.DTable (x, n, _, s) => + let + val t = (L.CFfi ("Basis", "string"), loc) + val t' = (L'.TFfi ("Basis", "string"), loc) + val e = (L'.EPrim (Prim.String s), loc) + in + SOME (Env.pushENamed env x n t NONE s, + fm, + (L'.DVal (x, n, t', e, s), loc)) + end end fun monoize env ds =
--- a/tests/query.ur Sun Aug 31 09:52:52 2008 -0400 +++ b/tests/query.ur Sun Aug 31 10:36:54 2008 -0400 @@ -6,7 +6,7 @@ val q1 = (SELECT * FROM t1) val r1 : transaction (list {A : int, B : string, C : float}) = query q1 - (fn fs _ acc => return (Cons (fs.T1, acc))) + (fn fs acc => return (Cons (fs.T1, acc))) Nil val r2 : transaction string =