From: Claudio Sacerdoti Coen Date: Fri, 24 Jun 2005 15:00:05 +0000 (+0000) Subject: New implementation of experimental_hint/auto (called new_experimental_hint) that X-Git-Tag: INDEXING_NO_PROOFS~72 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9eee519f40a2cf6dfaaaa0c5e37d23ad8748552c;p=helm.git New implementation of experimental_hint/auto (called new_experimental_hint) that dramatically cuts down the total time in certain cases. The idea of new_experimental_hint is to take in input the universe (the list of uris that occur in the signature) and to prune the results using the universe in place of the signature. Thus in place of doing a lot of sigmatches a sigmatch is done just once at the very beginning. NOTE: to reduce the size of the universe the empty set of constraints is not considered. --- diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 74b15015c..d18663fad 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -350,7 +350,9 @@ and signature_concl = | Cic.Meta _ | Cic.Sort _ | Cic.Implicit _ -> UriManagerSet.empty - | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty + | Cic.Var (u,exp_named_subst) -> + (*CSC: TODO if the var has a body it must be processed *) + UriManagerSet.empty | Cic.Const (u,exp_named_subst) -> UriManagerSet.singleton u | Cic.MutInd (u, t, exp_named_subst) -> @@ -421,8 +423,12 @@ let must_of_prefix ?(where = `Conclusion) m s = | `Conclusion -> [`InConclusion] | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None] in + let positions = + if m = None then `MainConclusion None :: positions else positions in let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in - `Obj (m, [`MainConclusion None]) :: s' + match m with + None -> s' + | Some m -> `Obj (m, [`MainConclusion None]) :: s' let escape = Str.global_replace (Str.regexp_string "\'") "\\'" @@ -477,17 +483,29 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes = List.concat (List.map (fun (m,s) -> - if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI)))) then + let is_eq,card = + match main with + None -> false,m + | Some main -> + (m = 0 && + UriManager.eq main + (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI))), + m+1 + in + if m = 0 && is_eq then (if facts then myspeciallist_of_facts else myspeciallist) else let res = + (* this gets rid of the ~750 objects of type Set/Prop/Type *) + if card = 0 then [] + else let must = must_of_prefix ~where main s in match where with - | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must - | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must + | `Conclusion -> at_least ~dbd ~concl_card:(Eq card) must + | `Statement -> at_least ~dbd ~full_card:(Eq card) must in - List.map (fun uri -> (m, uri)) res) + List.map (fun uri -> (card, uri)) res) prefixes) (* critical value reached, fallback to "only" constraints *) @@ -510,14 +528,15 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) union (List.map (fun (m,s) -> + let card = if main = None then m else m + 1 in let must = must_of_prefix ~where main s in (let res = match where with - | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must - | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must + | `Conclusion -> at_least ~dbd ~concl_card:(Gt card) must + | `Statement -> at_least ~dbd ~full_card:(Gt card) must in (* we tag the uri with m+1, for sorting purposes *) - List.map (fun uri -> (m+1, uri)) res)) + List.map (fun uri -> (card, uri)) res)) maximal_prefixes) in List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in @@ -541,7 +560,7 @@ let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = let all_constants = List.fold_right UriManagerSet.add types (UriManagerSet.add main constants) in - compute_with_only ~dbd ~facts main all_concl all_constants + compute_with_only ~dbd ~facts (Some main) all_concl all_constants | _, _ -> []) else (* in this case we compute all prefixes, and we do not need @@ -557,15 +576,7 @@ let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = in (match prefixes with Some main, all_concl -> - compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl -(* - List.concat - (List.map - (fun (m,s) -> - let must = must_of_prefix ~where:`Conclusion main s in - let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in - List.map (fun uri -> (m, uri)) res) - all_concl) *) + compute_exactly ~dbd ~facts ~where:`Conclusion (Some main) all_concl | _, _ -> []) let power_upto upto consts = @@ -586,31 +597,35 @@ let power consts = type where = [ `Conclusion | `Statement ] -let sigmatch ~(dbd:Mysql.dbd) - ?(facts=false) ?(where = `Conclusion) (main, constants) = - match main with - None -> [] - | Some (main, types) -> - let constants_no = UriManagerSet.cardinal constants in - if (constants_no > critical_value) then - let subsets = - let subsets = power_upto just_factor constants in - let types_no = List.length types in - List.map (function (n,l) -> (n+types_no,types@l)) subsets - in - let all_constants = - List.fold_right UriManagerSet.add types (UriManagerSet.add main constants) - in - compute_with_only ~dbd ~where main subsets all_constants - else - let subsets = - let subsets = power constants in - let types_no = List.length types in - if types_no > 0 then - (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets - else subsets - in - compute_exactly ~dbd ~facts ~where main subsets +let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) + (main, constants) += + let main,types = + match main with + None -> None,[] + | Some (main, types) -> Some main,types + in + let constants_no = UriManagerSet.cardinal constants in + if (constants_no > critical_value) then + let subsets = + let subsets = power_upto just_factor constants in + let types_no = List.length types in + List.map (function (n,l) -> (n+types_no,types@l)) subsets + in + let all_constants = + let all = match main with None -> types | Some m -> m::types in + List.fold_right UriManagerSet.add all constants + in + compute_with_only ~dbd ~where main subsets all_constants + else + let subsets = + let subsets = power constants in + let types_no = List.length types in + if types_no > 0 then + (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets + else subsets + in + compute_exactly ~dbd ~facts ~where main subsets (* match query wrappers *) diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 13dac415f..c7cdc97ac 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -27,10 +27,10 @@ (* let debug_print = fun _ -> () *) -let experimental_hint = - let profile = CicUtil.profile "experimental_hint" in - fun ~dbd ~facts ?signature status -> - profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status +let new_experimental_hint = + let profile = CicUtil.profile "new_experimental_hint" in + fun ~dbd ~facts ?signature ~universe status -> + profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status let search_theorems_in_context status = let (proof, goal) = status in @@ -246,6 +246,7 @@ let is_in_metasenv goal metasenv = with _ -> false 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 @@ -296,8 +297,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals new_search_theorems (fun status -> List.map snd - (experimental_hint - ~dbd ~facts:facts ?signature:sign status)) + (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 @@ -307,7 +308,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals Pervasives.compare (List.length goals1) (List.length goals2)) all_choices in - (match (auto_new dbd width already_seen_goals sorted_choices) + (match (auto_new dbd width already_seen_goals universe sorted_choices) with [] -> (* no proof has been found; we update the @@ -347,7 +348,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals | _ -> assert false) end -and auto_new dbd width already_seen_goals = function +and auto_new dbd width already_seen_goals universe = function [] -> [] | (subst,(proof, goals, sign))::tl -> let _,metasenv,_,_ = proof in @@ -358,24 +359,24 @@ and auto_new dbd width already_seen_goals = function true with _ -> false in let goals'= List.filter is_in_metasenv goals in - auto_new_aux dbd width already_seen_goals + auto_new_aux dbd width already_seen_goals universe ((subst,(proof, goals', sign))::tl) -and auto_new_aux dbd width already_seen_goals = function +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 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 tl + 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) + (width - (List.length gtl)) sign already_seen_goals) universe with - [] -> auto_new dbd width already_seen_goals tl + [] -> 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 @@ -388,7 +389,7 @@ and auto_new_aux dbd width already_seen_goals = function (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 all_choices + auto_new dbd width already_seen_goals universe all_choices | _ -> assert false ;; @@ -399,10 +400,11 @@ let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = let auto_tac dbd (proof,goal) = + let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in Hashtbl.clear inspected_goals; debug_print "Entro in Auto"; let id t = t in - match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with + match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with [] -> debug_print("Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index ed4418dd2..fab96475c 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -121,6 +121,15 @@ let intersect uris siguris = let inter = Constr.UriManagerSet.inter set1 set2 in List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris +let at_most = + let profiler = CicUtil.profile "at_most" in + fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri + +let sigmatch = + let profiler = CicUtil.profile "sigmatch" in + fun ~dbd ~facts ~where signature -> + profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature + let filter_uris_forward ~dbd (main, constants) uris = let main_uris = match main with @@ -130,12 +139,12 @@ let filter_uris_forward ~dbd (main, constants) uris = let full_signature = List.fold_right Constr.UriManagerSet.add main_uris constants in - List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris + List.filter (at_most ~dbd ~where:`Statement full_signature) uris let filter_uris_backward ~dbd ~facts signature uris = let siguris = List.map snd - (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature) + (sigmatch ~dbd ~facts ~where:`Statement signature) in intersect uris siguris @@ -245,6 +254,36 @@ let close_with_types s metasenv context = Constr.UriManagerSet.union bag (Constr.constants_of ty)) s s +let apply_tac_verbose = + let profiler = CicUtil.profile "apply_tac_verbose" in + fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status + +let sigmatch = + let profiler = CicUtil.profile "sigmatch" in + fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature + +let cmatch' = + let profiler = CicUtil.profile "cmatch'" in + fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature + +let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) = + let (_, metasenv, _, _) = proof in + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let main, sig_constants = Constr.signature_of ty in + let set = signature_of_hypothesis context in + let set = + match main with + None -> set + | Some (main,l) -> + List.fold_right Constr.UriManagerSet.add (main::l) set in + let set = Constr.UriManagerSet.union set sig_constants in + let all_constants_closed = close_with_types set metasenv context in + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in + let uris = List.filter nonvar (List.map snd uris) in + let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + uris + let experimental_hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in @@ -252,9 +291,9 @@ let experimental_hint let (uris, (main, sig_constants)) = match signature with | Some signature -> - (Constr.sigmatch ~dbd ~facts signature, signature) + (sigmatch ~dbd ~facts signature, signature) | None -> - (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty) + (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in @@ -308,7 +347,55 @@ let experimental_hint try let (subst,(proof, goal_list)) = (* debug_print ("STO APPLICANDO" ^ uri); *) - PrimitiveTactics.apply_tac_verbose + apply_tac_verbose + ~term:(CicUtil.term_of_uri uri) + status + in + let goal_list = + List.stable_sort (compare_goal_list proof) goal_list + in + Some (uri, (subst,(proof, goal_list))) + with ProofEngineTypes.Fail _ -> None + in + match status' with + | None -> aux tl + | Some status' -> status' :: aux tl) + in + List.stable_sort + (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) -> + Pervasives.compare (List.length goals1) (List.length goals2)) + (aux uris) + +let new_experimental_hint + ~(dbd:Mysql.dbd) ?(facts=false) ?signature ~universe + ((proof, goal) as status) += + let (_, metasenv, _, _) = proof in + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let (uris, (main, sig_constants)) = + match signature with + | Some signature -> + (sigmatch ~dbd ~facts signature, signature) + | None -> + (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in + let universe = + List.fold_left + (fun res u -> Constr.UriManagerSet.add u res) + Constr.UriManagerSet.empty universe in + let uris = + List.fold_left + (fun res (_,u) -> Constr.UriManagerSet.add u res) + Constr.UriManagerSet.empty uris in + let uris = Constr.UriManagerSet.inter uris universe in + let uris = Constr.UriManagerSet.elements uris in + let rec aux = function + | [] -> [] + | uri :: tl -> + (let status' = + try + let (subst,(proof, goal_list)) = + (* debug_print ("STO APPLICANDO" ^ uri); *) + apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status in diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index e8f81a438..36e0e7497 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -27,6 +27,10 @@ * false * @param pat shell like pattern matching over object names, a string where "*" * is interpreted as 0 or more characters and "?" as exactly one character *) + +val signature_of_goal: + dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + val locate: dbd:Mysql.dbd -> ?vars:bool -> string -> UriManager.uri list @@ -48,6 +52,16 @@ val experimental_hint: ((Cic.term -> Cic.term) * (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list +val new_experimental_hint: + dbd:Mysql.dbd -> + ?facts:bool -> + ?signature:MetadataConstraints.term_signature -> + universe:UriManager.uri list -> + ProofEngineTypes.status -> + (UriManager.uri * + ((Cic.term -> Cic.term) * + (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list + val match_term: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list (** @param string is an uri *)