X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=8dcbcd08abd3e3d9d0d585c4aa390c46223e4e89;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=c007a1dea4c34496bc80f513776142533e6bfc23;hpb=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c007a1dea..8dcbcd08a 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -26,16 +26,33 @@ open Printf module Constr = MetadataConstraints +module PET = ProofEngineTypes + + (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for + * the "like" operator (which uses '%' and '_'). Does not support escaping. *) +let sqlpat_of_shellglob = + let star_RE, qmark_RE, percent_RE, uscore_RE = + Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" + in + fun shellglob -> + Pcre.replace ~rex:star_RE ~templ:"%" + (Pcre.replace ~rex:qmark_RE ~templ:"_" + (Pcre.replace ~rex:percent_RE ~templ:"\\%" + (Pcre.replace ~rex:uscore_RE ~templ:"\\_" + shellglob))) let nonvar s = let len = String.length s in let suffix = String.sub s (len-4) 4 in not (suffix = ".var") -let locate ~(dbd:Mysql.dbd) ?(vars = false) name = +let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = + let sql_pat = sqlpat_of_shellglob pat in let query = - sprintf "SELECT source FROM %s WHERE value = \"%s\"" - MetadataTypes.name_tbl name + sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^ + "SELECT source FROM %s WHERE value LIKE \"%s\"") + (MetadataTypes.name_tbl ()) sql_pat + MetadataTypes.library_name_tbl sql_pat in let result = Mysql.exec dbd query in List.filter nonvar @@ -47,9 +64,16 @@ let match_term ~(dbd:Mysql.dbd) ty = let constants_no = MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty) in + let full_card = + if CicUtil.is_meta_closed ty then + Some (MetadataConstraints.Eq constants_no) + else + None (* we already require a set of constants to appear, this additional + constraints is useless *) +(* MetadataConstraints.Gt (constants_no - 1) *) + in let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no) - constraints + Constr.at_least ~dbd ?full_card constraints let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) @@ -82,37 +106,51 @@ 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 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 in - let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 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 = - if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0 - else 1 + 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 = - if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0 - else 1 + 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 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 +161,7 @@ let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) = let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in +(* 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 +170,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 +178,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 +193,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 +200,75 @@ 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 +(* 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];