# HG changeset patch # User Adam Chlipala # Date 1225459822 14400 # Node ID dfc8c991abd0785702e3aaa8222c9d57bdf80d9e # Parent f45f23ae20ed990cdff4f129846993f4ed1c379c Replace 'with' with '++' diff -r f45f23ae20ed -r dfc8c991abd0 lib/top.ur --- a/lib/top.ur Thu Oct 30 17:07:34 2008 -0400 +++ b/lib/top.ur Fri Oct 31 09:30:22 2008 -0400 @@ -4,6 +4,9 @@ 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 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 @@ 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 @@ 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 @@ {f [nm] [t] [rest] r}{acc}) +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 => + {f [nm] [t] [rest] r}{acc}) + + fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -143,6 +182,17 @@ {f [nm] [t] [rest] r1 r2}{acc}) +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 => + {f [nm] [t] [rest] r1 r2}{acc}) + + 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 -r f45f23ae20ed -r dfc8c991abd0 lib/top.urs --- a/lib/top.urs Thu Oct 30 17:07:34 2008 -0400 +++ b/lib/top.urs Fri Oct 31 09:30:22 2008 -0400 @@ -4,6 +4,9 @@ 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 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 @@ 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 @@ -> 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 @@ 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 @@ -> 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 -r f45f23ae20ed -r dfc8c991abd0 src/core.sml --- a/src/core.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/core.sml Fri Oct 31 09:30:22 2008 -0400 @@ -93,7 +93,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } - | EWith of exp * con * exp * { field : con, rest : con } + | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | EFold of kind diff -r f45f23ae20ed -r dfc8c991abd0 src/core_print.sml --- a/src/core_print.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/core_print.sml Fri Oct 31 09:30:22 2008 -0400 @@ -283,31 +283,26 @@ 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 ":", + space, + p_con env c1, + space, + string "++", + space, + p_exp' true env e2, + space, + string ":", + space, + p_con env c2] + else + box [p_exp' true 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 diff -r f45f23ae20ed -r dfc8c991abd0 src/core_util.sml --- a/src/core_util.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/core_util.sml Fri Oct 31 09:30:22 2008 -0400 @@ -424,19 +424,17 @@ 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 -r f45f23ae20ed -r dfc8c991abd0 src/corify.sml --- a/src/corify.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/corify.sml Fri Oct 31 09:30:22 2008 -0400 @@ -566,8 +566,8 @@ (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (corifyExp st e1, corifyCon st c, corifyExp st e2, - {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.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 -r f45f23ae20ed -r dfc8c991abd0 src/elab.sml --- a/src/elab.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/elab.sml Fri Oct 31 09:30:22 2008 -0400 @@ -108,7 +108,7 @@ | 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 -r f45f23ae20ed -r dfc8c991abd0 src/elab_print.sml --- a/src/elab_print.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/elab_print.sml Fri Oct 31 09:30:22 2008 -0400 @@ -317,33 +317,26 @@ 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 ":", + space, + p_con env c1, + space, + string "++", + space, + p_exp' true env e2, + space, + string ":", + space, + p_con env c2] + else + box [p_exp' true 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 diff -r f45f23ae20ed -r dfc8c991abd0 src/elab_util.sml --- a/src/elab_util.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/elab_util.sml Fri Oct 31 09:30:22 2008 -0400 @@ -309,19 +309,17 @@ 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 -r f45f23ae20ed -r dfc8c991abd0 src/elaborate.sml --- a/src/elaborate.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/elaborate.sml Fri Oct 31 09:30:22 2008 -0400 @@ -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 @@ ((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 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) + val (e2', e2t, gs2) = elabExp (env, denv) e2 + + val r1 = cunif (loc, ktype_record) + val r2 = cunif (loc, ktype_record) + + 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 -r f45f23ae20ed -r dfc8c991abd0 src/expl.sml --- a/src/expl.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/expl.sml Fri Oct 31 09:30:22 2008 -0400 @@ -90,7 +90,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } - | EWith of exp * con * exp * { field : con, rest : con } + | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | EFold of kind diff -r f45f23ae20ed -r dfc8c991abd0 src/expl_print.sml --- a/src/expl_print.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/expl_print.sml Fri Oct 31 09:30:22 2008 -0400 @@ -289,31 +289,26 @@ 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 ":", + space, + p_con env c1, + space, + string "++", + space, + p_exp' true env e2, + space, + string ":", + space, + p_con env c2] + else + box [p_exp' true 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 diff -r f45f23ae20ed -r dfc8c991abd0 src/expl_util.sml --- a/src/expl_util.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/expl_util.sml Fri Oct 31 09:30:22 2008 -0400 @@ -282,19 +282,17 @@ 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 -r f45f23ae20ed -r dfc8c991abd0 src/explify.sml --- a/src/explify.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/explify.sml Fri Oct 31 09:30:22 2008 -0400 @@ -101,8 +101,8 @@ | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) - | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (explifyExp e1, explifyCon c, explifyExp e2, - {field = explifyCon field, rest = explifyCon rest}), loc) + | L.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 -r f45f23ae20ed -r dfc8c991abd0 src/monoize.sml --- a/src/monoize.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/monoize.sml Fri Oct 31 09:30:22 2008 -0400 @@ -1920,7 +1920,7 @@ in ((L'.EField (e, monoName env x), loc), fm) end - | L.EWith _ => poly () + | L.EConcat _ => poly () | L.ECut _ => poly () | L.EFold _ => poly () diff -r f45f23ae20ed -r dfc8c991abd0 src/reduce.sml --- a/src/reduce.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/reduce.sml Fri Oct 31 09:30:22 2008 -0400 @@ -107,18 +107,18 @@ | _ => 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 -r f45f23ae20ed -r dfc8c991abd0 src/source.sml --- a/src/source.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/source.sml Fri Oct 31 09:30:22 2008 -0400 @@ -123,7 +123,7 @@ | ERecord of (con * exp) list | EField of exp * con - | EWith of exp * con * exp + | EConcat of exp * exp | ECut of exp * con | EFold diff -r f45f23ae20ed -r dfc8c991abd0 src/source_print.sml --- a/src/source_print.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/source_print.sml Fri Oct 31 09:30:22 2008 -0400 @@ -258,13 +258,11 @@ | 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 -r f45f23ae20ed -r dfc8c991abd0 src/termination.sml --- a/src/termination.sml Thu Oct 30 17:07:34 2008 -0400 +++ b/src/termination.sml Fri Oct 31 09:30:22 2008 -0400 @@ -265,7 +265,7 @@ 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 -r f45f23ae20ed -r dfc8c991abd0 src/urweb.grm --- a/src/urweb.grm Thu Oct 30 17:07:34 2008 -0400 +++ b/src/urweb.grm Fri Oct 31 09:30:22 2008 -0400 @@ -198,7 +198,7 @@ | 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 @@ %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 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 -r f45f23ae20ed -r dfc8c991abd0 src/urweb.lex --- a/src/urweb.lex Thu Oct 30 17:07:34 2008 -0400 +++ b/src/urweb.lex Fri Oct 31 09:30:22 2008 -0400 @@ -311,7 +311,6 @@ "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); "sequence" => (Tokens.SEQUENCE (pos yypos, pos yypos + size yytext)); "class" => (Tokens.CLASS (pos yypos, pos yypos + size yytext)); - "with" => (Tokens.WITH (pos yypos, pos yypos + size yytext)); "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));