let module S = CicSubstitution in
let module PET = ProofEngineTypes in
let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
| [] -> []
let compare_goals proof goal1 goal2 =
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
if List.mem ty already_seen_goals then [] else
let already_seen_goals = ty::already_seen_goals in
let facts = (depth = 1) in
- let _,metasenv,p,_ = proof in
+ let _,metasenv,p,_, _ = proof in
(* first of all we check if the goal has been already
inspected *)
assert (CicUtil.exists_meta goal metasenv);
and auto_new dbd width already_seen_goals universe = function
| [] -> []
| (subst,(proof, goals, sign))::tl ->
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let goals'=
List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
in
(List.length goals) > width ->
auto_new dbd width already_seen_goals universe tl
| (subst,(proof, (goal,depth)::gtl, sign))::tl ->
- let _,metasenv,p,_ = proof in
+ let _,metasenv,p,_, _ = proof in
let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
match (auto_single dbd proof goal ey ty depth
(width - (List.length gtl)) sign already_seen_goals) universe
| (_,(proof,[],_))::_ ->
let t2 = Unix.gettimeofday () in
debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_ = proof in
+ let _,_,p,_, _ = proof in
debug_print (lazy (CicPp.ppterm p));
- Printf.printf "tempo: %.9f\n" (t2 -. t1);
+ debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
(proof,[])
| _ -> assert false
in
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
(* argument parsing *)
- let int = int params
- and string = string params
- and bool = bool params in
- let newauto = bool "new" false in
+ let int = int params in
+ let bool = bool params in
+ let oldauto = bool "old" false in
+ let use_only_paramod = bool "paramodulation" false in
+ let oldauto = if use_only_paramod then false else oldauto in
let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
- let timeout = int "timeout" 0 in
- let use_paramod = bool "use_paramod" true in
- let use_only_paramod = bool "paramodulation" false in
- (* hacks to debug paramod *)
- let superposition = bool "superposition" false in
- let target = string "target" "" in
- let table = string "table" "" in
- let subterms_only = bool "subterms_only" false in
- let demod_table = string "demod_table" "" in
- let newauto = if use_only_paramod then true else newauto 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 ->
- if not newauto then
- auto_tac_old ~depth ~width ~dbd () (proof,goal)
- else
- (* this is the real auto *)
- let _, metasenv, _, _ = proof in
- let _, context, goalty = CicUtil.lookup_meta goal metasenv in
- let cache =
- let cache =
- AutoCache.cache_add_context context metasenv AutoCache.cache_empty
- in
- if use_only_paramod then (* only paramod *)
- cache
- else
- AutoCache.cache_add_library dbd proof [goal] cache
- in
- let oldmetasenv = metasenv in
- let flags = {
- AutoTypes.maxdepth =
- if use_only_paramod then 2 else depth;
- AutoTypes.maxwidth = width;
- AutoTypes.timeout =
- if timeout = 0 then float_of_int timeout
- else Unix.gettimeofday() +. (float_of_int timeout);
- AutoTypes.use_paramod = use_paramod;
- AutoTypes.use_only_paramod = use_only_paramod;
- AutoTypes.dont_cache_failures = false
- }
- in
- match Auto.auto dbd cache context metasenv [goal] flags 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
-;;
+ if oldauto then
+ auto_tac_old ~depth ~width ~dbd () (proof,goal)
+ else
+ ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal)
-let auto_tac ~params ~dbd =
- ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+let auto_tac ~params ~dbd ~universe=
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe)
;;
let pp_proofterm = Equality.pp_proofterm;;