Mercurial > urweb
changeset 123:e3041657d653
Parsing and elaborating (non-mutual) 'val rec'
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 17 Jul 2008 10:09:34 -0400 |
| parents | f7c6ceb87bbd |
| children | 541282b81454 |
| files | src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/rec.lac |
| diffstat | 11 files changed, 126 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/elab.sml Thu Jul 17 10:09:34 2008 -0400 @@ -111,6 +111,7 @@ datatype decl' = DCon of string * int * kind * con | DVal of string * int * con * exp + | DValRec of (string * int * con * exp) list | DSgn of string * int * sgn | DStr of string * int * sgn * str | DFfiStr of string * int * sgn
--- a/src/elab_env.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/elab_env.sml Thu Jul 17 10:09:34 2008 -0400 @@ -296,6 +296,7 @@ case d of DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) | DVal (x, n, t, _) => pushENamedAs env x n t + | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
--- a/src/elab_print.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/elab_print.sml Thu Jul 17 10:09:34 2008 -0400 @@ -391,7 +391,17 @@ end | SgnError => string "<ERROR>" -fun p_decl env ((d, _) : decl) = +fun p_vali env (x, n, t, e) = box [p_named x n, + space, + string ":", + space, + p_con env t, + space, + string "=", + space, + p_exp env e] + +fun p_decl env (dAll as (d, _) : decl) = case d of DCon (x, n, k, c) => box [string "con", space, @@ -404,17 +414,19 @@ string "=", space, p_con env c] - | DVal (x, n, t, e) => box [string "val", - space, - p_named x n, - space, - string ":", - space, - p_con env t, - space, - string "=", - space, - p_exp env e] + | DVal vi => box [string "val", + space, + p_vali env vi] + | DValRec vis => + let + val env = E.declBinds env dAll + in + box [string "val", + space, + string "rec", + space, + p_list_sep (box [newline, string "and", space]) (p_vali env) vis] + end | DSgn (x, n, sgn) => box [string "signature", space,
--- a/src/elab_util.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/elab_util.sml Thu Jul 17 10:09:34 2008 -0400 @@ -504,6 +504,8 @@ bind (ctx, NamedC (x, k)) | DVal (x, _, c, _) => bind (ctx, NamedE (x, c)) + | DValRec vis => + foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis | DSgn (x, _, sgn) => bind (ctx, Sgn (x, sgn)) | DStr (x, _, sgn, _) => @@ -546,12 +548,14 @@ S.map2 (mfc ctx c, fn c' => (DCon (x, n, k', c'), loc))) - | DVal (x, n, c, e) => - S.bind2 (mfc ctx c, - fn c' => - S.map2 (mfe ctx e, - fn e' => - (DVal (x, n, c', e'), loc))) + | DVal vi => + S.map2 (mfvi ctx vi, + fn vi' => + (DVal vi', loc)) + | DValRec vis => + S.map2 (ListUtil.mapfold (mfvi ctx) vis, + fn vis' => + (DValRec vis', loc)) | DSgn (x, n, sgn) => S.map2 (mfsg ctx sgn, fn sgn' => @@ -578,6 +582,13 @@ S.map2 (mfst ctx str, fn str' => (DExport (en, sgn', str'), loc))) + + and mfvi ctx (x, n, c, e) = + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfe ctx e, + fn e' => + (x, n, c', e'))) in mfd end
--- a/src/elaborate.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/elaborate.sml Thu Jul 17 10:09:34 2008 -0400 @@ -1593,13 +1593,14 @@ fun sgiOfDecl (d, loc) = case d of - L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) - | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) - | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc) - | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) - | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc) - | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc) - | L'.DExport _ => NONE + L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] + | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] + | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis + | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] + | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] + | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] + | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] + | L'.DExport _ => [] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -1789,7 +1790,7 @@ end | L.DVal (x, co, e) => let - val (c', ck, gs1) = case co of + val (c', _, gs1) = case co of NONE => (cunif (loc, ktype), ktype, []) | SOME c => elabCon (env, denv) c @@ -1800,6 +1801,36 @@ in ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs)) end + | L.DValRec vis => + let + val (vis, gs) = ListUtil.foldlMap + (fn ((x, co, e), gs) => + let + val (c', _, gs1) = case co of + NONE => (cunif (loc, ktype), ktype, []) + | SOME c => elabCon (env, denv) c + in + ((x, c', e), gs1 @ gs) + end) [] vis + + val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => + let + val (env, n) = E.pushENamed env x c' + in + ((x, n, c', e), env) + end) env vis + + val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => + let + val (e', et, gs1) = elabExp (env, denv) e + + val gs2 = checkCon (env, denv) e' et c' + in + ((x, n, c', e'), gs1 @ gs2 @ gs) + end) gs vis + in + ([(L'.DValRec vis, loc)], (env, denv, gs)) + end | L.DSgn (x, sgn) => let @@ -1970,7 +2001,7 @@ L.StrConst ds => let val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds - val sgis = List.mapPartial sgiOfDecl ds' + val sgis = ListUtil.mapConcat sgiOfDecl ds' val (sgis, _, _, _, _) = foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
--- a/src/explify.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/explify.sml Thu Jul 17 10:09:34 2008 -0400 @@ -111,6 +111,7 @@ case d of L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) + | L.DValRec _ => raise Fail "Expliofy DValRec" | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc) | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
--- a/src/lacweb.grm Sun Jul 13 20:25:25 2008 -0400 +++ b/src/lacweb.grm Thu Jul 17 10:09:34 2008 -0400 @@ -44,7 +44,7 @@ | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | DIVIDE | GT - | CON | LTYPE | VAL | FOLD | UNIT | KUNIT + | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR | TWIDDLE @@ -59,6 +59,8 @@ file of decl list | decls of decl list | decl of decl + | vali of string * con option * exp + | valis of (string * con option * exp) list | sgn of sgn | sgntm of sgn @@ -125,8 +127,8 @@ | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), s (LTYPEleft, cexpright)) - | VAL SYMBOL EQ eexp (DVal (SYMBOL, NONE, eexp), s (VALleft, eexpright)) - | VAL SYMBOL COLON cexp EQ eexp (DVal (SYMBOL, SOME cexp, eexp), s (VALleft, eexpright)) + | VAL vali (DVal vali, s (VALleft, valiright)) + | VAL REC valis (DValRec valis, s (VALleft, valisright)) | SIGNATURE CSYMBOL EQ sgn (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) | STRUCTURE CSYMBOL EQ str (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright)) @@ -149,6 +151,12 @@ | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) | EXPORT spath (DExport spath, s (EXPORTleft, spathright)) +vali : SYMBOL EQ eexp (SYMBOL, NONE, eexp) + | SYMBOL COLON cexp EQ eexp (SYMBOL, SOME cexp, eexp) + +valis : vali ([vali]) + | vali AND valis (vali :: valis) + sgn : sgntm (sgntm) | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))
--- a/src/lacweb.lex Sun Jul 13 20:25:25 2008 -0400 +++ b/src/lacweb.lex Thu Jul 17 10:09:34 2008 -0400 @@ -251,6 +251,8 @@ <INITIAL> "con" => (Tokens.CON (pos yypos, pos yypos + size yytext)); <INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext)); <INITIAL> "val" => (Tokens.VAL (pos yypos, pos yypos + size yytext)); +<INITIAL> "rec" => (Tokens.REC (pos yypos, pos yypos + size yytext)); +<INITIAL> "and" => (Tokens.AND (pos yypos, pos yypos + size yytext)); <INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext)); <INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
--- a/src/source.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/source.sml Thu Jul 17 10:09:34 2008 -0400 @@ -107,6 +107,7 @@ datatype decl' = DCon of string * kind option * con | DVal of string * con option * exp + | DValRec of (string * con option * exp) list | DSgn of string * sgn | DStr of string * sgn option * str | DFfiStr of string * sgn
--- a/src/source_print.sml Sun Jul 13 20:25:25 2008 -0400 +++ b/src/source_print.sml Thu Jul 17 10:09:34 2008 -0400 @@ -329,6 +329,23 @@ | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x]) +fun p_vali (x, co, e) = + case co of + NONE => box [string x, + space, + string "=", + space, + p_exp e] + | SOME t => box [string x, + space, + string ":", + space, + p_con t, + space, + string "=", + space, + p_exp e] + fun p_decl ((d, _) : decl) = case d of DCon (x, NONE, c) => box [string "con", @@ -349,24 +366,14 @@ string "=", space, p_con c] - | DVal (x, NONE, e) => box [string "val", - space, - string x, - space, - string "=", - space, - p_exp e] - | DVal (x, SOME t, e) => box [string "val", - space, - string x, - space, - string ":", - space, - p_con t, - space, - string "=", - space, - p_exp e] + | DVal vi => box [string "val", + space, + p_vali vi] + | DValRec vis => box [string "val", + space, + string "rec", + space, + p_list_sep (box [newline, string "and", space]) p_vali vis] | DSgn (x, sgn) => box [string "signature", space,