From 6e986001aac7cc63b0e7d13447caae3729e0f833 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Nov 2004 10:15:10 +0000 Subject: [PATCH] Added a new boolean parameter "facts" (default=false) to most of the methods. The idea is that when facts=true search should be restricted to facts (theorems without hypothesis). To be used at the maximum depth of automatic tactcis. --- helm/ocaml/metadata/metadataConstraints.ml | 54 +++++++++++++-------- helm/ocaml/metadata/metadataConstraints.mli | 8 +-- 2 files changed, 39 insertions(+), 23 deletions(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index f7707f90f..2ebd46c2a 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -25,8 +25,8 @@ open Printf -let critical_value = 6 -let just_factor = 3 +let critical_value = 7 +let just_factor = 4 module StringSet = Set.Make (String) module SetSet = Set.Make (StringSet) @@ -403,6 +403,8 @@ let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u = (* Special handling of equality. The problem is filtering out theorems just * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really * ad-hoc, no better solution found at the moment *) +let myspeciallist_of_facts = + [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] let myspeciallist = [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; 0,"cic:/Coq/Init/Logic/sym_eq.con"; @@ -411,12 +413,14 @@ let myspeciallist = 0,"cic:/Coq/Init/Logic/f_equal2.con"; 0,"cic:/Coq/Init/Logic/f_equal3.con"] -let compute_exactly ~(dbd:Mysql.dbd) where main prefixes = + +let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes = List.concat (List.map (fun (m,s) -> - if (m = 0) then - myspeciallist + if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then + (if facts then myspeciallist_of_facts + else myspeciallist) else let res = let must = must_of_prefix ~where main s in @@ -428,8 +432,9 @@ let compute_exactly ~(dbd:Mysql.dbd) where main prefixes = prefixes) (* critical value reached, fallback to "only" constraints *) -let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main - prefixes constants + +let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) + main prefixes constants = let max_prefix_length = match prefixes with @@ -457,18 +462,19 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main maximal_prefixes) in List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in - let equal_to = compute_exactly ~dbd where main prefixes in + let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in greater_than @ equal_to (* real match query implementation *) -let cmatch ~(dbd:Mysql.dbd) t = + +let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = let (main, constants) = signature_of t in match main with | None -> [] | Some (main, types) -> (* the type of eq is not counted in constants_no *) let types_no = List.length types in - let constants_no = StringSet.cardinal constants + types_no in + let constants_no = StringSet.cardinal constants in if (constants_no > critical_value) then let prefixes = prefixes just_factor t in (match prefixes with @@ -476,26 +482,31 @@ let cmatch ~(dbd:Mysql.dbd) t = let all_constants = List.fold_right StringSet.add types (StringSet.add main constants) in - compute_with_only ~dbd main all_concl all_constants + compute_with_only ~dbd ~facts main all_concl all_constants | _, _ -> []) else (* in this case we compute all prefixes, and we do not need to apply the only constraints *) let prefixes = - if constants_no = types_no then - Some main, [0, []; types_no, types] + if constants_no = 0 then + (if types_no = 0 then + Some main, [0, []] + else + Some main, [0, []; types_no, types]) else - prefixes constants_no t + prefixes (constants_no+types_no) 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) + all_concl) *) | _, _ -> []) let power_upto upto consts = @@ -516,7 +527,8 @@ let power consts = type where = [ `Conclusion | `Statement ] -let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) = +let sigmatch ~(dbd:Mysql.dbd) + ?(facts=false) ?(where = `Conclusion) (main, constants) = match main with None -> [] | Some (main, types) -> @@ -537,15 +549,17 @@ let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) = let types_no = List.length types in (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets in - compute_exactly ~dbd where main subsets + compute_exactly ~dbd ~facts ~where main subsets (* match query wrappers *) -let cmatch' = cmatch -let cmatch ~dbd term = + +let cmatch'= cmatch + +let cmatch ~dbd ?(facts=false) term = List.map snd (List.sort (fun x y -> Pervasives.compare (fst y) (fst x)) - (cmatch' ~dbd term)) + (cmatch' ~dbd ~facts term)) let constants_of = signature_concl diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index 3de99469c..72f808efb 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -35,18 +35,20 @@ type term_signature = (string * string list) option * StringSet.t (** @return sorted list of theorem URIs, first URIs in the least have higher * relevance *) -val cmatch: dbd:Mysql.dbd -> Cic.term -> string list +val cmatch: dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> string list (** as cmatch, but returned list is not sorted but rather tagged with * relevance information: higher the tag, higher the relevance *) -val cmatch': dbd:Mysql.dbd -> Cic.term -> (int * string) list +val cmatch': dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> (int * string) list type where = [ `Conclusion | `Statement ] (** signature matching extent *) (** @param where defaults to `Conclusion *) val sigmatch: dbd:Mysql.dbd -> - ?where:where -> term_signature -> + ?facts:bool -> + ?where:where -> + term_signature -> (int * string) list (** {2 Constraint engine} *) -- 2.39.2