Eat was erasing terms from C that made it diverge

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 7be80c430b9bbac484e4d8f8029f9dbd8073a5ee..b5a508691ea31dd83a8c930017df85d81f687b73 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -246,23 +246,27 @@ let eat p =
 print_cmd "EAT" "";\r
  let var, k = get_inert p.div in\r
  let phase = p.phase in\r
- let p, t =\r
+ let p =\r
   match phase with\r
   | `One ->\r
       let n = 1 + max\r
-       (compute_max_lambdas_at var k p.div)\r
-       (compute_max_lambdas_at var k p.conv) in\r
+       (compute_max_lambdas_at var (k-1) p.div)\r
+       (compute_max_lambdas_at var (k-1) p.conv) in\r
       (* apply fresh vars *)\r
       let p, t = fold_nat (fun (p, t) _ ->\r
         let p, v = freshvar p in\r
         p, A(t, V (v + k))\r
       ) (p, V 0) n in\r
-      let p = {p with phase=`Two} in p, A(t, delta)\r
-  | `Two -> p, delta in\r
- let subst = var, mk_lams t k in\r
- let p = subst_in_problem subst p in\r
- sanity p;\r
- let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
+      let p = {p with phase=`Two} in\r
+      let t = A(t, delta) in\r
+      let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
+      let subst = var, mk_lams t k in\r
+      let p = subst_in_problem subst p in\r
+      let _, args = get_inert p.div in\r
+      {p with div = inert_cut_at (args-k) p.div}\r
+  | `Two ->\r
+      let subst = var, mk_lams delta k in\r
+      subst_in_problem subst p in\r
  sanity p\r
 ;;\r
 \r
@@ -385,6 +389,13 @@ run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
  "x a a a a (_. _. _. _. x. y. x y)";\r
 ] ;;\r
 \r
+(* bug in eat that was erasing terms in convergent that then diverged *)\r
+run "x y z"\r
+[\r
+"x @ @";\r
+"z (y @ (y @))"\r
+] ;;\r
+\r
 (* bug in no_leading_lambdas where x in j-th position *)\r
 run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
 ["v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))"]\r