1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
(************************************************************************)
(* 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 10441 2008-01-15 16:37:46Z lmamane $ *)
(* Queues of a given length *)
open Util
(* - size is the count of elements actually in the queue
- depth is the the amount of elements pushed in the queue (and not popped)
in particular, depth >= size always and depth > size if the queue overflowed
(and forgot older elements)
*)
type 'a t = {mutable pos : int;
mutable size : int;
mutable depth : int;
stack : 'a array}
let create depth e =
{pos = 0;
size = 1;
depth = 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.depth <- bs.depth + 1;
bs.stack.(bs.pos) <- e
let pop bs =
if bs.size > 1 then begin
bs.size <- bs.size - 1;
bs.depth <- bs.depth - 1;
let oldpos = bs.pos in
decr_pos bs;
(* Release the memory at oldpos, by copying 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.depth
let size bs = bs.size
|
