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
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))
let hyp_constants =
Constr.StringSet.diff (signature_of_hypothesis context) types_constants
in
-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
let hyp_constants =
Constr.StringSet.diff (signature_of_hypothesis context) types_constants
in
-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