diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-06-03 13:04:37 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-06-03 13:04:37 -0400 |
| commit | b1d29df128dd1fa879e24f0eb3f5cdc1b74e16b7 (patch) | |
| tree | 370066a96da7c7aff61371c96f82804cde02fa75 /src/reduce.sml | |
| parent | ccc3c126378aaa53765f8d69c267c6ffee666acf (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/reduce.sml')
| -rw-r--r-- | src/reduce.sml | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/src/reduce.sml b/src/reduce.sml index b2911a5f..963863e8 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -65,6 +65,18 @@ val dangling = 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 @@ val edepth' = foldl (fn (UnknownE, n) => n + 1 | (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 @@ fun kindConAndExp (namedC, namedE) = 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 @@ fun kindConAndExp (namedC, namedE) = 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 |