From 4422e16f529359bb96c7eee214b2b6648958ef48 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Sep 2012 14:26:42 +0000 Subject: Cleaning interface of Util. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/util.mli | 41 +---------------------------------------- 1 file changed, 1 insertion(+), 40 deletions(-) (limited to 'lib/util.mli') diff --git a/lib/util.mli b/lib/util.mli index a7586547e..1333d1854 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -15,11 +15,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Going down pairs *) - -val down_fst : ('a -> 'b) -> 'a * 'c -> 'b -val down_snd : ('a -> 'b) -> 'c * 'a -> 'b - (** Mapping under triple *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd @@ -106,46 +101,12 @@ val delayed_force : 'a delayed -> 'a (** {6 Misc. } *) -type ('a,'b) union = Inl of 'a | Inr of 'b +type ('a, 'b) union = Inl of 'a | Inr of 'b module Intset : Set.S with type elt = int module Intmap : Map.S with type key = int -val intmap_in_dom : int -> 'a Intmap.t -> bool -val intmap_to_list : 'a Intmap.t -> (int * 'a) list -val intmap_inv : 'a Intmap.t -> 'a -> int list - -val interval : int -> int -> int list - -(** {6 Memoization. } *) - -(** General comments on memoization: - - cache is created whenever the function is supplied (because of - ML's polymorphic value restriction). - - cache is never flushed (unless the memoized fun is GC'd) - - One cell memory: memorizes only the last call *) -val memo1_1 : ('a -> 'b) -> ('a -> 'b) -val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c) - -(** with custom equality (used to deal with various arities) *) -val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b) - -(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *) -val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b) - -(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *) - -val size_w : 'a -> int -val size_b : 'a -> int -val size_kb : 'a -> int - -(** {6 Total size of the allocated ocaml heap. } *) - -val heap_size : unit -> int -val heap_size_kb : unit -> int - (** {6 ... } *) (** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) -- cgit v1.2.3