Wrapping works in Blog

6 files changed, 48 insertions, 9 deletions

diff --git a/src/core.sml b/src/core.sml
index baec6e41..0b81e50e 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -103,6 +103,8 @@ datatype exp' =
 
        | EClosure of int * exp list
 
+       | ELet of string * con * exp * exp
+
 withtype exp = exp' located
 
 datatype export_kind =
diff --git a/src/core_print.sml b/src/core_print.sml
index 1214a54f..cd31487e 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -362,6 +362,21 @@ fun p_exp' par env (e, _) =
                                                                       p_exp env e]) es,
                                  string ")"]
 
+      | 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/core_util.sml b/src/core_util.sml
index f0697183..2a690736 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -487,6 +487,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                      fn es' =>
                         (EClosure (n, es'), 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))))
+
         and mfp ctx (pAll as (p, loc)) =
             case p of
                 PWild => S.return2 pAll
diff --git a/src/corify.sml b/src/corify.sml
index ff9506fd..0ec98c69 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -580,6 +580,8 @@ fun corifyExp st (e, loc) =
 
       | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
 
+      | L.ELet (x, t, e1, e2) => (L'.ELet (x, corifyCon st t, corifyExp st e1, corifyExp st e2), loc)
+
 fun corifyDecl mods ((d, loc : EM.span), st) =
     case d of
         L.DCon (x, n, k, c) =>
diff --git a/src/monoize.sml b/src/monoize.sml
index 17e28034..79940842 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1954,6 +1954,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             in
                 ((L'.EClosure (n, es), loc), fm)
             end
+
+          | L.ELet (x, t, e1, e2) =>
+            let
+                val t' = monoType env t
+                val (e1, fm) = monoExp (env, st, fm) e1
+                val (e2, fm) = monoExp (Env.pushERel env x t, st, fm) e2
+            in
+                ((L'.ELet (x, t', e1, e2), loc), fm)
+            end
     end
 
 fun monoDecl (env, fm) (all as (d, loc)) =
diff --git a/src/unnest.sml b/src/unnest.sml
index e5eddc42..b305b467 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -206,29 +206,31 @@ fun exp ((ks, ts), e, st : state) =
 
                             val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
                                                           let
-                                                              val e = apply (ENamed n, loc)
+                                                              val dummy = (EError, ErrorMsg.dummySpan)
+                                                                          
+                                                              fun repeatLift k =
+                                                                  if k = 0 then
+                                                                      apply (ENamed n, loc)
+                                                                  else
+                                                                      E.liftExpInExp 0 (repeatLift (k - 1))
                                                           in
-                                                              (0, E.liftExpInExp (nr - i - 1) e)
+                                                              (0, repeatLift i)
                                                           end)
-                                            vis
+                                                      vis
+
                             val subs' = rev subs'
 
                             val cfv = IS.listItems cfv
                             val efv = IS.listItems efv
                             val efn = length efv
 
-                            (*val subsInner = subs
-                                            @ map (fn (i, e) =>
-                                                      (i + efn,
-                                                       E.liftExpInExp efn e)) subs'*)
-
                             val subs = subs @ subs'
 
                             val vis = map (fn (x, n, t, e) =>
                                               let
                                                   (*val () = Print.prefaces "preSubst"
                                                                           [("e", ElabPrint.p_exp E.empty e)]*)
-                                                  val e = doSubst e subs(*Inner*)
+                                                  val e = doSubst e subs
 
                                                   (*val () = Print.prefaces "squishCon"
                                                                           [("t", ElabPrint.p_con E.empty t)]*)