aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/wg_Completion.ml12
-rw-r--r--lib/system.ml25
-rw-r--r--library/libnames.ml3
-rw-r--r--library/libnames.mli4
-rw-r--r--pretyping/coercionops.ml12
-rw-r--r--printing/proof_diffs.ml40
-rw-r--r--printing/proof_diffs.mli9
-rw-r--r--proofs/goal.ml2
-rw-r--r--vernac/library.ml47
9 files changed, 54 insertions, 100 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index dcb71d96a1..a7f8c70499 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -8,17 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module StringOrd =
-struct
- type t = string
- let compare s1 s2 =
- (* we use first size, then usual comparison *)
- let d = String.length s1 - String.length s2 in
- if d <> 0 then d
- else compare s1 s2
-end
-
-module Proposals = Set.Make(StringOrd)
+module Proposals = CString.Set
(** Retrieve completion proposals in the buffer *)
let get_syntactic_completion (buffer : GText.buffer) pattern accu =
diff --git a/lib/system.ml b/lib/system.ml
index 68410e322a..d7f5fa26ab 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -11,7 +11,6 @@
(* $Id$ *)
open Pp
-open Util
include Minisys
@@ -42,15 +41,7 @@ let all_subdirs ~unix_path:root =
(* Caching directory contents for efficient syntactic equality of file
names even on case-preserving but case-insensitive file systems *)
-module StrMod = struct
- type t = string
- let compare = compare
-end
-
-module StrMap = Map.Make(StrMod)
-module StrSet = Set.Make(StrMod)
-
-let dirmap = ref StrMap.empty
+let dirmap = ref CString.Map.empty
let make_dir_table dir =
let entries =
@@ -59,8 +50,8 @@ let make_dir_table dir =
with Sys_error _ ->
warn_cannot_open_dir dir;
[||] in
- let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
- Array.fold_left filter_dotfiles StrSet.empty entries
+ let filter_dotfiles s f = if f.[0] = '.' then s else CString.Set.add f s in
+ Array.fold_left filter_dotfiles CString.Set.empty entries
(** Don't trust in interactive mode (the default) *)
let trust_file_cache = ref false
@@ -68,20 +59,20 @@ let trust_file_cache = ref false
let exists_in_dir_respecting_case dir bf =
let cache_dir dir =
let contents = make_dir_table dir in
- dirmap := StrMap.add dir contents !dirmap;
+ dirmap := CString.Map.add dir contents !dirmap;
contents in
let contents, fresh =
try
(* in batch mode, assume the directory content is still fresh *)
- StrMap.find dir !dirmap, !trust_file_cache
+ CString.Map.find dir !dirmap, !trust_file_cache
with Not_found ->
(* in batch mode, we are not yet sure the directory exists *)
- if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true
+ if !trust_file_cache && not (exists_dir dir) then CString.Set.empty, true
else cache_dir dir, true in
- StrSet.mem bf contents ||
+ CString.Set.mem bf contents ||
not fresh &&
(* rescan, there is a new file we don't know about *)
- StrSet.mem bf (cache_dir dir)
+ CString.Set.mem bf (cache_dir dir)
let file_exists_respecting_case path f =
(* This function ensures that a file with expected lowercase/uppercase
diff --git a/library/libnames.ml b/library/libnames.ml
index 6f55a8dc3d..88b2e41855 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -78,9 +78,6 @@ let dirpath_of_string s =
in
DirPath.make path
-module Dirset = Set.Make(DirPath)
-module Dirmap = Map.Make(DirPath)
-
(*s Section paths are absolute names *)
type full_path = {
diff --git a/library/libnames.mli b/library/libnames.mli
index 23792e54c2..a384510879 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Names
(** {6 Dirpaths } *)
@@ -34,9 +33,6 @@ val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool
-module Dirset : Set.S with type elt = DirPath.t
-module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
-
(** {6 Full paths are {e absolute} paths of declarations } *)
type full_path
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index d6458e1409..49401a9937 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -67,8 +67,6 @@ end
module ClTypMap = Map.Make(ClTyp)
-module IntMap = Map.Make(Int)
-
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type inheritance_path = coe_info_typ list
@@ -97,13 +95,13 @@ struct
module Index = struct include Int let print = Pp.int end
- type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
- let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
+ type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
+ let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = IntMap.find x b.v
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
+ let map x b = Int.Map.find x b.v
+ let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let add x y b =
- { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
+ { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index fb91ea7b5c..d73d1f2d1a 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -85,8 +85,6 @@ let log_out_ch = ref stdout
let cprintf s = cfprintf !log_out_ch s
[@@@ocaml.warning "+32"]
-module StringMap = Map.Make(String);;
-
let tokenize_string s =
(* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too.
But I don't understand how it's used--it looks like things get appended to it but
@@ -124,22 +122,22 @@ type hyp_info = {
let diff_hyps o_line_idents o_map n_line_idents n_map =
let rv : Pp.t list ref = ref [] in
- let is_done ident map = (StringMap.find ident map).done_ in
+ let is_done ident map = (CString.Map.find ident map).done_ in
let exists ident map =
- try let _ = StringMap.find ident map in true
+ try let _ = CString.Map.find ident map in true
with Not_found -> false in
let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in
let output old_ids_uo new_ids =
(* use the order from the old line in case it's changed in the new *)
let old_ids = if old_ids_uo = [] then [] else
- let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
+ let orig = (CString.Map.find (List.hd old_ids_uo) o_map).idents in
List.concat (List.map (contains orig) old_ids_uo)
in
let setup ids map = if ids = [] then ("", Pp.mt ()) else
let open Pp in
- let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in
+ let rhs_pp = (CString.Map.find (List.hd ids) map).rhs_pp in
let pp_ids = List.map (fun x -> str x) ids in
let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in
(string_of_ppcmds hyp_pp, hyp_pp)
@@ -151,11 +149,11 @@ let diff_hyps o_line_idents o_map n_line_idents n_map =
let hyp_diffs = diff_str ~tokenize_string o_line n_line in
let (has_added, has_removed) = has_changes hyp_diffs in
if show_removed () && has_removed then begin
- List.iter (fun x -> (StringMap.find x o_map).done_ <- true) old_ids;
+ List.iter (fun x -> (CString.Map.find x o_map).done_ <- true) old_ids;
rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
end;
if n_line <> "" then begin
- List.iter (fun x -> (StringMap.find x n_map).done_ <- true) new_ids;
+ List.iter (fun x -> (CString.Map.find x n_map).done_ <- true) new_ids;
rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
end
in
@@ -166,14 +164,14 @@ let diff_hyps o_line_idents o_map n_line_idents n_map =
match dtype with
| `Removed ->
if dtype = `Removed then begin
- let o_idents = (StringMap.find ident o_map).idents in
+ let o_idents = (CString.Map.find ident o_map).idents in
(* only show lines that have all idents removed here; other removed idents appear later *)
if show_removed () && not (is_done ident o_map) &&
List.for_all (fun x -> not (exists x n_map)) o_idents then
output (List.rev o_idents) []
end
| _ -> begin (* Added or Common case *)
- let n_idents = (StringMap.find ident n_map).idents in
+ let n_idents = (CString.Map.find ident n_map).idents in
(* Process a new hyp line, possibly splitting it. Duplicates some of
process_ident iteration, but easier to understand this way *)
@@ -184,13 +182,13 @@ let diff_hyps o_line_idents o_map n_line_idents n_map =
let fst_omap_idents = ref None in
let add ids id map =
ids := id :: !ids;
- (StringMap.find id map).done_ <- true in
+ (CString.Map.find id map).done_ <- true in
(* get identifiers shared by one old and one new line, plus
other Added in new and other Removed in old *)
let process_split ident3 =
if not (is_done ident3 n_map) then begin
- let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+ let this_omap_idents = try Some (CString.Map.find ident3 o_map).idents
with Not_found -> None in
if !fst_omap_idents = None then
fst_omap_idents := this_omap_idents;
@@ -290,7 +288,7 @@ map will contain:
concl_pp is the conclusion as a Pp.t
*)
let goal_info goal sigma =
- let map = ref StringMap.empty in
+ let map = ref CString.Map.empty in
let line_idents = ref [] in
let build_hyp_info env sigma hyp =
let (names, body, ty) = hyp in
@@ -308,7 +306,7 @@ let goal_info goal sigma =
let rhs_pp = mid ++ str " : " ++ ts in
let make_entry () = { idents; rhs_pp; done_ = false } in
- List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+ List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents
in
try
@@ -339,7 +337,7 @@ let unwrap g_s =
let goal = Evd.sig_it g_s in
let sigma = Refiner.project g_s in
goal_info goal sigma
- | None -> ([], StringMap.empty, Pp.mt ())
+ | None -> ([], CString.Map.empty, Pp.mt ())
let diff_goal_ide og_s ng nsigma =
diff_goal_info (unwrap og_s) (goal_info ng nsigma)
@@ -405,7 +403,7 @@ the call to db_goal_map and entering the following:
(conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof
*)
let match_goals ot nt =
- let nevar_to_oevar = ref StringMap.empty in
+ let nevar_to_oevar = ref CString.Map.empty in
(* ogname is "" when there is no difference on the current path.
It's set to the old goal's evar name once a rewritten goal is found,
at which point the code only searches for the replacing goals
@@ -514,7 +512,7 @@ let match_goals ot nt =
| CPatVar _, CPatVar _ -> ()
| CEvar (n,l), CEvar (n2,l2) ->
let oevar = if ogname = "" then Id.to_string n else ogname in
- nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar;
+ nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar;
iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2
| CEvar (n,l), nt' ->
(* pass down the old goal evar name *)
@@ -641,16 +639,16 @@ let make_goal_map_i op np =
(* >= 2 removals, >= 1 addition, need to match *)
let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
- let oevar_to_og = ref StringMap.empty in
+ let oevar_to_og = ref CString.Map.empty in
let Proof.{sigma=osigma} = Proof.data op in
- List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
+ List.iter (fun og -> oevar_to_og := CString.Map.add (goal_to_evar og osigma) og !oevar_to_og)
(Goal.Set.elements rem_gs);
let Proof.{sigma=nsigma} = Proof.data np in
let get_og ng =
let nevar = goal_to_evar ng nsigma in
- let oevar = StringMap.find nevar nevar_to_oevar in
- let og = StringMap.find oevar !oevar_to_og in
+ let oevar = CString.Map.find nevar nevar_to_oevar in
+ let og = CString.Map.find oevar !oevar_to_og in
og
in
Goal.Set.iter (fun ng ->
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 83e721d3d5..24b171770a 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -83,11 +83,4 @@ type hyp_info = {
mutable done_: bool;
}
-module StringMap :
-sig
- type +'a t
- val empty: hyp_info t
- val add : string -> hyp_info -> hyp_info t -> hyp_info t
-end
-
-val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
+val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
diff --git a/proofs/goal.ml b/proofs/goal.ml
index ede68e63b9..b1f8fd3e97 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -131,4 +131,4 @@ module V82 = struct
end
-module Set = Set.Make(struct type t = goal let compare = Evar.compare end)
+module Set = Evar.Set
diff --git a/vernac/library.ml b/vernac/library.ml
index 85645b92d4..7c629b08e7 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -103,17 +103,13 @@ type library_summary = {
libsum_digests : Safe_typing.vodigest;
}
-module LibraryOrdered = DirPath
-module LibraryMap = Map.Make(LibraryOrdered)
-module LibraryFilenameMap = Map.Make(LibraryOrdered)
-
(* This is a map from names to loaded libraries *)
-let libraries_table : library_summary LibraryMap.t ref =
- Summary.ref LibraryMap.empty ~name:"LIBRARY"
+let libraries_table : library_summary DPmap.t ref =
+ Summary.ref DPmap.empty ~name:"LIBRARY"
(* This is the map of loaded libraries filename *)
(* (not synchronized so as not to be caught in the states on disk) *)
-let libraries_filename_table = ref LibraryFilenameMap.empty
+let libraries_filename_table = ref DPmap.empty
(* These are the _ordered_ sets of loaded, imported and exported libraries *)
let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
@@ -121,7 +117,7 @@ let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
(* various requests to the tables *)
let find_library dir =
- LibraryMap.find dir !libraries_table
+ DPmap.find dir !libraries_table
let try_find_library dir =
try find_library dir
@@ -133,16 +129,16 @@ let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
(* from a previous play of the session *)
libraries_filename_table :=
- LibraryFilenameMap.add dir f !libraries_filename_table
+ DPmap.add dir f !libraries_filename_table
let library_full_filename dir =
- try LibraryFilenameMap.find dir !libraries_filename_table
+ try DPmap.find dir !libraries_filename_table
with Not_found -> "<unavailable filename>"
let overwrite_library_filenames f =
let f =
if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
- LibraryMap.iter (fun dir _ -> register_library_filename dir f)
+ DPmap.iter (fun dir _ -> register_library_filename dir f)
!libraries_table
let library_is_loaded dir =
@@ -167,7 +163,7 @@ let register_loaded_library m =
| m'::_ as l when DirPath.equal m' libname -> l
| m'::l' -> m' :: aux l' in
libraries_loaded_list := aux !libraries_loaded_list;
- libraries_table := LibraryMap.add libname m !libraries_table
+ libraries_table := DPmap.add libname m !libraries_table
let loaded_libraries () = !libraries_loaded_list
@@ -187,13 +183,13 @@ type 'a table_status =
| Fetched of 'a array
let opaque_tables =
- ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
+ ref (DPmap.empty : (Opaqueproof.opaque_proofterm table_status) DPmap.t)
let add_opaque_table dp st =
- opaque_tables := LibraryMap.add dp st !opaque_tables
+ opaque_tables := DPmap.add dp st !opaque_tables
let access_table what tables dp i =
- let t = match LibraryMap.find dp !tables with
+ let t = match DPmap.find dp !tables with
| Fetched t -> t
| ToFetch f ->
let dir_path = Names.DirPath.to_string dp in
@@ -206,7 +202,7 @@ let access_table what tables dp i =
str ") is inaccessible or corrupted,\ncannot load some " ++
str what ++ str " in it.\n")
in
- tables := LibraryMap.add dp (Fetched t) !tables;
+ tables := DPmap.add dp (Fetched t) !tables;
t
in
assert (i < Array.length t); t.(i)
@@ -261,14 +257,12 @@ let intern_from_file f =
| Some (_,false) ->
mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
-module DPMap = Map.Make(DirPath)
-
let rec intern_library ~lib_resolver (needed, contents) (dir, f) from =
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
(* Look if already listed and consequently its dependencies too *)
- try (DPMap.find dir contents).library_digests, (needed, contents)
+ try (DPmap.find dir contents).library_digests, (needed, contents)
with Not_found ->
Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
@@ -286,7 +280,7 @@ and intern_library_deps ~lib_resolver libs dir m from =
let needed, contents =
Array.fold_left (intern_mandatory_library ~lib_resolver dir from)
libs m.library_deps in
- (dir :: needed, DPMap.add dir m contents )
+ (dir :: needed, DPmap.add dir m contents )
and intern_mandatory_library ~lib_resolver caller from libs (dir,d) =
let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in
@@ -372,8 +366,8 @@ let warn_require_in_module =
strbrk "and optionally Import it inside another one.")
let require_library_from_dirpath ~lib_resolver modrefl export =
- let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in
- let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
+ let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in
+ let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in
let modrefl = List.map fst modrefl in
if Lib.is_module_or_modtype () then
begin
@@ -500,14 +494,11 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
let save_library_raw f sum lib univs proofs =
save_library_base f sum lib (Some univs) None proofs
-module StringOrd = struct type t = string let compare = String.compare end
-module StringSet = Set.Make(StringOrd)
-
let get_used_load_paths () =
- StringSet.elements
- (List.fold_left (fun acc m -> StringSet.add
+ String.Set.elements
+ (List.fold_left (fun acc m -> String.Set.add
(Filename.dirname (library_full_filename m)) acc)
- StringSet.empty !libraries_loaded_list)
+ String.Set.empty !libraries_loaded_list)
let _ = Nativelib.get_load_paths := get_used_load_paths
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:49:46 +0000