From 2ad3be49dd888a10237ee5391c7bbb2ff6e9c2df Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 18:30:38 +0200
Subject: [PATCH] Eat was erasing terms from C that made it diverge

---
 ocaml/simple.ml | 29 ++++++++++++++++++++---------
 1 file changed, 20 insertions(+), 9 deletions(-)

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 7be80c4..b5a5086 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -246,23 +246,27 @@ let eat p =
 print_cmd "EAT" "";
  let var, k = get_inert p.div in
  let phase = p.phase in
- let p, t =
+ let p =
   match phase with
   | `One ->
       let n = 1 + max
-       (compute_max_lambdas_at var k p.div)
-       (compute_max_lambdas_at var k p.conv) in
+       (compute_max_lambdas_at var (k-1) p.div)
+       (compute_max_lambdas_at var (k-1) p.conv) in
       (* apply fresh vars *)
       let p, t = fold_nat (fun (p, t) _ ->
         let p, v = freshvar p in
         p, A(t, V (v + k))
       ) (p, V 0) n in
-      let p = {p with phase=`Two} in p, A(t, delta)
-  | `Two -> p, delta in
- let subst = var, mk_lams t k in
- let p = subst_in_problem subst p in
- sanity p;
- let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in
+      let p = {p with phase=`Two} in
+      let t = A(t, delta) in
+      let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in
+      let subst = var, mk_lams t k in
+      let p = subst_in_problem subst p in
+      let _, args = get_inert p.div in
+      {p with div = inert_cut_at (args-k) p.div}
+  | `Two ->
+      let subst = var, mk_lams delta k in
+      subst_in_problem subst p in
  sanity p
 ;;
 
@@ -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)";
 ] ;;
 
+(* bug in eat that was erasing terms in convergent that then diverged *)
+run "x y z"
+[
+"x @ @";
+"z (y @ (y @))"
+] ;;
+
 (* bug in no_leading_lambdas where x in j-th position *)
 run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"
 ["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)))"]
-- 
2.39.2