From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jun 2018 15:01:41 +0000 (+0200)
Subject: Fix: find_eta_difference now works with inerts of arbitrary length
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1dc1445295ffe5e83cbce853387ff0b68d56f85f;p=fireball-separation.git

Fix: find_eta_difference now works with inerts of arbitrary length

All simple.x tests now pass (same for automatically generated ones)
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index bac3ddf..c318ebd 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -114,6 +114,16 @@ let rec get_inert = function
  | _ -> assert false
 ;;
 
+let args_of_inert =
+ let rec aux acc =
+  function
+   | V _ | C -> acc
+   | A(t, a) -> aux (a::acc) t
+   | _ -> assert false
+ in
+  aux []
+;;
+
 (* precomputes the number of leading lambdas in a term,
    after replacing _v_ w/ a term starting with n lambdas *)
 let rec no_leading_lambdas v n = function
@@ -216,19 +226,18 @@ let inert_cut_at n t =
 ;;
 
 (* return the index of the first argument with a difference
-   (the first argument is 0)
-   precondition: p.div and t have n+1 arguments
-   *)
-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 _ -> []
- | A(t1,t2), A(u1,u2) ->
-    print_endline (string_of_t t2 ^ " vs " ^ string_of_t u2);
-    if not (eta_eq t2 u2) then (k-1)::aux t1 u1 (k-1)
-    else aux t1 u1 (k-1)
- | _, _ -> assert false
- in aux p.div t argsno
+   (the first argument is 0) *)
+let find_eta_difference p t =
+ let divargs = args_of_inert p.div in
+ let conargs = args_of_inert t in
+ let rec aux k divargs conargs =
+  match divargs,conargs with
+     [],_ -> []
+   | _::_,[] -> [k]
+   | t1::divargs,t2::conargs ->
+      (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs
+ in
+  aux 0 divargs conargs
 ;;
 
 let compute_max_lambdas_at hd_var j =
@@ -312,7 +321,7 @@ let auto p =
   then (
     (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)
     List.iter (fun t -> try
-      let js = find_eta_difference p t n_args in
+      let js = find_eta_difference p t in
       (* print_endline (String.concat ", " (List.map string_of_int js)); *)
       if js = [] then problem_fail p "no eta difference found (div subterm of conv?)";
       let js = List.rev js in