# HG changeset patch # User Adam Chlipala # Date 1219949313 14400 # Node ID 2b9dfaffb008d814ae461324a10c42a24f796bb0 # Parent cc193f680193b36a77b16a417be9ef7c0abb967d Transactions and queries, at source level diff -r cc193f680193 -r 2b9dfaffb008 lib/basis.lig --- 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 diff -r cc193f680193 -r 2b9dfaffb008 src/elab_env.sig --- 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 diff -r cc193f680193 -r 2b9dfaffb008 src/elab_env.sml --- 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 diff -r cc193f680193 -r 2b9dfaffb008 src/elab_print.sml --- 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 "" | EUnif (ref (SOME e)) => p_exp env e diff -r cc193f680193 -r 2b9dfaffb008 src/elaborate.sml --- 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 diff -r cc193f680193 -r 2b9dfaffb008 src/lacweb.grm --- 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) diff -r cc193f680193 -r 2b9dfaffb008 src/lacweb.lex --- 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 @@ "~" => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext)); "|" => (Tokens.BAR (pos yypos, pos yypos + size yytext)); "*" => (Tokens.STAR (pos yypos, pos yypos + size yytext)); + "<-" => (Tokens.LARROW (pos yypos, pos yypos + size yytext)); + ";" => (Tokens.SEMI (pos yypos, pos yypos + size yytext)); "con" => (Tokens.CON (pos yypos, pos yypos + size yytext)); "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext)); diff -r cc193f680193 -r 2b9dfaffb008 tests/query.lac --- /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)