Replace 'with' with '++'

21 files changed, 189 insertions, 131 deletions

diff --git a/lib/top.ur b/lib/top.ur
index d36af3f3..347b2a35 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -4,6 +4,9 @@ con idT (t :: Type) = t
 con record (t :: {Type}) = $t
 con fstTT (t :: (Type * Type)) = t.1
 con sndTT (t :: (Type * Type)) = t.2
+con fstTTT (t :: (Type * Type * Type)) = t.1
+con sndTTT (t :: (Type * Type * Type)) = t.2
+con thdTTT (t :: (Type * Type * Type)) = t.3
 
 con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
                                          [nm = f t] ++ acc) []
@@ -14,6 +17,9 @@ con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
 con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
                                                    [nm = f t] ++ acc) []
 
+con mapT3T (f :: (Type * 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
 
@@ -80,6 +86,17 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
                  f [nm] [t] [rest] r.nm (acc (r -- nm)))
              (fn _ => i)
 
+fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
+            (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                 -> fn [[nm] ~ rest] =>
+                       tf t -> tr rest -> tr ([nm = t] ++ rest))
+            (i : tr []) =
+    fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r]
+             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+                              (acc : _ -> tr rest) [[nm] ~ rest] 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}
                  -> fn [[nm] ~ rest] =>
@@ -103,6 +120,18 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
                  f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
              (fn _ _ => i)
 
+fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
+             (tr :: {(Type * Type * Type)} -> Type)
+             (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                  -> fn [[nm] ~ rest] =>
+                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+             (i : tr []) =
+    fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r]
+             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+                              (acc : _ -> _ -> tr rest) [[nm] ~ rest] 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}
                  -> fn [[nm] ~ rest] =>
@@ -122,6 +151,16 @@ fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
                 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
             <xml/>
 
+fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
+             (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                  -> fn [[nm] ~ rest] =>
+                        tf t -> xml ctx [] []) =
+    foldT3R [tf] [fn _ => xml ctx [] []]
+            (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+                             [[nm] ~ rest] r acc =>
+                <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+            <xml/>
+
 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
              (f : nm :: Name -> t :: Type -> rest :: {Type}
                   -> fn [[nm] ~ rest] =>
@@ -143,6 +182,17 @@ fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
                  <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
              <xml/>
 
+fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
+              (ctx :: {Unit})
+              (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                   -> fn [[nm] ~ rest] =>
+                         tf1 t -> tf2 t -> xml ctx [] []) =
+    foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
+             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+                              [[nm] ~ rest] r1 r2 acc =>
+                 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+             <xml/>
+
 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
            (q : sql_query tables exps) [tables ~ exps]
            (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
diff --git a/lib/top.urs b/lib/top.urs
index 6e9dda4e..d52ec9d7 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -4,6 +4,9 @@ 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 fstTTT = fn t :: (Type * Type * Type) => t.1
+con sndTTT = fn t :: (Type * Type * Type) => t.2
+con thdTTT = fn t :: (Type * Type * Type) => t.3
 
 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
                                              [nm = f t] ++ acc) []
@@ -14,6 +17,9 @@ con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
                                                        [nm = f t] ++ acc) []
 
+con mapT3T = fn f :: (Type * 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
 
@@ -55,6 +61,12 @@ val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
                         tf t -> tr rest -> tr ([nm = t] ++ rest))
               -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
 
+val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
+              -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                  -> fn [[nm] ~ rest] =>
+                        tf t -> tr rest -> tr ([nm = t] ++ rest))
+              -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r
+
 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
               -> tr :: ({Type} -> Type)
               -> (nm :: Name -> t :: Type -> rest :: {Type}
@@ -71,6 +83,14 @@ val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                -> tr [] -> r :: {(Type * Type)}
                -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
 
+val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
+               -> tr :: ({(Type * Type * Type)} -> Type)
+               -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                   -> fn [[nm] ~ rest] =>
+                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+               -> tr [] -> r :: {(Type * Type * Type)}
+               -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r
+
 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
               -> (nm :: Name -> t :: Type -> rest :: {Type}
                   -> fn [[nm] ~ rest] =>
@@ -83,6 +103,12 @@ val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
                          tf t -> xml ctx [] [])
                -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
 
+val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
+               -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                   -> fn [[nm] ~ rest] =>
+                         tf t -> xml ctx [] [])
+               -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] []
+
 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
                -> (nm :: Name -> t :: Type -> rest :: {Type}
                    -> fn [[nm] ~ rest] =>
@@ -98,6 +124,15 @@ val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
                 -> r :: {(Type * Type)}
                 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
 
+
+val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
+                -> ctx :: {Unit}
+                -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+                    -> fn [[nm] ~ rest] =>
+                          tf1 t -> tf2 t -> xml ctx [] [])
+                -> r :: {(Type * Type * Type)}
+                -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] []
+
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
              -> sql_query tables exps
              -> fn [tables ~ exps] =>
