diff options
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/deque.ml | 99 | ||||
| -rw-r--r-- | clib/deque.mli | 60 |
2 files changed, 0 insertions, 159 deletions
diff --git a/clib/deque.ml b/clib/deque.ml deleted file mode 100644 index 9d0bbf12a..000000000 --- a/clib/deque.ml +++ /dev/null @@ -1,99 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -exception Empty - -type 'a t = { - face : 'a list; - rear : 'a list; - lenf : int; - lenr : int; -} - -let rec split i accu l = match l with -| [] -> - if Int.equal i 0 then (accu, []) else invalid_arg "split" -| t :: q -> - if Int.equal i 0 then (accu, l) - else split (pred i) (t :: accu) q - -let balance q = - let avg = (q.lenf + q.lenr) / 2 in - let dif = q.lenf + q.lenr - avg in - if q.lenf > succ (2 * q.lenr) then - let (ff, fr) = split avg [] q.face in - { face = List.rev ff ; rear = q.rear @ List.rev fr; lenf = avg; lenr = dif } - else if q.lenr > succ (2 * q.lenf) then - let (rf, rr) = split avg [] q.rear in - { face = q.face @ List.rev rr ; rear = List.rev rf; lenf = dif; lenr = avg } - else q - -let empty = { - face = []; - rear = []; - lenf = 0; - lenr = 0; -} - -let lcons x q = - balance { q with lenf = succ q.lenf; face = x :: q.face } - -let lhd q = match q.face with -| [] -> - begin match q.rear with - | [] -> raise Empty - | t :: _ -> t - end -| t :: _ -> t - -let ltl q = match q.face with -| [] -> - begin match q.rear with - | [] -> raise Empty - | t :: _ -> empty - end -| t :: r -> balance { q with lenf = pred q.lenf; face = r } - -let rcons x q = - balance { q with lenr = succ q.lenr; rear = x :: q.rear } - -let rhd q = match q.rear with -| [] -> - begin match q.face with - | [] -> raise Empty - | t :: r -> t - end -| t :: _ -> t - -let rtl q = match q.rear with -| [] -> - begin match q.face with - | [] -> raise Empty - | t :: r -> empty - end -| t :: r -> - balance { q with lenr = pred q.lenr; rear = r } - -let rev q = { - face = q.rear; - rear = q.face; - lenf = q.lenr; - lenr = q.lenf; -} - -let length q = q.lenf + q.lenr - -let is_empty q = Int.equal (length q) 0 - -let filter f q = - let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in - let (rf, lenf) = List.fold_left fold ([], 0) q.face in - let (rr, lenr) = List.fold_left fold ([], 0) q.rear in - balance { face = List.rev rf; rear = List.rev rr; lenf = lenf; lenr = lenr } diff --git a/clib/deque.mli b/clib/deque.mli deleted file mode 100644 index 1c03c384d..000000000 --- a/clib/deque.mli +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** * Purely functional, double-ended queues *) - -(** This module implements the banker's deque, from Okasaki. Most operations are - amortized O(1). *) - -type +'a t - -exception Empty - -(** {5 Constructor} *) - -val empty : 'a t - -(** The empty deque. *) - -(** {5 Left-side operations} *) - -val lcons : 'a -> 'a t -> 'a t -(** Pushes an element on the left side of the deque. *) - -val lhd : 'a t -> 'a -(** Returns the leftmost element in the deque. Raises [Empty] when empty. *) - -val ltl : 'a t -> 'a t -(** Returns the left-tail of the deque. Raises [Empty] when empty. *) - -(** {5 Right-side operations} *) - -val rcons : 'a -> 'a t -> 'a t -(** Same as [lcons] but on the right side. *) - -val rhd : 'a t -> 'a -(** Same as [lhd] but on the right side. *) - -val rtl : 'a t -> 'a t -(** Same as [ltl] but on the right side. *) - -(** {5 Operations} *) - -val rev : 'a t -> 'a t -(** Reverse deque. *) - -val length : 'a t -> int -(** Length of a deque. *) - -val is_empty : 'a t -> bool -(** Emptyness of a deque. *) - -val filter : ('a -> bool) -> 'a t -> 'a t -(** Filters the deque *) |