From ecf29d252b740979357afcfa26173b09ea4c95f9 Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 11 Jun 2018 16:55:46 +0200 Subject: [PATCH] Append the eaten arg + leftmost order in find_eta_difference simple.evil example works. --- ocaml/simple.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 9de1f2a..aa91996 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -206,12 +206,17 @@ let inert_cut_at n t = 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 _ -> problem_fail p "no eta difference found (div subterm of conv?)" + | V _, V _ -> None | A(t1,t2), A(u1,u2) -> - if not (eta_eq t2 u2) then (k-1) - else aux t1 u1 (k-1) + (match aux t1 u1 (k-1) with + | None -> + if not (eta_eq t2 u2) then Some (k-1) + else None + | Some j -> Some j) | _, _ -> assert false - in aux p.div t argsno + in match aux p.div t argsno with + | None -> problem_fail p "no eta difference found (div subterm of conv?)" + | Some j -> j ;; let compute_max_lambdas_at hd_var j = @@ -269,8 +274,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")") let p, v = freshvar p in p, A(t, V (v + k + 1)) ) (p, V 0) n in - let t = (* apply unused bound variables V_{k-1}..V_1 *) - fold_nat (fun t m -> A(t, V (k-m+1))) t k in + let t = (* apply bound variables V_k..V_0 *) + fold_nat (fun t m -> A(t, V (k-m+1))) t (k+1) in let t = mk_lams t (k+1) in (* make leading lambdas *) let subst = var, t in let p = subst_in_problem subst p in -- 2.39.2