Mercurial > urweb
changeset 1282:a9a500d22ebc
Roll back WHERE checking
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 27 Jul 2010 14:04:09 -0400 |
| parents | 60e19545841b |
| children | b04354e24d1b |
| 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 tests/equalKnown.ur tests/equalKnown.urp tests/equalKnown.urs |
| diffstat | 10 files changed, 18 insertions(+), 129 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Jul 27 12:12:08 2010 -0400 +++ b/lib/ur/basis.urs Tue Jul 27 14:04:09 2010 -0400 @@ -819,11 +819,6 @@ => sql_query [] ([Old = fs, New = fs] ++ tables) [] -> sql_policy -val equalAny : nm :: Name -> t ::: Type -> fs ::: {Type} -> ks ::: {{Unit}} - -> [[nm] ~ fs] => sql_table ([nm = t] ++ fs) ks -> sql_policy -val equalKnown : nm :: Name -> t ::: Type -> fs ::: {Type} -> ks ::: {{Unit}} - -> [[nm] ~ fs] => sql_table ([nm = t] ++ fs) ks -> sql_policy - val also : sql_policy -> sql_policy -> sql_policy val debug : string -> transaction unit
--- a/src/iflow.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/iflow.sml Tue Jul 27 14:04:09 2010 -0400 @@ -1228,9 +1228,6 @@ val allowSend : atom list * exp list -> unit val send : check -> unit - val allowEqual : { table : string, field : string, known : bool } -> unit - val mayTest : prop -> bool - val allowInsert : atom list -> unit val insert : ErrorMsg.span -> unit @@ -1509,40 +1506,11 @@ fun allowDelete v = deletable := v :: !deletable val delete = doable deletable -val testable = ref ([] : { table : string, field : string, known : bool } list) -fun allowEqual v = testable := v :: !testable -fun mayTest p = - case p of - Reln (Eq, [e1, e2]) => - let - val (_, hs, _) = !hyps - - fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x - | _ => false) hs - - fun allowed (tab, v) = - case tab of - Proj (Var tab, fd) => - List.exists (fn {table = tab', field = fd', known} => - fd' = fd - andalso tableInHyps (tab', tab) - andalso (not known orelse Cc.check (db, AReln (Known, [v])))) (!testable) - | _ => false - in - if allowed (e1, e2) orelse allowed (e2, e1) then - (assert [AReln (Eq, [e1, e2])]; - true) - else - false - end - | _ => false - fun reset () = (Cc.clear db; path := []; hyps := (0, [], ref false); nvar := 0; sendable := []; - testable := []; insertable := []; updatable := []; deletable := []) @@ -1692,8 +1660,7 @@ Add : atom -> unit, Save : unit -> 'a, Restore : 'a -> unit, - Cont : queryMode, - Send : exp -> unit + Cont : queryMode } fun doQuery (arg : 'a doQuery) (e as (_, loc)) = @@ -1732,24 +1699,24 @@ val saved = #Save arg () fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) - fun leavesE e = + fun usedFields e = case e of - Const _ => [] - | Var _ => [] - | Lvar _ => [] - | Func (_, es) => List.concat (map leavesE es) - | Recd xes => List.concat (map (leavesE o #2) xes) - | Proj _ => [e] - - fun leavesP p = - case p of - True => [] - | False => [] - | Unknown => [] - | And (p1, p2) => leavesP p1 @ leavesP p2 - | Or (p1, p2) => leavesP p1 @ leavesP p2 - | Reln (_, es) => List.concat (map leavesE es) - | Cond (e, p) => e :: leavesP p + SqConst _ => [] + | SqTrue => [] + | SqFalse => [] + | Null => [] + | SqNot e => usedFields e + | Field (v, f) => [(false, Proj (rvOf v, f))] + | Computed _ => [] + | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 + | SqKnown _ => [] + | Inj e => + (case deinj (#Env arg) e of + NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated"; + []) + | SOME e => [(true, e)]) + | SqFunc (_, e) => usedFields e + | Unmodeled => [] fun normal' () = case #Cont arg of @@ -1802,17 +1769,8 @@ inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) | inr p => p - fun getConjuncts p = - case p of - And (p1, p2) => getConjuncts p1 @ getConjuncts p2 - | _ => [p] - val saved = #Save arg () - - val conjs = getConjuncts p - val conjs = List.filter (not o St.mayTest) conjs in - app (fn p => app (#Send arg) (leavesP p)) conjs; decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} p (fn () => final () handle Cc.Contradiction => ()); #Restore arg saved @@ -2118,7 +2076,6 @@ Add = fn a => St.assert [a], Save = St.stash, Restore = St.reinstate, - Send = fn e => St.send (e, loc), Cont = AllCols (fn x => (St.assert [AReln (Eq, [r, x])]; evalExp (acc :: r :: env) b k))} q @@ -2491,7 +2448,6 @@ Add = fn a => atoms := a :: !atoms, Save = fn () => !atoms, Restore = fn ls => atoms := ls, - Send = fn _ => (), Cont = SomeCol (fn r => k (rev (!atoms), r))} fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) => @@ -2527,12 +2483,6 @@ St.allowSend ([p], outs) end | _ => ()) - | PolEqual {table = tab, field = nm, known} => - (case #1 tab of - EPrim (Prim.String tab) => St.allowEqual {table = String.extract (tab, 3, NONE), - field = nm, - known = known} - | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.") end | _ => ()
--- a/src/mono.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/mono.sml Tue Jul 27 14:04:09 2010 -0400 @@ -129,7 +129,6 @@ | PolDelete of exp | PolUpdate of exp | PolSequence of exp - | PolEqual of {table : exp, field : string, known : bool} datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list
--- a/src/mono_print.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/mono_print.sml Tue Jul 27 14:04:09 2010 -0400 @@ -429,13 +429,6 @@ | PolSequence e => box [string "sendOwnIds", space, p_exp env e] - | PolEqual {table = tab, field = nm, known} => box [string "equal", - string (if known then "Known" else "Any"), - string "[", - string nm, - string "]", - space, - p_exp env tab] fun p_decl env (dAll as (d, _) : decl) = case d of
--- a/src/mono_shake.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/mono_shake.sml Tue Jul 27 14:04:09 2010 -0400 @@ -67,7 +67,6 @@ | PolDelete e1 => e1 | PolUpdate e1 => e1 | PolSequence e1 => e1 - | PolEqual {table = e1, ...} => e1 in usedVars st e1 end
--- a/src/mono_util.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/mono_util.sml Tue Jul 27 14:04:09 2010 -0400 @@ -556,9 +556,6 @@ | PolSequence e => S.map2 (mfe ctx e, PolSequence) - | PolEqual {table = tab, field = nm, known = b} => - S.map2 (mfe ctx tab, - fn tab => PolEqual {table = tab, field = nm, known = b}) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t,
--- a/src/monoize.sml Tue Jul 27 12:12:08 2010 -0400 +++ b/src/monoize.sml Tue Jul 27 14:04:09 2010 -0400 @@ -3804,24 +3804,6 @@ (e, L'.PolUpdate) | L.EFfiApp ("Basis", "sendOwnIds", [e]) => (e, L'.PolSequence) - | L.EApp ((L.ECApp - ((L.ECApp - ((L.ECApp - ((L.ECApp - ((L.EFfi ("Basis", "equalKnown"), _), nm), _), _), _), - _), _), _), _), tab) => - (case #1 nm of - L.CName nm => (tab, fn tab => L'.PolEqual {table = tab, field = nm, known = true}) - | _ => (poly (); (e, L'.PolClient))) - | L.EApp ((L.ECApp - ((L.ECApp - ((L.ECApp - ((L.ECApp - ((L.EFfi ("Basis", "equalAny"), _), nm), _), _), _), - _), _), _), _), tab) => - (case #1 nm of - L.CName nm => (tab, fn tab => L'.PolEqual {table = tab, field = nm, known = false}) - | _ => (poly (); (e, L'.PolClient))) | _ => (poly (); (e, L'.PolClient)) val (e, fm) = monoExp (env, St.empty, fm) e
--- a/tests/equalKnown.ur Tue Jul 27 12:12:08 2010 -0400 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -type fruit = int -table fruit : { Id : fruit, Nam : string, Weight : float, Secret : string } - PRIMARY KEY Id, - CONSTRAINT Nam UNIQUE Nam - -policy sendClient (SELECT fruit.Id, fruit.Nam - FROM fruit) - -policy sendClient (SELECT fruit.Weight - FROM fruit - WHERE known(fruit.Secret)) - -policy equalKnown[#Secret] fruit - -fun main () = - x1 <- queryX (SELECT fruit.Id, fruit.Nam, fruit.Weight - FROM fruit - WHERE fruit.Nam = "apple" - AND fruit.Secret = "tasty") - (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}, {[x.Fruit.Weight]}</li></xml>); - - return <xml><body> - <ul>{x1}</ul> - </body></xml>