X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=e8d034a3298a9630fa0c8b1efe693579a1045ed2;hb=b0612e00b2a905510439d9a6e8908497c1b74c61;hp=63dc8631dbc8b4b564fded81c72ea44fcffe204c;hpb=41e76668e9389ce17e41747026e533f907a0311c;p=helm.git diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 63dc8631d..e8d034a32 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -269,8 +269,7 @@ and auto_new_aux dbd width already_seen_goals universe = function let default_depth = 5 let default_width = 3 -(* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) +let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof,goal) = @@ -281,215 +280,59 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) 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 "No Applicable theorem") + 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)); - Printf.printf "tempo: %.9f\n" (t2 -. t1); + debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); (proof,[]) | _ -> assert false in - ProofEngineTypes.mk_tactic (auto_tac dbd) + auto_tac dbd ;; -*) - -(* -let paramodulation_tactic = ref - (fun dbd ?full ?depth ?width status -> - raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; - -let term_is_equality = ref - (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -*) -let bool name params = - try let _ = List.assoc name params in true with - | Not_found -> false +let bool params name default = + try + let s = List.assoc name params in + if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true + else if s = "0" || s = "false" || s = "no" || s= "off" then false + else + let msg = "Unrecognized value for parameter "^name^"\n" in + let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in + raise (ProofEngineTypes.Fail (lazy msg)) + with Not_found -> default ;; -let string name params = +let string params name default = try List.assoc name params with - | Not_found -> "" + | Not_found -> default ;; -let int name params = +let int params name default = 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 auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) = (* argument parsing *) - let depth = int "depth" params in - let width = int "width" 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 demod_table = string "demod_table" 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 () - in - match superposition with - | true -> - ProofEngineTypes.mk_tactic - (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table) - | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) -;; + 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 + if oldauto then + auto_tac_old ~depth ~width ~dbd () (proof,goal) + else + ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal) -(********************** applyS *******************) - -let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = - let (consthead,newmetasenv,arguments,_) = - ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in - let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in - let proof',metasenv = - let (puri,metasenv,pbo,pty) = proof in - (puri,newmetasenv,pbo,pty),metasenv - in - let proof'',goals = - match LibraryObjects.eq_URI () with - | Some uri -> - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) - ~continuation: - (PrimitiveTactics.cut_tac - (CicSubstitution.lift 1 - (Cic.Appl - [Cic.MutInd (uri,0,[]); - Cic.Sort Cic.Prop; - consthead; - ty])))) (proof',goal) - | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) - in - match goals with - [g1;g2] -> - let proof'',goals = - ProofEngineTypes.apply_tactic - (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2) - in - let proof'',goals = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - ) (proof'',g1) - in - proof'', - (*CSC: Brrrr.... *) - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:(let _,m,_,_ = proof'' in m) - | _ -> assert false - -let rec count_prods context ty = - match CicReduction.whd context ty with - Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t - | _ -> 0 - -let applyS_tac ~dbd ~term (proof, goal) = - let module T = CicTypeChecker in - let module R = CicReduction in - let module C = Cic in - let (_,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in - let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = - match term with - C.Var (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Var (uri,exp_named_subst') - | C.Const (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | _ -> [],newmeta,[],term - in - let metasenv' = metasenv@newmetasenvfragment in - let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph - in - let termty = - CicSubstitution.subst_vars exp_named_subst_diff termty in - let goal_arity = count_prods context ty in - let res = - new_metasenv_and_unify_and_t dbd proof goal - newmeta' metasenv' context term' ty termty goal_arity - in - res +let auto_tac ~params ~dbd ~universe= + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe) +;; -let applyS_tac ~dbd ~term = - ProofEngineTypes.mk_tactic - (fun status -> - try applyS_tac ~dbd ~term status - with - | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (ProofEngineTypes.Fail msg)) +let pp_proofterm = Equality.pp_proofterm;;