changeset 1250:e80582b927f2

Add rand to Basis and handle it in Iflow
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 17:24:42 -0400
parents 7c6fc92f6c31
children 70092a661f70
files include/urweb.h lib/ur/basis.urs src/c/urweb.c src/iflow.sml src/settings.sml
diffstat 5 files changed, 28 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/include/urweb.h	Thu Apr 29 11:47:24 2010 -0400
+++ b/include/urweb.h	Thu Apr 29 17:24:42 2010 -0400
@@ -280,4 +280,6 @@
 
 void uw_set_client_data(uw_context, void *);
 
+uw_Basis_int uw_Basis_rand(uw_context);
+
 #endif
--- a/lib/ur/basis.urs	Thu Apr 29 11:47:24 2010 -0400
+++ b/lib/ur/basis.urs	Thu Apr 29 17:24:42 2010 -0400
@@ -821,3 +821,5 @@
 val also : sql_policy -> sql_policy -> sql_policy
 
 val debug : string -> transaction unit
+
+val rand : transaction int
--- a/src/c/urweb.c	Thu Apr 29 11:47:24 2010 -0400
+++ b/src/c/urweb.c	Thu Apr 29 17:24:42 2010 -0400
@@ -3404,3 +3404,8 @@
 
   return uw_unit_v;
 }
+
+uw_Basis_int uw_Basis_rand(uw_context ctx) {
+  uw_Basis_int n = abs(rand());
+  return n;
+}
--- a/src/iflow.sml	Thu Apr 29 11:47:24 2010 -0400
+++ b/src/iflow.sml	Thu Apr 29 17:24:42 2010 -0400
@@ -972,6 +972,7 @@
          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 @@
            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 @@
                 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 @@
                     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 @@
                                     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 @@
           | 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])
 
--- a/src/settings.sml	Thu Apr 29 11:47:24 2010 -0400
+++ b/src/settings.sml	Thu Apr 29 17:24:42 2010 -0400
@@ -115,7 +115,8 @@
                         "onDisconnect",
                         "onServerError",
                         "kc",
-                        "debug"]
+                        "debug",
+                        "rand"]
 
 val benign = ref benignBase
 fun setBenignEffectful ls = benign := S.addList (benignBase, ls)