Mercurial > urweb
changeset 1229:a2cd6664f57f
sendOwnIds policies
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 11 Apr 2010 17:55:37 -0400 |
| parents | 7dfa67560916 |
| children | 8768145eed1e |
| files | lib/ur/basis.urs src/iflow.sml src/mono.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml |
| diffstat | 7 files changed, 51 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Sun Apr 11 16:46:38 2010 -0400 +++ b/lib/ur/basis.urs Sun Apr 11 17:55:37 2010 -0400 @@ -804,6 +804,8 @@ -> [tables ~ exps] => sql_query [] tables exps -> sql_policy +val sendOwnIds : sql_sequence -> sql_policy + val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables] => sql_query [] ([New = fs] ++ tables) [] -> sql_policy
--- a/src/iflow.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/iflow.sml Sun Apr 11 17:55:37 2010 -0400 @@ -482,7 +482,7 @@ Consts : representative CM.map ref, Con0s : representative SM.map ref, Records : (representative SM.map * representative) list ref, - Funcs : ((string * representative list) * representative) list ref } + Funcs : ((string * representative list) * representative) list ref} fun database () = {Vars = ref IM.empty, Consts = ref CM.empty, @@ -847,6 +847,7 @@ else (); #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1))); + compactFuncs ()) and compactFuncs () = @@ -1450,9 +1451,9 @@ let fun default () = let - val (rvN, e) = rv rvN + val (rvN, e') = rv rvN in - (inl e, rvN) + (inl e', rvN) end in case e of @@ -1686,7 +1687,7 @@ let val t = case v of - "New" => "$New" + "New" => t ^ "$New" | _ => t in And (p, Reln (Sql t, [rvOf v])) @@ -1767,7 +1768,7 @@ let val t = case v of - "New" => "$New" + "New" => t ^ "$New" | _ => t in And (p, Reln (Sql t, [rvOf v])) @@ -1989,6 +1990,8 @@ let val (st, nv) = St.nextVar st in + (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e), + ("nv", p_exp (Var nv))];*) (Var nv, st) end @@ -2233,7 +2236,7 @@ st es in (Recd [], St.addInsert (st, (loc, And (St.ambient st, - Reln (Sql "$New", [Recd es]))))) + Reln (Sql (tab ^ "$New"), [Recd es]))))) end | Delete (tab, e) => let @@ -2302,13 +2305,19 @@ | (inr p, st) => (p, st) val p = And (p, - And (Reln (Sql "$New", [Recd fs]), + And (Reln (Sql (tab ^ "$New"), [Recd fs]), And (Reln (Sql "$Old", [Var old]), Reln (Sql tab, [Var old])))) in (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p)))) end) + | ENextval (EPrim (Prim.String seq), _) => + let + val (st, nv) = St.nextVar st + in + (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv])))) + end | ENextval _ => default () | ESetval _ => default () @@ -2416,6 +2425,16 @@ in (vals, inserts, deletes, updates, client, insert, delete, p :: update) end + | PolSequence e => + (case #1 e of + EPrim (Prim.String seq) => + let + val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0]) + val outs = [Lvar 0] + in + (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update) + end + | _ => (vals, inserts, deletes, updates, client, insert, delete, update)) end | _ => (vals, inserts, deletes, updates, client, insert, delete, update) @@ -2434,8 +2453,14 @@ if decompH p (fn hyps => List.exists (fn p' => - decompG p' - (fn goals => imply (hyps, goals, NONE))) + if decompG p' + (fn goals => imply (hyps, goals, NONE)) then + ((*reset (); + Print.prefaces "Match" [("hyp", p_prop p), + ("goal", p_prop p')];*) + true) + else + false) pols) then () else @@ -2487,7 +2512,11 @@ client orelse tryCombos (0, client, True, []) orelse (reset (); - Print.preface ("Untenable hypotheses", + Print.preface ("Untenable hypotheses" + ^ (case fl of + Control Where => " (WHERE clause)" + | Control Case => " (case discriminee)" + | Data => " (returned data value)"), Print.p_list p_atom hyps); false) end) then
--- a/src/mono.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/mono.sml Sun Apr 11 17:55:37 2010 -0400 @@ -128,6 +128,7 @@ | PolInsert of exp | PolDelete of exp | PolUpdate of exp + | PolSequence of exp datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list
--- a/src/mono_print.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/mono_print.sml Sun Apr 11 17:55:37 2010 -0400 @@ -426,6 +426,9 @@ | PolUpdate e => box [string "mayUpdate", space, p_exp env e] + | PolSequence e => box [string "sendOwnIds", + space, + p_exp env e] fun p_decl env (dAll as (d, _) : decl) = case d of
--- a/src/mono_shake.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/mono_shake.sml Sun Apr 11 17:55:37 2010 -0400 @@ -65,6 +65,7 @@ | PolInsert e1 => e1 | PolDelete e1 => e1 | PolUpdate e1 => e1 + | PolSequence e1 => e1 in usedVars st e1 end
--- a/src/mono_util.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/mono_util.sml Sun Apr 11 17:55:37 2010 -0400 @@ -553,6 +553,9 @@ | PolUpdate e => S.map2 (mfe ctx e, PolUpdate) + | PolSequence e => + S.map2 (mfe ctx e, + PolSequence) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t,
--- a/src/monoize.sml Sun Apr 11 16:46:38 2010 -0400 +++ b/src/monoize.sml Sun Apr 11 17:55:37 2010 -0400 @@ -3752,6 +3752,8 @@ (e, L'.PolDelete) | L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayUpdate"), _), _), _), _), _), e) => (e, L'.PolUpdate) + | L.EFfiApp ("Basis", "sendOwnIds", [e]) => + (e, L'.PolSequence) | _ => (poly (); (e, L'.PolClient)) val (e, fm) = monoExp (env, St.empty, fm) e