diff options
| -rw-r--r-- | src/expl.sml | 2 | ||||
| -rw-r--r-- | src/expl_print.sml | 46 | ||||
| -rw-r--r-- | src/expl_util.sml | 9 | ||||
| -rw-r--r-- | src/explify.sml | 7 |
4 files changed, 51 insertions, 13 deletions
diff --git a/src/expl.sml b/src/expl.sml index 2e96db54..8f531516 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -98,6 +98,8 @@ datatype exp' = | EWrite of exp + | ELet of string * con * exp * exp + withtype exp = exp' located datatype sgn_item' = diff --git a/src/expl_print.sml b/src/expl_print.sml index d19edeae..b19a6eff 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -83,10 +83,11 @@ fun p_con' par env (c, _) = 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 @@ fun p_patCon env pc = 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 @@ fun p_exp' par env (e, loc) = 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 @@ fun p_exp' par env (e, loc) = 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 = diff --git a/src/expl_util.sml b/src/expl_util.sml index bda602d3..e12186b0 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -325,6 +325,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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 diff --git a/src/explify.sml b/src/explify.sml index 1bca49c3..e19bb200 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -116,6 +116,13 @@ fun explifyExp (e, loc) = | 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) |