-let parse strs =\r
- let rec aux level = function\r
- | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
- | Parser_andrea.App (t1, t2) ->\r
- if level = 0 then mk_app (aux level t1) (aux level t2)\r
- else A(aux level t1, aux level t2)\r
- | Parser_andrea.Var v -> V v in\r
- let (tms, free) = Parser_andrea.parse_many strs in\r
- (List.map (aux 0) tms, free)\r
+let auto p =\r
+ let rec aux p =\r
+ let hd, n_args = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | B | A _ -> assert false\r
+ | V hd_var ->\r
+ let tms = get_subterms_with_head hd_var p.conv in\r
+ if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
+ then (\r
+ (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)\r
+ List.iter (fun t -> try\r
+ let js = find_eta_difference p t in\r
+ (* print_endline (String.concat ", " (List.map string_of_int js)); *)\r
+ if js = [] then problem_fail p "no eta difference found (div subterm of conv?)";\r
+ let js = List.rev js in\r
+ List.iter\r
+ (fun j ->\r
+ try\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
+ ignore (aux (step j k p))\r
+ with Fail(_, s) ->\r
+ print_endline ("Backtracking (eta_diff) because: " ^ s)) js;\r
+ raise (Fail(-1, "no eta difference"))\r
+ with Fail(_, s) ->\r
+ print_endline ("Backtracking (get_subterms) because: " ^ s)) tms;\r
+ raise (Fail(-1, "no similar terms"))\r
+ )\r
+ else\r
+ (let phase = p.phase in\r
+ let p = eat p in\r
+ if phase = `Two\r
+ then problem_fail p "Auto.2 did not complete the problem"\r
+ else aux p)\r
+ in\r
+ try\r
+ aux p\r
+ with Done sigma -> sigma\r