Mercurial > urweb
diff src/reduce.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 | beb67ff4c8a0 |
| children | 3b22c3c67f35 |
line wrap: on
line diff
--- a/src/reduce.sml Tue Jun 01 15:46:24 2010 -0400 +++ b/src/reduce.sml Thu Jun 03 13:04:37 2010 -0400 @@ -65,6 +65,18 @@ CoreUtil.Exp.RelE _ => n + 1 | _ => n} +val cdangling = + CoreUtil.Exp.existsB {kind = fn _ => false, + con = fn (n, c) => + case c of + CRel n' => n' >= n + | _ => false, + exp = fn _ => false, + bind = fn (n, b) => + case b of + CoreUtil.Exp.RelC _ => n + 1 + | _ => n} + datatype env_item = UnknownK | KnownK of kind @@ -86,6 +98,15 @@ | (Lift (_, _, n'), n) => n + n' | (_, n) => n) 0 +val cdepth = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (_, n) => n) 0 + +val cdepth' = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (Lift (_, n', _), n) => n + n' + | (_, n) => n) 0 + type env = env_item list fun ei2s ei = @@ -344,6 +365,11 @@ raise Fail "!") else ()*) + (*val () = if cdangling (cdepth env) all then + Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("env", Print.PD.string (e2s env))] + else + ()*) val r = case e of EPrim _ => all @@ -636,6 +662,12 @@ raise Fail "!!") else ();*) + (*if cdangling (cdepth' (deKnown env)) r then + (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("r", CorePrint.p_exp CoreEnv.empty r)]; + raise Fail "!!") + else + ();*) r end in