Mercurial > urweb
changeset 449:89f766f19d5b
Explify 'let'
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 01 Nov 2008 16:08:39 -0400 |
| parents | 85819353a84f |
| children | 07f6576aeb0a |
| files | src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml |
| diffstat | 4 files changed, 51 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/expl.sml Sat Nov 01 15:58:55 2008 -0400 +++ b/src/expl.sml Sat Nov 01 16:08:39 2008 -0400 @@ -98,6 +98,8 @@ | EWrite of exp + | ELet of string * con * exp * exp + withtype exp = exp' located datatype sgn_item' =
--- a/src/expl_print.sml Sat Nov 01 15:58:55 2008 -0400 +++ b/src/expl_print.sml Sat Nov 01 16:08:39 2008 -0400 @@ -83,10 +83,11 @@ p_con' true env c] | CRel n => - if !debug then - string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupCRel env n)) + ((if !debug then + string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupCRel env n))) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) | CNamed n => ((if !debug then string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) @@ -172,7 +173,7 @@ 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)) + handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | PConProj (m1, ms, x) => let val m1x = #1 (E.lookupStrNamed env m1) @@ -211,15 +212,17 @@ case e of EPrim p => Prim.p_t p | ERel n => - if !debug then - string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupERel env n)) + ((if !debug then + string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupERel env n))) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) | ENamed n => - if !debug then - string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) - else - string (#1 (E.lookupENamed env n)) + ((if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n))) + handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | EModProj (m1, ms, x) => let val (m1x, sgn) = E.lookupStrNamed env m1 @@ -362,6 +365,23 @@ space, p_exp env e]) pes]) + | ELet (x, t, e1, e2) => box [string "let", + space, + string x, + space, + string ":", + p_con env t, + space, + string "=", + space, + p_exp env e1, + space, + string "in", + newline, + p_exp (E.pushERel env x t) e2] + + + and p_exp env = p_exp' false env fun p_named x n =
--- a/src/expl_util.sml Sat Nov 01 15:58:55 2008 -0400 +++ b/src/expl_util.sml Sat Nov 01 16:08:39 2008 -0400 @@ -325,6 +325,15 @@ S.map2 (mfc ctx result, fn result' => (ECase (e', pes', {disc = disc', result = result'}), loc))))) + + | ELet (x, t, e1, e2) => + S.bind2 (mfc ctx t, + fn t' => + S.bind2 (mfe ctx e1, + fn e1' => + S.map2 (mfe ctx e2, + fn e2' => + (ELet (x, t', e1', e2'), loc)))) in mfe end
--- a/src/explify.sml Sat Nov 01 15:58:55 2008 -0400 +++ b/src/explify.sml Sat Nov 01 16:08:39 2008 -0400 @@ -116,6 +116,13 @@ | L.EUnif (ref (SOME e)) => explifyExp e | L.EUnif _ => raise Fail ("explifyExp: Undetermined EUnif at " ^ EM.spanToString loc) + | L.ELet (des, e) => + foldr (fn ((de, loc), e) => + case de of + L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains" + | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc)) + (explifyExp e) des + fun explifySgi (sgi, loc) = case sgi of L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)