From 16d3d1c3a6d1e78faab91076c20b76fdcb90edb9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 31 Jul 2008 16:28:55 -0400 Subject: Case through explify --- src/corify.sml | 1 + src/elab.sml | 2 +- src/elab_print.sml | 20 +++++++++----------- src/elaborate.sml | 15 ++++++--------- src/expl.sml | 15 +++++++++++++++ src/expl_print.sml | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ src/expl_util.sml | 11 +++++++++++ src/explify.sml | 17 ++++++++++++++++- 8 files changed, 114 insertions(+), 22 deletions(-) (limited to 'src') diff --git a/src/corify.sml b/src/corify.sml index 7332395c..cf6d5658 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -394,6 +394,7 @@ fun corifyExp st (e, 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.ECase _ => raise Fail "Corify ECase" | L.EWrite e => (L'.EWrite (corifyExp st e), loc) fun corifyDecl ((d, loc : EM.span), st) = diff --git a/src/elab.sml b/src/elab.sml index af21def0..58e69629 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -80,7 +80,7 @@ datatype pat' = | 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 diff --git a/src/elab_print.sml b/src/elab_print.sml index d0ff8d5f..591e019b 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -220,17 +220,15 @@ fun p_pat' par env (p, _) = | 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index 0a71aa8c..da38cbba 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1045,17 +1045,13 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) = 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 @@ fun exhaustive (env, denv, t, ps) = | 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 diff --git a/src/expl.sml b/src/expl.sml index 183dbc31..52dbee63 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -59,6 +59,19 @@ datatype con' = 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 @@ datatype exp' = | 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 diff --git a/src/expl_print.sml b/src/expl_print.sml index 7d0bfebd..3595f65a 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -155,6 +155,48 @@ and p_name env (all as (c, _)) = 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 @@ fun p_exp' par env (e, loc) = 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 = diff --git a/src/expl_util.sml b/src/expl_util.sml index e1a5d30f..685605c3 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -286,6 +286,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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 diff --git a/src/explify.sml b/src/explify.sml index da94ba94..7c23c2f5 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -71,6 +71,19 @@ fun explifyCon (c, loc) = | 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 @@ fun explifyExp (e, loc) = {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) -- cgit v1.2.3