let sequent_viewer = MatitaMathView.sequentViewer_instance () in
let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
sequent_viewer#set_href_callback
- (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri uri)));
+ (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri))));
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer status =
sequents_viewer#reset;
let browser = MatitaMathView.cicBrowser () in
let entry =
try
- `Uri Sys.argv.(1)
+ `Uri (UriManager.uri_of_string Sys.argv.(1))
with Invalid_argument _ -> `Dir "cic:/"
in
browser#load entry
exception Ambiguous_input
-type choose_uris_callback = id:string -> string list -> string list
+type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
type choose_interp_callback = (string * string) list list -> int list
let mono_uris_callback ~id = raise Ambiguous_input
* compiler) *)
exception Ambiguous_input
-type choose_uris_callback = id:string -> string list -> string list
+type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
type choose_interp_callback = (string * string) list list -> int list
val set_choose_uris_callback: choose_uris_callback -> unit
let non p x = not (p x)
let is_var_uri s =
+ let s = UriManager.string_of_uri s in
try
String.sub s (String.length s - 4) 4 = ".var"
with Invalid_argument _ -> false
| _ -> ()));
dialog#uriChoiceDialog#set_title title;
dialog#uriChoiceLabel#set_text msg;
- List.iter model#easy_append uris;
+ List.iter model#easy_append (List.map UriManager.string_of_uri uris);
dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
connect_button dialog#uriChoiceAutoButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();
ignore(win#whelpResultTreeview#connect#row_activated
~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
mathView#set_href_callback (Some (fun uri ->
- handle_error (fun () -> self#load (`Uri uri))));
+ handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri)))));
self#_load (`About `Blank);
toplevel#show ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Dir dir -> self#_loadDir dir
- | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
+ | `Uri uri -> self#_loadUriManagerUri uri
| `Whelp (query, results) ->
set_whelp_query query;
- self#_loadList (List.map (fun r -> "obj", r) results));
+ self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results));
self#setEntry entry
end
with
end else begin
let entry =
match txt with
- | txt when is_uri txt -> `Uri (fix_uri txt)
+ | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
| txt when is_dir txt -> `Dir (add_trailing_slash txt)
| txt ->
(try
let term = disambiguate term status in
let uri =
match term with
- | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
+ | Cic.MutInd (uri,n,_) -> UriManager.uri_of_string (UriManager.string_of_uriref (uri,[n]))
| _ -> failwith "Not a MutInd"
in
let l = MQ.elim ~dbd uri in
(TA.Executable (loc,
(TA.Tactical (loc,
TA.Tactic (loc,
- TA.Apply (loc, CicAst.Uri (uri,None)))))))
+ TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))))
in
let new_status = MatitaEngine.eval_ast status ast in
let extra_text =
MatitaLog.error
"The result of the urichooser should be only 1 uri, not:\n";
List.iter (
- fun u -> MatitaLog.error (u ^ "\n")
+ fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
) selected;
assert false)
| TA.Check (_,term) ->
buffer:GText.buffer ->
init:MatitaTypes.status ->
mathviewer: MatitaTypes.mathViewer->
- urichooser: (string list -> string list) ->
+ urichooser: (UriManager.uri list -> UriManager.uri list) ->
unit ->
script
| `Check of string (* term *)
| `Cic of Cic.term * Cic.metasenv
| `Dir of string (* "directory" in cic uris namespace *)
- | `Uri of string (* cic object uri *)
- | `Whelp of string * string list (* query and results *)
+ | `Uri of UriManager.uri (* cic object uri *)
+ | `Whelp of string * UriManager.uri list (* query and results *)
]
let string_of_entry = function
| `About `Us -> "about:us"
| `Check _ -> "check:"
| `Cic (_, _) -> "term:"
- | `Dir uri | `Uri uri -> uri
+ | `Dir uri -> uri
+ | `Uri uri -> UriManager.string_of_uri uri
| `Whelp (query, _) -> query
let entry_of_string = function
*)
method show_entry: ?reuse:bool -> mathViewer_entry -> unit
method show_uri_list:
- ?reuse:bool -> entry:mathViewer_entry -> string list -> unit
+ ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
let uris =
match uris with
| [] ->
- [UriManager.string_of_uri (C.input_or_locate_uri
+ [(C.input_or_locate_uri
~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
in
List.map
(fun uri ->
- (uri,
+ (UriManager.string_of_uri uri,
let term =
try
- CicUtil.term_of_uri uri
+ CicUtil.term_of_uri (UriManager.string_of_uri uri)
with exn ->
- debug_print uri;
+ debug_print (UriManager.string_of_uri uri);
debug_print (Printexc.to_string exn);
assert false
in
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> string list -> string list
+ title:string -> msg:string -> id:string -> UriManager.uri list ->
+ UriManager.uri list
val interactive_interpretation_choice:
(string * string) list list -> int list
val input_or_locate_uri:
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> string list -> string list
+ title:string -> msg:string -> id:string -> UriManager.uri list ->
+ UriManager.uri list
val interactive_interpretation_choice :
(string * string) list list -> int list
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
* http://helm.cs.unibo.it/
*)
-module StringSet : Set.S with type elt = string
+module UriManagerSet : Set.S with type elt = UriManager.uri
+
(** @return <main, constants>
* main: constant in main position and, for polymorphic constants, type
* instantitation
* constants: constants appearing in term *)
-type term_signature = (string * string list) option * StringSet.t
+type term_signature = (UriManager.uri * UriManager.uri list) option * UriManagerSet.t
(** {2 Candidates filtering} *)
(** @return sorted list of theorem URIs, first URIs in the least have higher
* relevance *)
-val cmatch: dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> string list
+val cmatch: dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> UriManager.uri list
(** as cmatch, but returned list is not sorted but rather tagged with
* relevance information: higher the tag, higher the relevance *)
-val cmatch': dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> (int * string) list
+val cmatch': dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> (int * UriManager.uri) list
type where = [ `Conclusion | `Statement ] (** signature matching extent *)
?facts:bool ->
?where:where ->
term_signature ->
- (int * string) list
+ (int * UriManager.uri) list
(** {2 Constraint engine} *)
?diff:cardinality_condition ->
?rating:rating_criterion ->
MetadataTypes.constr list ->
- string list
+ UriManager.uri list
(** @param where defaults to `Conclusion *)
val at_most:
dbd:Mysql.dbd ->
- ?where:where -> StringSet.t ->
- (string -> bool)
+ ?where:where -> UriManagerSet.t ->
+ (UriManager.uri -> bool)
val add_all_constr:
?tbl:string ->
dbd:Mysql.dbd ->
?rating:[ `Hits ] ->
int * string list * string list ->
- string list
+ UriManager.uri list
val signature_of: Cic.term -> term_signature
-val constants_of: Cic.term -> StringSet.t
+val constants_of: Cic.term -> UriManagerSet.t
let count_distinct position l =
- MetadataConstraints.StringSet.cardinal
+ MetadataConstraints.UriManagerSet.cardinal
(List.fold_left (fun acc d ->
match position with
| `Conclusion ->
(match d with
| `Obj (name,`InConclusion)
| `Obj (name,`MainConclusion _ ) ->
- MetadataConstraints.StringSet.add name acc
+ MetadataConstraints.UriManagerSet.add name acc
| _ -> acc)
| `Hypothesis ->
(match d with
| `Obj (name,`InHypothesis)
| `Obj (name,`MainHypothesis _) ->
- MetadataConstraints.StringSet.add name acc
+ MetadataConstraints.UriManagerSet.add name acc
| _ -> acc)
| `Statement ->
(match d with
| `Obj (name,`InBody) -> acc
- | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
+ | `Obj (name,_) -> MetadataConstraints.UriManagerSet.add name acc
| _ -> acc)
- ) MetadataConstraints.StringSet.empty l)
+ ) MetadataConstraints.UriManagerSet.empty l)
(*
let insert_const_no dbd uri =
let term = CicUtil.term_of_uri uri in
let no_full = count_distinct `Statement metadata in
let insert =
sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)"
- (count_tbl ()) uri no_concl no_hyp no_full
+ (count_tbl ()) (UriManager.string_of_uri uri) no_concl no_hyp no_full
in
ignore (Mysql.exec dbd insert)
let insert_name ~dbd ~uri ~name =
let query =
- sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) (UriManager.string_of_uri uri) name
in
ignore (Mysql.exec dbd query)
end
module MetadataSet = Set.Make (OrderedMetadata)
-module StringSet = Set.Make (String)
+module UriManagerSet = UriManager.UriSet
module S = MetadataSet
| Cic.Variable (_, Some body, _, _, _), _ -> true
| _ -> false
+let string_of_uriref s =
+ UriManager.uri_of_string (UriManager.string_of_uriref s)
+
let compute_term pos term =
let rec aux (pos: position) set = function
| Cic.Var (uri, subst) when var_has_body uri ->
(fun set term -> aux (next_pos pos) set term)
set tl
| Cic.Const (uri, subst) ->
- let set = S.add (`Obj (string_of_uri uri, pos)) set in
+ let set = S.add (`Obj (uri, pos)) set in
List.fold_left
(fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutInd (uri, typeno, subst) ->
- let uri = UriManager.string_of_uriref (uri, [typeno]) in
+ let uri = string_of_uriref (uri, [typeno]) in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutConstruct (uri, typeno, consno, subst) ->
- let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
+ let uri = string_of_uriref (uri, [typeno; consno]) in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
let compute_type pos uri typeno (name, _, ty, constructors) =
let consno = ref 0 in
let type_metadata =
- (UriManager.string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
+ (string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
in
let constructors_metadata =
List.map
(fun (name, term) ->
incr consno;
- let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
+ let uri = string_of_uriref (uri, [typeno; !consno]) in
(uri, name, (compute_term pos term)))
constructors
in
S.fold
(fun metadata uris ->
match metadata with
- | `Obj (uri, _) -> StringSet.add uri uris
+ | `Obj (uri, _) -> UriManagerSet.add uri uris
| _ -> uris)
- type_metadata StringSet.empty
+ type_metadata UriManagerSet.empty
in
S.union
(S.filter
(function
- | `Obj (uri, _) when StringSet.mem uri uris -> false
+ | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
| _ -> true)
body_metadata)
type_metadata
S.empty
params
in
- [ UriManager.string_of_uri uri,
+ [ uri,
UriManager.name_of_uri uri,
S.union metadata var_metadata ]
| Cic.InductiveDefinition (types, params, _, _) ->
(** @return tuples <uri, shortname, metadata> *)
val compute_obj:
UriManager.uri ->
- (string * string * MetadataTypes.metadata list) list
+ (UriManager.uri * string * MetadataTypes.metadata list) list
module IntSet: Set.S with type elt = int
let columns_of_metadata_aux ~about metadata =
let sort s = `String (CicPp.ppsort s) in
- let source = `String about in
- let occurrence u = `String u in
+ let source = `String (UriManager.string_of_uri about) in
+ let occurrence u = `String (UriManager.string_of_uri u) in
List.fold_left
(fun (sort_cols, rel_cols, obj_cols) metadata ->
match metadata with
(CicPp.ppsort sort) (String.concat ";" (List.map pp_position p))
| `Rel p -> sprintf "Rel [%s]" (String.concat ";" (List.map pp_position p))
| `Obj (uri, p) -> sprintf "Obj %s; [%s]"
- uri (String.concat ";" (List.map pp_position p))
+ (UriManager.string_of_uri uri) (String.concat ";" (List.map pp_position p))
(*
let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) =
(** @return columns for Sort, Rel, and Obj respectively *)
val columns_of_metadata:
- (string * string * MetadataTypes.metadata list) list ->
+ (UriManager.uri * string * MetadataTypes.metadata list) list ->
t list list * t list list * t list list
(*
type metadata =
[ `Sort of Cic.sort * main_position
| `Rel of main_position
- | `Obj of string * position
+ | `Obj of UriManager.uri * position
]
type constr =
[ `Sort of Cic.sort * main_position list
| `Rel of main_position list
- | `Obj of string * position list
+ | `Obj of UriManager.uri * position list
]
let constr_of_metadata: metadata -> constr = function
type metadata =
[ `Sort of Cic.sort * main_position
| `Rel of main_position
- | `Obj of string * position
+ | `Obj of UriManager.uri * position
]
type constr =
[ `Sort of Cic.sort * main_position list
| `Rel of main_position list
- | `Obj of string * position list
+ | `Obj of UriManager.uri * position list
]
val constr_of_metadata: metadata -> constr
let major = declaration hyp context in
match MetadataQuery.fwd_simpl ~dbd major with
| [] -> error fail_msg1
- | uri :: _ -> prerr_endline uri; (proof, [])
+ | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
in
PET.mk_tactic fwd_simpl_tac
let equivalent_objects =
(* finte costanti; i.e. costanti senza corpo *)
-[("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack0.con","finte costanti");
- ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ac10.con","finte costanti");
- ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack2.con","finte costanti")
+[UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack0.con"(*,"finte costanti"*);
+ UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ac10.con"(*,"finte costanti"*);
+ UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack2.con"(*,"finte costanti"*)
]@
(* inutili mostri *)
-[("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg0.con","useless monster");
- ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg1.con","useless monster");
- ("cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con","useless monster")
+[UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg0.con"(*,"useless monster"*);
+ UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg1.con"(*,"useless monster"*);
+ UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con"(*,"useless monster"*)
]@
(* istanze *)
- ("cic:/Coq/Init/Peano/eq_S.con","cic:/Coq/Init/Logic/f_equal.con")::
+ (UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_S.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con"*))::
[
-"cic:/Paris/ZF/src/useful/lem_iff_sym.con","cic:/Coq/Init/Logic/iff_sym.con";
-"cic:/Lyon/AUTOMATA/Ensf_types/False_imp_P.con","cic:/Coq/Init/Logic/False_ind.con";
-"cic:/Rocq/TreeAutomata/bases/plus_O_r.con","cic:/Coq/Arith/Plus/plus_0_r.con";
-"cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con";
-"cic:/Sophia-Antipolis/Bertrand/Misc/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_not_and.con","cic:/Coq/Logic/Classical_Prop/or_not_and.con";
-"cic:/Rocq/DEMOS/Sorting/diff_true_false.con","cic:/Coq/Bool/Bool/diff_true_false.con";
-"cic:/CoRN/metrics/CMetricSpaces/nz.con","cic:/Coq/Arith/Max/le_max_l.con";
-"cic:/Coq/Logic/Decidable/not_or.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
-"cic:/Coq/Init/Logic/sym_not_equal.con","cic:/Coq/Init/Logic/sym_not_eq.con";
-"cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con","cic:/Coq/Reals/R_sqrt/sqrt_def.con";
-"cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con","cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con";
-"cic:/Coq/Logic/Eqdep_dec/eqT2eq.con","cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
-"cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con","cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con";
-"cic:/Rocq/THREE_GAP/Nat_compl/en_plus.con","cic:/Coq/Arith/Plus/plus_0_r.con";
-"cic:/Nijmegen/QArith/Zaux/Zabs_10.con","cic:/Coq/ZArith/Zabs/Zabs_pos.con";
-"cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con";
-"cic:/Coq/Arith/Le/le_refl.con","cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)";
-"cic:/Rocq/TreeAutomata/bases/le_n_n.con","cic:/Coq/Arith/Le/le_refl.con";
-"cic:/Coq/ZArith/auxiliary/Zred_factor1.con","cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con";
-"cic:/Coq/Relations/Newman/caseRxy.con","cic:/Coq/Relations/Newman/Ind_proof.con";
-"cic:/Rocq/TreeAutomata/bases/S_plus_r.con","cic:/Coq/Init/Peano/plus_n_Sm.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/Zmult_ab0a0b0.con","cic:/Coq/ZArith/BinInt/Zmult_integral.con";
-"cic:/Sophia-Antipolis/Algebra/Z_group/ax8.con","cic:/Coq/NArith/BinPos/ZC2.con";
-"cic:/Sophia-Antipolis/Algebra/Z_group/Zlt_reg_l.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con";
-"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con";
-"cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con","cic:/Coq/Reals/RIneq/Rlt_0_1.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Classic.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
-"cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con","cic:/Coq/Reals/RIneq/Rlt_0_sqr.con";
-"cic:/Rocq/THREE_GAP/Nat_compl/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
-"cic:/Coq/Reals/Rtrigo_def/sin_antisym.con","cic:/Coq/Reals/Rtrigo/sin_neg.con";
-"cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/false_implies_everything.con","cic:/Coq/Init/Logic/False_ind.con";
-"cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con","cic:/Coq/ring/Ring_normalize/index_eq_prop.con";
-"cic:/CoRN/algebra/Basics/le_pred.con","cic:/Coq/Arith/Le/le_pred.con";
-"cic:/Lannion/continuations/FOUnify_cps/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con";
-"cic:/Coq/Sorting/Permutation/permut_right.con","cic:/Coq/Sorting/Permutation/permut_cons.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_mult_l.con","cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con";
-"cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con","cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con";
-"cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con";
-"cic:/CoRN/fta/KeyLemma/lem_1c.con","cic:/Coq/Arith/Minus/le_minus.con";
-"cic:/Coq/omega/OmegaLemmas/OMEGA20.con","cic:/Coq/omega/OmegaLemmas/OMEGA17.con";
-"cic:/Nijmegen/QArith/Zaux/pair_2.con","cic:/Coq/Init/Datatypes/injective_projections.con";
-"cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con";
-"cic:/CoRN/algebra/Basics/le_mult_right.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con";
-"cic:/Nijmegen/QArith/Zaux/Zle_lt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con";
-"cic:/Rocq/ARITH/Chinese/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
-"cic:/Rocq/THREE_GAP/Nat_compl/not_gt_le.con","cic:/Coq/Arith/Compare_dec/not_gt.con";
-"cic:/Rocq/ARITH/Chinese/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con";
-"cic:/CoRN/algebra/Basics/lt_mult_right.con","cic:/Coq/Arith/Mult/mult_lt_compat_r.con";
-"cic:/Rocq/ARITH/Chinese/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con";
-"cic:/Nijmegen/QArith/Zaux/Zabs_neg.con","cic:/Coq/ZArith/Zabs/Zabs_non_eq.con";
-"cic:/Lyon/FIRING-SQUAD/bib/plus_S.con","cic:/Coq/Init/Peano/plus_Sn_m.con";
-"cic:/Nijmegen/QArith/Qhomographic_Qpositive_to_Qpositive/one_non_negative.con","cic:/Coq/ZArith/Zorder/Zle_0_1.con";
-"cic:/Coq/fourier/Fourier_util/Rle_zero_1.con","cic:/Coq/Reals/RIneq/Rle_0_1.con";
-"cic:/Coq/Logic/Diaconescu/proof_irrel.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con";
-"cic:/Coq/Init/Logic/sym_equal.con","cic:/Coq/Init/Logic/sym_eq.con";
-"cic:/Coq/IntMap/Mapiter/pair_sp.con","cic:/Coq/Init/Datatypes/surjective_pairing.con";
-"cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_or_not.con","cic:/Coq/Logic/Classical_Prop/not_and_or.con";
-"cic:/CoRN/model/structures/Zsec/Zplus_wd0.con","cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con";
-"cic:/Coq/ZArith/auxiliary/Zred_factor6.con","cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/S_inj.con","cic:/Coq/Init/Peano/eq_add_S.con";
-"cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con","cic:/Coq/Reals/RIneq/IZN.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_orb.con","cic:/Coq/Bool/Bool/orb_comm.con";
-"cic:/Coq/Reals/PartSum/plus_sum.con","cic:/Coq/Reals/Cauchy_prod/sum_plus.con";
-"cic:/Nijmegen/QArith/Qpositive/minus_le.con","cic:/Coq/Arith/Minus/le_minus.con";
-"cic:/Lyon/FIRING-SQUAD/bib/plus_zero.con","cic:/Coq/Arith/Plus/plus_0_r.con";
-"cic:/Sophia-Antipolis/Cours-de-Coq/ex1_auto/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_andb.con","cic:/Coq/Bool/Bool/andb_comm.con";
-"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
-"cic:/Suresnes/BDD/canonicite/Prelude0/Morgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
-"cic:/Coq/Logic/ClassicalFacts/TrueP.con","cic:/Coq/Logic/ClassicalFacts/FalseP.con";
-"cic:/Nijmegen/QArith/Zaux/Zminus_eq.con","cic:/Coq/ZArith/BinInt/Zminus_eq.con";
-"cic:/Sophia-Antipolis/Cours-de-Coq/ex1/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
-"cic:/Nijmegen/QArith/Zaux/pair_1.con","cic:/Coq/Init/Datatypes/surjective_pairing.con";
-"cic:/Orsay/Maths/divide/Zabs_ind.con","cic:/Coq/ZArith/Zabs/Zabs_ind.con";
-"cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con","cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con";
-"cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con","cic:/Coq/Reals/RIneq/Req_le.con";
-"cic:/Rocq/TreeAutomata/bases/Sn_eq_Sm_n_eq_m.con","cic:/Coq/Init/Peano/eq_add_S.con";
-"cic:/Coq/Init/Logic/trans_equal.con","cic:/Coq/Init/Logic/trans_eq.con";
-"cic:/Coq/omega/OmegaLemmas/OMEGA2.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con";
-"cic:/Sophia-Antipolis/Bertrand/Raux/P_Rmin.con","cic:/Coq/Reals/Rpower/P_Rmin.con";
-"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con";
-"cic:/Sophia-Antipolis/Huffman/Aux/le_minus.con","cic:/Coq/Arith/Minus/le_minus.con";
-"cic:/Coq/Init/Peano/plus_O_n.con","cic:/Coq/Arith/Plus/plus_0_l.con";
-"cic:/Coq/Logic/Berardi/inv2.con","cic:/Coq/Logic/Berardi/AC.con";
-"cic:/Coq/Reals/SeqProp/not_Rlt.con","cic:/Coq/Reals/RIneq/Rnot_lt_ge.con";
-"cic:/Nancy/FOUnify/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con";
-"cic:/Rocq/TreeAutomata/bases/le_mult_l.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con";
-"cic:/Eindhoven/POCKLINGTON/natZ/isnat_mult.con","cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con";
-"cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con","cic:/Coq/Reals/RIneq/Req_le_sym.con";
-"cic:/Nijmegen/QArith/Zaux/Zabs_mult.con","cic:/Coq/ZArith/Zabs/Zabs_Zmult.con";
-"cic:/Rocq/TreeAutomata/bases/plus_n_O.con","cic:/Coq/Arith/Plus/plus_0_r.con";
-"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/classic.con";
-"cic:/Rocq/TreeAutomata/bases/le_mult_mult.con","cic:/Coq/Arith/Mult/mult_le_compat.con";
-"cic:/Coq/Bool/Bool/Is_true_eq_true2.con","cic:/Coq/Bool/Bool/Is_true_eq_left.con";
-"cic:/Eindhoven/POCKLINGTON/natZ/isnat_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con";
-"cic:/Rocq/TreeAutomata/bases/le_mult_r.con","cic:/Coq/Arith/Mult/mult_le_compat_l.con";
-"cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
-"cic:/Sophia-Antipolis/Algebra/Z_group/ax3.con","cic:/Coq/ZArith/Zorder/Zgt_pos_0.con";
-"cic:/Nijmegen/QArith/Zaux/Zabs_plus.con","cic:/Coq/ZArith/Zabs/Zabs_triangle.con";
-"cic:/Sophia-Antipolis/Buchberger/Buch/Sdep.con","cic:/Coq/Init/Datatypes/prod_ind.con";
-"cic:/Coq/Reals/PartSum/Rsum_abs.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con";
-"cic:/Cachan/SMC/mu/minus_n_m_le_n.con","cic:/Coq/Arith/Minus/le_minus.con";
-"cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con","cic:/Coq/Init/Peano/eq_S.con";
-"cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/predminus1.con","cic:/Coq/Arith/Minus/pred_of_minus.con";
-"cic:/Sophia-Antipolis/Bertrand/Raux/Rpower_pow.con","cic:/Coq/Reals/Rpower/Rpower_pow.con";
-"cic:/Lyon/FIRING-SQUAD/bib/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con";
-"cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_neq.con","cic:/Coq/ZArith/Zorder/Zlt_not_eq.con";
-"cic:/Coq/Arith/Lt/nat_total_order.con","cic:/Coq/Arith/Compare_dec/not_eq.con";
-"cic:/Rocq/TreeAutomata/bases/plus_O_l.con","cic:/Coq/Arith/Plus/plus_0_r.con";
-"cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/2)","cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/1)";
-"cic:/Nijmegen/QArith/Zaux/Zmult_pos_pos.con","cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con";
-"cic:/Nijmegen/QArith/Zaux/Zlt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con";
-"cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con","cic:/Coq/Logic/Classical_Prop/classic.con";
-"cic:/Sophia-Antipolis/Rsa/MiscRsa/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con"
+UriManager.uri_of_string "cic:/Paris/ZF/src/useful/lem_iff_sym.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/iff_sym.con"*);
+UriManager.uri_of_string "cic:/Lyon/AUTOMATA/Ensf_types/False_imp_P.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/False_ind.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_O_r.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Misc/eq_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_reg_l.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_not_and.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/or_not_and.con"*);
+UriManager.uri_of_string "cic:/Rocq/DEMOS/Sorting/diff_true_false.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/diff_true_false.con"*);
+UriManager.uri_of_string "cic:/CoRN/metrics/CMetricSpaces/nz.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Max/le_max_l.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/Decidable/not_or.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
+UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_not_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_not_eq.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/R_sqrt/sqrt_def.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/Eqdep_dec/eqT2eq.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con"*);
+UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/en_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_10.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_pos.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"*);
+UriManager.uri_of_string "cic:/Coq/Arith/Le/le_refl.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_n_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Le/le_refl.con"*);
+UriManager.uri_of_string "cic:/Coq/ZArith/auxiliary/Zred_factor1.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con"*);
+UriManager.uri_of_string "cic:/Coq/Relations/Newman/caseRxy.con"(*,UriManager.uri_of_string "cic:/Coq/Relations/Newman/Ind_proof.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/S_plus_r.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_n_Sm.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zmult_ab0a0b0.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_integral.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/ax8.con"(*,UriManager.uri_of_string "cic:/Coq/NArith/BinPos/ZC2.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/Zlt_reg_l.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_neutr.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_1_l.con"*);
+UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rlt_0_1.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Classic.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rlt_0_sqr.con"*);
+UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/Rtrigo_def/sin_antisym.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rtrigo/sin_neg.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/false_implies_everything.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/False_ind.con"*);
+UriManager.uri_of_string "cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con"(*,UriManager.uri_of_string "cic:/Coq/ring/Ring_normalize/index_eq_prop.con"*);
+UriManager.uri_of_string "cic:/CoRN/algebra/Basics/le_pred.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Le/le_pred.con"*);
+UriManager.uri_of_string "cic:/Lannion/continuations/FOUnify_cps/nat_complements/le_S_eqP.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare/le_le_S_eq.con"*);
+UriManager.uri_of_string "cic:/Coq/Sorting/Permutation/permut_right.con"(*,UriManager.uri_of_string "cic:/Coq/Sorting/Permutation/permut_cons.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_mult_l.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_1_r.con"*);
+UriManager.uri_of_string "cic:/CoRN/fta/KeyLemma/lem_1c.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
+UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA20.con"(*,UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA17.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/pair_2.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/injective_projections.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"*);
+UriManager.uri_of_string "cic:/CoRN/algebra/Basics/le_mult_right.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_r.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zle_lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con"*);
+UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
+UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/not_gt_le.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare_dec/not_gt.con"*);
+UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_commut.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_comm.con"*);
+UriManager.uri_of_string "cic:/CoRN/algebra/Basics/lt_mult_right.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_lt_compat_r.con"*);
+UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_neutr.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_1_l.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_neg.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_non_eq.con"*);
+UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/plus_S.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_Sn_m.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Qhomographic_Qpositive_to_Qpositive/one_non_negative.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zle_0_1.con"*);
+UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rle_0_1.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/Diaconescu/proof_irrel.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"*);
+UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"*);
+UriManager.uri_of_string "cic:/Coq/IntMap/Mapiter/pair_sp.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/surjective_pairing.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_or_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_and_or.con"*);
+UriManager.uri_of_string "cic:/CoRN/model/structures/Zsec/Zplus_wd0.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con"*);
+UriManager.uri_of_string "cic:/Coq/ZArith/auxiliary/Zred_factor6.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/S_inj.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_add_S.con"*);
+UriManager.uri_of_string "cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/IZN.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_orb.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/orb_comm.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/PartSum/plus_sum.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Cauchy_prod/sum_plus.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Qpositive/minus_le.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
+UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/plus_zero.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Cours-de-Coq/ex1_auto/not_not_converse.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_and_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_andb.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/andb_comm.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/canonicite/Prelude0/Morgan_and_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/TrueP.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/FalseP.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zminus_eq.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zminus_eq.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Cours-de-Coq/ex1/not_not_converse.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/pair_1.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/surjective_pairing.con"*);
+UriManager.uri_of_string "cic:/Orsay/Maths/divide/Zabs_ind.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_ind.con"*);
+UriManager.uri_of_string "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con"*);
+UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Req_le.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/Sn_eq_Sm_n_eq_m.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_add_S.con"*);
+UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con"*);
+UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA2.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Raux/P_Rmin.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rpower/P_Rmin.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_commut.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_comm.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Huffman/Aux/le_minus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
+UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_O_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_l.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/Berardi/inv2.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Berardi/AC.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/SeqProp/not_Rlt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rnot_lt_ge.con"*);
+UriManager.uri_of_string "cic:/Nancy/FOUnify/nat_complements/le_S_eqP.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare/le_le_S_eq.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_l.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_r.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/natZ/isnat_mult.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con"*);
+UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Req_le_sym.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_mult.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_Zmult.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_n_O.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
+UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/excluded_middle.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/classic.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_mult.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat.con"*);
+UriManager.uri_of_string "cic:/Coq/Bool/Bool/Is_true_eq_true2.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/Is_true_eq_left.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/natZ/isnat_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_lt_compat.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_r.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_l.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/excluded_middle.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/ax3.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zgt_pos_0.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_triangle.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Buchberger/Buch/Sdep.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/prod_ind.con"*);
+UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rsum_abs.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"*);
+UriManager.uri_of_string "cic:/Cachan/SMC/mu/minus_n_m_le_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
+UriManager.uri_of_string "cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_S.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_1_r.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/predminus1.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/pred_of_minus.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Raux/Rpower_pow.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rpower/Rpower_pow.con"*);
+UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_lt_compat.con"*);
+UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_neq.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zlt_not_eq.con"*);
+UriManager.uri_of_string "cic:/Coq/Arith/Lt/nat_total_order.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare_dec/not_eq.con"*);
+UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_O_l.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/2)"(*,UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/1)"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zmult_pos_pos.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con"*);
+UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zlt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con"*);
+UriManager.uri_of_string "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/classic.con"*);
+UriManager.uri_of_string "cic:/Sophia-Antipolis/Rsa/MiscRsa/eq_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_reg_l.con"*)
]
;;
let equiv_table = Hashtbl.create 503
;;
-let _ = List.iter (fun (a,b) -> Hashtbl.add equiv_table a b) equivalent_objects
+let _ = List.iter (fun a -> Hashtbl.add equiv_table a "") equivalent_objects
;;
let not_a_duplicate u =
(*********************************************************************)
-val not_a_duplicate : string -> bool
+val not_a_duplicate : UriManager.uri -> bool
shellglob)))
let nonvar s =
+ let s = UriManager.string_of_uri s in
let len = String.length s in
let suffix = String.sub s (len-4) 4 in
not (suffix = ".var")
let result = Mysql.exec dbd query in
List.filter nonvar
(Mysql.map result
- (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
+ (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
let match_term ~(dbd:Mysql.dbd) ty =
(* debug_print (CicPp.ppterm ty); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
- MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
+ MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
in
let full_card, diff =
if CicUtil.is_meta_closed ty then
| None -> set
| Some (_, Cic.Decl t)
| Some (_, Cic.Def (t, _)) ->
- Constr.StringSet.union set (Constr.constants_of t))
- Constr.StringSet.empty context
+ Constr.UriManagerSet.union set (Constr.constants_of t))
+ Constr.UriManagerSet.empty context
let intersect uris siguris =
- let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+ let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
let set2 =
- List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+ List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
in
- let inter = Constr.StringSet.inter set1 set2 in
- List.filter (fun s -> Constr.StringSet.mem s inter) uris
+ let inter = Constr.UriManagerSet.inter set1 set2 in
+ List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
let filter_uris_forward ~dbd (main, constants) uris =
let main_uris =
| Some (main, types) -> main :: types
in
let full_signature =
- List.fold_right Constr.StringSet.add main_uris constants
+ List.fold_right Constr.UriManagerSet.add main_uris constants
in
List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
let types_constants =
match main with
- | None -> Constr.StringSet.empty
+ | None -> Constr.UriManagerSet.empty
| Some (main, types) ->
- List.fold_right Constr.StringSet.add (main :: types)
- Constr.StringSet.empty
+ List.fold_right Constr.UriManagerSet.add (main :: types)
+ Constr.UriManagerSet.empty
in
let hyp_constants =
- Constr.StringSet.diff (signature_of_hypothesis context) types_constants
+ Constr.UriManagerSet.diff (signature_of_hypothesis context) types_constants
in
-(* Constr.StringSet.iter debug_print hyp_constants; *)
- let other_constants = Constr.StringSet.union sig_constants hyp_constants in
+(* Constr.UriManagerSet.iter debug_print hyp_constants; *)
+ let other_constants = Constr.UriManagerSet.union sig_constants hyp_constants in
let uris =
- let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+ let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
if ((List.length uris < pow) or (pow <= 0))
then begin
(* debug_print "MetadataQuery: large sig, falling back to old method"; *)
(* debug_print ("STO APPLICANDO " ^ uri); *)
PET.apply_tactic
(PrimitiveTactics.apply_tac
- ~term:(CicUtil.term_of_uri uri))
+ ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri)))
status
in
let goal_list =
of the experimentation we shall make a choice. *)
let close_with_types s metasenv context =
- Constr.StringSet.fold
+ Constr.UriManagerSet.fold
(fun e bag ->
- let t = CicUtil.term_of_uri e in
+ let t = CicUtil.term_of_uri (UriManager.string_of_uri e) in
let ty, _ =
CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
in
- Constr.StringSet.union bag (Constr.constants_of ty))
+ Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
let experimental_hint
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
let types_constants =
match main with
- | None -> Constr.StringSet.empty
+ | None -> Constr.UriManagerSet.empty
| Some (main, types) ->
- List.fold_right Constr.StringSet.add (main :: types)
- Constr.StringSet.empty
+ List.fold_right Constr.UriManagerSet.add (main :: types)
+ Constr.UriManagerSet.empty
in
let all_constants =
let hyp_and_sug =
- Constr.StringSet.union
+ Constr.UriManagerSet.union
(signature_of_hypothesis context)
sig_constants
in
let main =
match main with
- | None -> Constr.StringSet.empty
+ | None -> Constr.UriManagerSet.empty
| Some (main,_) ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+ metasenv context (CicUtil.term_of_uri (UriManager.string_of_uri main)) CicUniv.empty_ugraph
in
Constr.constants_of ty
in
- Constr.StringSet.union main hyp_and_sug
+ Constr.UriManagerSet.union main hyp_and_sug
in
-(* Constr.StringSet.iter debug_print hyp_constants; *)
+(* Constr.UriManagerSet.iter debug_print hyp_constants; *)
let all_constants_closed = close_with_types all_constants metasenv context in
let other_constants =
- Constr.StringSet.diff all_constants_closed types_constants
+ Constr.UriManagerSet.diff all_constants_closed types_constants
in
debug_print "all_constants_closed";
- Constr.StringSet.iter debug_print all_constants_closed;
+ Constr.UriManagerSet.iter debug_print all_constants_closed;
debug_print "other_constants";
- Constr.StringSet.iter debug_print other_constants;
+ Constr.UriManagerSet.iter debug_print other_constants;
let uris =
- let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+ let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
if ((List.length uris < pow) or (pow <= 0))
then begin
debug_print "MetadataQuery: large sig, falling back to old method";
let (subst,(proof, goal_list)) =
(* debug_print ("STO APPLICANDO" ^ uri); *)
PrimitiveTactics.apply_tac_verbose
- ~term:(CicUtil.term_of_uri uri)
+ ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri))
status
in
let goal_list =
let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
let no_full = MetadataDb.count_distinct `Statement metadata in
let is_dummy = function
- | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy"
+ | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
| _ -> true
in
let rec look_for_dummy_main = function
| [] -> None
| `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
- when ((String.sub s 0 10) = "cic:/dummy") ->
+ when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
+ let s = UriManager.string_of_uri s in
let len = String.length s in
let dummy_index = int_of_string (String.sub s 11 (len-11)) in
let dummy_type = List.nth types dummy_index in
in
let compare (_, x) (_, y) = compare x y in
let filter n (uri, rank) =
- if rank > 0 then Some uri else None
+ if rank > 0 then Some (UriManager.uri_of_string uri) else None
in
match get_metadata t with
| None -> []
* is interpreted as 0 or more characters and "?" as exactly one character *)
val locate:
dbd:Mysql.dbd ->
- ?vars:bool -> string -> string list
+ ?vars:bool -> string -> UriManager.uri list
val hint:
dbd:Mysql.dbd ->
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status ->
- (string *
+ (UriManager.uri *
(ProofEngineTypes.proof * ProofEngineTypes.goal list)) list
val experimental_hint:
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status ->
- (string *
+ (UriManager.uri *
((Cic.term -> Cic.term) *
(ProofEngineTypes.proof * ProofEngineTypes.goal list))) list
-val match_term: dbd:Mysql.dbd -> Cic.term -> string list
+val match_term: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
(** @param string is an uri *)
-val elim: dbd:Mysql.dbd -> string -> string list
+val elim: dbd:Mysql.dbd -> UriManager.uri -> UriManager.uri list
-val instance: dbd:Mysql.dbd -> Cic.term -> string list
+val instance: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
-val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> string list
+val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
* "cic:/a/b/c.ind#xpointer(1/1/1)" =>
* [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]
*)
-type uri = string array;;
+
+let fresh_id =
+ let id = ref 0 in
+ function () ->
+ incr id;
+ !id
+
+type uri = string array * int;;
let eq uri1 uri2 =
uri1 == uri2
;;
-let string_of_uri uri =
+let string_of_uri (uri,_) =
match uri.(Array.length uri - 1) with
| "" ->
uri.(Array.length uri - 3)
String.concat "#"
[ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
-let name_of_uri uri = uri.(Array.length uri - 2);;
-let buri_of_uri uri = uri.(Array.length uri - 4);;
-let depth_of_uri uri = Array.length uri - 3;;
+let name_of_uri (uri,_) = uri.(Array.length uri - 2);;
+let buri_of_uri (uri,_) = uri.(Array.length uri - 4);;
+let depth_of_uri (uri,_) = Array.length uri - 3;;
module OrderedStrings =
struct
let set_of_uri = ref SetOfStrings.empty;;
let set_of_prefixes = ref SetOfStrings.empty;;
-
+
(* hash conses an uri *)
let add_to_uriset ?suri uri =
let lookup_suri suri =
SetOfStrings.find str !set_of_uri
with
Not_found ->
- let uri = Array.of_list (mk_prefixes base xpointer) in
+ let uri = Array.of_list (mk_prefixes base xpointer), fresh_id () in
add_to_uriset ~suri:str uri
;;
-let strip_xpointer uri =
+let strip_xpointer (uri,_) =
let stripped_uri = Array.copy uri in
stripped_uri.(Array.length uri - 1) <- ""; (* reset xpointer field *)
- let suri = string_of_uri stripped_uri in
- add_to_uriset ~suri stripped_uri
+ let new_uri = stripped_uri,fresh_id () in
+ let suri = string_of_uri new_uri in
+ add_to_uriset ~suri new_uri
let cicuri_of_uri uri =
if completeuri = newcompleteuri then
uri
else
+ let uri = fst uri in
let newuri = Array.copy uri in
newuri.(Array.length uri - 3) <- newcompleteuri ;
- add_to_uriset newuri
+ add_to_uriset (newuri,fresh_id ())
;;
let annuri_of_uri uri =
if Str.string_match (Str.regexp ".*\\.ann$") completeuri 0 then
uri
else
+ let uri = fst uri in
let newuri = Array.copy uri in
newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ;
- add_to_uriset newuri
+ add_to_uriset (newuri,fresh_id ())
;;
let uri_is_annuri uri =
let bodyuri_of_uri uri =
let struri = string_of_uri uri in
if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then
+ let uri = fst uri in
let newuri = Array.copy uri in
newuri.(Array.length uri - 3) <- struri ^ ".body" ;
- Some (add_to_uriset newuri)
+ Some (add_to_uriset (newuri,fresh_id ()))
else
None
;;
let innertypesuri_of_uri uri =
let cicuri = cicuri_of_uri uri in
- let newuri = Array.copy cicuri in
- newuri.(Array.length cicuri - 3) <- (string_of_uri cicuri) ^ ".types" ;
- add_to_uriset newuri
+ let newuri = Array.copy (fst cicuri) in
+ newuri.(Array.length (fst cicuri) - 3) <- (string_of_uri cicuri) ^ ".types" ;
+ add_to_uriset (newuri,fresh_id ())
;;
type uriref = uri * (int list)
| [t] -> str ^ xp t ^ ")"
| t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"
-let compare u1 u2 =
- let su1 = string_of_uri u1 in
- let su2 = string_of_uri u2 in
- Pervasives.compare su1 su2
+let compare (_,id1) (_,id2) = id1 - id2
module OrderedUri =
struct
projects / helm.git / commitdiff