Detect useless stepping when selecting the eta-different subterms

[fireball-separation.git] / ocaml / simple.ml

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 45e605b7ee37160d42c606e864273a0971a31f88..c7b9a3a9998e33b5eeb822c416196373a536ceed 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -163,9 +163,9 @@ let rec subst top level delift ((flag, var, tm) as sub) =
         assert (match t1' with L _ -> false | _ -> true) ;\r
         (match flag with\r
           | `Some b when !b -> b := false\r
-          | `Some b ->\r
-            print_string "WARNING! Stepping on a useless argument!";\r
-            ignore(read_line())\r
+          | `Some b -> ()\r
+            (*print_string "WARNING! Stepping on a useless argument!";\r
+            ignore(read_line())*)\r
           | `Inherit | `Duplicate -> assert false);\r
         A(flag, t1', erase t2')\r
     | `Inherit | `Duplicate ->\r
@@ -283,10 +283,18 @@ let find_eta_difference p t argsno =
  let t = inert_cut_at argsno t in\r
  let rec aux t u k = match t, u with\r
  | V _, V _ -> None\r
- | A(_,t1,t2), A(_,u1,u2) ->\r
+ | A(b1,t1,t2), A(b2,u1,u2) ->\r
     (match aux t1 u1 (k-1) with\r
     | None ->\r
-      if not (eta_eq t2 u2) then Some (k-1)\r
+      if not (eta_eq t2 u2) then begin\r
+        let is_relevant = function `Some b -> !b | _ -> false in\r
+        if not (is_relevant b1 || is_relevant b2) then begin\r
+         print_string "WARNING! Stepping on a useless argument!";\r
+print_string (string_of_t  t ^ " <==> " ^ string_of_t u);\r
+         ignore(read_line())\r
+        end ;\r
+        Some (k-1)\r
+       end\r
       else None\r
     | Some j -> Some j)\r
  | _, _ -> assert false\r