From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 1 Jun 2018 12:27:15 +0000 (+0200)
Subject: More comments and improved find_eta_difference
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2dc39f89b90fc5b63d8ef4208e43557fb8e1206e;p=fireball-separation.git

More comments and improved find_eta_difference
---

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