diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /lib/bstack.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'lib/bstack.ml')
-rw-r--r-- | lib/bstack.ml | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/lib/bstack.ml b/lib/bstack.ml new file mode 100644 index 00000000..d4b995fb --- /dev/null +++ b/lib/bstack.ml @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: bstack.ml,v 1.3.2.1 2004/07/16 19:30:29 herbelin Exp $ *) + +(* Queues of a given length *) + +open Util + +type 'a t = {mutable pos : int; + mutable size : int; + stack : 'a array} + +let create depth e = + {pos = 0; + size = 1; + stack = Array.create depth e} + +(* +let set_depth bs n = bs.depth <- n +*) + +let incr_pos bs = + bs.pos <- if bs.pos = Array.length bs.stack - 1 then 0 else bs.pos + 1 + +let incr_size bs = + if bs.size < Array.length bs.stack then bs.size <- bs.size + 1 + +let decr_pos bs = + bs.pos <- if bs.pos = 0 then Array.length bs.stack - 1 else bs.pos - 1 + +let push bs e = + incr_pos bs; + incr_size bs; + bs.stack.(bs.pos) <- e + +let pop bs = + if bs.size > 1 then begin + bs.size <- bs.size - 1; + let oldpos = bs.pos in + decr_pos bs; + (* Release the memory at oldpos, by coyping what is at new pos *) + bs.stack.(oldpos) <- bs.stack.(bs.pos) + end + +let top bs = + if bs.size >= 1 then bs.stack.(bs.pos) + else error "Nothing on the stack" + +let app_push bs f = + if bs.size = 0 then error "Nothing on the stack" + else push bs (f (bs.stack.(bs.pos))) + +let app_repl bs f = + if bs.size = 0 then error "Nothing on the stack" + else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos)) + +let depth bs = bs.size |