From ba524ddfaabc80b31a439544de46c40366565ae8 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 6 Sep 2013 17:18:44 +0000 Subject: Moving Searchstack to CStack, and normalizing names a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/cStack.mli | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 lib/cStack.mli (limited to 'lib/cStack.mli') diff --git a/lib/cStack.mli b/lib/cStack.mli new file mode 100644 index 0000000000..edca854488 --- /dev/null +++ b/lib/cStack.mli @@ -0,0 +1,58 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '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 find_map : ('a -> 'b option) -> 'a t -> 'b +(** Find the first element that returns [Some _]. + @raise Not_found it there is none. *) + +val seek : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b +(** Find the first element that returns [Some _]. + @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. *) + -- cgit v1.2.3