Mercurial > urweb

changeset 243:2b9dfaffb008

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Transactions and queries, at source level
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 14:48:33 -0400
parents cc193f680193
children 71bafe66dbe1
files lib/basis.lig src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elaborate.sml src/lacweb.grm src/lacweb.lex tests/query.lac
diffstat 8 files changed, 105 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/lib/basis.lig	Thu Aug 28 14:05:47 2008 -0400
+++ b/lib/basis.lig	Thu Aug 28 14:48:33 2008 -0400
@@ -146,6 +146,26 @@
 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
 
 
+(*** Executing queries *)
+
+con transaction :: Type -> Type
+val return : t ::: Type
+        -> t -> transaction t
+val bind : t1 ::: Type -> t2 ::: Type
+        -> transaction t1 -> (t1 -> transaction t2)
+        -> transaction t2
+
+val query : tables ::: {{Type}} -> exps ::: {Type}
+        -> sql_query tables exps
+        -> state ::: Type
+        -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+                -> $exps
+                -> state
+                -> transaction state)
+        -> state
+        -> transaction state
+
+
 (** XML *)
 
 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
--- a/src/elab_env.sig	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/elab_env.sig	Thu Aug 28 14:48:33 2008 -0400
@@ -103,4 +103,6 @@
 
     val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn
 
+    val patBinds : env -> Elab.pat -> env
+
 end
--- a/src/elab_env.sml	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/elab_env.sml	Thu Aug 28 14:48:33 2008 -0400
@@ -1049,4 +1049,13 @@
             pushClass env n
         end
 
+fun patBinds env (p, loc) =
+    case p of
+        PWild => env
+      | PVar (x, t) => pushERel env x t
+      | PPrim _ => env
+      | PCon (_, _, _, NONE) => env
+      | PCon (_, _, _, SOME p) => patBinds env p
+      | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
+
 end
--- a/src/elab_print.sml	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/elab_print.sml	Thu Aug 28 14:48:33 2008 -0400
@@ -360,7 +360,7 @@
                                                                              space,
                                                                              string "=>",
                                                                              space,
-                                                                             p_exp env e]) pes])
+                                                                             p_exp (E.patBinds env p) e]) pes])
 
       | EError => string "<ERROR>"
       | EUnif (ref (SOME e)) => p_exp env e
--- a/src/elaborate.sml	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/elaborate.sml	Thu Aug 28 14:48:33 2008 -0400
@@ -1268,6 +1268,13 @@
        | Datatype of coverage IM.map
        | Record of coverage SM.map list
 
+fun c2s c =
+    case c of
+        Wild => "Wild"
+      | None => "None"
+      | Datatype _ => "Datatype"
+      | Record _ => "Record"
+
 fun exhaustive (env, denv, t, ps) =
     let
         fun pcCoverage pc =
@@ -1359,26 +1366,39 @@
             end
 
         fun coverageImp (c1, c2) =
-            case (c1, c2) of
-                (Wild, _) => true
-
-              | (Datatype cmap1, Datatype cmap2) =>
-                List.all (fn (n, c2) =>
-                             case IM.find (cmap1, n) of
-                                 NONE => false
-                               | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
-
-              | (Record fmaps1, Record fmaps2) =>
-                List.all (fn fmap2 =>
-                             List.exists (fn fmap1 =>
-                                             List.all (fn (x, c2) =>
-                                                          case SM.find (fmap1, x) of
-                                                              NONE => true
-                                                            | SOME c1 => coverageImp (c1, c2))
-                                                      (SM.listItemsi fmap2))
-                                         fmaps1) fmaps2
-
-              | _ => false
+            let
+                val r =
+                    case (c1, c2) of
+                        (Wild, _) => true
+
+                      | (Datatype cmap1, Datatype cmap2) =>
+                        List.all (fn (n, c2) =>
+                                     case IM.find (cmap1, n) of
+                                         NONE => false
+                                       | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
+                      | (Datatype cmap1, Wild) =>
+                        List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1)
+
+                      | (Record fmaps1, Record fmaps2) =>
+                        List.all (fn fmap2 =>
+                                     List.exists (fn fmap1 =>
+                                                     List.all (fn (x, c2) =>
+                                                                  case SM.find (fmap1, x) of
+                                                                      NONE => true
+                                                                    | SOME c1 => coverageImp (c1, c2))
+                                                              (SM.listItemsi fmap2))
+                                                 fmaps1) fmaps2
+
+                      | (Record fmaps1, Wild) =>
+                        List.exists (fn fmap1 =>
+                                        List.all (fn (x, c1) => coverageImp (c1, Wild))
+                                        (SM.listItemsi fmap1)) fmaps1
+
+                      | _ => false
+            in
+                (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*)
+                r
+            end
 
         fun isTotal (c, t) =
             case c of
--- a/src/lacweb.grm	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/lacweb.grm	Thu Aug 28 14:48:33 2008 -0400
@@ -154,7 +154,7 @@
  | CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
  | DATATYPE | OF
  | TYPE | NAME
- | ARROW | LARROW | DARROW | STAR
+ | ARROW | LARROW | DARROW | STAR | SEMI
  | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
  | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE
@@ -277,6 +277,8 @@
 
 %name Lacweb
 
+%right SEMI
+%nonassoc LARROW
 %nonassoc IF THEN ELSE
 %nonassoc DARROW
 %nonassoc COLON
@@ -286,7 +288,7 @@
 %right OR
 %right CAND
 %nonassoc EQ NE LT LE GT GE
-%right ARROW LARROW
+%right ARROW
 %right PLUSPLUS MINUSMINUS
 %right STAR
 %left NOT
@@ -586,6 +588,13 @@
                                              (ECase (eexp1, [((PCon (["Basis"], "True", NONE), loc), eexp2),
                                                              ((PCon (["Basis"], "False", NONE), loc), eexp3)]), loc)
                                          end)
