Add CutMulti

21 files changed, 187 insertions, 13 deletions

diff --git a/src/c/urweb.c b/src/c/urweb.c
index a347dd45..253cda87 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -869,6 +869,13 @@ uw_Basis_string uw_Basis_strdup(uw_context ctx, uw_Basis_string s1) {
   return s;
 }
 
+uw_Basis_string uw_Basis_maybe_strdup(uw_context ctx, uw_Basis_string s1) {
+  if (s1)
+    return uw_Basis_strdup(ctx, s1);
+  else
+    return NULL;
+}
+
 
 char *uw_Basis_sqlifyInt(uw_context ctx, uw_Basis_int n) {
   int len;
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 1c750b33..8c3c3d86 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -1481,7 +1481,7 @@ fun p_exp' par env (e, loc) =
         in
             box [string "({",
                  newline,
-                 string "uw_Basis_string request = uw_Basis_strdup(ctx, ",
+                 string "uw_Basis_string request = uw_Basis_maybe_strdup(ctx, ",
                  p_exp env e,
                  string ");",
                  newline,
diff --git a/src/core.sml b/src/core.sml
index 1a181a68..4623bb49 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -95,6 +95,7 @@ datatype exp' =
        | EField of exp * con * { field : con, rest : con }
        | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
+       | ECutMulti of exp * con * { rest : con }
        | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/core_print.sml b/src/core_print.sml
index f209b84f..53922936 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -325,6 +325,23 @@ fun p_exp' par env (e, _) =
                               string "--",
                               space,
                               p_con' true env c])
+      | ECutMulti (e, c, {rest}) =>
+        parenIf par (if !debug then
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c,
+                              space,
+                              string "[",
+                              p_con env rest,
+                              string "]"]
+                     else
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c])
       | EFold _ => string "fold"
 
       | ECase (e, pes, {disc, result}) =>
diff --git a/src/core_util.sml b/src/core_util.sml
index 38004f74..71efe16e 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -444,10 +444,16 @@ fun compare ((e1, _), (e2, _)) =
 
       | (ECut (e1, c1, _), ECut (e2, c2, _)) =>
         join (compare (e1, e2),
-              fn () => Con.compare (c1, c2))
+           fn () => Con.compare (c1, c2))
       | (ECut _, _) => LESS
       | (_, ECut _) => GREATER
 
+      | (ECutMulti (e1, c1, _), ECutMulti (e2, c2, _)) =>
+        join (compare (e1, e2),
+           fn () => Con.compare (c1, c2))
+      | (ECutMulti _, _) => LESS
+      | (_, ECutMulti _) => GREATER
+
       | (EFold _, EFold _) => EQUAL
       | (EFold _, _) => LESS
       | (_, EFold _) => GREATER
@@ -588,6 +594,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                              S.map2 (mfc ctx rest,
                                                   fn rest' =>
                                                      (ECut (e', c', {field = field', rest = rest'}), loc)))))