diff --git a/src/core.sml b/src/core.sml
index 11055aa4..baec6e41 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -93,7 +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 }
+       | EConcat of exp * con * exp * 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 0d470d39..1214a54f 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -283,31 +283,26 @@ fun p_exp' par env (e, _) =
             box [p_exp' true env e,
                  string ".",
                  p_con' true env c]
-      | EWith (e1, c, e2, {field, rest}) =>
+      | EConcat (e1, c1, e2, c2) =>
         parenIf par (if !debug then
-                         box [p_exp env e1,
+                         box [p_exp' true env e1,
                               space,
-                              string "with",
+                              string ":",
                               space,
-                              p_con' true env c,
+                              p_con env c1,
+                              space,
+                              string "++",
                               space,
-                              string "=",
                               p_exp' true env e2,
                               space,
-                              string "[",
-                              p_con env field,
+                              string ":",
                               space,
-                              string " in ",
-                              space,
-                              p_con env rest,
-                              string "]"]
+                              p_con env c2]
                      else
-                         box [p_exp env e1,
+                         box [p_exp' true 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
diff --git a/src/core_util.sml b/src/core_util.sml
index df8465ae..f0697183 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -424,19 +424,17 @@ 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}) =>
+              | EConcat (e1, c1, e2, c2) =>
                 S.bind2 (mfe ctx e1,
                       fn e1' =>
-                         S.bind2 (mfc ctx c,
-                              fn c' =>
+                         S.bind2 (mfc ctx c1,
+                              fn c1' =>
                                  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))))))
+                                          S.map2 (mfc ctx c2,
+                                               fn c2' =>
+                                                  (EConcat (e1', c1', e2', c2'),
+                                                   loc)))))
               | ECut (e, c, {field, rest}) =>
                 S.bind2 (mfe ctx e,
                       fn e' =>
diff --git a/src/corify.sml b/src/corify.sml
index 89d1e63f..ff9506fd 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -566,8 +566,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.EConcat (e1, c1, e2, c2) => (L'.EConcat (corifyExp st e1, corifyCon st c1, corifyExp st e2,
+                                                   corifyCon st c2), 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)
diff --git a/src/elab.sml b/src/elab.sml
index 9bb609bf..4202d367 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -108,7 +108,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 }
+       | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
        | EFold of kind
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c1bc5938..8c0b41f7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -317,33 +317,26 @@ fun p_exp' par env (e, _) =
             box [p_exp' true env e,
                  string ".",
                  p_con' true env c]
-      | EWith (e1, c, e2, {field, rest}) =>
+      | EConcat (e1, c1, e2, c2) =>
         parenIf par (if !debug then
-                         box [p_exp env e1,
+                         box [p_exp' true env e1,
                               space,
-                              string "with",
+                              string ":",
                               space,
-                              p_con' true env c,
+                              p_con env c1,
                               space,
-                              string "=",
-                              p_exp' true env e2,
+                              string "++",
                               space,
-                              string "[",
-                              p_con env field,
+                              p_exp' true env e2,
                               space,
-                              string " in ",
+                              string ":",
                               space,
-                              p_con env rest,
-                              string "]"]
+                              p_con env c2]
                      else
-                         box [p_exp env e1,
+                         box [p_exp' true 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
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 69ed3248..247e2b3a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -309,19 +309,17 @@ 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}) =>
+              | EConcat (e1, c1, e2, c2) =>
                 S.bind2 (mfe ctx e1,
                       fn e1' =>
-                         S.bind2 (mfc ctx c,
-                              fn c' =>
+                         S.bind2 (mfc ctx c1,
+                              fn c1' =>
                                  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))))))
