changeset 493:ae03d09043c1

Add CutMulti
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 19:20:37 -0500
parents 4a241d108a2c
children 1bbcc3345d12
files include/urweb.h src/c/urweb.c src/cjr_print.sml src/core.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml src/monoize.sml src/reduce.sml src/source.sml src/source_print.sml src/termination.sml src/urweb.grm src/urweb.lex tests/cut.ur tests/cut.urp
diffstat 24 files changed, 195 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/include/urweb.h	Tue Nov 11 18:39:38 2008 -0500
+++ b/include/urweb.h	Tue Nov 11 19:20:37 2008 -0500
@@ -75,6 +75,7 @@
 
 uw_Basis_string uw_Basis_strcat(uw_context, uw_Basis_string, uw_Basis_string);
 uw_Basis_string uw_Basis_strdup(uw_context, uw_Basis_string);
+uw_Basis_string uw_Basis_maybe_strdup(uw_context, uw_Basis_string);
 
 uw_Basis_string uw_Basis_sqlifyInt(uw_context, uw_Basis_int);
 uw_Basis_string uw_Basis_sqlifyFloat(uw_context, uw_Basis_float);
--- a/src/c/urweb.c	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/c/urweb.c	Tue Nov 11 19:20:37 2008 -0500
@@ -869,6 +869,13 @@
   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;
--- a/src/cjr_print.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/cjr_print.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -1481,7 +1481,7 @@
         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,
--- a/src/core.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/core.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -95,6 +95,7 @@
        | 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 }
--- a/src/core_print.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/core_print.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -325,6 +325,23 @@
                               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}) =>
--- a/src/core_util.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/core_util.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -444,10 +444,16 @@
 
       | (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 @@
                                              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' =>
--- a/src/corify.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/corify.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -590,6 +590,8 @@
                                                    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}) =>
--- a/src/elab.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/elab.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -110,6 +110,7 @@
        | 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 }
--- a/src/elab_print.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/elab_print.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -359,6 +359,24 @@
                               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",
--- a/src/elab_util.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/elab_util.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -338,6 +338,15 @@
                                                   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' =>
--- a/src/elaborate.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/elaborate.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -1664,6 +1664,21 @@
                 ((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 @@
         (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 @@
                                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 @@
                                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 @@
                          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
--- a/src/expl.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/expl.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -92,6 +92,7 @@
        | 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 }
--- a/src/expl_print.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/expl_print.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -334,6 +334,23 @@
                               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(",
--- a/src/expl_util.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/expl_util.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -303,6 +303,14 @@
                                              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' =>
--- a/src/explify.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/explify.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -105,6 +105,8 @@
                                        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}) =>
--- a/src/monoize.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/monoize.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -2014,6 +2014,7 @@
             end
           | L.EConcat _ => poly ()
           | L.ECut _ => poly ()
+          | L.ECutMulti _ => poly ()
           | L.EFold _ => poly ()
 
           | L.ECase (e, pes, {disc, result}) =>
--- a/src/reduce.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/reduce.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -133,6 +133,19 @@
                     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
--- a/src/source.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/source.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -123,6 +123,7 @@
        | EField of exp * con
        | EConcat of exp * exp
        | ECut of exp * con
+       | ECutMulti of exp * con
        | EFold
 
        | EWild
--- a/src/source_print.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/source_print.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -268,6 +268,11 @@
                                          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",
--- a/src/termination.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/termination.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -265,6 +265,12 @@
                         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
--- a/src/urweb.grm	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/urweb.grm	Tue Nov 11 19:20:37 2008 -0500
@@ -197,7 +197,7 @@
  | 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 @@
 %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 @@
                                          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)
--- a/src/urweb.lex	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/urweb.lex	Tue Nov 11 19:20:37 2008 -0500
@@ -251,6 +251,7 @@
 <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));
--- a/tests/cut.ur	Tue Nov 11 18:39:38 2008 -0500
+++ b/tests/cut.ur	Tue Nov 11 19:20:37 2008 -0500
@@ -1,6 +1,7 @@
 val r = {A = 1, B = "Hi", C = 0.0}
 val rA = r -- #A
+val rB = r --- [A = _, C = _]
 
-val main : unit -> page = fn () => <html><body>
-        {cdata rA.B}
-</body></html>
+fun main () : transaction page = return <xml>
+        {cdata rA.B}, {cdata rB.B}
+</xml>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/cut.urp	Tue Nov 11 19:20:37 2008 -0500
@@ -0,0 +1,3 @@
+debug
+
+cut