summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-24 10:09:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-24 10:09:21 -0400
commit9e860c86c7d9c763deb9d51490a6766d9c72ed25 (patch)
tree7ba7c7cada5e7afa00c3e46879eb9974849286cf /src
parentf19ae3bb20fa0c60e737606949b2bec6e3ae04f9 (diff)
Record cut
Diffstat (limited to 'src')
-rw-r--r--src/core.sml1
-rw-r--r--src/core_print.sml21
-rw-r--r--src/core_util.sml10
-rw-r--r--src/corify.sml2
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml21
-rw-r--r--src/elab_util.sml10
-rw-r--r--src/elaborate.sml18
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_print.sml21
-rw-r--r--src/expl_util.sml10
-rw-r--r--src/explify.sml2
-rw-r--r--src/lacweb.grm5
-rw-r--r--src/lacweb.lex1
-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
18 files changed, 142 insertions, 2 deletions
diff --git a/src/core.sml b/src/core.sml
index ffd149f3..f994d177 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -72,6 +72,7 @@ datatype exp' =
| ERecord of (con * exp * con) list
| EField of exp * con * { field : con, rest : con }
+ | ECut of exp * con * { field : con, rest : con }
| EFold of kind
| EWrite of exp
diff --git a/src/core_print.sml b/src/core_print.sml
index 590b90fd..364f9c06 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -226,6 +226,27 @@ fun p_exp' par env (e, _) =
box [p_exp' true env e,
string ".",
p_con' true env c]
+ | ECut (e, c, {field, 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 field,
+ space,
+ string " in ",
+ space,
+ 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/core_util.sml b/src/core_util.sml
index 9cde8ab9..1964ce9d 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -282,6 +282,16 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.map2 (mfc ctx rest,
fn rest' =>
(EField (e', c', {field = field', rest = rest'}), loc)))))
+ | ECut (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (ECut (e', c', {field = field', rest = rest'}), loc)))))
| EFold k =>
S.map2 (mfk k,
fn k' =>
diff --git a/src/corify.sml b/src/corify.sml
index 30b4a7df..4277c35e 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -371,6 +371,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.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)
| L.EWrite e => (L'.EWrite (corifyExp st e), loc)
diff --git a/src/elab.sml b/src/elab.sml
index 653539a6..1ba3b454 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -83,6 +83,7 @@ datatype exp' =
| ERecord of (con * exp * con) list
| EField of exp * con * { field : con, rest : con }
+ | ECut of exp * con * { field : con, rest : con }
| EFold of kind
| EError
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 81cbae69..e59fb9f7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -274,6 +274,27 @@ fun p_exp' par env (e, _) =
box [p_exp' true env e,
string ".",
p_con' true env c]
+ | ECut (e, c, {field, 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 field,
+ space,
+ string " in ",
+ space,
+ p_con env rest,
+ string "]"]
+ else
+ box [p_exp' true env e,
+ space,
+ string "--",
+ space,
+ p_con' true env c])
| EFold _ => string "fold"
| EError => string "<ERROR>"
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 35f4cfcd..0ff2d733 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -292,6 +292,16 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.map2 (mfc ctx rest,
fn rest' =>
(EField (e', c', {field = field', rest = rest'}), loc)))))
+ | ECut (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (ECut (e', c', {field = field', rest = rest'}), loc)))))
| EFold k =>
S.map2 (mfk k,
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b48a69f6..dd0b7187 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -895,6 +895,7 @@ fun typeof env (e, loc) =
| L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
| L'.EField (_, _, {field, ...}) => field
+ | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc)
| L'.EFold dom => foldType (dom, loc)
| L'.EError => cerror
@@ -1108,6 +1109,23 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
end
+ | L.ECut (e, c) =>
+ let
+ val (e', et, gs1) = elabExp (env, denv) e
+ val (c', ck, gs2) = elabCon (env, denv) c
+
+ val ft = cunif (loc, ktype)
+ val rest = cunif (loc, ktype_record)
+ val first = (L'.CRecord (ktype, [(c', ft)]), loc)
+
+ val gs3 =
+ checkCon (env, denv) e' et
+ (L'.TRecord (L'.CConcat (first, rest), loc), loc)
+ val gs4 = D.prove env denv (first, rest, loc)
+ in
+ ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
+ end
+
| L.EFold =>
let
val dom = kunif loc
diff --git a/src/expl.sml b/src/expl.sml
index 2bb25929..b1a0e389 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -71,6 +71,7 @@ datatype exp' =
| ERecord of (con * exp * con) list
| EField of exp * con * { field : con, rest : con }
+ | ECut of exp * con * { field : con, rest : con }
| EFold of kind
| EWrite of exp
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 2c4e7c89..58508097 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -237,6 +237,27 @@ fun p_exp' par env (e, loc) =
box [p_exp' true env e,
string ".",
p_con' true env c]
+ | ECut (e, c, {field, 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 field,
+ space,
+ string " in ",
+ space,
+ 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 c4f1b1d7..976df246 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -267,6 +267,16 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.map2 (mfc ctx rest,
fn rest' =>
(EField (e', c', {field = field', rest = rest'}), loc)))))
+ | ECut (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (ECut (e', c', {field = field', rest = rest'}), loc)))))
| EFold k =>
S.map2 (mfk k,
fn k' =>
diff --git a/src/explify.sml b/src/explify.sml
index db6b429d..2013f20a 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -85,6 +85,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.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)
| L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 4fd3dc8e..efe26719 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -47,7 +47,7 @@ fun uppercaseFirst "" = ""
| CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
| TYPE | NAME
| ARROW | LARROW | DARROW
- | FN | PLUSPLUS | DOLLAR | TWIDDLE
+ | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
| STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
| INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT
@@ -111,7 +111,7 @@ fun uppercaseFirst "" = ""
%nonassoc DCOLON TCOLON
%right COMMA
%right ARROW LARROW
-%right PLUSPLUS
+%right PLUSPLUS MINUSMINUS
%nonassoc TWIDDLE
%nonassoc DOLLAR
%left DOT
@@ -285,6 +285,7 @@ eexp : eapps (eapps)
end)
| LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
+ | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright))
eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
diff --git a/src/lacweb.lex b/src/lacweb.lex
index f6aeedf3..4412d9e4 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -235,6 +235,7 @@ notags = [^<{\n]+;
<INITIAL> "->" => (Tokens.ARROW (pos yypos, pos yypos + size yytext));
<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.EQ (pos yypos, pos yypos + size yytext));
<INITIAL> "," => (Tokens.COMMA (pos yypos, pos yypos + size yytext));
diff --git a/src/monoize.sml b/src/monoize.sml
index 505d6d98..b31613c1 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -370,6 +370,7 @@ fun monoExp env (all as (e, loc)) =
| L.ERecord xes => (L'.ERecord (map (fn (x, e, t) => (monoName env x, monoExp env e, monoType env t)) xes), loc)
| L.EField (e, x, _) => (L'.EField (monoExp env e, monoName env x), loc)
+ | L.ECut _ => poly ()
| L.EFold _ => poly ()
| L.EWrite e => (L'.EWrite (monoExp env e), loc)
diff --git a/src/reduce.sml b/src/reduce.sml
index 5b00ac5a..ecb0777d 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -164,6 +164,19 @@ fun exp env e =
| _ => false) xes of
SOME (_, e, _) => #1 e
| NONE => e)
+ | ECut (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
diff --git a/src/source.sml b/src/source.sml
index a04836bb..9427d6d6 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -100,6 +100,7 @@ datatype exp' =
| ERecord of (con * exp) list
| EField of exp * con
+ | ECut of exp * con
| EFold
withtype exp = exp' located
diff --git a/src/source_print.sml b/src/source_print.sml
index 245ee79e..ba9219be 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -232,6 +232,11 @@ fun p_exp' par (e, _) =
| EField (e, c) => box [p_exp' true e,
string ".",
p_con' true c]
+ | ECut (e, c) => parenIf par (box [p_exp' true e,
+ space,
+ string "--",
+ space,
+ p_con' true c])
| EFold => string "fold"
and p_exp e = p_exp' false e