Parsing and elaborating 'table'

10 files changed, 149 insertions, 5 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 011bc8d2..25ec6a79 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -119,6 +119,7 @@ datatype sgn_item' =
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
        | SgiConstraint of con * con
+       | SgiTable of string * int * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -142,6 +143,7 @@ datatype decl' =
        | DFfiStr of string * int * sgn
        | DConstraint of con * con
        | DExport of int * sgn * str
+       | DTable of string * int * con
 
      and str' =
          StrConst of decl list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index eac0c662..2d6afa4a 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -404,6 +404,16 @@ fun sgiBinds env (sgi, loc) =
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | SgiConstraint _ => env
 
+      | SgiTable (x, n, c) =>
+        (case lookupStr env "Basis" of
+             NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis"
+           | SOME (n, _) =>
+             let
+                 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
+             in
+                 pushENamedAs env x n t
+             end)
+
 fun sgnSeek f sgis =
     let
         fun seek (sgis, sgns, strs, cons) =
@@ -431,6 +441,7 @@ fun sgnSeek f sgis =
                       | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
                       | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
                       | SgiConstraint _ => seek (sgis, sgns, strs, cons)
+                      | SgiTable _ => seek (sgis, sgns, strs, cons)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty)
     end
@@ -666,6 +677,7 @@ fun sgnSeekConstraints (str, sgis) =
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
                   | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
+                  | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty, [])
     end
@@ -725,5 +737,14 @@ fun declBinds env (d, loc) =
       | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
       | DConstraint _ => env
       | DExport _ => env
+      | DTable (x, n, c) =>
+        (case lookupStr env "Basis" of
+             NONE => raise Fail "ElabEnv.declBinds: Can't find Basis"
+           | SOME (n, _) =>
+             let
+                 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
+             in
+                 pushENamedAs env x n t
+             end)
 
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index ceea43a9..a46a642a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -447,6 +447,13 @@ fun p_sgn_item env (sgi, _) =
                                        string "~",
                                        space,
                                        p_con env c2]
+      | SgiTable (x, n, c) => box [string "table",
+                                   space,
+                                   p_named x n,
+                                   space,
+                                   string ":",
+                                   space,
+                                   p_con env c]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -596,6 +603,13 @@ fun p_decl env (dAll as (d, _) : decl) =
                                       string ":",
                                       space,
                                       p_sgn env sgn]
+      | DTable (x, n, c) => box [string "table",
+                                 space,
+                                 p_named x n,
+                                 space,
+                                 string ":",
+                                 space,
+                                 p_con env c]
 
 and p_str env (str, _) =
     case str of
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 5fa0fa27..8cd02549 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -436,6 +436,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                             S.map2 (con ctx c2,
                                     fn c2' =>
                                        (SgiConstraint (c1', c2'), loc)))
