More comments and improved find_eta_difference

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 35874b69e5ec3e90f95e84586a8071f3b5eb9ec8..e5e829a5accccbf0e37ce2fbefe62b4a6c9f0ed5 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -218,16 +218,19 @@ let inert_cut_at n t =
  in snd (aux t)\r
 ;;\r
 \r
-(* FIXME! eta_difference dovrebbe restituire un int partendo da 0 *)\r
-let find_eta_difference p t n_args =\r
- let t = inert_cut_at n_args t in\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 _ -> assert false (* div subterm of conv *)\r
+ | V _, V _ -> problem_fail p "no eta difference found (div subterm of conv?)"\r
  | A(t1,t2), A(u1,u2) ->\r
-    if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k)\r
+    if not (eta_eq t2 u2) then (k-1)\r
     else aux t1 u1 (k-1)\r
  | _, _ -> assert false\r
- in aux p.div t n_args\r
+ in aux p.div t argsno\r
 ;;\r
 \r
 let compute_max_lambdas_at hd_var j =\r
@@ -306,7 +309,7 @@ let rec auto p =
       else auto p\r
     with Done sigma -> sigma)\r
  | Some t ->\r
-  let j = find_eta_difference p t n_args - 1 in\r
+  let j = find_eta_difference p t n_args in\r
   let k = 1 + max\r
    (compute_max_lambdas_at hd_var j p.div)\r
     (compute_max_lambdas_at hd_var j p.conv) in\r