X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=1ba1dd912495f63801c7ffbf90b0d785e93e883e;hb=679f6296c9a979213425104fa606809d9f1e3bad;hp=9f54c6cecc15764d460d307281f3fcf262749211;hpb=36eecd95ced29b1925913c8cfaf804c472599e66;p=helm.git diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 9f54c6cec..1ba1dd912 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,23 +247,23 @@ 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 @@ -281,14 +281,14 @@ 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 "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 "AUTO_TAC HA FINITO"); + let _,_,p,_ = proof in + debug_print (lazy (CicPp.ppterm p)); Printf.printf "tempo: %.9f\n" (t2 -. t1); - (proof,[]) + (proof,[]) | _ -> assert false in ProofEngineTypes.mk_tactic (auto_tac dbd) @@ -304,8 +304,35 @@ 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 bool name params = + try let _ = List.assoc name params in true with + | Not_found -> false +;; + +let string name params = + try List.assoc name params with + | Not_found -> "" +;; + +let int name params = + try int_of_string (List.assoc name params) with + | Not_found -> default_depth + | Failure _ -> + raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) +;; + +let auto_tac ~params ~(dbd:HMysql.dbd) = + (* 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 what = string "what" params in + let other = string "other" 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 @@ -317,24 +344,20 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] with [] -> debug_print(lazy "Auto failed"); - raise (ProofEngineTypes.Fail (lazy "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)); + 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,[]) + (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) + 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..."); @@ -352,7 +375,11 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ) else normal_auto () in - ProofEngineTypes.mk_tactic (auto_tac dbd) + match superposition with + | true -> + ProofEngineTypes.mk_tactic + (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate) + | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) ;; (********************** applyS *******************) @@ -368,37 +395,37 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' 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) + 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 ~paramodulation:"qualsiasi" ~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)) + 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'',g1) + in proof'', - (*CSC: Brrrr.... *) - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:(let _,m,_,_ = proof'' in m) + (*CSC: Brrrr.... *) + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:(let _,m,_,_ = proof'' in m) | _ -> assert false let rec count_prods context ty =