Transactions and queries, at source level

6 files changed, 69 insertions, 25 deletions

diff --git a/src/elab_env.sig b/src/elab_env.sig
index 32ba7906..1d265991 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -103,4 +103,6 @@ signature ELAB_ENV = sig
 
     val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn
 
+    val patBinds : env -> Elab.pat -> env
+
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 936d8fce..a1a68974 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1049,4 +1049,13 @@ fun declBinds env (d, loc) =
             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 --git a/src/elab_print.sml b/src/elab_print.sml
index 72453f29..337b1d8a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -360,7 +360,7 @@ fun p_exp' par env (e, _) =
                                                                              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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 746a06b7..b86514e7 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1268,6 +1268,13 @@ datatype coverage =
        | 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 @@ fun exhaustive (env, denv, t, ps) =
             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 --git a/src/lacweb.grm b/src/lacweb.grm
index 87fa4655..feff82df 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -154,7 +154,7 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
  | 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 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
 
 %name Lacweb
 
+%right SEMI
+%nonassoc LARROW
 %nonassoc IF THEN ELSE
 %nonassoc DARROW
 %nonassoc COLON
@@ -286,7 +288,7 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
 %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 @@ eexp   : eapps                          (eapps)
                                              (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 @@ pterm  : SYMBOL                         (PVar SYMBOL, s (SYMBOLleft, SYMBOLright
                                          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 @@ tables : table                          ([table])
 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 --git a/src/lacweb.lex b/src/lacweb.lex
index b7459675..e593c5fe 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -266,6 +266,8 @@ notags = [^<{\n]+;
 <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));