diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:39 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:39 +0000 |
commit | 6bac888419048aa8fe06b49bf94f64893228bb00 (patch) | |
tree | e01a628f3419265b786318feada5d98cbaba5ab8 | |
parent | 0faf3c5a53113ec8f31c1747c9cafe4118831282 (diff) |
Searchable stack data structure
It is like Stack but one can search without popping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.common | 2 | ||||
-rw-r--r-- | lib/lib.mllib | 1 | ||||
-rw-r--r-- | lib/searchstack.ml | 25 | ||||
-rw-r--r-- | lib/searchstack.mli | 25 |
4 files changed, 52 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 8aaf8fceb..1845f7164 100644 --- a/Makefile.common +++ b/Makefile.common @@ -208,7 +208,7 @@ endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo +IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/searchstack.cmo IDECMA:=ide/ide.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml diff --git a/lib/lib.mllib b/lib/lib.mllib index fec18486f..14a835872 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -2,6 +2,7 @@ Xml_lexer Xml_parser Xml_printer Errors +Searchstack Bigint Dyn Segmenttree diff --git a/lib/searchstack.ml b/lib/searchstack.ml new file mode 100644 index 000000000..8d160e572 --- /dev/null +++ b/lib/searchstack.ml @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type 'a t = 'a list ref +type ('a,'b) search = [ `Stop of 'b | `Cont of 'a ] + +let create () = ref [] +let push x l = l := x :: !l +let pop l = match !l with [] -> raise Stack.Empty | x::xs -> l := xs; x +let top l = match !l with [] -> raise Stack.Empty | x::_ -> x +let find f i l = + let rec aux i = function + | [] -> raise Not_found + | x::xs -> match f i x with `Stop x -> x | `Cont i -> aux i xs in + aux i !l +let is_empty l = match !l with [] -> true | _ -> false +let iter f l = List.iter f !l +let clear l = l := [] +let length l = List.length !l +let to_list l = !l diff --git a/lib/searchstack.mli b/lib/searchstack.mli new file mode 100644 index 000000000..6c81a2a9c --- /dev/null +++ b/lib/searchstack.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type 'a t +type ('a,'b) search = [ `Stop of 'b | `Cont of 'a ] + +val create : unit -> 'a t +val push : 'a -> 'a t -> unit +val find : ('c -> 'a -> ('c, 'b) search) -> 'c -> 'a t -> 'b +val is_empty : 'a t -> bool +val iter : ('a -> unit) -> 'a t -> unit +val clear : 'a t -> unit +val length : 'a t -> int + +(* may raise Stack.Empty *) +val pop : 'a t -> 'a +val top : 'a t -> 'a + +(* Extra *) +val to_list : 'a t -> 'a list |