+ match
+ Auto.auto_all_solutions universe cache commonctx metasenv l flags
+ with
+ | [],cache -> [],cache,universe
+ | solutions,cache ->
+ let solutions =
+ HExtlib.filter_map
+ (fun (subst,metasenv) ->
+ let opened =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv ~newmetasenv:metasenv
+ in
+ if opened = [] then
+ Some subst
+ else
+ None)
+ solutions
+ in
+ solutions,cache,universe
+;;
+
+let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+ (* argument parsing *)
+ let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in
+ let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in
+ let timeout = string "timeout" params in
+ let paramodulation = bool "paramodulation" params in
+ let full = bool "full" params in
+ let superposition = bool "superposition" params in
+ let target = string "target" params in
+ let table = string "table" params in
+ let subterms_only = bool "subterms_only" params in
+ let caso_strano = bool "caso_strano" params in
+ let demod_table = string "demod_table" params in
+ let timeout =
+ try Some (float_of_string timeout) with Failure _ -> None
+ in
+ match superposition with
+ | true ->
+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let use_paramodulation =
+ paramodulation && Equality.term_is_equality goalty
+ in
+ if use_paramodulation then
+ try
+ let rc =
+ Saturation.saturate
+ ~auto:(callback_for_paramodulation dbd)
+ caso_strano dbd ~depth ~width ~full
+ ?timeout (proof, goal)
+ in
+ prerr_endline (Saturation.get_stats ());rc
+ with exn ->
+ prerr_endline (Saturation.get_stats ());raise exn
+ else
+ let universe =
+ AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
+ in
+ let universe = (* we should get back a menv too XXX *)
+ AutoTypes.universe_of_context context metasenv universe
+ in
+ let oldmetasenv = metasenv in
+ match
+ Auto.auto universe AutoTypes.cache_empty context metasenv [goal]
+ {AutoTypes.default_flags with
+ AutoTypes.maxdepth = depth;
+ AutoTypes.maxwidth = width;
+(* AutoTypes.timeout = 0; *)
+ }
+ with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
+;;
+
+let auto_tac ~params ~dbd =
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)