changeset 706:1fb318c17546

Enhance table sig item support and get demo compiling again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 15:04:07 -0400
parents e6706a1df013
children d8217b4cb617
files demo/batchFun.ur demo/batchFun.urs demo/crud.ur demo/crud.urs demo/treeFun.ur demo/treeFun.urs src/elab_err.sig src/elab_err.sml src/elaborate.sml src/source.sml src/source_print.sml src/urweb.grm tests/crud.ur tests/crud.urs tests/table_sig.ur tests/table_sig.urp tests/table_sig.urs
diffstat 17 files changed, 161 insertions(+), 104 deletions(-) [+]
line wrap: on
line diff
--- a/demo/batchFun.ur	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/batchFun.ur	Tue Apr 07 15:04:07 2009 -0400
@@ -27,7 +27,7 @@
                  constraint [Id] ~ cols
                  val fl : folder cols
                           
-                 val tab : sql_table ([Id = int] ++ map fst cols)
+                 table tab : ([Id = int] ++ map fst cols)
                            
                  val title : string
                              
--- a/demo/batchFun.urs	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/batchFun.urs	Tue Apr 07 15:04:07 2009 -0400
@@ -17,7 +17,7 @@
                  constraint [Id] ~ cols
                  val fl : folder cols
 
-                 val tab : sql_table ([Id = int] ++ map fst cols)
+                 table tab : ([Id = int] ++ map fst cols)
 
                  val title : string
 
--- a/demo/crud.ur	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/crud.ur	Tue Apr 07 15:04:07 2009 -0400
@@ -35,7 +35,7 @@
                  constraint [Id] ~ cols
                  val fl : folder cols
 
-                 val tab : sql_table ([Id = int] ++ map fst cols)
+                 table tab : ([Id = int] ++ map fst cols)
 
                  val title : string
 
--- a/demo/crud.urs	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/crud.urs	Tue Apr 07 15:04:07 2009 -0400
@@ -18,7 +18,7 @@
                  constraint [Id] ~ cols
                  val fl : folder cols
 
-                 val tab : sql_table ([Id = int] ++ map fst cols)
+                 table tab : ([Id = int] ++ map fst cols)
 
                  val title : string
 
--- a/demo/treeFun.ur	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/treeFun.ur	Tue Apr 07 15:04:07 2009 -0400
@@ -9,7 +9,7 @@
                  val key_inj : sql_injectable key
                  val option_key_inj : sql_injectable (option key)
 
-                 table tab : [id = key, parent = option key] ++ cols
+                 table tab : ([id = key, parent = option key] ++ cols)
              end) = struct
 
     open M
--- a/demo/treeFun.urs	Tue Apr 07 14:11:32 2009 -0400
+++ b/demo/treeFun.urs	Tue Apr 07 15:04:07 2009 -0400
@@ -9,7 +9,7 @@
                  val key_inj : sql_injectable key
                  val option_key_inj : sql_injectable (option key)
 
-                 table tab : [id = key, parent = option key] ++ cols
+                 table tab : ([id = key, parent = option key] ++ cols)
              end) : sig
 
     con id = M.id
--- a/src/elab_err.sig	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/elab_err.sig	Tue Apr 07 15:04:07 2009 -0400
@@ -109,7 +109,7 @@
            | 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
 
--- a/src/elab_err.sml	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/elab_err.sml	Tue Apr 07 15:04:07 2009 -0400
@@ -328,7 +328,7 @@
        | 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 @@
       | 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)];
--- a/src/elaborate.sml	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/elaborate.sml	Tue Apr 07 15:04:07 2009 -0400
@@ -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 @@
             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 @@
              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 @@
             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 @@
           | 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 @@
                   ([], 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 @@
       | 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 @@
       | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
 
 
-fun positive self =
+and positive self =
     let
         open L
 
@@ -2760,7 +2801,7 @@
         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 @@
            | _ => 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 ()*)
--- a/src/source.sml	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/source.sml	Tue Apr 07 15:04:07 2009 -0400
@@ -77,12 +77,18 @@
 
 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 @@
   | SgnWhere of sgn * string * con
   | SgnProj of string * string list * string
 
-withtype sgn_item = sgn_item' located
-and sgn = sgn' 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 pat' =
-         PWild
-       | PVar of string
-       | PPrim of Prim.t
-       | PCon of string list * string * pat option
-       | PRecord of (string * pat) list * bool
+and exp' =
+    EAnnot of exp * con
 
-withtype pat = pat' located
+  | 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
 
-datatype inference =
-         Infer
-       | DontInfer
-       | TypesOnly
+  | EKAbs of string * exp
 
-datatype exp' =
-         EAnnot of exp * con
+  | ERecord of (con * exp) list
+  | EField of exp * con
+  | EConcat of exp * exp
+  | ECut of exp * con
+  | ECutMulti 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
+  | EWild
 
-       | EKAbs of string * exp
+  | ECase of exp * (pat * exp) list
 
-       | ERecord of (con * exp) list
-       | EField of exp * con
-       | EConcat of exp * exp
-       | ECut of exp * con
-       | ECutMulti of exp * con
-
-       | EWild
-
-       | 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
--- a/src/source_print.sml	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/source_print.sml	Tue Apr 07 15:04:07 2009 -0400
@@ -417,6 +417,17 @@
                               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,
--- a/src/urweb.grm	Tue Apr 07 14:11:32 2009 -0400
+++ b/src/urweb.grm	Tue Apr 07 15:04:07 2009 -0400
@@ -532,34 +532,32 @@
        | 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)
--- a/tests/crud.ur	Tue Apr 07 14:11:32 2009 -0400
+++ b/tests/crud.ur	Tue Apr 07 15:04:07 2009 -0400
@@ -33,7 +33,7 @@
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
-                 val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+                 table tab : ([Id = int] ++ mapT2T fstTT cols)
 
                  val title : string
 
--- a/tests/crud.urs	Tue Apr 07 14:11:32 2009 -0400
+++ b/tests/crud.urs	Tue Apr 07 15:04:07 2009 -0400
@@ -16,7 +16,7 @@
 functor Make(M : sig
                  con cols :: {(Type * Type)}
                  constraint [Id] ~ cols
-                 val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+                 table tab : ([Id = int] ++ mapT2T fstTT cols)
 
                  val title : string
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/table_sig.ur	Tue Apr 07 15:04:07 2009 -0400
@@ -0,0 +1,2 @@
+table t : { A : int }
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/table_sig.urp	Tue Apr 07 15:04:07 2009 -0400
@@ -0,0 +1,3 @@
+debug
+
+table_sig
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/table_sig.urs	Tue Apr 07 15:04:07 2009 -0400
@@ -0,0 +1,1 @@
+table t : { A : int }