+                                          S.map2 (mfc ctx c2,
+                                               fn c2' =>
+                                                  (EConcat (e1', c1', e2', c2'),
+                                                   loc)))))
               | ECut (e, c, {field, rest}) =>
                 S.bind2 (mfe ctx e,
                       fn e' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 6e23c760..4927e37d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1,29 +1,29 @@
 (* Copyright (c) 2008, Adam Chlipala
-  * All rights reserved.
-  *
-  * Redistribution and use in source and binary forms, with or without
-  * modification, are permitted provided that the following conditions are met:
-  *
-  * - Redistributions of source code must retain the above copyright notice,
-  *   this list of conditions and the following disclaimer.
-  * - Redistributions in binary form must reproduce the above copyright notice,
-  *   this list of conditions and the following disclaimer in the documentation
-  *   and/or other materials provided with the distribution.
-  * - 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"
-  * 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
-  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
-  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
-  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
-  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
-  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
-  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
-  * POSSIBILITY OF SUCH DAMAGE.
-  *)
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - 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"
+ * 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
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
 
  structure Elaborate :> ELABORATE = struct
 
@@ -1603,21 +1603,21 @@ 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) =>
+          | L.EConcat (e1, 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 (e2', e2t, gs2) = elabExp (env, denv) e2
 
-                val rest = cunif (loc, ktype_record)
-                val first = (L'.CRecord (ktype, [(c', e2t)]), loc)
+                val r1 = cunif (loc, ktype_record)
+                val r2 = cunif (loc, ktype_record)
 
-                val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc)
-                val gs5 = D.prove env denv (first, rest, loc)
+                val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc)
+                val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc)
+                val gs5 = D.prove env denv (r1, r2, 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)
+                ((L'.EConcat (e1', r1, e2', r2), loc),
+                 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc),
+                 gs1 @ gs2 @ enD gs3 @ enD gs4 @ enD gs5)
             end
           | L.ECut (e, c) =>
             let
diff --git a/src/expl.sml b/src/expl.sml
index 9e35d674..2e96db54 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -90,7 +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 }
+       | EConcat of exp * con * exp * 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 39df4e3f..d19edeae 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -289,31 +289,26 @@ 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}) =>
+      | EConcat (e1, c1, e2, c2) =>
         parenIf par (if !debug then
-                         box [p_exp env e1,
+                         box [p_exp' true env e1,
                               space,
-                              string "with",
+                              string ":",
                               space,
-                              p_con' true env c,
+                              p_con env c1,
+                              space,
+                              string "++",
                               space,
-                              string "=",
                               p_exp' true env e2,
                               space,
-                              string "[",
-                              p_con env field,
+                              string ":",
                               space,
-                              string " in ",
-                              space,
-                              p_con env rest,
-                              string "]"]
+                              p_con env c2]
                      else
-                         box [p_exp env e1,
+                         box [p_exp' true 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
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 8dec2687..bda602d3 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -282,19 +282,17 @@ 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}) =>
+              | EConcat (e1, c1, e2, c2) =>
                 S.bind2 (mfe ctx e1,
                       fn e1' =>
-                         S.bind2 (mfc ctx c,
-                              fn c' =>
+                         S.bind2 (mfc ctx c1,
+                              fn c1' =>
                                  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))))))
