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