X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=61d078c22140dce589be39211b1bc0289e48ed4c;hb=e9773d6f01666895a51ef2212619bfeafbb97221;hp=b4a3118199d517266147b7712a976a54ce841e08;hpb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;p=helm.git diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index b4a311819..61d078c22 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -314,17 +314,63 @@ 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 @@ -337,58 +383,64 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = let timeout = try Some (float_of_string timeout) with Failure _ -> None 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 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 - -(* with ProofEngineTypes.Fail _ -> *) -(* normal_auto () *) - ) else - normal_auto () - in match superposition with | true -> - ProofEngineTypes.mk_tactic - (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table) - | _ -> 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 ;; -(********************** applyS *******************) +let auto_tac ~params ~dbd = + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) +;; + +(* {{{ **************** applyS *******************) let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = @@ -500,4 +552,6 @@ let applyS_tac ~dbd ~term = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) +(* }}} ********************************) + let pp_proofterm = Equality.pp_proofterm;;