src/Tools/Metis/src/Heap.sig
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 39502 cffceed8e7fa
child 72004 913162a47d9f
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;

(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML                                                    *)
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

signature Heap =
sig

type 'a heap

val new : ('a * 'a -> order) -> 'a heap

val add : 'a heap -> 'a -> 'a heap

val null : 'a heap -> bool

val top : 'a heap -> 'a  (* raises Empty *)

val remove : 'a heap -> 'a * 'a heap  (* raises Empty *)

val size : 'a heap -> int

val app : ('a -> unit) -> 'a heap -> unit

val toList : 'a heap -> 'a list

val toStream : 'a heap -> 'a Stream.stream

val toString : 'a heap -> string

end