summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/urweb.h1
-rw-r--r--src/c/urweb.c7
-rw-r--r--src/cjr_print.sml2
-rw-r--r--src/core.sml1
-rw-r--r--src/core_print.sml17
-rw-r--r--src/core_util.sml16
-rw-r--r--src/corify.sml2
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml18
-rw-r--r--src/elab_util.sml9
-rw-r--r--src/elaborate.sml67
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_print.sml17
-rw-r--r--src/expl_util.sml8
-rw-r--r--src/explify.sml2
-rw-r--r--src/monoize.sml1
-rw-r--r--src/reduce.sml13
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml5
-rw-r--r--src/termination.sml6
-rw-r--r--src/urweb.grm5
-rw-r--r--src/urweb.lex1
-rw-r--r--tests/cut.ur7
-rw-r--r--tests/cut.urp3
24 files changed, 195 insertions, 16 deletions
diff --git a/include/urweb.h b/include/urweb.h
index d148654f..ad08c811 100644
--- a/include/urweb.h
+++ b/include/urweb.h
@@ -75,6 +75,7 @@ uw_Basis_time uw_Basis_unurlifyTime(uw_context, char **);
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);
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));
diff --git a/tests/cut.ur b/tests/cut.ur
index 6b7b4ef3..7d0ee77a 100644
--- a/tests/cut.ur
+++ b/tests/cut.ur
@@ -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>
diff --git a/tests/cut.urp b/tests/cut.urp
new file mode 100644
index 00000000..5c9c3e81
--- /dev/null
+++ b/tests/cut.urp
@@ -0,0 +1,3 @@
+debug
+
+cut
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 16:54:13 +0000