summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 16:46:16 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 16:46:16 -0400
commit2e59aaacd591f76ba5d509284b835c8c34a034f5 (patch)
tree27d86d6061f3e52708492b82d0cfb82157c098cd /src
parent1145290f6ac5b13fe94772c692caa3cdb55bbf5f (diff)
Wrapping works in Blog
Diffstat (limited to 'src')
-rw-r--r--src/core.sml2
-rw-r--r--src/core_print.sml15
-rw-r--r--src/core_util.sml9
-rw-r--r--src/corify.sml2
-rw-r--r--src/monoize.sml9
-rw-r--r--src/unnest.sml20
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)]*)