pqueue.mli 1.24 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
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
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)

(* Priority queue *)

module Make(X: Set.OrderedType) : sig

  type t

  type elt = X.t

  val create: dummy:elt -> t
    (** [dummy] will never be returned *)

  val is_empty: t -> bool

  val add: t -> elt -> unit
    (* inserts a new element *)

  exception Empty

  val get_min: t -> elt
    (* returns the minimal element (does not remove it)
       raises [Empty] if the queue is empty *)

  val remove_min: t -> unit
    (* removes the minimal element
       raises [Empty] if the queue is empty *)

  val extract_min: t -> elt
    (* removes and returns the minimal element
       raises [Empty] if the queue is empty *)

end