Crud supports INSERT

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