in
((n+2), from, where)
-let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+let exec ~(dbd:HSql.dbd) ?rating (n,from,where) =
let from = String.concat ", " from in
let where = String.concat " and " where in
let query =
from where
in
(* prerr_endline query; *)
- let result = HMysql.exec dbd query in
- HMysql.map result
+ let result = HSql.exec dbd query in
+ HSql.map result
(fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
(metadata: MetadataTypes.constr list)
=
let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
;;
let at_least
- ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
+ ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating
(metadata: MetadataTypes.constr list)
=
if are_tables_ownerized () then
let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
-let get_constants (dbd:HMysql.dbd) ~where uri =
+let get_constants (dbd:HSql.dbd) ~where uri =
let uri = escape (UriManager.string_of_uri uri) in
let positions =
match where with
MetadataTypes.library_obj_tbl uri pos_predicate
in
- let result = HMysql.exec dbd query in
+ let result = HSql.exec dbd query in
let set = ref UriManagerSet.empty in
- HMysql.iter result
+ HSql.iter result
(fun col ->
match col.(0) with
| Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
| _ -> assert false);
!set
-let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u =
let inconcl = get_constants dbd ~where u in
UriManagerSet.subset inconcl only
0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
-let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HSql.dbd) ?(facts=false) ~where main prefixes =
List.concat
(List.map
(fun (m,s) ->
(* critical value reached, fallback to "only" constraints *)
-let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let compute_with_only ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
main prefixes constants
=
let max_prefix_length =
maximal_prefixes)
in
(* Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *)
+(*
List.filter (function (_,uri) ->
-(* prerr_endline ("W" ^UriManager.string_of_uri uri); *)
- at_most ~dbd ~where constants uri) all
+ at_most ~dbd ~where constants uri)
+*)
+ all
in
let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
greater_than @ equal_to
(* real match query implementation *)
-let cmatch ~(dbd:HMysql.dbd) ?(facts=false) t =
+let cmatch ~(dbd:HSql.dbd) ?(facts=false) t =
let (main, constants) = signature_of t in
match main with
| None -> []
type where = [ `Conclusion | `Statement ]
-let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
(main, constants)
=
let main,types =
let subsets = power_upto just_factor constants in
(* let _ = prerr_endline (("subsets: ")^
(string_of_int (List.length subsets))) in *)
- let types_no = List.length types in
- List.map (function (n,l) -> (n+types_no,types@l)) subsets
+ let types_no = List.length types in
+ if types_no > 0 then
+ List.map (function (n,l) -> (n+types_no,types@l)) subsets
+ else subsets
in
prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
let all_constants =
in
compute_with_only ~dbd ~where main subsets all_constants
else
+ (prerr_endline ("all subsets..." ^ string_of_int constants_no);
let subsets =
let subsets = power constants in
let types_no = List.length types in
if types_no > 0 then
(0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
else subsets
- in
- compute_exactly ~dbd ~facts ~where main subsets
+ in
+ prerr_endline "fine1";
+ compute_exactly ~dbd ~facts ~where main subsets)
(* match query wrappers *)