diff options
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cArray.ml | 4 | ||||
| -rw-r--r-- | clib/canary.ml | 28 | ||||
| -rw-r--r-- | clib/canary.mli | 27 | ||||
| -rw-r--r-- | clib/clib.mllib | 1 | ||||
| -rw-r--r-- | clib/dyn.ml | 194 | ||||
| -rw-r--r-- | clib/dyn.mli | 63 | ||||
| -rw-r--r-- | clib/hashcons.ml | 40 | ||||
| -rw-r--r-- | clib/hashcons.mli | 3 |
8 files changed, 135 insertions, 225 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml index b26dae7298..fc87a74cf6 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -280,7 +280,7 @@ let fold_left2_i f a v1 v2 = let rec fold a n = if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n)) (succ n) in - if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; + if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i"; fold a 0 let fold_left3 f a v1 v2 v3 = @@ -290,7 +290,7 @@ let fold_left3 f a v1 v2 v3 = else fold (f a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then - invalid_arg "Array.fold_left2"; + invalid_arg "Array.fold_left3"; fold a 0 let fold_left4 f a v1 v2 v3 v4 = diff --git a/clib/canary.ml b/clib/canary.ml deleted file mode 100644 index b8b79ed7f3..0000000000 --- a/clib/canary.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t = Obj.t - -let obj = Obj.new_block Obj.closure_tag 0 - (** This is an empty closure block. In the current implementation, it is - sufficient to allow marshalling but forbid equality. Sadly still allows - hash. *) - (** FIXME : use custom blocks somehow. *) - -module type Obj = sig type t end - -module Make(M : Obj) = -struct - type canary = t - type t = (canary * M.t) - - let prj (_, x) = x - let inj x = (obj, x) -end diff --git a/clib/canary.mli b/clib/canary.mli deleted file mode 100644 index d993eabcfd..0000000000 --- a/clib/canary.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t -(** Type of canaries. Canaries are used to ensure that an object does not use - generic operations. *) - -val obj : t -(** Canary. In the current implementation, this object is marshallable, - forbids generic comparison but still allows generic hashes. *) - -module type Obj = sig type t end - -module Make(M : Obj) : -sig - type t - val prj : t -> M.t - val inj : M.t -> t -end -(** Adds a canary to any type. *) diff --git a/clib/clib.mllib b/clib/clib.mllib index c9b4d72fce..afece4074c 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -1,4 +1,3 @@ -Canary CObj CEphemeron diff --git a/clib/dyn.ml b/clib/dyn.ml index e9b0419881..6c45767246 100644 --- a/clib/dyn.ml +++ b/clib/dyn.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module type TParam = +module type ValueS = sig type 'a t end @@ -16,40 +16,38 @@ end module type MapS = sig type t - type 'a obj type 'a key + type 'a value val empty : t - val add : 'a key -> 'a obj -> t -> t + val add : 'a key -> 'a value -> t -> t val remove : 'a key -> t -> t - val find : 'a key -> t -> 'a obj + val find : 'a key -> t -> 'a value val mem : 'a key -> t -> bool - type any = Any : 'a key * 'a obj -> any - - type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + type map = { map : 'a. 'a key -> 'a value -> 'a value } val map : map -> t -> t + type any = Any : 'a key * 'a value -> any val iter : (any -> unit) -> t -> unit val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r end module type PreS = sig -type 'a tag -type t = Dyn : 'a tag * 'a -> t - -val create : string -> 'a tag -val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option -val repr : 'a tag -> string + type 'a tag + type t = Dyn : 'a tag * 'a -> t -type any = Any : 'a tag -> any + val create : string -> 'a tag + val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + val repr : 'a tag -> string -val name : string -> any option + val dump : unit -> (int * string) list -module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag - -val dump : unit -> (int * string) list + type any = Any : 'a tag -> any + val name : string -> any option + module Map(Value : ValueS) : + MapS with type 'a key = 'a tag and type 'a value = 'a Value.t end module type S = @@ -57,104 +55,100 @@ sig include PreS module Easy : sig - val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) val inj : 'a -> 'a tag -> t val prj : t -> 'a tag -> 'a option end - end module Make () = struct -module Self : PreS = struct -(* Dynamics, programmed with DANGER !!! *) - -type 'a tag = int -type t = Dyn : 'a tag * 'a -> t - -type any = Any : 'a tag -> any - -let dyntab = ref (Int.Map.empty : string Int.Map.t) -(** Instead of working with tags as strings, which are costly, we use their - hash. We ensure unicity of the hash in the [create] function. If ever a - collision occurs, which is unlikely, it is sufficient to tweak the offending - dynamic tag. *) - -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 +module Self : PreS = struct + (* Dynamics, programmed with DANGER !!! *) + + type 'a tag = int + + type t = Dyn : 'a tag * 'a -> t + + type any = Any : 'a tag -> any + + let dyntab = ref (Int.Map.empty : string Int.Map.t) + (** Instead of working with tags as strings, which are costly, we use their + hash. We ensure unicity of the hash in the [create] function. If ever a + collision occurs, which is unlikely, it is sufficient to tweak the offending + dynamic tag. *) + + 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 + hash + + 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 + + let repr s = + try Int.Map.find s !dyntab + with Not_found -> + let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in assert false - in - let () = dyntab := Int.Map.add hash s !dyntab in - hash - -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 - -let repr s = - try Int.Map.find s !dyntab - with Not_found -> - let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in - assert false - -let name s = - let hash = Hashtbl.hash s in - if Int.Map.mem hash !dyntab then Some (Any hash) else None - -let dump () = Int.Map.bindings !dyntab - -module Map(M : TParam) = -struct -type t = Obj.t M.t Int.Map.t -type 'a obj = 'a M.t -type 'a key = 'a tag -let cast : 'a M.t -> 'b M.t = Obj.magic -let empty = Int.Map.empty -let add tag v m = Int.Map.add tag (cast v) m -let remove tag m = Int.Map.remove tag m -let find tag m = cast (Int.Map.find tag m) -let mem = Int.Map.mem - -type any = Any : 'a tag * 'a M.t -> any - -type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } -let map f m = Int.Map.mapi f.map m - -let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m -let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu -end + let name s = + let hash = Hashtbl.hash s in + if Int.Map.mem hash !dyntab then Some (Any hash) else None + + let dump () = Int.Map.bindings !dyntab + + module Map(Value: ValueS) = + struct + type t = Obj.t Value.t Int.Map.t + type 'a key = 'a tag + type 'a value = 'a Value.t + let cast : 'a value -> 'b value = Obj.magic + let empty = Int.Map.empty + let add tag v m = Int.Map.add tag (cast v) m + let remove tag m = Int.Map.remove tag m + let find tag m = cast (Int.Map.find tag m) + let mem = Int.Map.mem + + type map = { map : 'a. 'a tag -> 'a value -> 'a value } + let map f m = Int.Map.mapi f.map m + + type any = Any : 'a tag * 'a value -> any + let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m + let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu + end end include Self module Easy = struct - -(* now tags are opaque, we can do the trick *) -let make_dyn_tag (s : string) = - (fun (type a) (tag : a tag) -> - let infun : (a -> t) = fun x -> Dyn (tag, x) in - let outfun : (t -> a) = fun (Dyn (t, x)) -> - match eq tag t with - | None -> assert false - | Some CSig.Refl -> x - in - infun, outfun, tag) - (create s) - -let make_dyn (s : string) = - let inf, outf, _ = make_dyn_tag s in inf, outf - -let inj x tag = Dyn(tag,x) -let prj : type a. t -> a tag -> a option = + (* now tags are opaque, we can do the trick *) + let make_dyn_tag (s : string) = + (fun (type a) (tag : a tag) -> + let infun : (a -> t) = fun x -> Dyn (tag, x) in + let outfun : (t -> a) = fun (Dyn (t, x)) -> + match eq tag t with + | None -> assert false + | Some CSig.Refl -> x + in + infun, outfun, tag) + (create s) + + let make_dyn (s : string) = + let inf, outf, _ = make_dyn_tag s in inf, outf + + let inj x tag = Dyn(tag,x) + let prj : type a. t -> a tag -> a option = fun (Dyn(tag',x)) tag -> - match eq tag tag' with - | None -> None - | Some CSig.Refl -> Some x + match eq tag tag' with + | None -> None + | Some CSig.Refl -> Some x end end diff --git a/clib/dyn.mli b/clib/dyn.mli index 51d3091429..ff9762bd6b 100644 --- a/clib/dyn.mli +++ b/clib/dyn.mli @@ -10,7 +10,7 @@ (** Dynamically typed values *) -module type TParam = +module type ValueS = sig type 'a t end @@ -18,51 +18,66 @@ end module type MapS = sig type t - type 'a obj type 'a key + type 'a value val empty : t - val add : 'a key -> 'a obj -> t -> t + val add : 'a key -> 'a value -> t -> t val remove : 'a key -> t -> t - val find : 'a key -> t -> 'a obj + val find : 'a key -> t -> 'a value val mem : 'a key -> t -> bool - type any = Any : 'a key * 'a obj -> any - - type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + type map = { map : 'a. 'a key -> 'a value -> 'a value } val map : map -> t -> t + type any = Any : 'a key * 'a value -> any val iter : (any -> unit) -> t -> unit val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r end module type S = sig -type 'a tag -type t = Dyn : 'a tag * 'a -> t + type 'a tag + (** Type of dynamic tags *) -val create : string -> 'a tag -val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option -val repr : 'a tag -> string + type t = Dyn : 'a tag * 'a -> t + (** Type of dynamic values *) -type any = Any : 'a tag -> any + val create : string -> 'a tag + (** [create n] returns a tag describing a type called [n]. + [create] raises an exception if [n] is already registered. + Type names are hashed, so [create] may raise even if no type with + the exact same name was registered due to a collision. *) -val name : string -> any option + 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. *) -module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag + val repr : 'a tag -> string + (** [repr tag] returns the name of the type represented by [tag]. *) -val dump : unit -> (int * string) list + val dump : unit -> (int * string) list + (** [dump ()] returns a list of (tag, name) pairs for every type tag registered + in this [Dyn.Make] instance. *) -module Easy : sig + type any = Any : 'a tag -> any + (** Type of boxed dynamic tags *) - (* To create a dynamic type on the fly *) - val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag - val make_dyn : string -> ('a -> t) * (t -> 'a) + val name : string -> any option + (** [name n] returns [Some t] where t is a boxed tag previously registered + with [create n], or [None] if there is no such tag. *) - (* For types declared with the [create] function above *) - val inj : 'a -> 'a tag -> t - val prj : t -> 'a tag -> 'a option -end + module Map(Value : ValueS) : + MapS with type 'a key = 'a tag and type 'a value = 'a Value.t + (** Map from type tags to values parameterized by the tag type *) + + module Easy : sig + (* To create a dynamic type on the fly *) + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag + val make_dyn : string -> ('a -> t) * (t -> 'a) + (* For types declared with the [create] function above *) + val inj : 'a -> 'a tag -> t + val prj : t -> 'a tag -> 'a option + end end module Make () : S diff --git a/clib/hashcons.ml b/clib/hashcons.ml index ec73c6d934..39969ebf75 100644 --- a/clib/hashcons.ml +++ b/clib/hashcons.ml @@ -10,8 +10,6 @@ (* Hash consing of datastructures *) -(* The generic hash-consing functions (does not use Obj) *) - (* [t] is the type of object to hash-cons * [u] is the type of hash-cons functions for the sub-structures * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). @@ -148,41 +146,3 @@ module Hstring = Make( let len = String.length s in hash len s 0 0 end) - -(* Obj.t *) -exception NotEq - -(* From CAMLLIB/caml/mlvalues.h *) -let no_scan_tag = 251 -let tuple_p obj = Obj.is_block obj && (Obj.tag obj < no_scan_tag) - -let comp_obj o1 o2 = - if tuple_p o1 && tuple_p o2 then - let n1 = Obj.size o1 and n2 = Obj.size o2 in - if n1=n2 then - try - for i = 0 to pred n1 do - if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq - done; true - with NotEq -> false - else false - else o1=o2 - -let hash_obj hrec o = - begin - if tuple_p o then - let n = Obj.size o in - for i = 0 to pred n do - Obj.set_field o i (hrec (Obj.field o i)) - done - end; - o - -module Hobj = Make( - struct - type t = Obj.t - type u = (Obj.t -> Obj.t) * unit - let hashcons (hrec,_) = hash_obj hrec - let eq = comp_obj - let hash = Hashtbl.hash - end) diff --git a/clib/hashcons.mli b/clib/hashcons.mli index 3e396ff23c..223dd2a4d2 100644 --- a/clib/hashcons.mli +++ b/clib/hashcons.mli @@ -87,6 +87,3 @@ module Hstring : (S with type t = string and type u = unit) module Hlist (D:HashedType) : (S with type t = D.t list and type u = (D.t list -> D.t list)*(D.t->D.t)) (** Hashconsing of lists. *) - -module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit) -(** Hashconsing of OCaml values. *) |