Enhance table sig item support and get demo compiling again

6 files changed, 147 insertions, 96 deletions

diff --git a/src/elab_err.sig b/src/elab_err.sig
index 3b14406b..c0a90e19 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -109,7 +109,7 @@ signature ELAB_ERR = sig
            | NotFunctor of Elab.sgn
            | FunctorRebind of ErrorMsg.span
            | UnOpenable of Elab.sgn
-           | NotType of Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+           | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
            | DuplicateConstructor of string * ErrorMsg.span
            | NotDatatype of ErrorMsg.span
 
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 221e4981..4f24e225 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -328,7 +328,7 @@ datatype str_error =
        | NotFunctor of sgn
        | FunctorRebind of ErrorMsg.span
        | UnOpenable of sgn
-       | NotType of kind * (kind * kind * kunify_error)
+       | NotType of ErrorMsg.span * kind * (kind * kind * kunify_error)
        | DuplicateConstructor of string * ErrorMsg.span
        | NotDatatype of ErrorMsg.span
 
@@ -344,8 +344,8 @@ fun strError env err =
       | UnOpenable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
          eprefaces' [("Signature", p_sgn env sgn)])
-      | NotType (k, (k1, k2, ue)) =>
-        (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
+      | NotType (loc, k, (k1, k2, ue)) =>
+        (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
          eprefaces' [("Kind", p_kind env k),
                      ("Subkind 1", p_kind env k1),
                      ("Subkind 2", p_kind env k2)];
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 224c3e50..d83af65b 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -871,16 +871,7 @@
      let
          fun err f = raise CUnify' (f (c1All, c2All))
 
-         fun isRecord () = unifyRecordCons env (c1All, c2All)
-     in
-         (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
-                                  ("c2All", p_con env c2All)];*)
-
-         case (c1, c2) of
-             (L'.CError, _) => ()
-           | (_, L'.CError) => ()
-
-           | (L'.CProj (c1, n1), _) =>
+         fun projSpecial1 (c1, n1, onFail) =
              let
                  fun trySnd () =
                      case #1 (hnormCon env c2All) of
@@ -890,7 +881,7 @@
                                  if n1 = n2 then
                                      unifyCons' env c1 c2
                                  else
-                                     err CIncompatible
+                                     onFail ()
                          in
                              case #1 (hnormCon env c2) of
                                  L'.CUnif (_, k, _, r) =>
@@ -906,7 +897,7 @@
                                     | _ => tryNormal ())
                             | _ => tryNormal ()
                          end
-                       | _ => err CIncompatible
+                       | _ => onFail ()
              in
                  case #1 (hnormCon env c1) of
                      L'.CUnif (_, k, _, r) =>
@@ -923,20 +914,35 @@
                    | _ => trySnd ()
              end
 
-           | (_, L'.CProj (c2, n2)) =>
-             (case #1 (hnormCon env c2) of
-                  L'.CUnif (_, k, _, r) =>
-                  (case #1 (hnormKind k) of
-                       L'.KTuple ks =>
-                       let
-                           val loc = #2 c2
-                           val us = map (fn k => cunif (loc, k)) ks
-                       in
-                           r := SOME (L'.CTuple us, loc);
-                           unifyCons' env c1All (List.nth (us, n2 - 1))
-                       end
-                     | _ => err CIncompatible)
-                | _ => err CIncompatible)
+         fun projSpecial2 (c2, n2, onFail) =
+             case #1 (hnormCon env c2) of
+                 L'.CUnif (_, k, _, r) =>
+                 (case #1 (hnormKind k) of
+                      L'.KTuple ks =>
+                      let
+                          val loc = #2 c2
+                          val us = map (fn k => cunif (loc, k)) ks
+                      in
+                          r := SOME (L'.CTuple us, loc);
+                          unifyCons' env c1All (List.nth (us, n2 - 1))
+                      end
+                    | _ => onFail ())
+               | _ => onFail ()
+
+         fun isRecord' () = unifyRecordCons env (c1All, c2All)
+
+         fun isRecord () =
+             case (c1, c2) of
+                 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
+               | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
+               | _ => isRecord' ()
+     in
+         (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
+                                  ("c2All", p_con env c2All)];*)
+
+         case (c1, c2) of
+             (L'.CError, _) => ()
+           | (_, L'.CError) => ()
 
            | (L'.CRecord _, _) => isRecord ()
            | (_, L'.CRecord _) => isRecord ()
@@ -1020,6 +1026,9 @@
              ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
               handle ListPair.UnequalLengths => err CIncompatible)
 
+           | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
+           | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
+
            | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
              (unifyKinds env dom1 dom2;
               unifyKinds env ran1 ran2)
@@ -2013,11 +2022,43 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             val c' = normClassConstraint env c'
         in
             (unifyKinds env ck ktype
-             handle KUnify ue => strError env (NotType (ck, ue)));
+             handle KUnify ue => strError env (NotType (loc, ck, ue)));
 
             ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
         end
 
+      | L.SgiTable (x, c, e) =>
+        let
+            val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
+            val x' = x ^ "_hidden_constraints"
+            val (env', hidden_n) = E.pushCNamed env x' cstK NONE
+            val hidden = (L'.CNamed hidden_n, loc)
+
+            val (c', ck, gs') = elabCon (env, denv) c
+            val visible = cunif (loc, cstK)
+            val uniques = (L'.CConcat (visible, hidden), loc)
+
+            val ct = tableOf ()
+            val ct = (L'.CApp (ct, c'), loc)
+            val ct = (L'.CApp (ct, uniques), loc)
+
+            val (env', n) = E.pushENamed env' x ct
+
+            val (e', et, gs'') = elabExp (env, denv) e
+            val gs'' = List.mapPartial (fn Disjoint x => SOME x
+                                         | _ => NONE) gs''
+
+            val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
+            val cst = (L'.CApp (cst, c'), loc)
+            val cst = (L'.CApp (cst, visible), loc)
+        in
+            checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
+            checkCon env' e' et cst;
+
+            ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
+              (L'.SgiVal (x, n, ct), loc)], (env', denv, gs'' @ gs' @ gs))
+        end
+
       | L.SgiStr (x, sgn) =>
         let
             val (sgn', gs') = elabSgn (env, denv) sgn
@@ -2213,7 +2254,7 @@ and elabSgn (env, denv) (sgn, loc) =
              end)
                                                               
 
-fun selfify env {str, strs, sgn} =
+and selfify env {str, strs, sgn} =
     case #1 (hnormSgn env sgn) of
         L'.SgnError => sgn
       | L'.SgnVar _ => sgn
@@ -2238,7 +2279,7 @@ fun selfify env {str, strs, sgn} =
             NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
           | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
 
-fun selfifyAt env {str, sgn} =
+and selfifyAt env {str, sgn} =
     let
         fun self (str, _) =
             case str of
@@ -2254,7 +2295,7 @@ fun selfifyAt env {str, sgn} =
           | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
     end
 
-fun dopen env {str, strs, sgn} =
+and dopen env {str, strs, sgn} =
     let
         val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
                 (L'.StrVar str, #2 sgn) strs
@@ -2307,7 +2348,7 @@ fun dopen env {str, strs, sgn} =
                   ([], env))
     end
 
-fun sgiOfDecl (d, loc) =
+and sgiOfDecl (d, loc) =
     case d of
         L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
       | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
@@ -2326,7 +2367,7 @@ fun sgiOfDecl (d, loc) =
       | L'.DDatabase _ => []
       | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
 
-fun subSgn env sgn1 (sgn2 as (_, loc2)) =
+and subSgn env sgn1 (sgn2 as (_, loc2)) =
     ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
                         ("sgn2", p_sgn env sgn2)];*)
     case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -2694,7 +2735,7 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
       | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
 
 
-fun positive self =
+and positive self =
     let
         open L
 
@@ -2760,7 +2801,7 @@ fun positive self =
         pos
     end
 
-fun wildifyStr env (str, sgn) =
+and wildifyStr env (str, sgn) =
     case #1 (hnormSgn env sgn) of
         L'.SgnConst sgis =>
         (case #1 str of
@@ -2922,7 +2963,7 @@ fun wildifyStr env (str, sgn) =
            | _ => str)
       | _ => str
 
-fun elabDecl (dAll as (d, loc), (env, denv, gs)) =
+and elabDecl (dAll as (d, loc), (env, denv, gs)) =
     let
         (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
         (*val befor = Time.now ()*)
diff --git a/src/source.sml b/src/source.sml
index 42927ef3..0dca39ab 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -77,12 +77,18 @@ datatype con' =
 
 withtype con = con' located
 
+datatype inference =
+         Infer
+       | DontInfer
+       | TypesOnly
+
 datatype sgn_item' =
          SgiConAbs of string * kind
        | SgiCon of string * kind option * con
        | SgiDatatype of string * string list * (string * con option) list
        | SgiDatatypeImp of string * string list * string
        | SgiVal of string * con
+       | SgiTable of string * con * exp
        | SgiStr of string * sgn
        | SgiSgn of string * sgn
        | SgiInclude of sgn
@@ -97,56 +103,51 @@ and sgn' =
   | SgnWhere of sgn * string * con
   | SgnProj of string * string list * string
 
-withtype sgn_item = sgn_item' located
-and sgn = sgn' located
-
-datatype pat' =
-         PWild
-       | PVar of string
-       | PPrim of Prim.t
-       | PCon of string list * string * pat option
-       | PRecord of (string * pat) list * bool
-
-withtype pat = pat' located
+and pat' =
+    PWild
+  | PVar of string
+  | PPrim of Prim.t
+  | PCon of string list * string * pat option
+  | PRecord of (string * pat) list * bool
 
-datatype inference =
-         Infer
-       | DontInfer
-       | TypesOnly
-
-datatype exp' =
-         EAnnot of exp * con
+and exp' =
+    EAnnot of exp * con
 
-       | EPrim of Prim.t
-       | EVar of string list * string * inference
-       | EApp of exp * exp
-       | EAbs of string * con option * exp
-       | ECApp of exp * con
-       | ECAbs of explicitness * string * kind * exp
-       | EDisjoint of con * con * exp
-       | EDisjointApp of exp
+  | EPrim of Prim.t
+  | EVar of string list * string * inference
+  | EApp of exp * exp
+  | EAbs of string * con option * exp
+  | ECApp of exp * con
+  | ECAbs of explicitness * string * kind * exp
+  | EDisjoint of con * con * exp
+  | EDisjointApp of exp
 
-       | EKAbs of string * exp
+  | EKAbs of string * exp
 
-       | ERecord of (con * exp) list
-       | EField of exp * con
-       | EConcat of exp * exp
-       | ECut of exp * con
-       | ECutMulti of exp * con
+  | ERecord of (con * exp) list
+  | EField of exp * con
+  | EConcat of exp * exp
+  | ECut of exp * con
+  | ECutMulti of exp * con
 
-       | EWild
+  | EWild
 
-       | ECase of exp * (pat * exp) list
+  | ECase of exp * (pat * exp) list
 
-       | ELet of edecl list * exp
+  | ELet of edecl list * exp
 
 and edecl' =
     EDVal of string * con option * exp
   | EDValRec of (string * con option * exp) list
 
-withtype exp = exp' located
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+and pat = pat' located
+and exp = exp' located
 and edecl = edecl' located
 
+
+
 datatype decl' =
          DCon of string * kind option * con
        | DDatatype of string * string list * (string * con option) list
diff --git a/src/source_print.sml b/src/source_print.sml
index d1c9b6df..c145dc63 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -417,6 +417,17 @@ fun p_sgn_item (sgi, _) =
                               string ":",
                               space,
                               p_con c]
+      | SgiTable (x, c, e) => box [string "table",
+                                space,
+                                string x,
+                                space,
+                                string ":",
+                                space,
+                                p_con c,
+                                space,
+                                string "constraints",
+                                space,
+                                p_exp e]
       | SgiStr (x, sgn) => box [string "structure",
                                 space,
                                 string x,
diff --git a/src/urweb.grm b/src/urweb.grm
index ad92ff11..0f4b58d7 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -532,34 +532,32 @@ sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
        | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
        | LPAREN sgn RPAREN              (sgn)
 
-sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, kindright))
-       | LTYPE SYMBOL                   (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
-                                         s (LTYPEleft, SYMBOLright))
-       | CON SYMBOL EQ cexp             (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
-       | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
-       | LTYPE SYMBOL EQ cexp           (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
-                                         s (LTYPEleft, cexpright))
-       | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+sgi    : CON SYMBOL DCOLON kind         ((SgiConAbs (SYMBOL, kind), s (CONleft, kindright)))
+       | LTYPE SYMBOL                   ((SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
+                                          s (LTYPEleft, SYMBOLright)))
+       | CON SYMBOL EQ cexp             ((SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)))
+       | CON SYMBOL DCOLON kind EQ cexp ((SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)))
+       | LTYPE SYMBOL EQ cexp           ((SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
+                                          s (LTYPEleft, cexpright)))
+       | DATATYPE SYMBOL dargs EQ barOpt dcons((SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)))
        | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
                 (case dargs of
                      [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
                    | _ => raise Fail "Arguments specified for imported datatype")
-       | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
+       | VAL SYMBOL COLON cexp          ((SgiVal (SYMBOL, cexp), s (VALleft, cexpright)))
 
-       | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
-       | SIGNATURE CSYMBOL EQ sgn       (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
+       | STRUCTURE CSYMBOL COLON sgn    ((SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)))
+       | SIGNATURE CSYMBOL EQ sgn       ((SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)))
        | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
-                                        (SgiStr (CSYMBOL1,
-                                                 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
-                                         s (FUNCTORleft, sgn2right))
-       | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
-       | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
-       | TABLE SYMBOL COLON cexp        (let
-                                             val loc = s (TABLEleft, cexpright)
-                                             val t = (CApp ((CVar (["Basis"], "sql_table"), loc),
-                                                            entable cexp), loc)
+                                        ((SgiStr (CSYMBOL1,
+                                                  (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
+                                          s (FUNCTORleft, sgn2right)))
+       | INCLUDE sgn                    ((SgiInclude sgn, s (INCLUDEleft, sgnright)))
+       | CONSTRAINT cterm TWIDDLE cterm ((SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)))
+       | TABLE SYMBOL COLON cterm cstopt(let
+                                             val loc = s (TABLEleft, ctermright)
                                          in
-                                             (SgiVal (SYMBOL, t), loc)
+                                             (SgiTable (SYMBOL, entable cterm, cstopt), loc)
                                          end)
        | SEQUENCE SYMBOL                (let
                                              val loc = s (SEQUENCEleft, SYMBOLright)