From e896eda9771bf0e9fd6cee3c8c9f25314d9d6736 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Jun 2018 15:05:06 +0200 Subject: [PATCH] Detect useless stepping when selecting the eta-different subterms --- ocaml/simple.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) 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 -- 2.39.2