English
Insert a new node into the queue and possibly eject the tail element if the size limit is exceeded, by removing the worst (greatest) element.
Русский
Вставить новый узел в очередь и при превышении максимального размера удалить хвостовой элемент с наибольшим приоритетом.
LaTeX
$$insertAndEject(q,n,l) = if maxSize is none then q.insert n l else if q.size < max then q.insert n l else (q.maxEntry? with some m => q.insert n l).erase m.1$$
Lean4
/-- Add a new `MLList m β` to the `BestFirstQueue`, and if this takes the size above `maxSize`,
eject a `MLList` from the tail of the queue.
-/
-- Note this ejects the element with the greatest estimated priority,
-- not necessarily the greatest priority!
def insertAndEject (q : BestFirstQueue prio ε m β maxSize) (n : BestFirstNode prio ε) (l : MLList m β) :
BestFirstQueue prio ε m β maxSize :=
match maxSize with
| none => q.insert n l
| some max =>
if q.size < max then q.insert n l
else
match q.maxEntry? with
| none => TreeMap.empty
| some m => q.insert n l |>.erase m.1
