Mercurial > urweb
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 } +