Mercurial > urweb
diff src/iflow.sml @ 2216:70ec9bb337be
Progress towards invalidation based on equalities of fields.
| author | Ziv Scully <ziv@mit.edu> |
|---|---|
| date | Mon, 10 Nov 2014 22:04:40 -0500 |
| parents | 4d64af730e35 |
| children | 278e10629ba1 |
line wrap: on
line diff
--- a/src/iflow.sml Fri Oct 31 09:25:03 2014 -0400 +++ b/src/iflow.sml Mon Nov 10 22:04:40 2014 -0500 @@ -16,7 +16,7 @@ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN @@ -115,36 +115,36 @@ | PCon1 s => box [string (s ^ "("), p_list p_exp es, string ")"] - | Eq => p_bop "=" es - | Ne => p_bop "<>" es - | Lt => p_bop "<" es - | Le => p_bop "<=" es - | Gt => p_bop ">" es - | Ge => p_bop ">=" es + | Cmp Eq => p_bop "=" es + | Cmp Ne => p_bop "<>" es + | Cmp Lt => p_bop "<" es + | Cmp Le => p_bop "<=" es + | Cmp Gt => p_bop ">" es + | Cmp Ge => p_bop ">=" es fun p_prop p = case p of True => string "True" | False => string "False" | Unknown => string "??" - | And (p1, p2) => box [string "(", - p_prop p1, - string ")", - space, - string "&&", - space, - string "(", - p_prop p2, - string ")"] - | Or (p1, p2) => box [string "(", - p_prop p1, - string ")", - space, - string "||", - space, - string "(", - p_prop p2, - string ")"] + | Lop (And, p1, p2) => box [string "(", + p_prop p1, + string ")", + space, + string "&&", + space, + string "(", + p_prop p2, + string ")"] + | Lop (Or, p1, p2) => box [string "(", + p_prop p1, + string ")", + space, + string "||", + space, + string "(", + p_prop p2, + string ")"] | Reln (r, es) => p_reln r es | Cond (e, p) => box [string "(", p_exp e, @@ -518,7 +518,7 @@ Variety = Nothing, Known = ref (!(#Known (unNode r))), Ge = ref NONE}) - + val r'' = ref (Node {Id = nodeId (), Rep = ref NONE, Cons = #Cons (unNode r), @@ -529,7 +529,7 @@ #Rep (unNode r) := SOME r''; r' end - | _ => raise Contradiction + | _ => raise Contradiction end in rep e @@ -687,9 +687,9 @@ end | _ => raise Contradiction end - | (Eq, [e1, e2]) => + | (Cmp Eq, [e1, e2]) => markEq (representative (db, e1), representative (db, e2)) - | (Ge, [e1, e2]) => + | (Cmp Ge, [e1, e2]) => let val r1 = representative (db, e1) val r2 = representative (db, e2) @@ -734,14 +734,14 @@ (case #Variety (unNode (representative (db, e))) of Dt1 (f', _) => f' = f | _ => false) - | (Eq, [e1, e2]) => + | (Cmp Eq, [e1, e2]) => let val r1 = representative (db, e1) val r2 = representative (db, e2) in repOf r1 = repOf r2 end - | (Ge, [e1, e2]) => + | (Cmp Ge, [e1, e2]) => let val r1 = representative (db, e1) val r2 = representative (db, e2) @@ -848,7 +848,7 @@ (hyps := (n', hs, ref false); Cc.clear db; app (fn a => Cc.assert (db, a)) hs) - end + end fun useKeys () = let @@ -872,7 +872,7 @@ let val r = Cc.check (db, - AReln (Eq, [Proj (r1, f), + AReln (Cmp Eq, [Proj (r1, f), Proj (r2, f)])) in (*Print.prefaces "Fs" @@ -888,7 +888,7 @@ r end)) ks then (changed := true; - Cc.assert (db, AReln (Eq, [r1, r2])); + Cc.assert (db, AReln (Cmp Eq, [r1, r2])); finder (hyps, acc)) else finder (hyps, a :: acc) @@ -1115,7 +1115,7 @@ val (_, hs, _) = !hyps in hnames := n + 1; - hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false) + hyps := (n, List.filter (fn AReln (Cmp Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false) end fun check a = Cc.check (db, a) @@ -1138,7 +1138,7 @@ val ls = removeDups ls in if List.exists (fn x' => x' = x) ls then - ls + ls else x :: ls end @@ -1171,7 +1171,7 @@ | Null => inl (Func (DtCon0 "None", [])) | SqNot e => inr (case expIn e of - inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])]) + inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.False", [])]) | inr _ => Unknown) | Field (v, f) => inl (Proj (rvOf v, f)) | Computed _ => default () @@ -1181,15 +1181,15 @@ val e2 = expIn e2 in inr (case (bo, e1, e2) of - (Exps f, inl e1, inl e2) => f (e1, e2) - | (Props f, v1, v2) => + (RCmp c, inl e1, inl e2) => Reln (Cmp c, [e1, e2]) + | (RLop l, v1, v2) => let fun pin v = case v of - inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) + inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) | inr p => p in - f (pin v1, pin v2) + Lop (l, pin v1, pin v2) end | _ => Unknown) end @@ -1205,7 +1205,7 @@ (case expIn e of inl e => inl (Func (Other f, [e])) | _ => default ()) - + | Unmodeled => inl (Func (Other "allow", [rv ()])) end in @@ -1219,8 +1219,8 @@ True => (k () handle Cc.Contradiction => ()) | False => () | Unknown => () - | And (p1, p2) => go p1 (fn () => go p2 k) - | Or (p1, p2) => + | Lop (And, p1, p2) => go p1 (fn () => go p2 k) + | Lop (Or, p1, p2) => let val saved = save () in @@ -1351,7 +1351,7 @@ | SOME e => let val p = case expIn e of - inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) + inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) | inr p => p val saved = #Save arg () @@ -1365,9 +1365,9 @@ fun normal () = doWhere normal' in (case #Select r of - [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => - (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of - Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => + [SqExp (Binop (RCmp bo, Count, SqConst (Prim.Int 0)), f)] => + (case bo of + Gt => (case #Cont arg of SomeCol _ => () | AllCols k => @@ -1469,7 +1469,7 @@ evalExp env e (fn e => doArgs (es, e :: acc)) in doArgs (es, []) - end + end in case #1 e of EPrim p => k (Const p) @@ -1519,7 +1519,7 @@ ([], []) => (evalExp env' (#body rf) (fn _ => ()); St.reinstate saved; default ()) - + | (arg :: args, mode :: modes) => evalExp env arg (fn arg => let @@ -1663,7 +1663,7 @@ Save = St.stash, Restore = St.reinstate, Cont = AllCols (fn x => - (St.assert [AReln (Eq, [r, x])]; + (St.assert [AReln (Cmp Eq, [r, x])]; evalExp (acc :: r :: env) b k))} q end) | EDml (e, _) => @@ -1697,15 +1697,15 @@ | Delete (tab, e) => let val old = St.nextVar () - + val expIn = expIn (Var o St.nextVar) env (fn "T" => Var old | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE") val p = case expIn e of - inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" + inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" | inr p => p - + val saved = St.stash () in St.assert [AReln (Sql (tab ^ "$Old"), [Var old]), @@ -1748,7 +1748,7 @@ (f, Proj (Var old, f)) :: fs) fs fs' val p = case expIn e of - inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" + inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" | inr p => p val saved = St.stash () in @@ -1764,7 +1764,7 @@ k (Recd [])) handle Cc.Contradiction => ()) end) - + | ENextval (EPrim (Prim.String (_, seq)), _) => let val nv = St.nextVar () @@ -1780,7 +1780,7 @@ val e = Var (St.nextVar ()) val e' = Func (Other ("cookie/" ^ cname), []) in - St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])]; + St.assert [AReln (Known, [e]), AReln (Cmp Eq, [e, e'])]; k e end @@ -2159,7 +2159,7 @@ end | _ => ()) end - + | _ => () in app decl (#1 file)