From bcacd9c7aca307547ebff8dc7038b6f78156b507 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 1 Nov 2008 16:08:39 -0400
Subject: Explify 'let'

---
 src/expl.sml       |  2 ++
 src/expl_print.sml | 46 +++++++++++++++++++++++++++++++++-------------
 src/expl_util.sml  |  9 +++++++++
 src/explify.sml    |  7 +++++++
 4 files changed, 51 insertions(+), 13 deletions(-)

(limited to 'src')

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)
-- 
cgit v1.2.3