aboutsummaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
Diffstat (limited to 'clib')
-rw-r--r--clib/backtrace.ml4
-rw-r--r--clib/bigint.mli1
-rw-r--r--clib/cArray.ml10
-rw-r--r--clib/cSig.mli1
-rw-r--r--clib/cString.mli4
-rw-r--r--clib/dune2
-rw-r--r--clib/dyn.ml22
-rw-r--r--clib/dyn.mli6
-rw-r--r--clib/exninfo.ml22
-rw-r--r--clib/hMap.ml6
-rw-r--r--clib/hMap.mli1
-rw-r--r--clib/hashcons.mli9
-rw-r--r--clib/hashset.mli5
-rw-r--r--clib/int.ml11
-rw-r--r--clib/int.mli3
-rw-r--r--clib/segmenttree.ml38
-rw-r--r--clib/store.ml83
-rw-r--r--clib/store.mli9
-rw-r--r--clib/trie.ml2
19 files changed, 126 insertions, 113 deletions
diff --git a/clib/backtrace.ml b/clib/backtrace.ml
index 27ed6fbf72..64faa5fd2e 100644
--- a/clib/backtrace.ml
+++ b/clib/backtrace.ml
@@ -87,8 +87,8 @@ let get_backtrace e =
let add_backtrace e =
if !is_recording then
- (** This must be the first function call, otherwise the stack may be
- destroyed *)
+ (* This must be the first function call, otherwise the stack may be
+ destroyed *)
let current = get_exception_backtrace () in
let info = Exninfo.info e in
begin match current with
diff --git a/clib/bigint.mli b/clib/bigint.mli
index ac66b41fb7..88297c353d 100644
--- a/clib/bigint.mli
+++ b/clib/bigint.mli
@@ -25,6 +25,7 @@ val one : bigint
val two : bigint
val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *)
+
val add_1 : bigint -> bigint
val sub_1 : bigint -> bigint
val mult_2 : bigint -> bigint
diff --git a/clib/cArray.ml b/clib/cArray.ml
index c3a693ff16..e0a1859184 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -451,7 +451,7 @@ struct
end
done;
if !i < len then begin
- (** The array is not the same as the original one *)
+ (* The array is not the same as the original one *)
let ans : 'a array = Array.copy ar in
let v = match !temp with None -> assert false | Some x -> x in
Array.unsafe_set ans !i v;
@@ -483,7 +483,7 @@ struct
end
done;
if !i < len then begin
- (** The array is not the same as the original one *)
+ (* The array is not the same as the original one *)
let ans : 'a array = Array.copy ar in
let v = match !temp with None -> assert false | Some x -> x in
Array.unsafe_set ans !i v;
@@ -504,7 +504,7 @@ struct
let i = ref 0 in
let break = ref true in
let r = ref accu in
- (** This variable is never accessed unset *)
+ (* This variable is never accessed unset *)
let temp = ref None in
while !break && (!i < len) do
let v = Array.unsafe_get ar !i in
@@ -539,7 +539,7 @@ struct
let i = ref 0 in
let break = ref true in
let r = ref accu in
- (** This variable is never accessed unset *)
+ (* This variable is never accessed unset *)
let temp = ref None in
while !break && (!i < len) do
let v = Array.unsafe_get ar !i in
@@ -620,7 +620,7 @@ struct
end
done;
if !i < len then begin
- (** The array is not the same as the original one *)
+ (* The array is not the same as the original one *)
let ans : 'a array = Array.copy ar in
let v = match !temp with None -> assert false | Some x -> x in
Array.unsafe_set ans !i v;
diff --git a/clib/cSig.mli b/clib/cSig.mli
index fb36cc5b51..859018ca4b 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -83,6 +83,7 @@ sig
val choose: 'a t -> (key * 'a)
val split: key -> 'a t -> 'a t * 'a option * 'a t
val find: key -> 'a t -> 'a
+ val find_opt : key -> 'a t -> 'a option
val map: ('a -> 'b) -> 'a t -> 'b t
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
end
diff --git a/clib/cString.mli b/clib/cString.mli
index a73c2729d0..364b6a34b1 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -31,8 +31,8 @@ sig
(** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *)
val strip : string -> string
- (** Alias for [String.trim] *)
[@@ocaml.deprecated "Use [trim]"]
+ (** Alias for [String.trim] *)
val drop_simple_quotes : string -> string
(** Remove the eventual first surrounding simple quotes of a string. *)
@@ -53,8 +53,8 @@ sig
(** Generate the ordinal number in English. *)
val split : char -> string -> string list
- (** [split c s] alias of [String.split_on_char] *)
[@@ocaml.deprecated "Use [split_on_char]"]
+ (** [split c s] alias of [String.split_on_char] *)
val is_sub : string -> string -> int -> bool
(** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
diff --git a/clib/dune b/clib/dune
index 689a955ab7..10c75d6aa2 100644
--- a/clib/dune
+++ b/clib/dune
@@ -4,5 +4,5 @@
(public_name coq.clib)
(wrapped false)
(modules_without_implementation cSig)
- (libraries threads str unix dynlink))
+ (libraries str unix threads))
diff --git a/clib/dyn.ml b/clib/dyn.ml
index 6c45767246..22c49706be 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -38,6 +38,7 @@ sig
type t = Dyn : 'a tag * 'a -> t
val create : string -> 'a tag
+ val anonymous : int -> 'a tag
val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
val repr : 'a tag -> string
@@ -81,15 +82,22 @@ module Self : PreS = struct
let create (s : string) =
let hash = Hashtbl.hash s in
- let () =
- if Int.Map.mem hash !dyntab then
- let old = Int.Map.find hash !dyntab in
- let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
- assert false
- in
- let () = dyntab := Int.Map.add hash s !dyntab in
+ if Int.Map.mem hash !dyntab then begin
+ let old = Int.Map.find hash !dyntab in
+ Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old;
+ assert false
+ end;
+ dyntab := Int.Map.add hash s !dyntab;
hash
+ let anonymous n =
+ if Int.Map.mem n !dyntab then begin
+ Printf.eprintf "Dynamic tag collision: %d\n%!" n;
+ assert false
+ end;
+ dyntab := Int.Map.add n "<anonymous>" !dyntab;
+ n
+
let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
diff --git a/clib/dyn.mli b/clib/dyn.mli
index ff9762bd6b..1bd78b2db8 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -48,6 +48,12 @@ sig
Type names are hashed, so [create] may raise even if no type with
the exact same name was registered due to a collision. *)
+ val anonymous : int -> 'a tag
+ (** [anonymous i] returns a tag describing an [i]-th anonymous type.
+ If [anonymous] is not used together with [create], [max_int] anonymous types
+ are available.
+ [anonymous] raises an exception if [i] is already registered. *)
+
val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
(** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *)
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 2d13049882..78ebd81f7e 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -89,18 +89,18 @@ let find_and_remove () =
let info e =
let (src, data) = find_and_remove () in
if src == e then
- (** Slightly unsound, some exceptions may not be unique up to pointer
- equality. Though, it should be quite exceptional to be in a situation
- where the following holds:
-
- 1. An argument-free exception is raised through the enriched {!raise};
- 2. It is not captured by any enriched with-clause (which would reset
- the current data);
- 3. The same exception is raised through the standard raise, accessing
- the wrong data.
+ (* Slightly unsound, some exceptions may not be unique up to pointer
+ equality. Though, it should be quite exceptional to be in a situation
+ where the following holds:
+
+ 1. An argument-free exception is raised through the enriched {!raise};
+ 2. It is not captured by any enriched with-clause (which would reset
+ the current data);
+ 3. The same exception is raised through the standard raise, accessing
+ the wrong data.
. *)
data
else
- (** Mismatch: the raised exception is not the one stored, either because the
- previous raise was not instrumented, or because something went wrong. *)
+ (* Mismatch: the raised exception is not the one stored, either because the
+ previous raise was not instrumented, or because something went wrong. *)
Store.empty
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 9c80398e4d..5d634b7af0 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -353,6 +353,12 @@ struct
let m = Int.Map.find h s in
Map.find k m
+ let find_opt k s =
+ let h = M.hash k in
+ match Int.Map.find_opt h s with
+ | None -> None
+ | Some m -> Map.find_opt k m
+
let get k s = try find k s with Not_found -> assert false
let split k s = assert false (** Cannot be implemented efficiently *)
diff --git a/clib/hMap.mli b/clib/hMap.mli
index b26d0e04e3..ab2a6bbf15 100644
--- a/clib/hMap.mli
+++ b/clib/hMap.mli
@@ -13,6 +13,7 @@ sig
type t
val compare : t -> t -> int
(** Total ordering *)
+
val hash : t -> int
(** Hashing function compatible with [compare], i.e. [compare x y = 0] implies
[hash x = hash y]. *)
diff --git a/clib/hashcons.mli b/clib/hashcons.mli
index 223dd2a4d2..e97708cdf3 100644
--- a/clib/hashcons.mli
+++ b/clib/hashcons.mli
@@ -29,17 +29,21 @@ module type HashconsedType =
type t
(** Type of objects to hashcons. *)
+
type u
(** Type of hashcons functions for the sub-structures contained in [t].
Usually a tuple of functions. *)
+
val hashcons : u -> t -> t
(** The actual hashconsing function, using its fist argument to recursively
hashcons substructures. It should be compatible with [eq], that is
[eq x (hashcons f x) = true]. *)
+
val eq : t -> t -> bool
(** A comparison function. It is allowed to use physical equality
on the sub-terms hashconsed by the [hashcons] function, but it should be
insensible to shallow copy of the compared object. *)
+
val hash : t -> int
(** A hash function passed to the underlying hashtable structure. [hash]
should be compatible with [eq], i.e. if [eq x y = true] then
@@ -50,14 +54,19 @@ module type S =
sig
type t
(** Type of objects to hashcons. *)
+
type u
(** Type of hashcons functions for the sub-structures contained in [t]. *)
+
type table
(** Type of hashconsing tables *)
+
val generate : u -> table
(** This create a hashtable of the hashconsed objects. *)
+
val hcons : table -> t -> t
(** Perform the hashconsing of the given object within the table. *)
+
val stats : table -> Hashset.statistics
(** Recover statistics of the hashconsing table. *)
end
diff --git a/clib/hashset.mli b/clib/hashset.mli
index 0699d4e848..6ed93d5fe7 100644
--- a/clib/hashset.mli
+++ b/clib/hashset.mli
@@ -31,18 +31,23 @@ type statistics = {
module type S = sig
type elt
(** Type of hashsets elements. *)
+
type t
(** Type of hashsets. *)
+
val create : int -> t
(** [create n] creates a fresh hashset with initial size [n]. *)
+
val clear : t -> unit
(** Clear the contents of a hashset. *)
+
val repr : int -> elt -> t -> elt
(** [repr key constr set] uses [key] to look for [constr]
in the hashet [set]. If [constr] is in [set], returns the
specific representation that is stored in [set]. Otherwise,
[constr] is stored in [set] and will be used as the canonical
representation of this value in the future. *)
+
val stats : t -> statistics
(** Recover statistics on the table. *)
end
diff --git a/clib/int.ml b/clib/int.ml
index 3ae836aec9..3924c152d6 100644
--- a/clib/int.ml
+++ b/clib/int.ml
@@ -41,6 +41,13 @@ struct
if i < k then find i l
else if i = k then v
else find i r
+
+ let rec find_opt i s = match map_prj s with
+ | MEmpty -> None
+ | MNode (l, k, v, r, h) ->
+ if i < k then find_opt i l
+ else if i = k then Some v
+ else find_opt i r
end
module List = struct
@@ -114,8 +121,8 @@ struct
let () = t := DSet (i, old, res) in
res
else match v with
- | None -> t (** Nothing to do! *)
- | Some _ -> (** we must resize *)
+ | None -> t (* Nothing to do! *)
+ | Some _ -> (* we must resize *)
let nlen = next len (succ i) in
let nlen = min nlen Sys.max_array_length in
let () = assert (i < nlen) in
diff --git a/clib/int.mli b/clib/int.mli
index 76aecf057b..e02ca90916 100644
--- a/clib/int.mli
+++ b/clib/int.mli
@@ -33,10 +33,13 @@ sig
type 'a t
(** Persistent, auto-resizable arrays. The [get] and [set] functions never
fail whenever the index is between [0] and [Sys.max_array_length - 1]. *)
+
val empty : int -> 'a t
(** The empty array, with a given starting size. *)
+
val get : 'a t -> int -> 'a option
(** Get a value at the given index. Returns [None] if undefined. *)
+
val set : 'a t -> int -> 'a option -> 'a t
(** Set/unset a value at the given index. *)
end
diff --git a/clib/segmenttree.ml b/clib/segmenttree.ml
index 24243b7a99..c3f1b44ef4 100644
--- a/clib/segmenttree.ml
+++ b/clib/segmenttree.ml
@@ -34,16 +34,16 @@ type elt = int
integers which are _not_ in the set of keys handled by the tree. On
leaves, a domain represents the st of integers which are in the set of
keys. *)
-type domain =
- (** On internal nodes, a domain [Interval (a, b)] represents
- the interval [a + 1; b - 1]. On leaves, it represents [a; b].
- We always have [a] <= [b]. *)
+type domain =
| Interval of elt * elt
- (** On internal node or root, a domain [Universe] represents all
- the integers. When the tree is not a trivial root,
- [Universe] has no interpretation on leaves. (The lookup
- function should never reach the leaves.) *)
+ (** On internal nodes, a domain [Interval (a, b)] represents
+ the interval [a + 1; b - 1]. On leaves, it represents [a; b].
+ We always have [a] <= [b]. *)
| Universe
+ (** On internal node or root, a domain [Universe] represents all
+ the integers. When the tree is not a trivial root,
+ [Universe] has no interpretation on leaves. (The lookup
+ function should never reach the leaves.) *)
(** We use an array to store the almost complete tree. This array
contains at least one element. *)
@@ -71,26 +71,26 @@ let make segments =
let tree = create nsegments (Universe, None) in
let leaves_offset = (1 lsl (log2n nsegments)) - 1 in
- (** The algorithm proceeds in two steps using an intermediate tree
- to store minimum and maximum of each subtree as annotation of
- the node. *)
+ (* The algorithm proceeds in two steps using an intermediate tree
+ to store minimum and maximum of each subtree as annotation of
+ the node. *)
- (** We start from leaves: the last level of the tree is initialized
- with the given segments... *)
- list_iteri
+ (* We start from leaves: the last level of the tree is initialized
+ with the given segments... *)
+ list_iteri
(fun i ((start, stop), value) ->
let k = leaves_offset + i in
let i = Interval (start, stop) in
tree.(k) <- (i, Some i))
segments;
- (** ... the remaining leaves are initialized with neutral information. *)
+ (* ... the remaining leaves are initialized with neutral information. *)
for k = leaves_offset + nsegments to Array.length tree -1 do
tree.(k) <- (Universe, Some Universe)
done;
- (** We traverse the tree bottom-up and compute the interval and
- annotation associated to each node from the annotations of its
- children. *)
+ (* We traverse the tree bottom-up and compute the interval and
+ annotation associated to each node from the annotations of its
+ children. *)
for k = leaves_offset - 1 downto 0 do
let node, annotation =
match value_of (left_child k) tree, value_of (right_child k) tree with
@@ -104,7 +104,7 @@ let make segments =
tree.(k) <- (node, Some annotation)
done;
- (** Finally, annotation are replaced with the image related to each leaf. *)
+ (* Finally, annotation are replaced with the image related to each leaf. *)
let final_tree =
Array.mapi (fun i (segment, value) -> (segment, None)) tree
in
diff --git a/clib/store.ml b/clib/store.ml
index 1469358c9d..79e26908d7 100644
--- a/clib/store.ml
+++ b/clib/store.ml
@@ -20,70 +20,37 @@ module type S =
sig
type t
type 'a field
+ val field : unit -> 'a field
val empty : t
val set : t -> 'a field -> 'a -> t
val get : t -> 'a field -> 'a option
val remove : t -> 'a field -> t
val merge : t -> t -> t
- val field : unit -> 'a field
end
-module Make () : S =
+module Make() : S =
struct
-
- let next =
- let count = ref 0 in fun () ->
- let n = !count in
- incr count;
- n
-
- type t = Obj.t option array
- (** Store are represented as arrays. For small values, which is typicial,
- is slightly quicker than other implementations. *)
-
-type 'a field = int
-
-let allocate len : t = Array.make len None
-
-let empty : t = [||]
-
-let set (s : t) (i : 'a field) (v : 'a) : t =
- let len = Array.length s in
- let nlen = if i < len then len else succ i in
- let () = assert (0 <= i) in
- let ans = allocate nlen in
- Array.blit s 0 ans 0 len;
- Array.unsafe_set ans i (Some (Obj.repr v));
- ans
-
-let get (s : t) (i : 'a field) : 'a option =
- let len = Array.length s in
- if len <= i then None
- else Obj.magic (Array.unsafe_get s i)
-
-let remove (s : t) (i : 'a field) =
- let len = Array.length s in
- let () = assert (0 <= i) in
- let ans = allocate len in
- Array.blit s 0 ans 0 len;
- if i < len then Array.unsafe_set ans i None;
- ans
-
-let merge (s1 : t) (s2 : t) : t =
- let len1 = Array.length s1 in
- let len2 = Array.length s2 in
- let nlen = if len1 < len2 then len2 else len1 in
- let ans = allocate nlen in
- (** Important: No more allocation from here. *)
- Array.blit s2 0 ans 0 len2;
- for i = 0 to pred len1 do
- let v = Array.unsafe_get s1 i in
- match v with
- | None -> ()
- | Some _ -> Array.unsafe_set ans i v
- done;
- ans
-
-let field () = next ()
-
+ module Dyn = Dyn.Make()
+ module Map = Dyn.Map(struct type 'a t = 'a end)
+
+ type t = Map.t
+ type 'a field = 'a Dyn.tag
+
+ let next = ref 0
+ let field () =
+ let f = Dyn.anonymous !next in
+ incr next;
+ f
+
+ let empty =
+ Map.empty
+ let set s f v =
+ Map.add f v s
+ let get s f =
+ try Some (Map.find f s)
+ with Not_found -> None
+ let remove s f =
+ Map.remove f s
+ let merge s1 s2 =
+ Map.fold (fun (Map.Any (f, v)) s -> Map.add f v s) s1 s2
end
diff --git a/clib/store.mli b/clib/store.mli
index 0c2b2e0856..7cdd1d3bed 100644
--- a/clib/store.mli
+++ b/clib/store.mli
@@ -19,6 +19,9 @@ sig
type 'a field
(** Type of field of such stores *)
+ val field : unit -> 'a field
+ (** Create a new field *)
+
val empty : t
(** Empty store *)
@@ -33,11 +36,7 @@ sig
val merge : t -> t -> t
(** [merge s1 s2] adds all the fields of [s1] into [s2]. *)
-
- val field : unit -> 'a field
- (** Create a new field *)
-
end
-module Make () : S
+module Make() : S
(** Create a new store type. *)
diff --git a/clib/trie.ml b/clib/trie.ml
index ea43e9e0bd..96de2b920c 100644
--- a/clib/trie.ml
+++ b/clib/trie.ml
@@ -51,7 +51,7 @@ let next (Node (_,m)) lbl = T_codom.find lbl m
let get (Node (hereset,_)) = hereset
let labels (Node (_,m)) =
- (** FIXME: this is order-dependent. Try to find a more robust presentation? *)
+ (* FIXME: this is order-dependent. Try to find a more robust presentation? *)
List.rev (T_codom.fold (fun x _ acc -> x::acc) m [])
let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 23:45:06 +0000