From: Andrea Asperti Date: Thu, 4 Nov 2004 10:22:18 +0000 (+0000) Subject: New version(s) of hint. One more stable (hint) and one more experimental X-Git-Tag: v_0_6_4_1~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7065757f75d899ef1751cfc3b30fa523fe903bf8;p=helm.git New version(s) of hint. One more stable (hint) and one more experimental experimental_hint. The latter uses apply_verbose, since it needs to get back the subproof of the goal, usually not returned by tactics. --- diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c007a1dea..bb5594a35 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -26,6 +26,7 @@ open Printf module Constr = MetadataConstraints +module PET = ProofEngineTypes let nonvar s = let len = String.length s in @@ -82,11 +83,12 @@ let filter_uris_forward ~dbd (main, constants) uris = in List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris -let filter_uris_backward ~dbd signature uris = +let filter_uris_backward ~dbd ~facts signature uris = let siguris = - List.map snd (MetadataConstraints.sigmatch ~dbd ~where:`Statement signature) + List.map snd + (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature) in - intersect uris siguris + intersect uris siguris let compare_goal_list proof goal1 goal2 = let _,metasenv,_,_ = proof in @@ -104,15 +106,16 @@ let compare_goal_list proof goal1 goal2 = in prop1 - prop2 -let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = +let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((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 -> (Constr.sigmatch ~dbd signature, signature) - | None -> (Constr.cmatch' ~dbd ty, Constr.signature_of ty) + | Some signature -> (Constr.sigmatch ~dbd ~facts signature, signature) + | None -> (Constr.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 let types_constants = match main with | None -> Constr.StringSet.empty @@ -123,6 +126,8 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in +prerr_endline "HYP SIGNATURE"; +Constr.StringSet.iter prerr_endline hyp_constants; let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in @@ -131,7 +136,7 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = prerr_endline "MetadataQuery: large sig, falling back to old method"; filter_uris_forward ~dbd (main, other_constants) uris end else - filter_uris_backward ~dbd (main, other_constants) uris + filter_uris_backward ~dbd ~facts (main, other_constants) uris in let rec aux = function | [] -> [] @@ -139,8 +144,10 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = (let status' = try let (proof, goal_list) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) + prerr_endline ("STO APPLICANDO " ^ uri); + PET.apply_tactic + (PrimitiveTactics.apply_tac + ~term:(CicUtil.term_of_uri uri)) status in let goal_list = @@ -152,7 +159,6 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = match status' with | None -> aux tl | Some status' -> - prerr_endline ("HO APPLICATO " ^ uri); status' :: aux tl) in List.stable_sort @@ -160,6 +166,76 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = Pervasives.compare (List.length goals1) (List.length goals2)) (aux uris) +(* experimental_hint is a version of hint for experimental + purposes. It uses auto_tac_verbose instead of auto tac. + Auto_tac verbose also returns a substitution - for the moment + as a function from cic to cic, to be changed into an association + list in the future -. This substitution is used to build a + hash table of the inspected goals with their associated proofs. + The cose is a cut and paste of the previous one: at the end + of the experimentation we shall make a choice. *) + +let experimental_hint + ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((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 -> + (Constr.sigmatch ~dbd ~facts signature, signature) + | None -> + (Constr.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 + let types_constants = + match main with + | None -> Constr.StringSet.empty + | Some (main, types) -> + List.fold_right Constr.StringSet.add (main :: types) + Constr.StringSet.empty + in + let hyp_constants = + Constr.StringSet.diff (signature_of_hypothesis context) types_constants + in +prerr_endline "HYP SIGNATURE"; +Constr.StringSet.iter prerr_endline hyp_constants; + let other_constants = Constr.StringSet.union sig_constants hyp_constants in + let uris = + let pow = 2 ** (Constr.StringSet.cardinal other_constants) in + if ((List.length uris < pow) or (pow <= 0)) + then begin + prerr_endline "MetadataQuery: large sig, falling back to old method"; + filter_uris_forward ~dbd (main, other_constants) uris + end else + filter_uris_backward ~dbd ~facts (main, other_constants) uris + in + let rec aux = function + | [] -> [] + | uri :: tl -> + (let status' = + try + let (subst,(proof, goal_list)) = + prerr_endline ("STO APPLICANDO" ^ uri); + PrimitiveTactics.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 elim ~dbd uri = let constraints = [`Rel [`MainConclusion None]; diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index f7a08d31f..b3b506de9 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -31,9 +31,20 @@ val locate: val hint: dbd:Mysql.dbd -> + ?facts:bool -> ?signature:MetadataConstraints.term_signature -> ProofEngineTypes.status -> - (string * (ProofEngineTypes.proof * ProofEngineTypes.goal list)) list + (string * + (ProofEngineTypes.proof * ProofEngineTypes.goal list)) list + +val experimental_hint: + dbd:Mysql.dbd -> + ?facts:bool -> + ?signature:MetadataConstraints.term_signature -> + ProofEngineTypes.status -> + (string * + ((Cic.term -> Cic.term) * + (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list val match_term: dbd:Mysql.dbd -> Cic.term -> string list