+              | SgiTable (x, n, c) =>
+                S.map2 (con ctx c,
+                        fn c' =>
+                           (SgiTable (x, n, c'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -458,7 +462,8 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, Str (x, sgn))
                                                  | SgiSgn (x, _, sgn) =>
                                                    bind (ctx, Sgn (x, sgn))
-                                                 | SgiConstraint _ => ctx,
+                                                 | SgiConstraint _ => ctx
+                                                 | SgiTable _ => ctx,
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -594,7 +599,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                  | DFfiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
                                                  | DConstraint _ => ctx
-                                                 | DExport _ => ctx,
+                                                 | DExport _ => ctx
+                                                 | DTable _ => ctx,
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -682,6 +688,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                     fn str' =>
                                        (DExport (en, sgn', str'), loc)))
 
+              | DTable (x, n, c) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (DTable (x, n, c'), loc))
+
         and mfvi ctx (x, n, c, e) =
             S.bind2 (mfc ctx c,
                   fn c' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 976db303..b6073e7f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -163,6 +163,7 @@ val strerror = (L'.StrError, dummy)
 val int = ref cerror
 val float = ref cerror
 val string = ref cerror
+val table = ref cerror
 
 local
     val count = ref 0
@@ -1735,6 +1736,15 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
         end
 
+      | L.SgiTable (x, c) =>
+        let
+            val (c', k, gs) = elabCon (env, denv) c
+            val (env, n) = E.pushENamed env x c'
+        in
+            checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
+            ([(L'.SgiTable (x, n, c'), loc)], (env, denv, gs))
+        end
+
 and elabSgn (env, denv) (sgn, loc) =
     case sgn of
         L.SgnConst sgis =>
@@ -1795,7 +1805,13 @@ and elabSgn (env, denv) (sgn, loc) =
                                    else
                                        ();
                                    (cons, vals, sgns, SS.add (strs, x)))
-                                | L'.SgiConstraint _ => (cons, vals, sgns, strs))
+                                | L'.SgiConstraint _ => (cons, vals, sgns, strs)
+                                | L'.SgiTable (x, _, _) =>
+                                  (if SS.member (vals, x) then
+                                       sgnError env (DuplicateVal (loc, x))
+                                   else
+                                       ();
+                                   (cons, SS.add (vals, x), sgns, strs)))
                     (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
         in
             ((L'.SgnConst sgis', loc), gs)
@@ -1894,6 +1910,11 @@ fun selfifyAt env {str, sgn} =
           | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
     end
 
+fun tableOf env =
+    case E.lookupStr env "Basis" of
+        NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
+      | SOME (n, _) => (L'.CModProj (n, [], "sql_table"), ErrorMsg.dummySpan)
+
 fun dopen (env, denv) {str, strs, sgn} =
     let
         val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
@@ -1925,6 +1946,9 @@ fun dopen (env, denv) {str, strs, sgn} =
                                               (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
                                             | L'.SgiConstraint (c1, c2) =>
                                               (L'.DConstraint (c1, c2), loc)
+                                            | L'.SgiTable (x, n, c) =>
+                                              (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc),
+                                                        (L'.EModProj (str, strs, x), loc)), loc)
                                   in
                                       (d, (E.declBinds env' d, denv'))
                                   end)
@@ -1977,6 +2001,7 @@ fun sgiOfDecl (d, loc) =
       | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
       | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
       | L'.DExport _ => []
+      | L'.DTable (x, n, c) => [(L'.SgiTable (x, n, c), loc)]
 
 fun sgiBindsD (env, denv) (sgi, _) =
     case sgi of
@@ -2169,6 +2194,16 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                  SOME (env, denv))
                                      else
                                          NONE
+                                   | L'.SgiTable (x', n1, c1) =>
+                                     if x = x' then
+                                         (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of
+                                              [] => SOME (env, denv)
+                                            | _ => NONE)
+                                         handle CUnify (c1, c2, err) =>
+                                                (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                 SOME (env, denv))
+                                     else
+                                         NONE
                                    | _ => NONE)
 
                       | L'.SgiStr (x, n2, sgn2) =>
@@ -2230,6 +2265,21 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      else
                                          NONE
                                    | _ => NONE)
+
+                      | L'.SgiTable (x, n2, c2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiTable (x', n1, c1) =>
+                                     if x = x' then
+                                         (case unifyCons (env, denv) c1 c2 of
+                                              [] => SOME (env, denv)
+                                            | _ => NONE)
+                                         handle CUnify (c1, c2, err) =>
+                                                (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                 SOME (env, denv))
+                                     else
+                                         NONE
+                                   | _ => NONE)
                 end
         in
             ignore (foldl folder (env, denv) sgis2)
@@ -2579,6 +2629,15 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
             ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs))
         end
 
+      | L.DTable (x, c) =>
+        let
+            val (c', k, gs) = elabCon (env, denv) c
+            val (env, n) = E.pushENamed env x c'
+        in
+            checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
+            ([(L'.DTable (x, n, c'), loc)], (env, denv, gs))
+        end
+
 and elabStr (env, denv) (str, loc) =
     case str of
         L.StrConst ds =>