+                                          S.map2 (mfc ctx c2,
+                                               fn c2' =>
+                                                  (EConcat (e1', c1', e2', c2'),
+                                                   loc)))))
               | ECut (e, c, {field, rest}) =>
                 S.bind2 (mfe ctx e,
                       fn e' =>
diff --git a/src/explify.sml b/src/explify.sml
index 72531d7a..1bca49c3 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -101,8 +101,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.EConcat (e1, c1, e2, c2) => (L'.EConcat (explifyExp e1, explifyCon c1, explifyExp e2, explifyCon c2),
+                                       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/monoize.sml b/src/monoize.sml
index df775554..17e28034 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1920,7 +1920,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             in
                 ((L'.EField (e, monoName env x), loc), fm)
             end
-          | L.EWith _ => poly ()
+          | L.EConcat _ => poly ()
           | L.ECut _ => poly ()
           | L.EFold _ => poly ()
 
diff --git a/src/reduce.sml b/src/reduce.sml
index 8dc4527f..1404b598 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -107,18 +107,18 @@ fun exp env e =
                                       | _ => false) xes of
                          SOME (_, e, _) => #1 e
                        | NONE => e)
-                  | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
+                  | EConcat (r1 as (_, loc), (CRecord (k, xts1), _), r2, (CRecord (_, xts2), _)) =>
                     let
-                        fun fields (remaining, passed) =
+                        fun fields (r, 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)
+                                 t) :: fields (r, rest, (x, t) :: passed)
                     in
-                        #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
+                        #1 (reduceExp env (ERecord (fields (r1, xts1, []) @ fields (r2, xts2, [])), loc))
                     end
                   | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
                     let
diff --git a/src/source.sml b/src/source.sml
index 23d2089f..386b1a83 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -123,7 +123,7 @@ datatype exp' =
 
        | ERecord of (con * exp) list
        | EField of exp * con
-       | EWith of exp * con * exp
+       | EConcat of exp * exp
        | ECut of exp * con
        | EFold
 
diff --git a/src/source_print.sml b/src/source_print.sml
index f9fc8a53..a25be2d4 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -258,13 +258,11 @@ 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])
+      | EConcat (e1, e2) => parenIf par (box [p_exp' true e1,
+                                              space,
+                                              string "++",
+                                              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 1bae7592..b0716eca 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -265,7 +265,7 @@ fun declOk' env (d, loc) =
                         in
                             (Rabble, calls)
                         end
-                      | EWith (e1, _, e2, _) =>
+                      | EConcat (e1, _, e2, _) =>
                         let
                             val (_, calls) = exp parent (penv, calls) e1
                             val (_, calls) = exp parent (penv, calls) e2
diff --git a/src/urweb.grm b/src/urweb.grm
index 3f56cb94..143b6935 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -198,7 +198,7 @@ fun tagIn bt =
  | TYPE | NAME
  | ARROW | LARROW | DARROW | STAR | SEMI
  | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
- | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | WITH | SQL
+ | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL
  | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE
  | CASE | IF | THEN | ELSE
 
@@ -344,7 +344,6 @@ fun tagIn bt =
 %right CAND
 %nonassoc EQ NE LT LE GT GE
 %right ARROW
-%left WITH
 %right PLUSPLUS MINUSMINUS
 %left PLUS MINUS
 %left STAR DIVIDE MOD
@@ -699,7 +698,7 @@ eexp   : eapps                          (eapps)
        | eexp GT eexp                   (native_op ("gt", eexp1, eexp2, s (eexp1left, eexp2right)))
        | eexp GE eexp                   (native_op ("ge", eexp1, eexp2, s (eexp1left, eexp2right)))
 
-       | eexp WITH cterm EQ eexp        (EWith (eexp1, cterm, eexp2), s (eexp1left, eexp2right))
+       | eexp PLUSPLUS eexp             (EConcat (eexp1, eexp2), s (eexp1left, eexp2right))
 
 bind   : SYMBOL LARROW eapps            (SYMBOL, NONE, eapps)
        | UNIT LARROW eapps              (let
diff --git a/src/urweb.lex b/src/urweb.lex
index fc8db17f..cc0f5b7c 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -311,7 +311,6 @@ 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));