1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: bstack.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
11
(* Queues of a given length *)
15
(* - size is the count of elements actually in the queue
16
- depth is the the amount of elements pushed in the queue (and not popped)
17
in particular, depth >= size always and depth > size if the queue overflowed
18
(and forgot older elements)
21
type 'a t = {mutable pos : int;
30
stack = Array.create depth e}
33
let set_depth bs n = bs.depth <- n
37
bs.pos <- if bs.pos = Array.length bs.stack - 1 then 0 else bs.pos + 1
40
if bs.size < Array.length bs.stack then bs.size <- bs.size + 1
43
bs.pos <- if bs.pos = 0 then Array.length bs.stack - 1 else bs.pos - 1
48
bs.depth <- bs.depth + 1;
49
bs.stack.(bs.pos) <- e
52
if bs.size > 1 then begin
53
bs.size <- bs.size - 1;
54
bs.depth <- bs.depth - 1;
55
let oldpos = bs.pos in
57
(* Release the memory at oldpos, by copying what is at new pos *)
58
bs.stack.(oldpos) <- bs.stack.(bs.pos)
62
if bs.size >= 1 then bs.stack.(bs.pos)
63
else error "Nothing on the stack"
66
if bs.size = 0 then error "Nothing on the stack"
67
else push bs (f (bs.stack.(bs.pos)))
70
if bs.size = 0 then error "Nothing on the stack"
71
else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
73
let depth bs = bs.depth