# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225570119 14400
# Node ID 89f766f19d5bf6fb2f4801f0f90b737a0f40f7ba
# Parent  85819353a84fb3863901e2ba464691bd12250540
Explify 'let'

diff -r 85819353a84f -r 89f766f19d5b src/expl.sml
--- 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' =
diff -r 85819353a84f -r 89f766f19d5b src/expl_print.sml
--- 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 =
diff -r 85819353a84f -r 89f766f19d5b src/expl_util.sml
--- 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
diff -r 85819353a84f -r 89f766f19d5b src/explify.sml
--- 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)