From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jun 2018 13:05:06 +0000 (+0200)
Subject: Detect useless stepping when selecting the eta-different subterms
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e896eda9771bf0e9fd6cee3c8c9f25314d9d6736;p=fireball-separation.git

Detect useless stepping when selecting the eta-different subterms
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 45e605b..c7b9a3a 100644
--- 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) ;
         (match flag with
           | `Some b when !b -> b := false
-          | `Some b ->
-            print_string "WARNING! Stepping on a useless argument!";
-            ignore(read_line())
+          | `Some b -> ()
+            (*print_string "WARNING! Stepping on a useless argument!";
+            ignore(read_line())*)
           | `Inherit | `Duplicate -> assert false);
         A(flag, t1', erase t2')
     | `Inherit | `Duplicate ->
@@ -283,10 +283,18 @@ let find_eta_difference p t argsno =
  let t = inert_cut_at argsno t in
  let rec aux t u k = match t, u with
  | V _, V _ -> None
- | A(_,t1,t2), A(_,u1,u2) ->
+ | A(b1,t1,t2), A(b2,u1,u2) ->
     (match aux t1 u1 (k-1) with
     | None ->
-      if not (eta_eq t2 u2) then Some (k-1)
+      if not (eta_eq t2 u2) then begin
+        let is_relevant = function `Some b -> !b | _ -> false in
+        if not (is_relevant b1 || is_relevant b2) then begin
+         print_string "WARNING! Stepping on a useless argument!";
+print_string (string_of_t  t ^ " <==> " ^ string_of_t u);
+         ignore(read_line())
+        end ;
+        Some (k-1)
+       end
       else None
     | Some j -> Some j)
  | _, _ -> assert false