+              | ECutMulti (e, c, {rest}) =>
+                S.bind2 (mfe ctx e,
+                      fn e' =>
+                         S.bind2 (mfc ctx c,
+                              fn c' =>
+                                 S.map2 (mfc ctx rest,
+                                      fn rest' =>
+                                         (ECutMulti (e', c', {rest = rest'}), loc))))
               | EFold k =>
                 S.map2 (mfk k,
                          fn k' =>
diff --git a/src/corify.sml b/src/corify.sml
index fdb4e7b7..8bb1a925 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -590,6 +590,8 @@ fun corifyExp st (e, loc) =
                                                    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.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c,
+                                                      {rest = corifyCon st rest}), loc)
       | L.EFold k => (L'.EFold (corifyKind k), loc)
 
       | L.ECase (e, pes, {disc, result}) =>
diff --git a/src/elab.sml b/src/elab.sml
index d00d1f1a..d997b7ec 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -110,6 +110,7 @@ datatype exp' =
        | EField of exp * con * { field : con, rest : con }
        | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
+       | ECutMulti of exp * con * { rest : con }
        | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2afedef1..62b1ea02 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -359,6 +359,24 @@ fun p_exp' par env (e, _) =
                               string "--",
                               space,
                               p_con' true env c])
+      | ECutMulti (e, c, {rest}) =>
+        parenIf par (if !debug then
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c,
+                              space,
+                              string "[",
+                              p_con env rest,
+                              string "]"]
+                     else
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c])
+
       | EFold _ => string "fold"
 
       | ECase (e, pes, _) => parenIf par (box [string "case",
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 9c25ae86..6e2c76f6 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -338,6 +338,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                                   fn rest' =>
                                                      (ECut (e', c', {field = field', rest = rest'}), loc)))))
 
+              | ECutMulti (e, c, {rest}) =>
+                S.bind2 (mfe ctx e,
+                      fn e' =>
+                         S.bind2 (mfc ctx c,
+                              fn c' =>
+                                 S.map2 (mfc ctx rest,
+                                      fn rest' =>
+                                         (ECutMulti (e', c', {rest = rest'}), loc))))
+
               | EFold k =>
                 S.map2 (mfk k,
                          fn k' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 70429c1b..e3d334eb 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1664,6 +1664,21 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
                  gs1 @ enD gs2 @ enD gs3 @ enD gs4)
             end
+          | L.ECutMulti (e, c) =>
+            let
+                val (e', et, gs1) = elabExp (env, denv) e
+                val (c', ck, gs2) = elabCon (env, denv) c
+
+                val rest = cunif (loc, ktype_record)
+                            
+                val gs3 =
+                    checkCon (env, denv) e' et
+                             (L'.TRecord (L'.CConcat (c', rest), loc), loc)
+                val gs4 = D.prove env denv (c', rest, loc)
+            in
+                ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
+                 gs1 @ enD gs2 @ enD gs3 @ enD gs4)
+            end
 
           | L.EFold =>
             let
@@ -2694,6 +2709,33 @@ fun wildifyStr env (str, sgn) =
         (case #1 str of
              L.StrConst ds =>
              let
+                 fun decompileKind (k, loc) =
+                     case k of
+                         L'.KType => SOME (L.KType, loc)
+                       | L'.KArrow (k1, k2) =>
+                         (case (decompileKind k1, decompileKind k2) of
+                              (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc)
+                            | _ => NONE)
+                       | L'.KName => SOME (L.KName, loc)
+                       | L'.KRecord k =>
+                         (case decompileKind k of
+                              SOME k => SOME (L.KRecord k, loc)
+                            | _ => NONE)
+                       | L'.KUnit => SOME (L.KUnit, loc)
+                       | L'.KTuple ks =>
+                         let
+                             val ks' = List.mapPartial decompileKind ks
+                         in
+                             if length ks' = length ks then
+                                 SOME (L.KTuple ks', loc)
+                             else
+                                 NONE
+                         end
+
+                       | L'.KError => NONE
+                       | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
+                       | L'.KUnif _ => NONE
+
                  fun decompileCon env (c, loc) =
                      case c of
                          L'.CRel i =>
@@ -2741,7 +2783,7 @@ fun wildifyStr env (str, sgn) =
                                let
                                    val (needed, constraints, neededV) =
                                        case sgi of
-                                           L'.SgiConAbs (x, _, _) => (SS.add (neededC, x), constraints, neededV)
+                                           L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV)
                                          | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
 
                                          | L'.SgiVal (x, _, t) =>
@@ -2764,18 +2806,18 @@ fun wildifyStr env (str, sgn) =
                                in
                                    (needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
                                end)
-                           (SS.empty, [], SS.empty, env) sgis
+                           (SM.empty, [], SS.empty, env) sgis
                                                               
                  val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
                                                     case d of
-                                                        L.DCon (x, _, _) => ((SS.delete (neededC, x), neededV)
+                                                        L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
                                                                              handle NotFound =>
                                                                                     needed)
-                                                      | L.DClass (x, _) => ((SS.delete (neededC, x), neededV)
+                                                      | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV)
                                                                             handle NotFound => needed)
                                                       | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
                                                                              handle NotFound => needed)
-                                                      | L.DOpen _ => (SS.empty, SS.empty)
+                                                      | L.DOpen _ => (SM.empty, SS.empty)
                                                       | _ => needed)
                                                 (neededC, neededV) ds
 
@@ -2797,13 +2839,20 @@ fun wildifyStr env (str, sgn) =
                          end
 
                  val ds' =
-                     case SS.listItems neededC of
+                     case SM.listItemsi neededC of
                          [] => ds'
                        | xs =>
                          let
-                             val kwild = (L.KWild, #2 str)
-                             val cwild = (L.CWild kwild, #2 str)
-                             val ds'' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+                             val ds'' = map (fn (x, k) =>
+                                                let
+                                                    val k =
+                                                        case decompileKind k of
+                                                            NONE => (L.KWild, #2 str)
+                                                          | SOME k => k
+                                                    val cwild = (L.CWild k, #2 str)
+                                                in
+                                                    (L.DCon (x, NONE, cwild), #2 str)
+                                                end) xs
                          in
                              ds'' @ ds'
                          end
diff --git a/src/expl.sml b/src/expl.sml
index 57396684..cce0fc22 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -92,6 +92,7 @@ datatype exp' =
        | EField of exp * con * { field : con, rest : con }
        | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
+       | ECutMulti of exp * con * { rest : con }
        | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/expl_print.sml b/src/expl_print.sml
index e3153ef2..2ce0c5e2 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -334,6 +334,23 @@ fun p_exp' par env (e, loc) =
                               string "--",
                               space,
                               p_con' true env c])
+      | ECutMulti (e, c, {rest}) =>
+        parenIf par (if !debug then
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c,
+                              space,
+                              string "[",
+                              p_con env rest,
+                              string "]"]
+                     else
+                         box [p_exp' true env e,
+                              space,
+                              string "---",
+                              space,
+                              p_con' true env c])
       | EFold _ => string "fold"
 
       | EWrite e => box [string "write(",
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 2bd9eabd..d2073a23 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -303,6 +303,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                              S.map2 (mfc ctx rest,
                                                   fn rest' =>
                                                      (ECut (e', c', {field = field', rest = rest'}), loc)))))
+              | ECutMulti (e, c, {rest}) =>
+                S.bind2 (mfe ctx e,
+                      fn e' =>
+                         S.bind2 (mfc ctx c,
+                              fn c' =>
+                                 S.map2 (mfc ctx rest,
+                                      fn rest' =>
+                                         (ECutMulti (e', c', {rest = rest'}), loc))))
               | EFold k =>
                 S.map2 (mfk k,
                          fn k' =>
diff --git a/src/explify.sml b/src/explify.sml
index 4115476b..e3c22f20 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -105,6 +105,8 @@ fun explifyExp (e, loc) =
                                        loc)
       | L.ECut (e1, c, {field, rest}) => (L'.ECut (explifyExp e1, explifyCon c,
                                                      {field = explifyCon field, rest = explifyCon rest}), loc)
+      | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c,
+                                                      {rest = explifyCon rest}), loc)
       | L.EFold k => (L'.EFold (explifyKind k), loc)
 
       | L.ECase (e, pes, {disc, result}) =>
diff --git a/src/monoize.sml b/src/monoize.sml
index a4f38dc6..28ea5946 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -2014,6 +2014,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             end
           | L.EConcat _ => poly ()
           | L.ECut _ => poly ()
+          | L.ECutMulti _ => poly ()
           | L.EFold _ => poly ()
 
           | L.ECase (e, pes, {disc, result}) =>
diff --git a/src/reduce.sml b/src/reduce.sml
index 1404b598..e480dea2 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -133,6 +133,19 @@ fun exp env e =
                     in
                         #1 (reduceExp env (ERecord (fields (xts, [])), loc))
                     end
+                  | ECutMulti (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
+                    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 (fields (xts, [])), loc))
+                    end
 
                   | _ => e
     in
diff --git a/src/source.sml b/src/source.sml
index 2a348338..7685bb2f 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -123,6 +123,7 @@ datatype exp' =
        | EField of exp * con
        | EConcat of exp * exp
        | ECut of exp * con
+       | ECutMulti of exp * con
        | EFold
 
        | EWild
diff --git a/src/source_print.sml b/src/source_print.sml
index 3c26812f..77f2d749 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -268,6 +268,11 @@ fun p_exp' par (e, _) =
                                          string "--",
                                          space,
                                          p_con' true c])
+      | ECutMulti (e, c) => parenIf par (box [p_exp' true e,
+                                              space,
+                                              string "---",
+                                              space,
+                                              p_con' true c])
       | EFold => string "fold"
 
       | ECase (e, pes) => parenIf par (box [string "case",
diff --git a/src/termination.sml b/src/termination.sml
index 2db5bb11..e89f329e 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -265,6 +265,12 @@ fun declOk' env (d, loc) =
                         in
                             (Rabble, calls)
                         end
+                      | ECutMulti (e, _, _) =>
+                        let
+                            val (_, calls) = exp parent (penv, calls) e
+                        in
+                            (Rabble, calls)
+                        end
                       | EConcat (e1, _, e2, _) =>
                         let
                             val (_, calls) = exp parent (penv, calls) e1
diff --git a/src/urweb.grm b/src/urweb.grm
index 5241ed20..8a3bee7f 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -197,7 +197,7 @@ fun tagIn bt =
  | DATATYPE | OF
  | TYPE | NAME
  | ARROW | LARROW | DARROW | STAR | SEMI
- | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
+ | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE
  | LET | IN
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL
  | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE
@@ -348,7 +348,7 @@ fun tagIn bt =
 %right CAND
 %nonassoc EQ NE LT LE GT GE IS
 %right ARROW
-%right PLUSPLUS MINUSMINUS
+%right PLUSPLUS MINUSMINUS MINUSMINUSMINUS
 %left PLUS MINUS
 %left STAR DIVIDE MOD
 %left NOT
@@ -692,6 +692,7 @@ eexp   : eapps                          (eapps)
                                          end)
        | eexp COLON cexp                (EAnnot (eexp, cexp), s (eexpleft, cexpright))
        | eexp MINUSMINUS cexp           (ECut (eexp, cexp), s (eexpleft, cexpright))
+       | eexp MINUSMINUSMINUS cexp      (ECutMulti (eexp, cexp), s (eexpleft, cexpright))
        | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright))
        | IF eexp THEN eexp ELSE eexp    (let
                                              val loc = s (IFleft, eexp3right)
diff --git a/src/urweb.lex b/src/urweb.lex
index 642282ec..aef68ad1 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -251,6 +251,7 @@ notags = [^<{\n]+;
 <INITIAL> "=>"        => (Tokens.DARROW (pos yypos, pos yypos + size yytext));
 <INITIAL> "++"        => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext));
 <INITIAL> "--"        => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext));
+<INITIAL> "---"       => (Tokens.MINUSMINUSMINUS (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "="         => (Tokens.EQ (pos yypos, pos yypos + size yytext));
 <INITIAL> "<>"        => (Tokens.NE (pos yypos, pos yypos + size yytext));