diff options
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cStack.ml | 44 | ||||
| -rw-r--r-- | clib/cStack.mli | 58 | ||||
| -rw-r--r-- | clib/clib.mllib | 2 |
3 files changed, 0 insertions, 104 deletions
diff --git a/clib/cStack.ml b/clib/cStack.ml deleted file mode 100644 index 0432e29fad..0000000000 --- a/clib/cStack.ml +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <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) *) -(************************************************************************) - -exception Empty = Stack.Empty - -type 'a t = { - mutable stack : 'a list; -} - -let create () = { stack = [] } - -let push x s = s.stack <- x :: s.stack - -let pop = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::xs } as s -> s.stack <- xs; x - -let top = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::_ } -> x - -let to_list { stack = s } = s - -let find f s = List.find f (to_list s) - -let find_map f s = CList.find_map f s.stack - -let fold_until f accu s = CList.fold_left_until f accu s.stack - -let is_empty { stack = s } = s = [] - -let iter f { stack = s } = List.iter f s - -let clear s = s.stack <- [] - -let length { stack = s } = List.length s - diff --git a/clib/cStack.mli b/clib/cStack.mli deleted file mode 100644 index de802160e7..0000000000 --- a/clib/cStack.mli +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <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) *) -(************************************************************************) - -(** Extended interface for OCaml stacks. *) - -type 'a t - -exception Empty -(** Alias for Stack.Empty. *) - -val create : unit -> 'a t -(** Create an empty stack. *) - -val push : 'a -> 'a t -> unit -(** Add an element to a stack. *) - -val find : ('a -> bool) -> 'a t -> 'a -(** Find the first element satisfying the predicate. - @raise Not_found it there is none. *) - -val is_empty : 'a t -> bool -(** Whether a stack is empty. *) - -val iter : ('a -> unit) -> 'a t -> unit -(** Iterate a function over elements, from the last added one. *) - -val clear : 'a t -> unit -(** Empty a stack. *) - -val length : 'a t -> int -(** Length of a stack. *) - -val pop : 'a t -> 'a -(** Remove and returns the first element of the stack. - @raise Empty if empty. *) - -val top : 'a t -> 'a -(** Remove the first element of the stack without modifying it. - @raise Empty if empty. *) - -val to_list : 'a t -> 'a list -(** Convert to a list. *) - -val find_map : ('a -> 'b option) -> 'a t -> 'b -(** Find the first element that returns [Some _]. - @raise Not_found it there is none. *) - -val fold_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a t -> 'c -(** Like CList.fold_left_until. - The stack is traversed from the top and is not altered. *) - diff --git a/clib/clib.mllib b/clib/clib.mllib index 5a2c9a9ce9..be3b5971be 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -9,7 +9,6 @@ CSet CMap CList CString -CStack Int Range @@ -33,7 +32,6 @@ Unionfind Dyn Store Exninfo -Backtrace IStream Terminal Monad |