+ let divs, p = subst_in_problem subst p in\r
+ divs, p\r
+;;\r
+\r
+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