Mercurial > urweb
changeset 176:33d4a8eea484
Case through explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 31 Jul 2008 16:28:55 -0400 |
| parents | b2d752455182 |
| children | 5d030ee143e2 |
| files | src/corify.sml src/elab.sml src/elab_print.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml |
| diffstat | 8 files changed, 114 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/corify.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/corify.sml Thu Jul 31 16:28:55 2008 -0400 @@ -394,6 +394,7 @@ | 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.ECase _ => raise Fail "Corify ECase" | L.EWrite e => (L'.EWrite (corifyExp st e), loc) fun corifyDecl ((d, loc : EM.span), st) =
--- a/src/elab.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/elab.sml Thu Jul 31 16:28:55 2008 -0400 @@ -80,7 +80,7 @@ | PVar of string | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list * con option + | PRecord of (string * pat) list withtype pat = pat' located
--- a/src/elab_print.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/elab_print.sml Thu Jul 31 16:28:55 2008 -0400 @@ -220,17 +220,15 @@ | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc, space, p_pat' true env p]) - | PRecord (xps, flex) => - let - val pps = map (fn (x, p) => box [string x, space, string "=", space, p_pat env p]) xps - in - box [string "{", - p_list_sep (box [string ",", space]) (fn x => x) - (case flex of - NONE => pps - | SOME _ => pps @ [string "..."]), - string "}"] - end + | PRecord xps => + box [string "{", + p_list_sep (box [string ",", space]) (fn (x, p) => + box [string x, + space, + string "=", + space, + p_pat env p]) xps, + string "}"] and p_pat x = p_pat' false x
--- a/src/elaborate.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/elaborate.sml Thu Jul 31 16:28:55 2008 -0400 @@ -1045,17 +1045,13 @@ val k = (L'.KType, loc) val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc) - val (flex, c) = + val c = if flex then - let - val flex = cunif (loc, (L'.KRecord k, loc)) - in - (SOME flex, (L'.CConcat (c, flex), loc)) - end + (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc) else - (NONE, c) + c in - (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts, flex), loc), + (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts), loc), (L'.TRecord c, loc)), (env, bound)) end @@ -1089,8 +1085,9 @@ | L'.PPrim _ => None | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) - | L'.PRecord (xps, _) => Record [foldl (fn ((x, p), fmap) => + | L'.PRecord xps => Record [foldl (fn ((x, p), fmap) => SM.insert (fmap, x, coverage p)) SM.empty xps] + fun merge (c1, c2) = case (c1, c2) of (None, _) => c2
--- a/src/expl.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/expl.sml Thu Jul 31 16:28:55 2008 -0400 @@ -59,6 +59,19 @@ withtype con = con' located +datatype patCon = + PConVar of int + | PConProj of int * string list * string + +datatype pat' = + PWild + | PVar of string + | PPrim of Prim.t + | PCon of patCon * pat option + | PRecord of (string * pat) list + +withtype pat = pat' located + datatype exp' = EPrim of Prim.t | ERel of int @@ -74,6 +87,8 @@ | ECut of exp * con * { field : con, rest : con } | EFold of kind + | ECase of exp * (pat * exp) list * con + | EWrite of exp withtype exp = exp' located
--- a/src/expl_print.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/expl_print.sml Thu Jul 31 16:28:55 2008 -0400 @@ -155,6 +155,48 @@ CName s => string s | _ => p_con env all +fun p_patCon env pc = + case pc of + PConVar n => + ((if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n))) + handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n)) + | PConProj (m1, ms, x) => + let + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 + + val m1s = if !debug then + m1x ^ "__" ^ Int.toString m1 + else + m1x + in + p_list_sep (string ".") string (m1x :: ms @ [x]) + end + +fun p_pat' par env (p, _) = + case p of + PWild => string "_" + | PVar s => string s + | PPrim p => Prim.p_t p + | PCon (pc, NONE) => p_patCon env pc + | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc, + space, + p_pat' true env p]) + | PRecord xps => + box [string "{", + p_list_sep (box [string ",", space]) (fn (x, p) => + box [string x, + space, + string "=", + space, + p_pat env p]) xps, + string "}"] + +and p_pat x = p_pat' false x + fun p_exp' par env (e, loc) = case e of EPrim p => Prim.p_t p @@ -264,6 +306,19 @@ p_exp env e, string ")"] + | ECase (e, pes, _) => parenIf par (box [string "case", + space, + p_exp env e, + space, + string "of", + space, + p_list_sep (box [space, string "|", space]) + (fn (p, e) => box [p_pat env p, + space, + string "=>", + space, + p_exp env e]) pes]) + and p_exp env = p_exp' false env fun p_named x n =
--- a/src/expl_util.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/expl_util.sml Thu Jul 31 16:28:55 2008 -0400 @@ -286,6 +286,17 @@ S.map2 (mfe ctx e, fn e' => (EWrite e', loc)) + + | ECase (e, pes, t) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (ListUtil.mapfold (fn (p, e) => + S.map2 (mfe ctx e, + fn e' => (p, e'))) pes, + fn pes' => + S.map2 (mfc ctx t, + fn t' => + (ECase (e', pes', t'), loc)))) in mfe end
--- a/src/explify.sml Thu Jul 31 13:08:57 2008 -0400 +++ b/src/explify.sml Thu Jul 31 16:28:55 2008 -0400 @@ -71,6 +71,19 @@ | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) +fun explifyPatCon pc = + case pc of + L.PConVar n => L'.PConVar n + | L.PConProj x => L'.PConProj x + +fun explifyPat (p, loc) = + case p of + L.PWild => (L'.PWild, loc) + | L.PVar x => (L'.PVar x, loc) + | L.PPrim p => (L'.PPrim p, loc) + | L.PCon (pc, po) => (L'.PCon (explifyPatCon pc, Option.map explifyPat po), loc) + | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, explifyPat p)) xps), loc) + fun explifyExp (e, loc) = case e of L.EPrim p => (L'.EPrim p, loc) @@ -89,7 +102,9 @@ {field = explifyCon field, rest = explifyCon rest}), loc) | L.EFold k => (L'.EFold (explifyKind k), loc) - | L.ECase _ => raise Fail "Explify ECase" + | L.ECase (e, pes, t) => (L'.ECase (explifyExp e, + map (fn (p, e) => (explifyPat p, explifyExp e)) pes, + explifyCon t), loc) | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)