summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/basis.urs5
-rw-r--r--lib/top.ur50
-rw-r--r--lib/top.urs31
-rw-r--r--src/core.sml1
-rw-r--r--src/core_print.sml26
-rw-r--r--src/core_util.sml13
-rw-r--r--src/corify.sml33
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_err.sig2
-rw-r--r--src/elab_err.sml6
-rw-r--r--src/elab_ops.sml74
-rw-r--r--src/elab_print.sml28
-rw-r--r--src/elab_util.sml13
-rw-r--r--src/elaborate.sml28
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_print.sml26
-rw-r--r--src/expl_util.sml13
-rw-r--r--src/explify.sml2
-rw-r--r--src/reduce.sml13
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml7
-rw-r--r--src/termination.sml7
-rw-r--r--src/urweb.grm7
-rw-r--r--src/urweb.lex2
-rw-r--r--tests/crud.ur58
-rw-r--r--tests/crud.urs16
-rw-r--r--tests/crud1.ur39
-rw-r--r--tests/with.ur5
-rw-r--r--tests/with.urp5
29 files changed, 471 insertions, 42 deletions
diff --git a/lib/basis.urs b/lib/basis.urs
index 672153b6..ed217e3a 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -257,13 +257,14 @@ con xhtml = xml [Html]
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 li : bodyTag []
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
diff --git a/lib/top.ur b/lib/top.ur
index 3fac43a7..15f2a732 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -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 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
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 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
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 @@ fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
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 @@ fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
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)
diff --git a/lib/top.urs b/lib/top.urs
index 8fb6e480..17ce5c28 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -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 @@ val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
-> 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)
diff --git a/src/core.sml b/src/core.sml
index 1fcf26c4..11055aa4 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -93,6 +93,7 @@ datatype exp' =
| 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
diff --git a/src/core_print.sml b/src/core_print.sml
index 6e32dde3..0d470d39 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -283,6 +283,32 @@ fun p_exp' par env (e, _) =
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,
diff --git a/src/core_util.sml b/src/core_util.sml
index 9b6b7d39..76f1b2c0 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -424,6 +424,19 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
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' =>
diff --git a/src/corify.sml b/src/corify.sml
index 92c429ef..e20cdd2c 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -90,6 +90,7 @@ structure St : sig
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 lookupStrById ({basis, strs, ...} : t) n =
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 lookupFunctorById ({funs, ...} : t) n =
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 @@ fun corifyExp st (e, loc) =
(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 @@ fun corifyDecl ((d, loc : EM.span), st) =
| 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)
diff --git a/src/elab.sml b/src/elab.sml
index 2e8d12f6..0ce86726 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -109,6 +109,7 @@ datatype exp' =
| 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
diff --git a/src/elab_err.sig b/src/elab_err.sig
index 7682cd31..1fd234b7 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -58,7 +58,7 @@ signature ELAB_ERR = sig
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
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 34e26cd1..8131633c 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -144,7 +144,7 @@ datatype exp_error =
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 @@ fun expError env err =
("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);
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index d73180ff..e236e62d 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -149,6 +149,72 @@ fun hnormCon env (cAll as (c, loc)) =
(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 @@ fun hnormCon env (cAll as (c, loc)) =
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 ()
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 4dc41ca7..36d6a48e 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -326,6 +326,34 @@ fun p_exp' par env (e, _) =
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,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 02b95130..cc4fbe4a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -317,6 +317,19 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
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' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0c313f14..70404cf1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1019,9 +1019,11 @@ fun elabHead (env, denv) (e as (_, loc)) t =
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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((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
diff --git a/src/expl.sml b/src/expl.sml
index c55461fc..9e35d674 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -90,6 +90,7 @@ datatype exp' =
| 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
diff --git a/src/expl_print.sml b/src/expl_print.sml
index dd328bb5..39df4e3f 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -289,6 +289,32 @@ fun p_exp' par env (e, loc) =
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,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index b8376b5b..8dec2687 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -282,6 +282,19 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
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' =>
diff --git a/src/explify.sml b/src/explify.sml
index c45e7305..573ddf51 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -102,6 +102,8 @@ fun explifyExp (e, loc) =
| 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)
diff --git a/src/reduce.sml b/src/reduce.sml
index 9cc57cb2..0250175f 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -130,6 +130,19 @@ fun exp env e =
| _ => 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) =
diff --git a/src/source.sml b/src/source.sml
index bfb54194..14d4d6f8 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -119,6 +119,7 @@ datatype exp' =
| ERecord of (con * exp) list
| EField of exp * con
+ | EWith of exp * con * exp
| ECut of exp * con
| EFold
diff --git a/src/source_print.sml b/src/source_print.sml
index 4844e508..e1a8de7a 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -267,6 +267,13 @@ fun p_exp' par (e, _) =
| 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 "--",
diff --git a/src/termination.sml b/src/termination.sml
index 65c770df..e2337e54 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -264,6 +264,13 @@ fun declOk' env (d, loc) =
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, _) =>
diff --git a/src/urweb.grm b/src/urweb.grm
index e9d081a5..d3e7fe5b 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -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 @@ fun tagIn bt =
| 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 @@ fun tagIn bt =
%right CAND
%nonassoc EQ NE LT LE GT GE
%right ARROW
+%left WITH
%right PLUSPLUS MINUSMINUS
%right STAR
%left NOT
@@ -660,6 +661,7 @@ eexp : eapps (eapps)
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 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
| 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
diff --git a/src/urweb.lex b/src/urweb.lex
index 8d861082..6f6bb63f 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -300,6 +300,7 @@ notags = [^<{\n]+;
<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 @@ notags = [^<{\n]+;
<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));
diff --git a/tests/crud.ur b/tests/crud.ur
index 75136226..0a7efeec 100644
--- a/tests/crud.ur
+++ b/tests/crud.ur
@@ -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 confirm (id : int) = return <html><body>
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 @@ fun main () : transaction page =
<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 @@ fun main () : transaction page =
</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
diff --git a/tests/crud.urs b/tests/crud.urs
index 988c5458..d445ed6e 100644
--- a/tests/crud.urs
+++ b/tests/crud.urs
@@ -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
diff --git a/tests/crud1.ur b/tests/crud1.ur
index f9d67ed8..fa539dd3 100644
--- a/tests/crud1.ur
+++ b/tests/crud1.ur
@@ -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)
diff --git a/tests/with.ur b/tests/with.ur
new file mode 100644
index 00000000..458153b3
--- /dev/null
+++ b/tests/with.ur
@@ -0,0 +1,5 @@
+val r = ({A = 1, B = 2} with #C = "Hi") with #D = "Bye"
+
+fun main () : transaction page = return <html><body>
+ {cdata r.C}, {cdata r.D}
+</body></html>
diff --git a/tests/with.urp b/tests/with.urp
new file mode 100644
index 00000000..9e1e7fb6
--- /dev/null
+++ b/tests/with.urp
@@ -0,0 +1,5 @@
+debug
+database dbname=test
+exe /tmp/webapp
+
+with
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 05:45:42 +0000