+let problem_of (label, div, convs, ps, var_names) =\r
+ print_hline ();\r
+ let rec aux = function\r
+ | `Lam(_, t) -> L (aux t)\r
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args\r
+ | `Var(v,_) -> V v\r
+ | `N _ | `Match _ -> assert false in\r
+ assert (List.length ps = 0);\r
+ let convs = List.rev convs in\r
+ let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let var_names = "@" :: var_names in\r
+ let div = match div with\r
+ | Some div -> aux (div :> Num.nf)\r
+ | None -> assert false 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\r
+;;\r
+\r
+let solve p =\r
+ if eta_subterm p.div p.conv\r
+ then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
+ else check p (auto p)\r
+;;\r
+\r
+Problems.main (solve ++ problem_of);\r
+\r
+(* Example usage of interactive: *)\r
+\r
+(* let interactive div conv cmds =\r