X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=e8d034a3298a9630fa0c8b1efe693579a1045ed2;hb=115915f23df4f56832d68b2f6b5b80c5afe019fc;hp=7aabf9f3378321e8de1e1737d17afef25d421329;hpb=6d7654db91570337a96c8f8129ef061df08f8b80;p=helm.git diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 7aabf9f33..e8d034a32 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -46,7 +46,7 @@ type exitus = No of int | Yes of Cic.term * int | NotYetInspected - + let inspected_goals = Hashtbl.create 503;; let search_theorems_in_context status = @@ -93,17 +93,17 @@ let compare_goals proof goal1 goal2 = 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 + CicUniv.empty_ugraph in let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 - CicUniv.empty_ugraph in + CicUniv.empty_ugraph in let prop1 = let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 - CicUniv.empty_ugraph in + 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 + CicUniv.empty_ugraph in if b then 0 else 1 in prop1 - prop2 @@ -139,90 +139,90 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals let is_meta_closed = CicUtil.is_meta_closed ty in begin match exitus with - Yes (bo,_) -> + Yes (bo,_) -> (* debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); - debug_print (lazy (CicPp.ppterm ty)); + 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))] + 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)); + (* 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; + 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; + (subst,(proof,[],sign))::tl1 + | _ -> assert false) end and auto_new dbd width already_seen_goals universe = function @@ -232,7 +232,7 @@ and auto_new dbd width already_seen_goals universe = function let goals'= List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals in - auto_new_aux dbd + 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 @@ -247,30 +247,29 @@ and auto_new_aux dbd width already_seen_goals universe = function 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 + (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 + [] -> 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_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof,goal) = @@ -281,74 +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); - (proof,[]) + 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 - 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 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 term_is_equality = ref - (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -*) +let string params name default = + try List.assoc name params with + | Not_found -> default +;; -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 || (Equality.term_is_equality meta_goal) - in - if paramodulation_ok then ( - debug_print (lazy "USO PARAMODULATION..."); -(* try *) - try - Saturation.saturate dbd ~depth ~width ~full (proof, goal) - with exn -> - prerr_endline (Saturation.get_stats ()); - raise exn - -(* with ProofEngineTypes.Fail _ -> *) -(* normal_auto () *) - ) else - normal_auto () - in - ProofEngineTypes.mk_tactic (auto_tac dbd) +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) ~universe (proof, goal) = + (* argument parsing *) + 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) + +let auto_tac ~params ~dbd ~universe= + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe) ;; + +let pp_proofterm = Equality.pp_proofterm;;