From a7b90d2494f7d580faa54ecd2835bd4649129763 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jun 2005 13:05:08 +0000 Subject: [PATCH] many strings that are supposed to be URIs are now UriManager.uri --- helm/matita/matita.ml | 4 +- helm/matita/matitaDisambiguator.ml | 2 +- helm/matita/matitaDisambiguator.mli | 2 +- helm/matita/matitaGui.ml | 7 +- helm/matita/matitaMathView.ml | 8 +- helm/matita/matitaScript.ml | 6 +- helm/matita/matitaScript.mli | 2 +- helm/matita/matitaTypes.ml | 9 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +- .../cic_disambiguation/disambiguateTypes.ml | 3 +- .../cic_disambiguation/disambiguateTypes.mli | 3 +- helm/ocaml/metadata/metadataConstraints.ml | 139 +++++----- helm/ocaml/metadata/metadataConstraints.mli | 21 +- helm/ocaml/metadata/metadataDb.ml | 14 +- helm/ocaml/metadata/metadataExtractor.ml | 23 +- helm/ocaml/metadata/metadataExtractor.mli | 2 +- helm/ocaml/metadata/metadataPp.ml | 6 +- helm/ocaml/metadata/metadataPp.mli | 2 +- helm/ocaml/metadata/metadataTypes.ml | 4 +- helm/ocaml/metadata/metadataTypes.mli | 4 +- helm/ocaml/tactics/fwdSimplTactic.ml | 2 +- helm/ocaml/tactics/hashtbl_equiv.ml | 254 +++++++++--------- helm/ocaml/tactics/hashtbl_equiv.mli | 2 +- helm/ocaml/tactics/metadataQuery.ml | 74 ++--- helm/ocaml/tactics/metadataQuery.mli | 14 +- helm/ocaml/urimanager/uriManager.ml | 48 ++-- 26 files changed, 342 insertions(+), 321 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6c3459c4a..34b41e4cc 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -92,7 +92,7 @@ let _ = 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; @@ -192,7 +192,7 @@ let _ = 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 diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index f6db501b3..e286fb550 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -29,7 +29,7 @@ open MatitaTypes 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 diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 6d251cc7a..740de989e 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -29,7 +29,7 @@ open MatitaTypes * 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 diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index cdbfc799a..8915f7681 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -402,6 +402,7 @@ let instance = singleton gui 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 @@ -446,7 +447,7 @@ let interactive_uri_choice | _ -> ())); 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; @@ -464,11 +465,11 @@ let interactive_uri_choice 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 (); diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 9c8ef985b..776a9ada5 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -407,7 +407,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 () @@ -476,10 +476,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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 @@ -583,7 +583,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 26a0f2487..c7859a7c7 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -169,7 +169,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text 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 @@ -195,7 +195,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text (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 = @@ -207,7 +207,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_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) -> diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index df3ec4e1e..b6b3d8ae2 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -65,7 +65,7 @@ val script: buffer:GText.buffer -> init:MatitaTypes.status -> mathviewer: MatitaTypes.mathViewer-> - urichooser: (string list -> string list) -> + urichooser: (UriManager.uri list -> UriManager.uri list) -> unit -> script diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index d7dc383b7..580f022f5 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -150,8 +150,8 @@ type mathViewer_entry = | `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 @@ -160,7 +160,8 @@ 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 @@ -177,6 +178,6 @@ class type mathViewer = *) 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 diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 2f9bb97a5..27122ef1d 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -622,7 +622,7 @@ module Make (C: Callbacks) = 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] | _ -> @@ -635,12 +635,12 @@ module Make (C: Callbacks) = 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 diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 078297a26..64fcdb5a8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -62,7 +62,8 @@ module type Callbacks = 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: diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index bd9ba5e99..89d529015 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -48,7 +48,8 @@ module type Callbacks = 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 diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 15177ddb1..fb2a49424 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -29,10 +29,10 @@ open MetadataTypes 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 @@ -122,7 +122,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = | `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]) @ @@ -166,7 +166,7 @@ let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) = (* 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 @@ -201,19 +201,22 @@ let at_least (** 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) @@ -221,11 +224,11 @@ let rec inspect_children n childs = 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 @@ -236,13 +239,13 @@ and inspect_conclusion n t = | 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) @@ -251,13 +254,13 @@ and 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 @@ -279,37 +282,37 @@ let rec inspect_term n t = | 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 @@ -318,7 +321,7 @@ let rec inspect_term n t = 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 @@ -328,7 +331,7 @@ let add_cardinality s = 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) @@ -342,8 +345,8 @@ let prefixes n t = 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 *) @@ -352,61 +355,61 @@ and signature_concl = 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 @@ -432,7 +435,7 @@ let must_of_prefix ?(where = `Conclusion) m s = 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 ] @@ -452,37 +455,37 @@ let get_constants (dbd:Mysql.dbd) ~where uri = 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 @@ -538,13 +541,13 @@ let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = | 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 | _, _ -> []) @@ -574,7 +577,7 @@ let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = | _, _ -> []) 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 -> @@ -583,7 +586,7 @@ let power_upto upto consts = [(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)) @@ -596,7 +599,7 @@ let sigmatch ~(dbd:Mysql.dbd) 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 @@ -604,7 +607,7 @@ let sigmatch ~(dbd:Mysql.dbd) 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 diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index 0d6655741..4f84ce9a7 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -23,23 +23,24 @@ * http://helm.cs.unibo.it/ *) -module StringSet : Set.S with type elt = string +module UriManagerSet : Set.S with type elt = UriManager.uri + (** @return * 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 *) @@ -49,7 +50,7 @@ val sigmatch: ?facts:bool -> ?where:where -> term_signature -> - (int * string) list + (int * UriManager.uri) list (** {2 Constraint engine} *) @@ -83,13 +84,13 @@ val at_least: ?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 -> @@ -103,8 +104,8 @@ val exec: 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 diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index d82894ed6..51b432a4f 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -74,27 +74,27 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) = 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 @@ -119,13 +119,13 @@ let insert_const_no dbd (uri,metadata) = 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) diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index a1c24d9c6..5a7522b90 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -56,7 +56,7 @@ module OrderedMetadata = end module MetadataSet = Set.Make (OrderedMetadata) -module StringSet = Set.Make (String) +module UriManagerSet = UriManager.UriSet module S = MetadataSet @@ -72,6 +72,9 @@ let var_has_body uri = | 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 -> @@ -130,17 +133,17 @@ let compute_term pos term = (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 @@ -241,13 +244,13 @@ let compute_metas term = 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 @@ -268,14 +271,14 @@ let compute (pos:position) ~body ~ty = 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 @@ -321,7 +324,7 @@ let compute_obj uri = S.empty params in - [ UriManager.string_of_uri uri, + [ uri, UriManager.name_of_uri uri, S.union metadata var_metadata ] | Cic.InductiveDefinition (types, params, _, _) -> diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli index 8308c0ee0..68af269a9 100644 --- a/helm/ocaml/metadata/metadataExtractor.mli +++ b/helm/ocaml/metadata/metadataExtractor.mli @@ -31,7 +31,7 @@ val compute: (** @return tuples *) 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 diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index fdbbaf071..acf425ce1 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -71,8 +71,8 @@ type t = [ `Int of int | `String of string | `Null ] 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 @@ -102,7 +102,7 @@ let pp_constr = (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) = diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index d9ef885ed..cffb24c48 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -38,7 +38,7 @@ type t = (** @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 (* diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 334553083..81eb35817 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -56,13 +56,13 @@ type pi_depth = int 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 diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli index 5a2456de1..f86ff84f5 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -53,13 +53,13 @@ type pi_depth = int 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 diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index c1a5347f4..7981ac875 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -82,6 +82,6 @@ let fwd_simpl_tac ~hyp ~dbd = 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 diff --git a/helm/ocaml/tactics/hashtbl_equiv.ml b/helm/ocaml/tactics/hashtbl_equiv.ml index b489e089a..543528de6 100644 --- a/helm/ocaml/tactics/hashtbl_equiv.ml +++ b/helm/ocaml/tactics/hashtbl_equiv.ml @@ -41,144 +41,144 @@ 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 = diff --git a/helm/ocaml/tactics/hashtbl_equiv.mli b/helm/ocaml/tactics/hashtbl_equiv.mli index 723e6831b..d2608b862 100644 --- a/helm/ocaml/tactics/hashtbl_equiv.mli +++ b/helm/ocaml/tactics/hashtbl_equiv.mli @@ -34,5 +34,5 @@ (*********************************************************************) -val not_a_duplicate : string -> bool +val not_a_duplicate : UriManager.uri -> bool diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 1e7bbe690..644e764ef 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -44,6 +44,7 @@ let sqlpat_of_shellglob = 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") @@ -59,13 +60,13 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = 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 @@ -113,16 +114,16 @@ let signature_of_hypothesis context = | 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 = @@ -131,7 +132,7 @@ let filter_uris_forward ~dbd (main, constants) 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 @@ -182,18 +183,18 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = 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"; *) @@ -210,7 +211,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = (* 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 = @@ -239,13 +240,13 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = 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 @@ -263,40 +264,40 @@ 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"; @@ -312,7 +313,7 @@ let experimental_hint 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 = @@ -366,13 +367,14 @@ let instance ~dbd t = 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 @@ -496,7 +498,7 @@ let fwd_simpl ~dbd t = 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 -> [] diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 035f3ae73..e8f81a438 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -29,14 +29,14 @@ * 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: @@ -44,16 +44,16 @@ 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 diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 0697fb73b..4eae6799d 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -30,13 +30,20 @@ * "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) @@ -44,9 +51,9 @@ let string_of_uri uri = 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 @@ -63,7 +70,7 @@ module SetOfStrings = Map.Make(OrderedStrings);; 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 = @@ -131,15 +138,16 @@ let uri_of_string str = 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 = @@ -151,9 +159,10 @@ 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 = @@ -161,9 +170,10 @@ 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 = @@ -173,18 +183,19 @@ 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) @@ -197,10 +208,7 @@ let string_of_uriref (uri, fi) = | [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 -- 2.39.2