X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=4b713d46492aa10d0ec03316f3a3dedcbcd828bc;hb=00d48171bacce45b5e7fcc17d841694aee4dba70;hp=42df90768263b2749c30f9ff81c1c0dcf4f9b12c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 42df90768..4b713d464 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -30,320 +30,94 @@ (* let debug_print = fun _ -> () *) -(* Profiling code -let new_experimental_hint = - let profile = CicUtil.profile "new_experimental_hint" in - fun ~dbd ~facts ?signature ~universe status -> - profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status -*) let new_experimental_hint = MetadataQuery.new_experimental_hint - -(* In this versions of auto_tac we maintain an hash table of all inspected - goals. We assume that the context is invariant for application. - To this aim, it is essential to sall hint_verbose, that in turns calls - apply_verbose. *) - -type exitus = - No of int - | Yes of Cic.term * int - | NotYetInspected - -let inspected_goals = Hashtbl.create 503;; - -let search_theorems_in_context status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let module PET = ProofEngineTypes in - let module PT = PrimitiveTactics in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let rec find n = function - | [] -> [] - | hd::tl -> - let res = - (* we should check that the hypothesys has not been cleared *) - if List.nth context (n-1) = None then - None - else - try - let (subst,(proof, goal_list)) = - PT.apply_tac_verbose ~term:(C.Rel n) status - in - (* - let goal_list = - List.stable_sort (compare_goal_list proof) goal_list in - *) - Some (subst,(proof, goal_list)) - with - PET.Fail _ -> None +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 params name default = + try List.assoc name params with + | Not_found -> default +;; + +let int params name default = + try int_of_string (List.assoc name params) with + | Not_found -> default + | Failure _ -> + raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) +;; + +let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = + (* argument parsing *) + let int = int params + and string = string params + and bool = bool params 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 + 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 cache = + let cache = + AutoCache.cache_add_context context metasenv AutoCache.cache_empty in - (match res with - | Some res -> res::(find (n+1) tl) - | None -> find (n+1) tl) - in - try - find 1 context - with Failure s -> [] -;; - - -let compare_goals proof goal1 goal2 = - 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 - CicUniv.empty_ugraph in - let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 - CicUniv.empty_ugraph in - let prop1 = - let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 - CicUniv.empty_ugraph in - if b then 0 else 1 - in - let prop2 = - let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 - CicUniv.empty_ugraph in - if b then 0 else 1 - in - prop1 - prop2 - - -let new_search_theorems f dbd proof goal depth sign = - let choices = f (proof,goal) - in - List.map - (function (subst,(proof, goallist)) -> - (* let goallist = reorder_goals dbd sign proof goallist in *) - let goallist = List.sort (compare_goals proof) goallist in - (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign))) - choices -;; - -exception NoOtherChoices;; - -let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals - universe - = - if depth = 0 then [] else - 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 - (* first of all we check if the goal has been already - inspected *) - assert (CicUtil.exists_meta goal metasenv); - let exitus = - try Hashtbl.find inspected_goals ty - with Not_found -> NotYetInspected in - let is_meta_closed = CicUtil.is_meta_closed ty in - begin - match exitus with - Yes (bo,_) -> - (* - debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); - debug_print (lazy (CicPp.ppterm ty)); - *) - let subst_in = - (* if we just apply the subtitution, the type - is irrelevant: we may use Implicit, since it will - be dropped *) - CicMetaSubst.apply_subst - [(goal,(ey, bo, Cic.Implicit None))] in - let (proof,_) = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst_in metasenv in - [(subst_in,(proof,[],sign))] - | No d when (d >= depth) -> - (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) - [] (* the empty list means no choices, i.e. failure *) - | No _ - | NotYetInspected -> - debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); - debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); - debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); - let sign, new_sign = - if is_meta_closed then - None, Some (MetadataConstraints.signature_of ty) - else sign,sign in (* maybe the union ? *) - let local_choices = - new_search_theorems - search_theorems_in_context dbd - proof goal (depth-1) new_sign in - let global_choices = - new_search_theorems - (fun status -> - List.map snd - (new_experimental_hint - ~dbd ~facts:facts ?signature:sign ~universe status)) - dbd proof goal (depth-1) new_sign in - let all_choices = - local_choices@global_choices in - let sorted_choices = - List.stable_sort - (fun (_, (_, goals1, _)) (_, (_, goals2, _)) -> - Pervasives.compare - (List.length goals1) (List.length goals2)) - all_choices in - (match (auto_new dbd width already_seen_goals universe sorted_choices) - with - [] -> - (* no proof has been found; we update the - hastable *) - (* if is_meta_closed then *) - Hashtbl.add inspected_goals ty (No depth); - [] - | (subst,(proof,[],sign))::tl1 -> - (* a proof for goal has been found: - in order to get the proof we apply subst to - Meta[goal] *) - if is_meta_closed then - begin - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable ey in - let meta_proof = - subst (Cic.Meta(goal,irl)) in - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); -(* - begin - let cty,_ = - CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph - in - if not (cty = ty) then - begin - debug_print (lazy ("ty = "^CicPp.ppterm ty)); - debug_print (lazy ("cty = "^CicPp.ppterm cty)); - assert false - end - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); - end; -*) - end; - (subst,(proof,[],sign))::tl1 - | _ -> assert false) - end - -and auto_new dbd width already_seen_goals universe = function - | [] -> [] - | (subst,(proof, goals, sign))::tl -> - let _,metasenv,_,_ = proof in - let goals'= - List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals + 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 - auto_new_aux dbd - width already_seen_goals universe ((subst,(proof, goals', sign))::tl) - -and auto_new_aux dbd width already_seen_goals universe = function - | [] -> [] - | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl - | (subst,(proof, (goal,0)::_, _))::tl -> - auto_new dbd width already_seen_goals universe tl - | (subst,(proof, goals, _))::tl when - (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 (_, 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 - with - [] -> auto_new dbd width already_seen_goals universe tl - | (local_subst,(proof,[],sign))::tl1 -> - let new_subst f t = f (subst t) in - let is_meta_closed = CicUtil.is_meta_closed ty in - let all_choices = - if is_meta_closed then - (new_subst local_subst,(proof,gtl,sign))::tl - else - let tl2 = - (List.map - (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1) - in - (new_subst local_subst,(proof,gtl,sign))::tl2@tl in - auto_new dbd width already_seen_goals universe all_choices - | _ -> assert false - ;; - -let default_depth = 5 -let default_width = 3 - -(* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) - () -= - let auto_tac dbd (proof,goal) = - 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 "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); - (proof,[]) - | _ -> assert false - in - ProofEngineTypes.mk_tactic (auto_tac dbd) + 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 ;; -*) - -(* -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 auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation - ?full ~(dbd:HMysql.dbd) () = - 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 full = match full with None -> false | Some _ -> true in - let paramodulation_ok = - match paramodulation with - | None -> false - | Some _ -> - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - full || (Inference.term_is_equality meta_goal) - in - if paramodulation_ok then ( - debug_print (lazy "USO PARAMODULATION..."); -(* try *) - Saturation.saturate dbd ~depth ~width ~full (proof, goal) -(* with ProofEngineTypes.Fail _ -> *) -(* normal_auto () *) - ) else - normal_auto () - in - ProofEngineTypes.mk_tactic (auto_tac dbd) +let auto_tac ~params ~dbd = + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) ;; + +let pp_proofterm = Equality.pp_proofterm;;