English
Convert a BestFirstQueue into a MLList by popping all elements, yielding a list of pairs.
Русский
Преобразовать BestFirstQueue в MLList путём извлечения всех элементов, получив список пар.
LaTeX
$$BestFirstQueue.toMLList(q) = q.toMLList.map (λ t, (t.1.1, t.2))$$
Lean4
/-- Core implementation of `bestFirstSearch`, that works by iteratively updating an internal state,
consisting of a priority queue of `MLList m α`.
At each step we pop an element off the queue,
compute its children (lazily) and put these back on the queue.
-/
def impl (maxSize : Option Nat) (f : α → MLList m α) (a : α) : MLList m α :=
let init : BestFirstQueue prio ε m α maxSize := TreeMap.empty.insert ⟨a, ⊥⟩ (f a)
cons a (iterate go |>.runState' init)
where/-- A single step of the best first search.
Pop an element, and insert its children back into the queue,
with a trivial estimator for their priority. -/
go : StateT (BestFirstQueue prio ε m α maxSize) m α := fun s => do
match ← s.pop with
| none =>
failure
| some ((_, b), s') =>
pure (b, s'.insertAndEject ⟨b, ⊥⟩ (f b))
