-let problem_of div conv =\r
- print_hline ();\r
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
- let varno = List.length var_names in\r
- let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
- (* initial sanity check *)\r
- sanity p; p\r
-;;\r
-\r
-let exec div conv cmds =\r
- let p = problem_of div conv in\r
- try\r
- problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
- with\r
- | Done _ -> ()\r
+let finish p =\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 -> max n (aux 0 t)\r
+ | V _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let j = div_nargs - 1 in\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 ~isfinish:true j n p in\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let rec aux m = function\r
+ A(_,t1,t2) -> if is_var t2 then\r
+ (let delta_var, _ = get_inert t2 in\r
+ if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None\r
+ then m, delta_var\r
+ else aux (m-1) t1) else aux (m-1) t1\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
+ let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
+ sanity p\r