@@ -2669,7 +2728,17 @@ and elabStr (env, denv) (str, loc) =
                               in
                                   ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs))
+                            | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
+                            | L'.SgiTable (x, n, c) =>
+                              let
+                                  val (vals, x) =
+                                      if SS.member (vals, x) then
+                                          (vals, "?" ^ x)
+                                      else
+                                          (SS.add (vals, x), x)
+                              in
+                                  ((L'.SgiTable (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+                              end)
 
                 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
         in
@@ -2751,6 +2820,7 @@ fun elabFile basis env file =
         val () = discoverC int "int"
         val () = discoverC float "float"
         val () = discoverC string "string"
+        val () = discoverC table "sql_table"
 
         fun elabDecl' (d, (env, gs)) =
             let
diff --git a/src/explify.sml b/src/explify.sml
index 9fe24ebe..f33d2b64 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -123,6 +123,7 @@ fun explifySgi (sgi, loc) =
       | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
       | L.SgiConstraint _ => NONE
+      | L.SgiTable _ => raise Fail "Explify SgiTable"
 
 and explifySgn (sgn, loc) =
     case sgn of
@@ -151,6 +152,7 @@ fun explifyDecl (d, loc : EM.span) =
       | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
       | L.DConstraint (c1, c2) => NONE
       | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
+      | L.DTable _ => raise Fail "Explify DTable"
 
 and explifyStr (str, loc) =
     case str of
diff --git a/src/lacweb.grm b/src/lacweb.grm
index f1cb5ce3..0ca7298d 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -34,6 +34,11 @@ val s = ErrorMsg.spanOf
 fun uppercaseFirst "" = ""
   | uppercaseFirst s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
 
+fun entable t =
+    case #1 t of
+        TRecord c => c
+      | _ => t
+
 %%
 %header (functor LacwebLrValsFn(structure Token : TOKEN))
 
@@ -50,7 +55,7 @@ fun uppercaseFirst "" = ""
  | ARROW | LARROW | DARROW | STAR
  | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
- | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT
+ | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE
  | CASE | IF | THEN | ELSE
 
  | XML_BEGIN of string | XML_END
@@ -177,6 +182,7 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
                                            | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
        | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))
+       | TABLE SYMBOL COLON cexp        (DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))
 
 dargs  :                                ([])
        | SYMBOL dargs                   (SYMBOL :: dargs)
@@ -234,6 +240,7 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
                                          s (FUNCTORleft, sgn2right))
        | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
        | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
+       | TABLE SYMBOL COLON cexp        (SgiTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 0bb5ca38..8a9756d1 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -279,6 +279,7 @@ notags = [^<{\n]+;
 <INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));
 <INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext));
 <INITIAL> "export"    => (Tokens.EXPORT (pos yypos, pos yypos + size yytext));
+<INITIAL> "table"     => (Tokens.TABLE (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 505dd172..4e4ddc54 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -78,6 +78,7 @@ datatype sgn_item' =
        | SgiSgn of string * sgn
        | SgiInclude of sgn
        | SgiConstraint of con * con
+       | SgiTable of string * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -131,6 +132,7 @@ datatype decl' =
        | DConstraint of con * con
        | DOpenConstraints of string * string list
        | DExport of str
+       | DTable of string * con
 
      and str' =
          StrConst of decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index 15bb6015..75c8ad3a 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -360,6 +360,13 @@ fun p_sgn_item (sgi, _) =
                                        string "~",
                                        space,
                                        p_con c2]
+      | SgiTable (x, c) => box [string "table",
+                                space,
+                                string x,
+                                space,
+                                string ":",
+                                space,
+                                p_con c]
 
 and p_sgn (sgn, _) =
     case sgn of
@@ -505,6 +512,13 @@ fun p_decl ((d, _) : decl) =
       | DExport str => box [string "export",
                             space,
                             p_str str]
+      | DTable (x, c) => box [string "table",
+                              space,
+                              string x,
+                              space,
+                              string ":",
+                              space,
+                              p_con c]
 
 and p_str (str, _) =
     case str of