Mercurial > urweb
diff src/iflow.sml @ 1229:a2cd6664f57f
sendOwnIds policies
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 11 Apr 2010 17:55:37 -0400 |
parents | 7dfa67560916 |
children | 8768145eed1e |
line wrap: on
line diff
--- 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