summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/expl.sml2
-rw-r--r--src/expl_print.sml46
-rw-r--r--src/expl_util.sml9
-rw-r--r--src/explify.sml7
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)