diff options
| -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 |