(* 
Priority Queue of ELT

this version stores (item,priority) pairs, like ("hi",2) or (15,0)
it also makes the collection or items are any one priority stay in queue order
We treat 0 as highest priority... the smaller the interger, the higher the priority

new    :                   --> PQUE
insert : PQUE x ELT x int  --> PQUE

getv   : PQUE        --> ELT u err
getp   : PQUE        --> nat u err
delete : PQUE        --> PQUE

size   : PQUE        --> nat
empty  : PQUE        --> boolean


size(new) = 0
size(insert(Q,e,i)) = size(Q) + 1

empty(new) = true
empty(insert(Q,e,i)) = false


getv(new) = err
getv(insert(Q,e,i)) = if (empty(Q)) then e
                        else if (i<getp(Q)) then e
                        else getv(Q)

(alt) getv(insert(new,e,i)) = e

getp(new) = err
getp(insert(Q,e,i)) = if (empty(Q)) then i
                        else if (i<getp(Q)) then i
                        else getp(Q)


delete(new) = new
delete(insert(Q,e,i)) = if (empty(Q)) then New
                          else if (i<getp(Q)) then Q
                          else insert(delete(Q),e,i)

*)


datatype 'elt PQue = 
   New  
   | Insert of 'elt PQue * 'elt * int 
   ;

fun size (New) = 0
  | size (Insert(pq,e,i)) = size(pq)+1 
  ;

fun empty (New) = true
  | empty (Insert(pq,e,i)) = false
  ;

exception getpNewErr;
fun getp ( New )             = raise getpNewErr
  | getp ( Insert(pq,e,i) )  = if empty(pq) then i
                                else if i<getp(pq) then i
                                else getp(pq)
  ;

exception getvNewErr;

fun getv ( New )             = raise getvNewErr
  | getv ( Insert(pq,e,i) )  = if empty(pq) then e
                                else if i<getp(pq) then e
                                else getv(pq)
  ;

fun delete ( New )            = New
  | delete ( Insert(pq,e,i) ) = if empty(pq) then New
                                 else if i<getp(pq) then pq
                                 else Insert(delete(pq),e,i)
  ;