X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=0e86d8ccecf56b8a9005cec598b0e5d585cd875b;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=bb5594a35693f50917f86516419df44858e373b0;hpb=7065757f75d899ef1751cfc3b30fa523fe903bf8;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index bb5594a35..0e86d8cce 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -28,15 +28,31 @@ 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 @@ -44,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)) @@ -94,15 +144,27 @@ 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 @@ -126,8 +188,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?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; +(* 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 @@ -144,7 +205,7 @@ Constr.StringSet.iter prerr_endline hyp_constants; (let status' = try let (proof, goal_list) = - prerr_endline ("STO APPLICANDO " ^ uri); +(* prerr_endline ("STO APPLICANDO " ^ uri); *) PET.apply_tactic (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) @@ -198,8 +259,7 @@ let experimental_hint let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -prerr_endline "HYP SIGNATURE"; -Constr.StringSet.iter prerr_endline hyp_constants; +(* 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 @@ -216,7 +276,7 @@ Constr.StringSet.iter prerr_endline hyp_constants; (let status' = try let (subst,(proof, goal_list)) = - prerr_endline ("STO APPLICANDO" ^ uri); + (* prerr_endline ("STO APPLICANDO" ^ uri); *) PrimitiveTactics.apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status