Mercurial > urweb
changeset 339:075b36dbb1a4
Crud supports INSERT
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 14 Sep 2008 15:10:04 -0400 |
| parents | e976b187d73a |
| children | 5ccb1c6412e4 |
| files | lib/basis.urs lib/top.ur lib/top.urs src/core.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_err.sig src/elab_err.sml src/elab_ops.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml src/reduce.sml src/source.sml src/source_print.sml src/termination.sml src/urweb.grm src/urweb.lex tests/crud.ur tests/crud.urs tests/crud1.ur tests/with.ur tests/with.urp |
| diffstat | 29 files changed, 471 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.urs Sun Sep 14 11:02:18 2008 -0400 +++ b/lib/basis.urs Sun Sep 14 15:10:04 2008 -0400 @@ -257,13 +257,14 @@ con page = xhtml [] [] con xbody = xml [Body] [] [] con xtr = xml [Body, Tr] [] [] +con xform = xml [Body, LForm] [] [] (*** HTML details *) con html = [Html] con head = [Head] con body = [Body] -con lform = [Body, LForm] +con form = [Body, LForm] con tabl = [Body, Table] con tr = [Body, Tr] @@ -289,7 +290,7 @@ val a : bodyTag [Link = transaction page] val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type} - -> xml lform [] bind + -> xml form [] bind -> xml ([Body] ++ ctx) [] [] con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} => ctx ::: {Unit} -> [LForm] ~ ctx
--- a/lib/top.ur Sun Sep 14 11:02:18 2008 -0400 +++ b/lib/top.ur Sun Sep 14 15:10:04 2008 -0400 @@ -1,9 +1,21 @@ con idT = fn t :: Type => t con record = fn t :: {Type} => $t +con fstTT = fn t :: (Type * Type) => t.1 +con sndTT = fn t :: (Type * Type) => t.2 con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc => [nm = f t] ++ acc) [] +con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc => [nm] ~ acc => + [nm = f t] ++ acc) [] + +con ex = fn tf :: (Type -> Type) => + res ::: Type -> (choice :: Type -> tf choice -> res) -> res + +fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf = + fn (res ::: Type) (f : choice :: Type -> tf choice -> res) => + f [choice] body + fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v) @@ -18,6 +30,16 @@ fn r => f [nm] [t] [rest] r.nm (acc (r -- nm))) (fn _ => i) +fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) => + [[nm] ~ rest] => + fn r => f [nm] [t] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) @@ -28,6 +50,16 @@ fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) +fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) => + [[nm] ~ rest] => + fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf t -> xml ctx [] []) = @@ -37,6 +69,15 @@ fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>) <xml></xml> +fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf t -> xml ctx [] []) = + foldT2R [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => + [[nm] ~ rest] => + fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>) + <xml></xml> + fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf1 t -> tf2 t -> xml ctx [] []) = @@ -46,6 +87,15 @@ fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) <xml></xml> +fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf1 t -> tf2 t -> xml ctx [] []) = + foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => + [[nm] ~ rest] => + fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) + <xml></xml> + fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) = [tables ~ exps] => fn (f : $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
--- a/lib/top.urs Sun Sep 14 11:02:18 2008 -0400 +++ b/lib/top.urs Sun Sep 14 15:10:04 2008 -0400 @@ -1,9 +1,19 @@ con idT = fn t :: Type => t con record = fn t :: {Type} => $t +con fstTT = fn t :: (Type * Type) => t.1 +con sndTT = fn t :: (Type * Type) => t.2 con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc => [nm = f t] ++ acc) [] +con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc => [nm] ~ acc => + [nm = f t] ++ acc) [] + +con ex = fn tf :: (Type -> Type) => + res ::: Type -> (choice :: Type -> tf choice -> res) -> res + +val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf + val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) @@ -15,21 +25,42 @@ -> tf t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r +val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r + val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r +val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) + -> tr :: ({(Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r + val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf t -> xml ctx [] []) -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] +val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf t -> xml ctx [] []) + -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] + val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf1 t -> tf2 t -> xml ctx [] []) -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] +val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest + -> tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> tables ~ exps -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
--- a/src/core.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/core.sml Sun Sep 14 15:10:04 2008 -0400 @@ -93,6 +93,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } + | EWith of exp * con * exp * { field : con, rest : con } | ECut of exp * con * { field : con, rest : con } | EFold of kind
--- a/src/core_print.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/core_print.sml Sun Sep 14 15:10:04 2008 -0400 @@ -283,6 +283,32 @@ box [p_exp' true env e, string ".", p_con' true env c] + | EWith (e1, c, e2, {field, rest}) => + parenIf par (if !debug then + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + string "=", + p_exp' true env e2, + space, + string "[", + p_con env field, + space, + string " in ", + space, + p_con env rest, + string "]"] + else + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then box [p_exp' true env e,
--- a/src/core_util.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/core_util.sml Sun Sep 14 15:10:04 2008 -0400 @@ -424,6 +424,19 @@ S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) + | EWith (e1, c, e2, {field, rest}) => + S.bind2 (mfe ctx e1, + fn e1' => + S.bind2 (mfc ctx c, + fn c' => + S.bind2 (mfe ctx e2, + fn e2' => + S.bind2 (mfc ctx field, + fn field' => + S.map2 (mfc ctx rest, + fn rest' => + (EWith (e1', c', e2', {field = field', rest = rest'}), + loc)))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' =>
--- a/src/corify.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/corify.sml Sun Sep 14 15:10:04 2008 -0400 @@ -90,6 +90,7 @@ val bindStr : t -> string -> int -> t -> t val lookupStrById : t -> int -> t val lookupStrByName : string * t -> t + val lookupStrByNameOpt : string * t -> t option val bindFunctor : t -> string -> int -> string -> int -> L.str -> t val lookupFunctorById : t -> int -> string * int * L.str @@ -363,9 +364,15 @@ fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) = (case SM.find (strs, m) of - NONE => raise Fail "Corify.St.lookupStrByName" + NONE => raise Fail "Corify.St.lookupStrByName [1]" | SOME f => dummy (basis, f)) - | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" + | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName [2]" + +fun lookupStrByNameOpt (m, {basis, current = FNormal {strs, ...}, ...} : t) = + (case SM.find (strs, m) of + NONE => NONE + | SOME f => SOME (dummy (basis, f))) + | lookupStrByNameOpt _ = NONE fun bindFunctor ({basis, cons, constructors, vals, strs, funs, current = FNormal {cons = mcons, constructors = mconstructors, @@ -392,9 +399,9 @@ fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = (case SM.find (funs, m) of - NONE => raise Fail "Corify.St.lookupFunctorByName" + NONE => raise Fail "Corify.St.lookupFunctorByName [1]" | SOME v => v) - | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" + | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName [2]" end @@ -530,6 +537,8 @@ (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (corifyExp st e1, corifyCon st c, corifyExp st e2, + {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.EFold k => (L'.EFold (corifyKind k), loc) @@ -668,6 +677,22 @@ | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => ([], St.bindFunctor st x n xa na str) + | L.DStr (x, n, _, (L.StrProj (str, x'), _)) => + let + val (ds, {inner, outer}) = corifyStr (str, st) + + val st = case St.lookupStrByNameOpt (x', inner) of + SOME st' => St.bindStr st x n st' + | NONE => + let + val (x', n', str') = St.lookupFunctorByName (x', inner) + in + St.bindFunctor st x n x' n' str' + end + in + ([], st) + end + | L.DStr (x, n, _, str) => let val (ds, {inner, outer}) = corifyStr (str, st)
--- a/src/elab.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab.sml Sun Sep 14 15:10:04 2008 -0400 @@ -109,6 +109,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } + | EWith of exp * con * exp * { field : con, rest : con } | ECut of exp * con * { field : con, rest : con } | EFold of kind
--- a/src/elab_err.sig Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_err.sig Sun Sep 14 15:10:04 2008 -0400 @@ -58,7 +58,7 @@ UnboundExp of ErrorMsg.span * string | UnboundStrInExp of ErrorMsg.span * string | Unify of Elab.exp * Elab.con * Elab.con * cunify_error - | Unif of string * Elab.con + | Unif of string * ErrorMsg.span * Elab.con | WrongForm of string * Elab.exp * Elab.con | IncompatibleCons of Elab.con * Elab.con | DuplicatePatternVariable of ErrorMsg.span * string
--- a/src/elab_err.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_err.sml Sun Sep 14 15:10:04 2008 -0400 @@ -144,7 +144,7 @@ UnboundExp of ErrorMsg.span * string | UnboundStrInExp of ErrorMsg.span * string | Unify of exp * con * con * cunify_error - | Unif of string * con + | Unif of string * ErrorMsg.span * con | WrongForm of string * exp * con | IncompatibleCons of con * con | DuplicatePatternVariable of ErrorMsg.span * string @@ -173,8 +173,8 @@ ("Have con", p_con env c1), ("Need con", p_con env c2)]; cunifyError env uerr) - | Unif (action, c) => - (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action); + | Unif (action, loc, c) => + (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action); eprefaces' [("Con", p_con env c)]) | WrongForm (variety, e, t) => (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
--- a/src/elab_ops.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_ops.sml Sun Sep 14 15:10:04 2008 -0400 @@ -149,6 +149,72 @@ (CDisjoint (_, _, c), _) => unconstraint c | c => c val c = unconstraint c + + fun tryFusion () = + let + fun fuse (dom, new_v, r') = + let + val ran = #2 ks + + val f = (CApp (f, (CRel 2, loc)), loc) + val f = (CApp (f, new_v), loc) + val f = (CApp (f, (CRel 0, loc)), loc) + val f = (CAbs ("acc", ran, f), loc) + val f = (CAbs ("v", dom, f), loc) + val f = (CAbs ("nm", (KName, loc), f), loc) + + val c = (CFold (dom, ran), loc) + val c = (CApp (c, f), loc) + val c = (CApp (c, i), loc) + val c = (CApp (c, r'), loc) + in + hnormCon env c + end + in + case #1 (hnormCon env c2) of + CApp (f, r') => + (case #1 (hnormCon env f) of + CApp (f, inner_i) => + (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of + (CApp (f, inner_f), CRecord (_, [])) => + (case #1 (hnormCon env f) of + CFold (dom, _) => + let + val c = inner_f + val c = (CApp (c, nm), loc) + val c = (CApp (c, v), loc) + val c = (CApp (c, r), loc) + val c = unconstraint c + + (*val () = Print.prefaces "Onto something!" + [("c", ElabPrint.p_con env cAll), + ("c'", ElabPrint.p_con env c)]*) + + in + case #1 (hnormCon env c) of + CConcat (first, rest) => + (case (#1 (hnormCon env first), + #1 (hnormCon env rest)) of + (CRecord (_, [(nm', v')]), + CUnif (_, _, _, rR')) => + (case #1 (hnormCon env nm') of + CUnif (_, _, _, nmR') => + if rR' = rR andalso nmR' = nmR then + (nmR := SOME (CRel 2, loc); + vR := SOME (CRel 1, loc); + rR := SOME (CError, loc); + fuse (dom, v', r')) + else + default () + | _ => default ()) + | _ => default ()) + | _ => default () + end + | _ => default ()) + | _ => default ()) + | _ => default ()) + | _ => default () + end in (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) case (hnormCon env i, unconstraint c) of @@ -163,10 +229,10 @@ if nmR' = nmR andalso vR' = vR andalso rR' = rR then hnormCon env c2 else - default () - | _ => default ()) - | _ => default ()) - | _ => default () + tryFusion () + | _ => tryFusion ()) + | _ => tryFusion ()) + | _ => tryFusion () end) | _ => default ()) | _ => default ()
--- a/src/elab_print.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_print.sml Sun Sep 14 15:10:04 2008 -0400 @@ -326,6 +326,34 @@ box [p_exp' true env e, string ".", p_con' true env c] + | EWith (e1, c, e2, {field, rest}) => + parenIf par (if !debug then + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + string "=", + p_exp' true env e2, + space, + string "[", + p_con env field, + space, + string " in ", + space, + p_con env rest, + string "]"] + else + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + string "=", + space, + p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then box [p_exp' true env e,
--- a/src/elab_util.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_util.sml Sun Sep 14 15:10:04 2008 -0400 @@ -317,6 +317,19 @@ S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) + | EWith (e1, c, e2, {field, rest}) => + S.bind2 (mfe ctx e1, + fn e1' => + S.bind2 (mfc ctx c, + fn c' => + S.bind2 (mfe ctx e2, + fn e2' => + S.bind2 (mfc ctx field, + fn field' => + S.map2 (mfc ctx rest, + fn rest' => + (EWith (e1', c', e2', {field = field', rest = rest'}), + loc)))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' =>
--- a/src/elaborate.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elaborate.sml Sun Sep 14 15:10:04 2008 -0400 @@ -1019,9 +1019,11 @@ let val u = cunif (loc, k) - val (e, t, gs') = unravel (subConInCon (0, u) t', - (L'.ECApp (e, u), loc)) + val t'' = subConInCon (0, u) t' + val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc)) in + (*prefaces "Unravel" [("t'", p_con env t'), + ("t''", p_con env t'')];*) (e, t, enD gs @ gs') end | _ => (e, t, enD gs) @@ -1477,7 +1479,7 @@ let val () = checkKind env c' ck k val eb' = subConInCon (0, c') eb - handle SynUnif => (expError env (Unif ("substitution", eb)); + handle SynUnif => (expError env (Unif ("substitution", loc, eb)); cerror) in (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), @@ -1489,10 +1491,6 @@ ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4) end - | L'.CUnif _ => - (expError env (Unif ("application", et)); - (eerror, cerror, [])) - | _ => (expError env (WrongForm ("constructor function", e', et)); (eerror, cerror, [])) @@ -1586,6 +1584,22 @@ ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) end + | L.EWith (e1, c, e2) => + let + val (e1', e1t, gs1) = elabExp (env, denv) e1 + val (c', ck, gs2) = elabCon (env, denv) c + val (e2', e2t, gs3) = elabExp (env, denv) e2 + + val rest = cunif (loc, ktype_record) + val first = (L'.CRecord (ktype, [(c', e2t)]), loc) + + val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc) + val gs5 = D.prove env denv (first, rest, loc) + in + ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc), + (L'.TRecord ((L'.CConcat (first, rest), loc)), loc), + gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5) + end | L.ECut (e, c) => let val (e', et, gs1) = elabExp (env, denv) e
--- a/src/expl.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/expl.sml Sun Sep 14 15:10:04 2008 -0400 @@ -90,6 +90,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } + | EWith of exp * con * exp * { field : con, rest : con } | ECut of exp * con * { field : con, rest : con } | EFold of kind
--- a/src/expl_print.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/expl_print.sml Sun Sep 14 15:10:04 2008 -0400 @@ -289,6 +289,32 @@ box [p_exp' true env e, string ".", p_con' true env c] + | EWith (e1, c, e2, {field, rest}) => + parenIf par (if !debug then + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + string "=", + p_exp' true env e2, + space, + string "[", + p_con env field, + space, + string " in ", + space, + p_con env rest, + string "]"] + else + box [p_exp env e1, + space, + string "with", + space, + p_con' true env c, + space, + p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then box [p_exp' true env e,
--- a/src/expl_util.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/expl_util.sml Sun Sep 14 15:10:04 2008 -0400 @@ -282,6 +282,19 @@ S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) + | EWith (e1, c, e2, {field, rest}) => + S.bind2 (mfe ctx e1, + fn e1' => + S.bind2 (mfc ctx c, + fn c' => + S.bind2 (mfe ctx e2, + fn e2' => + S.bind2 (mfc ctx field, + fn field' => + S.map2 (mfc ctx rest, + fn rest' => + (EWith (e1', c', e2', {field = field', rest = rest'}), + loc)))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' =>
--- a/src/explify.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/explify.sml Sun Sep 14 15:10:04 2008 -0400 @@ -102,6 +102,8 @@ | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) + | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (explifyExp e1, explifyCon c, explifyExp e2, + {field = explifyCon field, rest = explifyCon rest}), loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) | L.EFold k => (L'.EFold (explifyKind k), loc)
--- a/src/reduce.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/reduce.sml Sun Sep 14 15:10:04 2008 -0400 @@ -130,6 +130,19 @@ | _ => false) xes of SOME (_, e, _) => #1 e | NONE => e) + | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) => + let + fun fields (remaining, passed) = + case remaining of + [] => [] + | (x, t) :: rest => + (x, + (EField (r, x, {field = t, + rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), + t) :: fields (rest, (x, t) :: passed) + in + #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc)) + end | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => let fun fields (remaining, passed) =
--- a/src/source.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/source.sml Sun Sep 14 15:10:04 2008 -0400 @@ -119,6 +119,7 @@ | ERecord of (con * exp) list | EField of exp * con + | EWith of exp * con * exp | ECut of exp * con | EFold
--- a/src/source_print.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/source_print.sml Sun Sep 14 15:10:04 2008 -0400 @@ -267,6 +267,13 @@ | EField (e, c) => box [p_exp' true e, string ".", p_con' true c] + | EWith (e1, c, e2) => parenIf par (box [p_exp e1, + space, + string "with", + space, + p_con' true c, + space, + p_exp' true e2]) | ECut (e, c) => parenIf par (box [p_exp' true e, space, string "--",
--- a/src/termination.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/termination.sml Sun Sep 14 15:10:04 2008 -0400 @@ -264,6 +264,13 @@ in (Rabble, calls) end + | EWith (e1, _, e2, _) => + let + val (_, calls) = exp (penv, calls) e1 + val (_, calls) = exp (penv, calls) e2 + in + (Rabble, calls) + end | EFold _ => (Rabble, calls) | ECase (e, pes, _) =>
--- a/src/urweb.grm Sun Sep 14 11:02:18 2008 -0400 +++ b/src/urweb.grm Sun Sep 14 15:10:04 2008 -0400 @@ -12,7 +12,7 @@ * - The names of contributors may not be used to endorse or promote products * derived from this software without specific prior written permission. * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * THIS SOFTARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE @@ -172,7 +172,7 @@ | TYPE | NAME | ARROW | LARROW | DARROW | STAR | SEMI | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | WITH | SQL | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE | CASE | IF | THEN | ELSE @@ -316,6 +316,7 @@ %right CAND %nonassoc EQ NE LT LE GT GE %right ARROW +%left WITH %right PLUSPLUS MINUSMINUS %right STAR %left NOT @@ -660,6 +661,7 @@ end) | eexp EQ eexp (native_op ("eq", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp NE eexp (native_op ("ne", eexp1, eexp2, s (eexp1left, eexp2right))) + | eexp WITH cterm EQ eexp (EWith (eexp1, cterm, eexp2), s (eexp1left, eexp2right)) eargs : earg (earg) | eargl (eargl) @@ -771,6 +773,7 @@ | LPAREN query RPAREN (query) | LPAREN CWHERE sqlexp RPAREN (sqlexp) + | LPAREN SQL sqlexp RPAREN (sqlexp) | LPAREN INSERT INTO texp LPAREN fields RPAREN VALUES LPAREN sqlexps RPAREN RPAREN (let
--- a/src/urweb.lex Sun Sep 14 11:02:18 2008 -0400 +++ b/src/urweb.lex Sun Sep 14 15:10:04 2008 -0400 @@ -300,6 +300,7 @@ <INITIAL> "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); <INITIAL> "sequence" => (Tokens.SEQUENCE (pos yypos, pos yypos + size yytext)); <INITIAL> "class" => (Tokens.CLASS (pos yypos, pos yypos + size yytext)); +<INITIAL> "with" => (Tokens.WITH (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)); @@ -309,6 +310,7 @@ <INITIAL> "FROM" => (Tokens.FROM (pos yypos, pos yypos + size yytext)); <INITIAL> "AS" => (Tokens.AS (pos yypos, pos yypos + size yytext)); <INITIAL> "WHERE" => (Tokens.CWHERE (pos yypos, pos yypos + size yytext)); +<INITIAL> "SQL" => (Tokens.SQL (pos yypos, pos yypos + size yytext)); <INITIAL> "GROUP" => (Tokens.GROUP (pos yypos, pos yypos + size yytext)); <INITIAL> "ORDER" => (Tokens.ORDER (pos yypos, pos yypos + size yytext)); <INITIAL> "BY" => (Tokens.BY (pos yypos, pos yypos + size yytext));
--- a/tests/crud.ur Sun Sep 14 11:02:18 2008 -0400 +++ b/tests/crud.ur Sun Sep 14 15:10:04 2008 -0400 @@ -1,19 +1,41 @@ -con colMeta' = fn t :: Type => {Nam : string, Show : t -> xbody} -con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols) +con colMeta = fn t_formT :: (Type * Type) => { + Nam : string, + Show : t_formT.1 -> xbody, + Widget : nm :: Name -> xml form [] [nm = t_formT.2], + Parse : t_formT.2 -> t_formT.1, + Inject : sql_injectable t_formT.1 +} +con colsMeta = fn cols :: {(Type * Type)} => $(Top.mapT2T colMeta cols) functor Make(M : sig - con cols :: {Type} + con cols :: {(Type * Type)} constraint [Id] ~ cols - val tab : sql_table ([Id = int] ++ cols) + val tab : sql_table ([Id = int] ++ mapT2T fstTT cols) val title : string - val cols : colMeta cols + val cols : colsMeta cols end) = struct open constraints M val tab = M.tab +sequence seq + +fun create (inputs : $(mapT2T sndTT M.cols)) = + id <- nextval seq; + () <- dml (insert tab (foldT2R2 [sndTT] [colMeta] + [fn cols => $(mapT2T (fn t :: (Type * Type) => + sql_exp [T = [Id = int] ++ mapT2T fstTT M.cols] [] [] t.1) cols)] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => + [[nm] ~ rest] => + fn input col acc => acc with nm = sql_inject col.Inject (col.Parse input)) + {} [M.cols] inputs M.cols + with #Id = (SQL {id}))); + return <html><body> + Inserted with ID {txt _ id}. + </body></html> + fun delete (id : int) = () <- dml (DELETE FROM tab WHERE Id = {id}); return <html><body> @@ -28,11 +50,11 @@ fun main () : transaction page = rows <- queryX (SELECT * FROM tab AS T) - (fn (fs : {T : $([Id = int] ++ M.cols)}) => <body> + (fn (fs : {T : $([Id = int] ++ mapT2T fstTT M.cols)}) => <body> <tr> <td>{txt _ fs.T.Id}</td> - {foldTRX2 [idT] [colMeta'] [tr] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) => + {foldT2RX2 [fstTT] [colMeta] [tr] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => [[nm] ~ rest] => fn v col => <tr> <td>{col.Show v}</td> @@ -51,8 +73,8 @@ <table border={1}> <tr> <th>ID</th> - {foldTRX [colMeta'] [tr] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) => + {foldT2RX [colMeta] [tr] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => [[nm] ~ rest] => fn col => <tr> <th>{cdata col.Nam}</th> @@ -61,6 +83,22 @@ </tr> {rows} </table> + + <br/> + + <lform> + {foldT2R [colMeta] [fn cols :: {(Type * Type)} => xml form [] (mapT2T sndTT cols)] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) => + [[nm] ~ rest] => + fn (col : colMeta t) (acc : xml form [] (mapT2T sndTT rest)) => <lform> + <li> {cdata col.Nam}: {col.Widget [nm]}</li> + {useMore acc} + </lform>) + <lform></lform> + [M.cols] M.cols} + + <submit action={create}/> + </lform> </body></html> end
--- a/tests/crud.urs Sun Sep 14 11:02:18 2008 -0400 +++ b/tests/crud.urs Sun Sep 14 15:10:04 2008 -0400 @@ -1,14 +1,20 @@ -con colMeta' = fn t :: Type => {Nam : string, Show : t -> xbody} -con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols) +con colMeta = fn t_formT :: (Type * Type) => { + Nam : string, + Show : t_formT.1 -> xbody, + Widget : nm :: Name -> xml form [] [nm = t_formT.2], + Parse : t_formT.2 -> t_formT.1, + Inject : sql_injectable t_formT.1 +} +con colsMeta = fn cols :: {(Type * Type)} => $(Top.mapT2T colMeta cols) functor Make(M : sig - con cols :: {Type} + con cols :: {(Type * Type)} constraint [Id] ~ cols - val tab : sql_table ([Id = int] ++ cols) + val tab : sql_table ([Id = int] ++ mapT2T fstTT cols) val title : string - val cols : colMeta cols + val cols : colsMeta cols end) : sig val main : unit -> transaction page end
--- a/tests/crud1.ur Sun Sep 14 11:02:18 2008 -0400 +++ b/tests/crud1.ur Sun Sep 14 15:10:04 2008 -0400 @@ -1,14 +1,45 @@ table t1 : {Id : int, A : int, B : string, C : float, D : bool} open Crud.Make(struct + con cols :: {(Type * Type)} = [ + A = (int, string), + B = (string, string), + C = (float, string), + D = (bool, string) + ] + val tab = t1 val title = "Crud1" val cols = { - A = {Nam = "A", Show = txt _}, - B = {Nam = "B", Show = txt _}, - C = {Nam = "C", Show = txt _}, - D = {Nam = "D", Show = txt _} + A = { + Nam = "A", + Show = txt _, + Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, + Parse = readError _, + Inject = sql_int + }, + B = { + Nam = "B", + Show = txt _, + Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, + Parse = readError _, + Inject = sql_string + }, + C = { + Nam = "C", + Show = txt _, + Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, + Parse = readError _, + Inject = sql_float + }, + D = { + Nam = "D", + Show = txt _, + Widget = fn nm :: Name => <lform><textbox{nm}/></lform>, + Parse = readError _, + Inject = sql_bool + } } end)