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/hashcons.ml | 40 | ||||
| -rw-r--r-- | clib/hashcons.mli | 3 |
6 files changed, 2 insertions, 101 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/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. *) |