X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=49472ed7204f084cb160ac9fdb46378eae334b48;hb=3605d724ae0b95e17e668b6e140c35ab19568bb2;hp=c007a1dea4c34496bc80f513776142533e6bfc23;hpb=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c007a1dea..49472ed72 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 @@ -43,13 +60,47 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) name = (fun cols -> match cols.(0) with Some s -> s | _ -> assert false)) let match_term ~(dbd:Mysql.dbd) ty = +(* prerr_endline (CicPp.ppterm ty); *) let metadata = MetadataExtractor.compute ~body:None ~ty in let constants_no = MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty) in + let full_card, diff = + if CicUtil.is_meta_closed ty then + Some (MetadataConstraints.Eq constants_no), None + else + let diff_no = + let (hyp_constants, concl_constants) = + (* collect different constants in hypotheses and conclusions *) + List.fold_left + (fun ((hyp, concl) as acc) metadata -> + match (metadata: MetadataTypes.metadata) with + | `Sort _ | `Rel _ -> acc + | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) + when not (List.mem uri concl) -> (hyp, uri :: concl) + | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) + when not (List.mem uri hyp) -> (uri :: hyp, concl) + | `Obj _ -> acc) + ([], []) + metadata + in + List.length hyp_constants - List.length concl_constants + in + let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in + let diff = + if MetadataExtractor.IntSet.equal concl_metas hyp_metas then + Some (MetadataConstraints.Eq diff_no) + else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then + Some (MetadataConstraints.Gt (diff_no - 1)) + else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then + Some (MetadataConstraints.Lt (diff_no + 1)) + else + None + in + None, diff + 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 ?diff constraints let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) @@ -82,37 +133,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 +188,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 +197,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 +205,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 +220,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 +227,118 @@ 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 close_with_types s metasenv context = + Constr.StringSet.fold + (fun e bag -> + let t = CicUtil.term_of_uri e in + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + in + Constr.StringSet.union bag (Constr.constants_of ty)) + s s + +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 = + if facts then + ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] + else + ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; + (* "cic:/Coq/Init/Logic/trans_eq.con"; *) + "cic:/Coq/Init/Logic/f_equal.con"; + "cic:/Coq/Init/Logic/f_equal2.con"; + "cic:/Coq/Init/Logic/f_equal3.con"] + 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 all_constants = + let hyp_and_sug = + Constr.StringSet.union + (signature_of_hypothesis context) + sig_constants + in + let main = + match main with + | None -> Constr.StringSet.empty + | Some (main,_) -> + let ty, _ = + CicTypeChecker.type_of_aux' + metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph + in + Constr.constants_of ty + in + Constr.StringSet.union main hyp_and_sug + in +(* Constr.StringSet.iter prerr_endline hyp_constants; *) + let all_constants_closed = close_with_types all_constants metasenv context in + let other_constants = + Constr.StringSet.diff all_constants_closed types_constants + in + prerr_endline "all_constants_closed"; + Constr.StringSet.iter prerr_endline all_constants_closed; + prerr_endline "other_constants"; + Constr.StringSet.iter prerr_endline other_constants; + 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]; @@ -168,5 +347,34 @@ let elim ~dbd uri = `Obj (uri,[`InHypothesis]); ] in - MetadataConstraints.at_least ~dbd constraints + MetadataConstraints.at_least ~rating:`Hits ~dbd constraints + + +let fill_with_dummy_constants t = + let rec aux i = + function + Cic.Lambda (n,s,t) -> + let dummy_uri = + UriManager.uri_of_string ("dummy_"^(string_of_int i)) in + (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) + | t -> t + in aux 0 t + +let instance ~dbd t = + let t' = fill_with_dummy_constants t in + let metadata = MetadataExtractor.compute ~body:None ~ty:t' in + let no_concl = MetadataDb.count_distinct `Conclusion metadata in + let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in + let no_full = MetadataDb.count_distinct `Statement metadata in + let is_dummy = + function + `Obj(s, _) -> (String.sub s 0 5) = "dummy" + | _ -> false in + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints +