open MetadataTypes
let critical_value = 7
-let just_factor = 4
+let just_factor = 3
module UriManagerSet = UriManager.UriSet
module SetSet = Set.Make (UriManagerSet)
in
((n+2), from, where)
-let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
+let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
let from = String.concat ", " from in
let where = String.concat " and " where in
let query =
match rating with
- | None -> sprintf "select table0.source from %s where %s" from where
+ | None -> sprintf "select distinct table0.source from %s where %s" from where
| Some `Hits ->
sprintf
- ("select table0.source from %s, hits where %s
+ ("select distinct table0.source from %s, hits where %s
and table0.source = hits.source order by hits.no desc")
from where
in
-(* prerr_endline query; *)
- let result = Mysql.exec dbd query in
- Mysql.map result
+ (* 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)
-let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
(metadata: MetadataTypes.constr list)
=
let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables
exec ~dbd ?rating (n,from,where)
let at_least
- ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
+ ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
(metadata: MetadataTypes.constr list)
=
if are_tables_ownerized () then
in
filter_by_card n res
-let string_of_uriref i =
- UriManager.uri_of_string (UriManager.string_of_uriref i)
-
let rec inspect_children n childs =
List.fold_left
(fun res term -> merge n (inspect_conclusion n term) res)
SetSet.singleton (UriManagerSet.singleton u)
| Cic.MutInd (u, t, exp_named_subst) ->
SetSet.singleton (UriManagerSet.singleton
- (string_of_uriref (u, [t])))
+ (UriManager.uri_of_uriref u t None))
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
SetSet.singleton (UriManagerSet.singleton
- (string_of_uriref (u, [t; c])))
+ (UriManager.uri_of_uriref u t (Some c)))
| Cic.Cast (t, _) -> inspect_conclusion n t
| Cic.Prod (_, 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.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = u in
- add_root (n-1) suri l
+ add_root (n-1) u l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t]) in
- add_root (n-1) suri l
+ let uri = UriManager.uri_of_uriref u t None in
+ add_root (n-1) uri l
| Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t; c]) in
+ let suri = UriManager.uri_of_uriref u t (Some c) in
add_root (n-1) suri l
| Cic.Appl l ->
SetSet.empty
| Cic.Const (u,exp_named_subst) ->
Some u, SetSet.empty
| Cic.MutInd (u, t, exp_named_subst) ->
- let uri = string_of_uriref (u, [t]) in
+ let uri = UriManager.uri_of_uriref u t None in
Some uri, SetSet.empty
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let uri = string_of_uriref (u, [t; c]) in
+ let uri = UriManager.uri_of_uriref u t (Some c) in
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.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = u in
let childunion = inspect_children (n-1) l in
- Some suri, childunion
+ Some u, childunion
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t]) in
+ let suri = UriManager.uri_of_uriref u t None in
if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
(* equality is handled in a special way: in particular,
the type, if defined, is always added to the prefix,
and n is not decremented - it should have been n-2 *)
match l with
Cic.Const (u1,exp_named_subst1)::l1 ->
- let suri1 = u1 in
- let inconcl = add_root (n-1) suri1 l1 in
+ let inconcl = add_root (n-1) u1 l1 in
Some suri, inconcl
| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
- let suri1 = string_of_uriref (u1, [t1]) in
+ let suri1 = UriManager.uri_of_uriref u1 t1 None in
let inconcl = add_root (n-1) suri1 l1 in
Some suri, inconcl
| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
- let suri1 = string_of_uriref (u1, [t1; c1]) in
+ let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
let inconcl = add_root (n-1) suri1 l1 in
Some suri, inconcl
| _ :: _ -> Some suri, SetSet.empty
let childunion = inspect_children (n-1) l in
Some suri, childunion
| Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t; c]) in
+ let suri = UriManager.uri_of_uriref u t(Some c) in
let childunion = inspect_children (n-1) l in
Some suri, childunion
| _ -> None, SetSet.empty
| Cic.Meta _
| Cic.Sort _
| Cic.Implicit _ -> UriManagerSet.empty
- | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty
+ | Cic.Var (u,exp_named_subst) ->
+ (*CSC: TODO if the var has a body it must be processed *)
+ UriManagerSet.empty
| Cic.Const (u,exp_named_subst) ->
UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
- let uri = string_of_uriref (u, [t]) in
+ let uri = UriManager.uri_of_uriref u t None in
UriManagerSet.singleton uri
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let uri = string_of_uriref (u, [t;c]) in
+ let uri = UriManager.uri_of_uriref u t (Some c) in
UriManagerSet.singleton uri
| Cic.Cast (t, _) -> signature_concl t
| Cic.Prod (_, s, t) ->
| Cic.Prod (_, _, t) -> signature_of t
| Cic.LetIn (_, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = u in
- Some (suri, []), add l
+ Some (u, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t]) in
+ let suri = UriManager.uri_of_uriref u t None in
if u = HelmLibraryObjects.Logic.eq_URI then
(* equality is handled in a special way: in particular,
the type, if defined, is always added to the prefix,
and n is not decremented - it should have been n-2 *)
match l with
Cic.Const (u1,exp_named_subst1)::l1 ->
- let suri1 = u1 in
- let inconcl = UriManagerSet.remove suri1 (add l1) in
- Some (suri, [suri1]), inconcl
+ let inconcl = UriManagerSet.remove u1 (add l1) in
+ Some (suri, [u1]), inconcl
| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
- let suri1 = string_of_uriref (u1, [t1]) in
+ let suri1 = UriManager.uri_of_uriref u1 t1 None in
let inconcl = UriManagerSet.remove suri1 (add l1) in
Some (suri, [suri1]), inconcl
| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
- let suri1 = string_of_uriref (u1, [t1;c1]) in
+ let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
let inconcl = UriManagerSet.remove suri1 (add l1) in
Some (suri, [suri1]), inconcl
| _ :: _ -> Some (suri, []), UriManagerSet.empty
else
Some (suri, []), add l
| Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = string_of_uriref (u, [t;c]) in
+ let suri = UriManager.uri_of_uriref u t (Some c) in
Some (suri, []), add l
| t -> None, signature_concl t
| `Conclusion -> [`InConclusion]
| `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
in
- let s' = List.map (fun u -> `Obj (u, positions)) s in
- `Obj (m, [`MainConclusion None]) :: s'
+ let positions =
+ if m = None then `MainConclusion None :: positions else positions in
+ let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in
+ match m with
+ None -> s'
+ | Some m -> `Obj (m, [`MainConclusion None]) :: s'
let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
-let get_constants (dbd:Mysql.dbd) ~where uri =
+let get_constants (dbd:HMysql.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 = Mysql.exec dbd query in
+ let result = HMysql.exec dbd query in
let set = ref UriManagerSet.empty in
- Mysql.iter result
+ HMysql.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:Mysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HMysql.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/eq.ind#xpointer(1/1/1)"]
let myspeciallist =
[0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
- (* 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"; *)
+ (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
0,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con";
0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con";
0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal2.con";
0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
-let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
List.concat
(List.map
(fun (m,s) ->
- if ((m = 0) && (main = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI)) then
+ let is_eq,card =
+ match main with
+ None -> false,m
+ | Some main ->
+ (m = 0 &&
+ UriManager.eq main
+ (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI))),
+ m+1
+ in
+ if m = 0 && is_eq then
(if facts then myspeciallist_of_facts
else myspeciallist)
else
let res =
+ (* this gets rid of the ~750 objects of type Set/Prop/Type *)
+ if card = 0 then []
+ else
let must = must_of_prefix ~where main s in
match where with
- | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
- | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Eq card) must
+ | `Statement -> at_least ~dbd ~full_card:(Eq card) must
in
- List.map (fun uri -> (m, uri)) res)
+ List.map (fun uri -> (card, uri)) res)
prefixes)
(* critical value reached, fallback to "only" constraints *)
-let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
main prefixes constants
=
let max_prefix_length =
| (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
| _::_-> res in
filter [] prefixes in
- let greater_than =
+ let greater_than =
let all =
union
(List.map
(fun (m,s) ->
+ let card = if main = None then m else m + 1 in
let must = must_of_prefix ~where main s in
(let res =
match where with
- | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
- | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Gt card) must
+ | `Statement -> at_least ~dbd ~full_card:(Gt card) must
in
(* we tag the uri with m+1, for sorting purposes *)
- List.map (fun uri -> (m+1, uri)) res))
+ List.map (fun uri -> (card, uri)) res))
maximal_prefixes)
in
+ Printf.fprintf stderr "all: %d\n" (List.length all);flush_all ();
List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
- let equal_to = compute_exactly ~dbd ~facts ~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) ?(facts=false) t =
+let cmatch ~(dbd:HMysql.dbd) ?(facts=false) t =
let (main, constants) = signature_of t in
match main with
| None -> []
let all_constants =
List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
in
- compute_with_only ~dbd ~facts main all_concl all_constants
+ compute_with_only ~dbd ~facts (Some main) all_concl all_constants
| _, _ -> [])
else
(* in this case we compute all prefixes, and we do not need
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) *)
+ compute_exactly ~dbd ~facts ~where:`Conclusion (Some main) all_concl
| _, _ -> [])
let power_upto upto consts =
List.sort (fun (n,_) (m,_) -> m - n)
(List.fold_left
(fun res a ->
- List.filter (function (n,l) -> n <= upto)
- res@(List.map (function (n,l) -> (n+1,a::l)) res))
+ let res' =
+ List.filter (function (n,l) -> n <= upto)
+ (List.map (function (n,l) -> (n+1,a::l)) res) in
+ res@res')
[(0,[])] l)
let power consts =
type where = [ `Conclusion | `Statement ]
-let sigmatch ~(dbd:Mysql.dbd)
- ?(facts=false) ?(where = `Conclusion) (main, constants) =
- match main with
- None -> []
- | Some (main, types) ->
- let constants_no = UriManagerSet.cardinal constants in
- if (constants_no > critical_value) then
- let subsets =
- let subsets = power_upto just_factor constants in
- let types_no = List.length types in
- List.map (function (n,l) -> (n+types_no,types@l)) subsets
- in
- let all_constants =
- List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
- in
- compute_with_only ~dbd ~where main subsets all_constants
- else
- 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
+let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+ (main, constants)
+=
+ let main,types =
+ match main with
+ None -> None,[]
+ | Some (main, types) -> Some main,types
+ in
+ let constants_no = UriManagerSet.cardinal constants in
+ (* prerr_endline (("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
+ in
+ 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
+ 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
(* match query wrappers *)