summaryrefslogtreecommitdiff
path: root/src/unnest.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-06-03 13:04:37 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-06-03 13:04:37 -0400
commit63f77395df8d7e78c21437876ce585b01517f0cc (patch)
tree370066a96da7c7aff61371c96f82804cde02fa75 /src/unnest.sml
parent4c67cd1d61cb79224bbe90dbdb229e0d9b58d3c9 (diff)
Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
Diffstat (limited to 'src/unnest.sml')
-rw-r--r--src/unnest.sml16
1 files changed, 13 insertions, 3 deletions
diff --git a/src/unnest.sml b/src/unnest.sml
index 77589bfb..a2ec32b0 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -204,12 +204,19 @@ fun exp ((ks, ts), e as old, st : state) =
| PRecord xpcs =>
foldl (fn ((_, p, _), ts) => doVars (p, ts))
ts xpcs
+
+ fun bindOne subs = ((0, (ERel 0, #2 ed))
+ :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
+
+ fun bindMany (n, subs) =
+ case n of
+ 0 => subs
+ | _ => bindMany (n - 1, bindOne subs)
in
([(EDVal (p, t, e), #2 ed)],
(doVars (p, ts),
maxName, ds,
- ((0, (ERel 0, #2 ed))
- :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs),
+ bindMany (E.patBindsN p, subs),
by))
end
| EDValRec vis =>
@@ -310,6 +317,7 @@ fun exp ((ks, ts), e as old, st : state) =
let
(*val () = print (Int.toString ex ^ "\n")*)
val (name, t') = List.nth (ts, ex)
+ val t' = squishCon cfv t'
in
((EAbs (name,
t',
@@ -354,6 +362,8 @@ fun exp ((ks, ts), e as old, st : state) =
(*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
+ (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
+ ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
(ELet (eds, e', t),
{maxName = maxName,
decls = ds})