open Printf
open MetadataTypes
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
+
let critical_value = 7
let just_factor = 1
in
((n+2), from, where)
-let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+let exec dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) =
let from = String.concat ", " from in
let where = String.concat " and " where in
let query =
and table0.source = hits.source order by hits.no desc")
from where
in
- (* prerr_endline query; *)
- let result = HMysql.exec dbd query in
- HMysql.map result
- (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-
+ (* debug_print (lazy query); *)
+ let result = HSql.exec dbtype dbd query in
+ HSql.map result
+ ~f:(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 dbtype ~(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 (n,from,where) =
add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
in
- exec ~dbd ?rating (n,from,where)
+ exec dbtype ~dbd ?rating (n,from,where)
;;
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
- (at_least
- ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
- (at_least
- ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
+ at_least
+ HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.User ~dbd ?concl_card ?full_card ?diff ?rating
+ (current_tables ()) metadata
+
else
at_least
- ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata
+ HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
(** Prefix handling *)
merge n (inspect_conclusion n s) (inspect_conclusion n t)
| Cic.Lambda (_, s, t) ->
merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.LetIn (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
+ | Cic.LetIn (_, s, ty, t) ->
+ merge n (inspect_conclusion n s)
+ (merge n (inspect_conclusion n ty) (inspect_conclusion n t))
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
add_root (n-1) u l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
Some uri, SetSet.empty
| Cic.Cast (t, _) -> inspect_term n t
| Cic.Prod (_, _, t) -> inspect_term n t
- | Cic.LetIn (_, _, t) -> inspect_term n t
+ | Cic.LetIn (_, _, _, t) -> inspect_term n t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
let childunion = inspect_children (n-1) l in
Some u, childunion
| Cic.Const (u,exp_named_subst) ->
UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
+ let rec projections_of uris =
+ List.flatten
+ (List.map
+ (fun uri ->
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+ projections_of (CicUtil.projections_of_record o uri))
+ uris)
+ in
let uri = UriManager.uri_of_uriref u t None in
- UriManagerSet.singleton uri
+ List.fold_right UriManagerSet.add
+ (projections_of [u]) (UriManagerSet.singleton uri)
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
let uri = UriManager.uri_of_uriref u t (Some c) in
- UriManagerSet.singleton uri
+ UriManagerSet.singleton uri
| Cic.Cast (t, _) -> signature_concl t
| Cic.Prod (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.Lambda (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
- | Cic.LetIn (_, s, t) ->
- UriManagerSet.union (signature_concl s) (signature_concl t)
+ | Cic.LetIn (_, s, ty, t) ->
+ UriManagerSet.union (signature_concl s)
+ (UriManagerSet.union (signature_concl ty) (signature_concl t))
| Cic.Appl l -> add l
| Cic.MutCase _
| Cic.Fix _
let rec signature_of = function
| Cic.Cast (t, _) -> signature_of t
| Cic.Prod (_, _, t) -> signature_of t
- | Cic.LetIn (_, _, t) -> signature_of t
+ | Cic.LetIn (_, _, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
Some (u, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
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.mainconcl_pos; MetadataTypes.inconcl_pos;
MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
in
- let query =
- let pos_predicate =
- String.concat " OR "
- (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
- in
- sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
- "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
- (MetadataTypes.obj_tbl ()) uri pos_predicate
- MetadataTypes.library_obj_tbl uri pos_predicate
-
+ let pos_predicate =
+ String.concat " OR "
+ (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+ in
+ let query tbl =
+ sprintf "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)"
+ tbl uri pos_predicate
+ in
+ let db = [
+ HSql.Library, MetadataTypes.library_obj_tbl;
+ HSql.Legacy, MetadataTypes.library_obj_tbl;
+ HSql.User, MetadataTypes.obj_tbl ()]
in
- let result = HMysql.exec dbd query in
let set = ref UriManagerSet.empty in
- HMysql.iter result
- (fun col ->
- match col.(0) with
- | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
- | _ -> assert false);
+ List.iter
+ (fun (dbtype, table) ->
+ let result = HSql.exec dbtype dbd (query table) in
+ HSql.iter result
+ (fun col ->
+ match col.(0) with
+ | Some uri ->
+ set := UriManagerSet.add (UriManager.uri_of_string uri) !set
+ | _ -> assert false))
+ db;
!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 =
| Some (main, types) -> Some main,types
in
let constants_no = UriManagerSet.cardinal constants in
- (* prerr_endline (("constants_no: ")^(string_of_int constants_no)); *)
+ (* debug_print (lazy (("constants_no: ")^(string_of_int constants_no))); *)
if (constants_no > critical_value) then
let subsets =
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 _ = debug_print (lazy (("subsets: ")^
+ (string_of_int (List.length subsets)))) in *)
+ 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);
+ debug_print (lazy ("critical_value exceded..." ^ string_of_int constants_no));
let all_constants =
let all = match main with None -> types | Some m -> m::types in
List.fold_right UriManagerSet.add all constants
in
compute_with_only ~dbd ~where main subsets all_constants
else
+ (debug_print (lazy ("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
+ debug_print (lazy "fine1");
+ compute_exactly ~dbd ~facts ~where main subsets)
(* match query wrappers *)
projects / helm.git / blobdiff