Crud supports INSERT

21 files changed, 283 insertions, 21 deletions

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));