let rec subst level delift sub =\r
function\r
| V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
- | L t -> L (subst (level + 1) delift sub t)\r
+ | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t\r
| A (t1,t2) ->\r
let t1 = subst level delift sub t1 in\r
let t2 = subst level delift sub t2 in\r
mk_app t1 t2\r
| B -> B\r
-and mk_app t1 t2 = if t1 = delta && t2 = delta then B else match t1 with\r
- | B | _ when t2 = B -> B\r
+and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
+ else match t1 with\r
+ | B -> B\r
| L t1 -> subst 0 true (0, t2) t1\r
- | t1 -> A (t1, t2)\r
+ | _ -> A (t1, t2)\r
and lift n =\r
let rec aux lev =\r
function\r
;;\r
\r
let check p sigma =\r
+ print_endline "Checking...";\r
let div = purify p.div in\r
let conv = purify p.conv in\r
let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
let sanity p =\r
print_endline (string_of_problem p); (* non cancellare *)\r
if p.conv = B then problem_fail p "p.conv diverged";\r
- (* if p.div = B then raise (Done p.sigma); *)\r
+ if p.div = B then raise (Done p.sigma);\r
if p.phase = `Two && p.div = delta then raise (Done p.sigma);\r
if not (is_inert p.div) then problem_fail p "p.div converged"\r
;;\r