diff options
| -rw-r--r-- | demo/batchFun.ur | 2 | ||||
| -rw-r--r-- | demo/batchFun.urs | 2 | ||||
| -rw-r--r-- | demo/crud.ur | 2 | ||||
| -rw-r--r-- | demo/crud.urs | 2 | ||||
| -rw-r--r-- | demo/treeFun.ur | 2 | ||||
| -rw-r--r-- | demo/treeFun.urs | 2 | ||||
| -rw-r--r-- | src/elab_err.sig | 2 | ||||
| -rw-r--r-- | src/elab_err.sml | 6 | ||||
| -rw-r--r-- | src/elaborate.sml | 111 | ||||
| -rw-r--r-- | src/source.sml | 73 | ||||
| -rw-r--r-- | src/source_print.sml | 11 | ||||
| -rw-r--r-- | src/urweb.grm | 40 | ||||
| -rw-r--r-- | tests/crud.ur | 2 | ||||
| -rw-r--r-- | tests/crud.urs | 2 | ||||
| -rw-r--r-- | tests/table_sig.ur | 2 | ||||
| -rw-r--r-- | tests/table_sig.urp | 3 | ||||
| -rw-r--r-- | tests/table_sig.urs | 1 |
17 files changed, 161 insertions, 104 deletions
diff --git a/demo/batchFun.ur b/demo/batchFun.ur index 2eed464b..35276d0e 100644 --- a/demo/batchFun.ur +++ b/demo/batchFun.ur @@ -27,7 +27,7 @@ functor Make(M : sig 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 diff --git a/demo/batchFun.urs b/demo/batchFun.urs index 695576c5..e3acb197 100644 --- a/demo/batchFun.urs +++ b/demo/batchFun.urs @@ -17,7 +17,7 @@ functor Make(M : sig 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 diff --git a/demo/crud.ur b/demo/crud.ur index dc9a5b7c..cf120697 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -35,7 +35,7 @@ functor Make(M : sig 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 diff --git a/demo/crud.urs b/demo/crud.urs index 57ab3808..9b1055b2 100644 --- a/demo/crud.urs +++ b/demo/crud.urs @@ -18,7 +18,7 @@ functor Make(M : sig 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 diff --git a/demo/treeFun.ur b/demo/treeFun.ur index 15fe60f5..25d11927 100644 --- a/demo/treeFun.ur +++ b/demo/treeFun.ur @@ -9,7 +9,7 @@ functor Make(M : sig 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 diff --git a/demo/treeFun.urs b/demo/treeFun.urs index 501a0575..64a14f4f 100644 --- a/demo/treeFun.urs +++ b/demo/treeFun.urs @@ -9,7 +9,7 @@ functor Make(M : sig 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 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) diff --git a/tests/crud.ur b/tests/crud.ur index 8aff038d..f085b44e 100644 --- a/tests/crud.ur +++ b/tests/crud.ur @@ -33,7 +33,7 @@ fun bool name = {Nam = name, 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 diff --git a/tests/crud.urs b/tests/crud.urs index 33090421..ffb1d3f1 100644 --- a/tests/crud.urs +++ b/tests/crud.urs @@ -16,7 +16,7 @@ val bool : string -> colMeta (bool, bool) 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 diff --git a/tests/table_sig.ur b/tests/table_sig.ur new file mode 100644 index 00000000..0603d755 --- /dev/null +++ b/tests/table_sig.ur @@ -0,0 +1,2 @@ +table t : { A : int } + diff --git a/tests/table_sig.urp b/tests/table_sig.urp new file mode 100644 index 00000000..6a161ed1 --- /dev/null +++ b/tests/table_sig.urp @@ -0,0 +1,3 @@ +debug + +table_sig diff --git a/tests/table_sig.urs b/tests/table_sig.urs new file mode 100644 index 00000000..40dde3c0 --- /dev/null +++ b/tests/table_sig.urs @@ -0,0 +1 @@ +table t : { A : int } |