diff options
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 |