let critical_value = 7
let just_factor = 4
-module StringSet = Set.Make (String)
-module SetSet = Set.Make (StringSet)
+module UriManagerSet = UriManager.UriSet
+module SetSet = Set.Make (UriManagerSet)
-type term_signature = (string * string list) option * StringSet.t
+type term_signature = (UriManager.uri * UriManager.uri list) option * UriManagerSet.t
type cardinality_condition =
| Eq of int
| `Obj (uri, positions) ->
let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
let where =
- (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
+ (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl (UriManager.string_of_uri uri)) ::
mk_positions positions cur_tbl ::
(if n=start then []
else [sprintf "%s.source = %s.source" start_table cur_tbl]) @
(* prerr_endline query; *)
let result = Mysql.exec dbd query in
Mysql.map result
- (fun row -> match row.(0) with Some s -> s | _ -> assert false)
+ (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
(** Prefix handling *)
let filter_by_card n =
- SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
+ SetSet.filter (fun t -> (UriManagerSet.cardinal t) <= n)
let merge n a b =
let init = SetSet.union a b in
let merge_single_set s1 b =
SetSet.fold
- (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
+ (fun s2 res -> SetSet.add (UriManagerSet.union s1 s2) res)
b SetSet.empty in
let res =
SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
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)
and add_root n root childs =
let childunion = inspect_children n childs in
- let addroot = StringSet.add root in
+ let addroot = UriManagerSet.add root in
SetSet.fold
(fun child newsets -> SetSet.add (addroot child) newsets)
childunion
- (SetSet.singleton (StringSet.singleton root))
+ (SetSet.singleton (UriManagerSet.singleton root))
and inspect_conclusion n t =
if n = 0 then SetSet.empty
| Cic.Implicit _ -> SetSet.empty
| Cic.Var (u,exp_named_subst) -> SetSet.empty
| Cic.Const (u,exp_named_subst) ->
- SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
+ SetSet.singleton (UriManagerSet.singleton u)
| Cic.MutInd (u, t, exp_named_subst) ->
- SetSet.singleton (StringSet.singleton
- (UriManager.string_of_uriref (u, [t])))
+ SetSet.singleton (UriManagerSet.singleton
+ (string_of_uriref (u, [t])))
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
- SetSet.singleton (StringSet.singleton
- (UriManager.string_of_uriref (u, [t; c])))
+ SetSet.singleton (UriManagerSet.singleton
+ (string_of_uriref (u, [t; 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 = UriManager.string_of_uri u in
+ let suri = u in
add_root (n-1) suri l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = UriManager.string_of_uriref (u, [t]) in
+ let suri = string_of_uriref (u, [t]) in
add_root (n-1) suri l
| Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = UriManager.string_of_uriref (u, [t; c]) in
+ let suri = string_of_uriref (u, [t; c]) in
add_root (n-1) suri l
| Cic.Appl l ->
SetSet.empty
| Cic.Implicit _ -> None, SetSet.empty
| Cic.Var (u,exp_named_subst) -> None, SetSet.empty
| Cic.Const (u,exp_named_subst) ->
- Some (UriManager.string_of_uri u), SetSet.empty
+ Some u, SetSet.empty
| Cic.MutInd (u, t, exp_named_subst) ->
- let uri = UriManager.string_of_uriref (u, [t]) in
+ let uri = string_of_uriref (u, [t]) in
Some uri, SetSet.empty
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let uri = UriManager.string_of_uriref (u, [t; c]) in
+ let uri = string_of_uriref (u, [t; 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 = UriManager.string_of_uri u in
+ let suri = u in
let childunion = inspect_children (n-1) l in
Some suri, childunion
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = UriManager.string_of_uriref (u, [t]) in
+ let suri = string_of_uriref (u, [t]) 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 = UriManager.string_of_uri u1 in
+ let suri1 = u1 in
let inconcl = add_root (n-1) suri1 l1 in
Some suri, inconcl
| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
- let suri1 = UriManager.string_of_uriref (u1, [t1]) in
+ let suri1 = string_of_uriref (u1, [t1]) in
let inconcl = add_root (n-1) suri1 l1 in
Some suri, inconcl
| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
- let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
+ let suri1 = string_of_uriref (u1, [t1; 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 = UriManager.string_of_uriref (u, [t; c]) in
+ let suri = string_of_uriref (u, [t; c]) in
let childunion = inspect_children (n-1) l in
Some suri, childunion
| _ -> None, SetSet.empty
let res =
List.map
(fun set ->
- let el = StringSet.elements set in
+ let el = UriManagerSet.elements set in
(List.length el, el)) l in
(* ordered by descending cardinality *)
List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
let rec add children =
List.fold_left
- (fun acc t -> StringSet.union (signature_concl t) acc)
- (StringSet.empty) children
+ (fun acc t -> UriManagerSet.union (signature_concl t) acc)
+ (UriManagerSet.empty) children
(* this function creates the set of all different constants appearing in
the conclusion of the term *)
Cic.Rel _
| Cic.Meta _
| Cic.Sort _
- | Cic.Implicit _ -> StringSet.empty
- | Cic.Var (u,exp_named_subst) -> StringSet.empty
+ | Cic.Implicit _ -> UriManagerSet.empty
+ | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty
| Cic.Const (u,exp_named_subst) ->
- StringSet.singleton (UriManager.string_of_uri u)
+ UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
- let uri = UriManager.string_of_uriref (u, [t]) in
- StringSet.singleton uri
+ let uri = string_of_uriref (u, [t]) in
+ UriManagerSet.singleton uri
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let uri = UriManager.string_of_uriref (u, [t;c]) in
- StringSet.singleton uri
+ let uri = string_of_uriref (u, [t;c]) in
+ UriManagerSet.singleton uri
| Cic.Cast (t, _) -> signature_concl t
| Cic.Prod (_, s, t) ->
- StringSet.union (signature_concl s) (signature_concl t)
+ UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.Lambda (_, s, t) ->
- StringSet.union (signature_concl s) (signature_concl t)
+ UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.LetIn (_, s, t) ->
- StringSet.union (signature_concl s) (signature_concl t)
+ UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.Appl l -> add l
| Cic.MutCase _
| Cic.Fix _
| Cic.CoFix _ ->
- StringSet.empty
+ UriManagerSet.empty
let rec signature_of = function
| Cic.Cast (t, _) -> signature_of t
| Cic.Prod (_, _, t) -> signature_of t
| Cic.LetIn (_, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = UriManager.string_of_uri u in
+ let suri = u in
Some (suri, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = UriManager.string_of_uriref (u, [t]) in
+ let suri = string_of_uriref (u, [t]) 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 = UriManager.string_of_uri u1 in
- let inconcl = StringSet.remove suri1 (add l1) in
+ let suri1 = u1 in
+ let inconcl = UriManagerSet.remove suri1 (add l1) in
Some (suri, [suri1]), inconcl
| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
- let suri1 = UriManager.string_of_uriref (u1, [t1]) in
- let inconcl = StringSet.remove suri1 (add l1) in
+ let suri1 = string_of_uriref (u1, [t1]) in
+ let inconcl = UriManagerSet.remove suri1 (add l1) in
Some (suri, [suri1]), inconcl
| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
- let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
- let inconcl = StringSet.remove suri1 (add l1) in
+ let suri1 = string_of_uriref (u1, [t1;c1]) in
+ let inconcl = UriManagerSet.remove suri1 (add l1) in
Some (suri, [suri1]), inconcl
- | _ :: _ -> Some (suri, []), StringSet.empty
+ | _ :: _ -> Some (suri, []), UriManagerSet.empty
| _ -> assert false (* args number must be > 0 *)
else
Some (suri, []), add l
| Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = UriManager.string_of_uriref (u, [t;c]) in
+ let suri = string_of_uriref (u, [t;c]) in
Some (suri, []), add l
| t -> None, signature_concl t
let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
let get_constants (dbd:Mysql.dbd) ~where uri =
- let uri = escape uri in
+ let uri = escape (UriManager.string_of_uri uri) in
let positions =
match where with
| `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
in
let result = Mysql.exec dbd query in
- let set = ref StringSet.empty in
+ let set = ref UriManagerSet.empty in
Mysql.iter result
(fun col ->
match col.(0) with
- | Some uri -> set := StringSet.add uri !set
+ | 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 inconcl = get_constants dbd ~where u in
- StringSet.subset inconcl only
+ UriManagerSet.subset inconcl only
(* 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)"]
+ [0,UriManager.uri_of_string "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"; *)
- 0,"cic:/Coq/Init/Logic/trans_eq.con";
- 0,"cic:/Coq/Init/Logic/f_equal.con";
- 0,"cic:/Coq/Init/Logic/f_equal2.con";
- 0,"cic:/Coq/Init/Logic/f_equal3.con"]
+ [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,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 =
List.concat
(List.map
(fun (m,s) ->
- if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
+ if ((m = 0) && (main = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI)) then
(if facts then myspeciallist_of_facts
else myspeciallist)
else
| 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 in
+ let constants_no = UriManagerSet.cardinal constants in
if (constants_no > critical_value) then
let prefixes = prefixes just_factor t in
(match prefixes with
| Some main, all_concl ->
let all_constants =
- List.fold_right StringSet.add types (StringSet.add main constants)
+ List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
in
compute_with_only ~dbd ~facts main all_concl all_constants
| _, _ -> [])
| _, _ -> [])
let power_upto upto consts =
- let l = StringSet.elements consts in
+ let l = UriManagerSet.elements consts in
List.sort (fun (n,_) (m,_) -> m - n)
(List.fold_left
(fun res a ->
[(0,[])] l)
let power consts =
- let l = StringSet.elements consts in
+ let l = UriManagerSet.elements consts in
List.sort (fun (n,_) (m,_) -> m - n)
(List.fold_left
(fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
match main with
None -> []
| Some (main, types) ->
- let constants_no = StringSet.cardinal constants in
+ let constants_no = UriManagerSet.cardinal constants in
if (constants_no > critical_value) then
let subsets =
let subsets = power_upto just_factor constants in
List.map (function (n,l) -> (n+types_no,types@l)) subsets
in
let all_constants =
- List.fold_right StringSet.add types (StringSet.add main constants)
+ List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
in
compute_with_only ~dbd ~where main subsets all_constants
else