Mercurial > urweb
diff src/unnest.sml @ 1272:56bd4a4f6e66
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
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 03 Jun 2010 13:04:37 -0400 |
| parents | c316ca3c9ec6 |
| children | b4480a56cab7 |
line wrap: on
line diff
--- a/src/unnest.sml Tue Jun 01 15:46:24 2010 -0400 +++ b/src/unnest.sml Thu Jun 03 13:04:37 2010 -0400 @@ -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 @@ | 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 @@ 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 @@ (*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})