diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 10:09:21 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 10:09:21 -0400 |
commit | 9e860c86c7d9c763deb9d51490a6766d9c72ed25 (patch) | |
tree | 7ba7c7cada5e7afa00c3e46879eb9974849286cf /src | |
parent | f19ae3bb20fa0c60e737606949b2bec6e3ae04f9 (diff) |
Record cut
Diffstat (limited to 'src')
-rw-r--r-- | src/core.sml | 1 | ||||
-rw-r--r-- | src/core_print.sml | 21 | ||||
-rw-r--r-- | src/core_util.sml | 10 | ||||
-rw-r--r-- | src/corify.sml | 2 | ||||
-rw-r--r-- | src/elab.sml | 1 | ||||
-rw-r--r-- | src/elab_print.sml | 21 | ||||
-rw-r--r-- | src/elab_util.sml | 10 | ||||
-rw-r--r-- | src/elaborate.sml | 18 | ||||
-rw-r--r-- | src/expl.sml | 1 | ||||
-rw-r--r-- | src/expl_print.sml | 21 | ||||
-rw-r--r-- | src/expl_util.sml | 10 | ||||
-rw-r--r-- | src/explify.sml | 2 | ||||
-rw-r--r-- | src/lacweb.grm | 5 | ||||
-rw-r--r-- | src/lacweb.lex | 1 | ||||
-rw-r--r-- | src/monoize.sml | 1 | ||||
-rw-r--r-- | src/reduce.sml | 13 | ||||
-rw-r--r-- | src/source.sml | 1 | ||||
-rw-r--r-- | src/source_print.sml | 5 |
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 |