+let finish p arity =\r
+ (* one-step version of eat *)\r
+ let compute_max_arity =\r
+ let rec aux n = function\r
+ | A(t1,t2) -> max (aux (n+1) t1) (aux 0 t2)\r
+ | L(t,g) -> List.fold_right (max ++ (aux 0)) (t::g) 0\r
+ | _ -> n\r
+ in aux 0 in\r
+ (* First, a step on the last argument of the divergent.\r
+ Because of the sanity check, it will never be a constant term. *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> raise (Backtrack "Cannot finish on constant tm") in\r
+ let j = match\r
+ smallest_such_that (fun i t -> i >= arity && not (is_constant t)) (args_of_inert p.div)\r
+ with Some j -> j | None -> raise (Backtrack "") in\r
+ print_endline "\n>> FINISHING";\r
+ let arity = compute_max_arity p.conv in\r
+ let n = 1 + arity + max\r
+ (compute_max_lambdas_at div_hd j p.div)\r
+ (compute_max_lambdas_at div_hd j p.conv) in\r
+ let _, p = step j n p in\r
+ (* Now, find first argument of div that is a variable never applied anywhere.\r
+ It must exist because of some invariant, since we just did a step,\r
+ and because of the arity of the divergent *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> assert false in\r
+ let rec aux m = function\r
+ | A(t, V delta_var) ->\r
+ if delta_var <> div_hd && get_subterms_with_head delta_var p.conv = []\r
+ then m, delta_var\r
+ else aux (m-1) t\r
+ | A(t,_) -> aux (m-1) t\r
+ | _ -> assert false in\r
+ let m, delta_var = aux div_nargs p.div in\r
+ let _, p = subst_in_problem (delta_var, delta) p in\r
+ ignore (subst_in_problem (div_hd, mk_lams delta (m-1)) p);\r
+ assert false\r
+;;\r
+\r
+let auto p =\r
+ let rec aux p =\r
+ if eta_subterm p.div p.conv\r
+ then raise (Backtrack "div is subterm of conv");\r
+ match p.div with\r
+ | L _ as t -> (* case p.div is an abstraction *)\r
+ print_endline "\nSOTTO UN LAMBDA";\r
+ let t, g = mk_app t C in\r
+ aux ({p with div=mk_apps C (t::g)})\r
+ | V _ | C -> raise (Backtrack "V | C")\r
+ | A _ -> (\r
+ if is_constant p.div (* case p.div is rigid inert *)\r
+ then (print_endline "\nSOTTO UN C"; try_all "auto.C"\r
+ (fun div -> aux (sanity {p with div})) (args_of_inert p.div))\r
+ else (* case p.div is flexible inert *)\r
+ let hd, n_args = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | A _ -> assert false\r
+ | V hd_var ->\r
+ let tms = get_subterms_with_head hd_var p.conv in\r
+ let arity = List.fold_right (max ++ (snd ++ get_inert)) tms 0 in\r
+ try_both "???" (finish p) arity\r
+ (fun _ ->\r
+ let jss = List.concat (List.map (find_eta_difference p) tms) in\r
+ let jss = List.sort_uniq compare jss in\r
+ let f = try_all "no differences"\r
+ (fun j ->\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
+ let divs, p = step j k p in\r
+ try_all "p.div" (fun div -> aux (sanity {p with div})) divs\r
+ ) in\r
+ try_both "step, then diverge arguments"\r
+ f jss\r
+ (try_all "tried p.div arguments" (fun div -> aux {p with div})) (args_of_inert p.div)\r
+ ) ()\r
+ ) in try\r
+ aux p\r
+ with Done sigma -> sigma\r