From 2dc39f89b90fc5b63d8ef4208e43557fb8e1206e Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 1 Jun 2018 14:27:15 +0200 Subject: [PATCH] More comments and improved find_eta_difference --- ocaml/simple.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) 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 -- 2.39.2