X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;fp=ocaml%2Fsimple.ml;h=b5a508691ea31dd83a8c930017df85d81f687b73;hb=2ad3be49dd888a10237ee5391c7bbb2ff6e9c2df;hp=7be80c430b9bbac484e4d8f8029f9dbd8073a5ee;hpb=b529f51389b1a5f2f2e5f035f8c1abdafe5a0a4c;p=fireball-separation.git

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)))"]