28 lines
1006 B
Plaintext
28 lines
1006 B
Plaintext
)abbrev Domain ORDKE OrderedKeyEntry
|
|
OrderedKeyEntry(Key:OrderedSet,Entry:SetCategory): Exports == Implementation where
|
|
Exports == OrderedSet with
|
|
construct: (Key,Entry) -> %
|
|
elt: (%,"key") -> Key
|
|
elt: (%,"entry") -> Entry
|
|
Implementation == add
|
|
Rep := Record(k:Key,e:Entry)
|
|
x,y: %
|
|
construct(a,b) == construct(a,b)$Rep @ %
|
|
elt(x,"key"):Key == (x@Rep).k
|
|
elt(x,"entry"):Entry == (x@Rep).e
|
|
x < y == x.key < y.key
|
|
x = y == x.key = y.key
|
|
hash x == hash(x.key)
|
|
if Entry has CoercibleTo OutputForm then
|
|
coerce(x):OutputForm == bracket [(x.key)::OutputForm,(x.entry)::OutputForm]
|
|
)abbrev Domain PRIORITY PriorityQueue
|
|
S ==> OrderedKeyEntry(Key,Entry)
|
|
PriorityQueue(Key:OrderedSet,Entry:SetCategory): Exports == Implementation where
|
|
Exports == PriorityQueueAggregate S with
|
|
heap : List S -> %
|
|
setelt: (%,Key,Entry) -> Entry
|
|
Implementation == Heap(S) add
|
|
setelt(x:%,key:Key,entry:Entry) ==
|
|
insert!(construct(key,entry)$S,x)
|
|
entry
|