+       | SYMBOL LARROW eexp SEMI eexp   (let
+                                             val loc = s (SYMBOLleft, eexp2right)
+                                             val e = (EVar (["Basis"], "bind"), loc)
+                                             val e = (EApp (e, eexp1), loc)
+                                         in
+                                             (EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc)
+                                         end)
 
 eargs  : earg                           (earg)
        | eargl                          (eargl)
@@ -725,8 +734,10 @@
                                          s (LPARENleft, RPARENright))
 
 rpat   : CSYMBOL EQ pat                 ([(CSYMBOL, pat)], false)
+       | INT EQ pat                     ([(Int64.toString INT, pat)], false)
        | DOTDOTDOT                      ([], true)
        | CSYMBOL EQ pat COMMA rpat      ((CSYMBOL, pat) :: #1 rpat, #2 rpat)
+       | INT EQ pat COMMA rpat          ((Int64.toString INT, pat) :: #1 rpat, #2 rpat)
 
 ptuple : pat COMMA pat                  ([pat1, pat2])
        | pat COMMA ptuple               (pat :: ptuple)
@@ -892,12 +903,12 @@
 tname  : CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
        | LBRACE cexp RBRACE             (cexp)
 
-table  : SYMBOL                         ((CName SYMBOL, s (SYMBOLleft, SYMBOLright)),
+table  : SYMBOL                         ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)),
                                          (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
        | SYMBOL AS tname                (tname, (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
        | LBRACE LBRACE eexp RBRACE RBRACE AS tname    (tname, eexp)
 
-tident : SYMBOL                         (CName SYMBOL, s (SYMBOLleft, SYMBOLright))
+tident : SYMBOL                         (CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright))
        | CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
        | LBRACE LBRACE cexp RBRACE RBRACE (cexp)
 
--- a/src/lacweb.lex	Thu Aug 28 14:05:47 2008 -0400
+++ b/src/lacweb.lex	Thu Aug 28 14:48:33 2008 -0400
@@ -266,6 +266,8 @@
 <INITIAL> "~"         => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext));
 <INITIAL> "|"         => (Tokens.BAR (pos yypos, pos yypos + size yytext));
 <INITIAL> "*"         => (Tokens.STAR (pos yypos, pos yypos + size yytext));
+<INITIAL> "<-"        => (Tokens.LARROW (pos yypos, pos yypos + size yytext));
+<INITIAL> ";"         => (Tokens.SEMI (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "con"       => (Tokens.CON (pos yypos, pos yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/query.lac	Thu Aug 28 14:48:33 2008 -0400
@@ -0,0 +1,16 @@
+table t1 : {A : int, B : string, C : float}
+table t2 : {A : float, D : int}
+
+datatype list a = Nil | Cons of a * list a
+
+val q1 = (SELECT * FROM t1)
+val r1 : transaction (list {A : int, B : string, C : float}) =
+        query q1
+        (fn fs _ acc => return (Cons (fs.T1, acc)))
+        Nil
+
+val r2 : transaction int =
+        ls <- r1;
+        return (case ls of
+                    Nil => 0
+                  | Cons ({A = a, ...}, _) => a)