X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=61d078c22140dce589be39211b1bc0289e48ed4c;hb=bc9899a797f5d6e8e37a76923172d18c774e7573;hp=1ba1dd912495f63801c7ffbf90b0d785e93e883e;hpb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;p=helm.git diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 1ba1dd912..61d078c22 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -314,75 +314,133 @@ let string name params = | Not_found -> "" ;; -let int name params = +let int name default params = try int_of_string (List.assoc name params) with - | Not_found -> default_depth + | Not_found -> default | Failure _ -> raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -let auto_tac ~params ~(dbd:HMysql.dbd) = +(* +let callback_for_paramodulation dbd width depth t l = + let _,y,x,xx = t in + let universe = MetadataQuery.universe_of_goals ~dbd t l in + let todo = List.map (fun g -> (g, depth)) l in + prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx); + prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y); + match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with + | (_,(proof,[],_))::_ -> proof + | _ -> raise (Failure "xxx") +;; +*) + +let callback_for_paramodulation dbd flags proof commonctx ?universe cache l = + let _,metasenv,_,_ = proof in + let oldmetasenv = metasenv in + let universe = + match universe with + | Some u -> u + | None -> + let universe = + AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe + in + AutoTypes.universe_of_context commonctx metasenv universe + in + 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" params in - let width = int "width" params in + 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 what = string "what" params in - let other = string "other" params in + let target = string "target" params in + let table = string "table" params in let subterms_only = bool "subterms_only" params in - let demodulate = bool "demodulate" params in - (* the real tactic *) - let auto_tac dbd (proof, goal) = - let normal_auto () = - let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in - Hashtbl.clear inspected_goals; - debug_print (lazy "Entro in Auto"); - let id t = t in - let t1 = Unix.gettimeofday () in - match - auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] - with - [] -> debug_print(lazy "Auto failed"); - raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) - | (_,(proof,[],_))::_ -> - let t2 = Unix.gettimeofday () in - debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in - debug_print (lazy (CicPp.ppterm p)); - debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); - (proof,[]) - | _ -> assert false - in - let paramodulation_ok = - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - paramodulation && (full || (Equality.term_is_equality meta_goal)) - in - if paramodulation_ok then ( - debug_print (lazy "USO PARAMODULATION..."); -(* try *) - try - let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in - prerr_endline (Saturation.get_stats ()); - rc - with exn -> - prerr_endline (Saturation.get_stats ()); - raise exn - -(* with ProofEngineTypes.Fail _ -> *) -(* normal_auto () *) - ) else - normal_auto () + 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 -> - ProofEngineTypes.mk_tactic - (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate) - | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) + (* 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) ;; -(********************** applyS *******************) +(* {{{ **************** applyS *******************) let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = @@ -412,7 +470,7 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' [g1;g2] -> let proof'',goals = ProofEngineTypes.apply_tactic - (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2) + (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2) in let proof'',goals = ProofEngineTypes.apply_tactic @@ -493,3 +551,7 @@ let applyS_tac ~dbd ~term = | CicUnification.UnificationFailure msg | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) + +(* }}} ********************************) + +let pp_proofterm = Equality.pp_proofterm;;