diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/c/urweb.c | 5 | ||||
-rw-r--r-- | src/iflow.sml | 19 | ||||
-rw-r--r-- | src/settings.sml | 3 |
3 files changed, 24 insertions, 3 deletions
diff --git a/src/c/urweb.c b/src/c/urweb.c index 7821a999..6815c85b 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -3404,3 +3404,8 @@ uw_Basis_unit uw_Basis_debug(uw_context ctx, uw_Basis_string s) { return uw_unit_v; } + +uw_Basis_int uw_Basis_rand(uw_context ctx) { + uw_Basis_int n = abs(rand()); + return n; +} diff --git a/src/iflow.sml b/src/iflow.sml index 1e6d2411..862ed1b9 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -972,6 +972,7 @@ datatype sqexp = SqConst of Prim.t | SqTrue | SqFalse + | SqNot of sqexp | Field of string * string | Computed of string | Binop of Rel * sqexp * sqexp @@ -1075,6 +1076,8 @@ fun sqexp chs = wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",") (follow (keep (fn ch => ch <> #")")) (const ")"))))) (fn ((), (e, _)) => e), + wrap (follow (const "(NOT ") (follow sqexp (const ")"))) + (fn ((), (e, _)) => SqNot e), wrap (follow (ws (const "(")) (follow (wrap (follow sqexp @@ -1471,8 +1474,8 @@ fun doable pols (loc : ErrorMsg.span) = val (_, hs, _) = !hyps in ErrorMsg.errorAt loc "The database update policy may be violated here."; - Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs), - ("E-graph", Cc.p_database db)] + Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*, + ("E-graph", Cc.p_database db)*)] end end @@ -1558,6 +1561,10 @@ fun expIn rv env rvOf = SqConst p => inl (Const p) | SqTrue => inl (Func (DtCon0 "Basis.bool.True", [])) | SqFalse => inl (Func (DtCon0 "Basis.bool.False", [])) + | SqNot e => + inr (case expIn e of + inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])]) + | inr _ => Unknown) | Field (v, f) => inl (Proj (rvOf v, f)) | Computed _ => default () | Binop (bo, e1, e2) => @@ -1674,6 +1681,7 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) = SqConst _ => [] | SqTrue => [] | SqFalse => [] + | SqNot e => usedFields e | Field (v, f) => [(false, Proj (rvOf v, f))] | Computed _ => [] | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 @@ -1865,6 +1873,13 @@ fun evalExp env (e as (_, loc)) k = | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e]))) | EFfi _ => default () + | EFfiApp ("Basis", "rand", []) => + let + val e = Var (St.nextVar ()) + in + St.assert [AReln (Known, [e])]; + k e + end | EFfiApp x => doFfi x | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e]) diff --git a/src/settings.sml b/src/settings.sml index 3d163ca5..967efe07 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -115,7 +115,8 @@ val benignBase = basis ["get_cookie", "onDisconnect", "onServerError", "kc", - "debug"] + "debug", + "rand"] val benign = ref benignBase fun setBenignEffectful ls = benign := S.addList (benignBase, ls) |