diff options
Diffstat (limited to 'src/iflow.sml')
| -rw-r--r-- | src/iflow.sml | 86 |
1 files changed, 18 insertions, 68 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index c70240a7..92e568a1 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -1228,9 +1228,6 @@ structure St :> sig 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 @@ val deletable = ref ([] : atom list list) 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 @@ type 'a doQuery = { 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 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) = 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 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) = 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 @@ fun evalExp env (e as (_, loc)) k = 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 @@ fun check file = 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 @@ fun check file = 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 | _ => () |