structure Aesop.BestFirstQueue.ActiveGoal : Type

• goal : Aesop.GoalRef
• priority : Aesop.Percent
• lastExpandedInIteration : Aesop.Iteration
• addedInIteration : Aesop.Iteration

def Aesop.BestFirstQueue.ActiveGoal.le (g : Aesop.BestFirstQueue.ActiveGoal) (h : Aesop.BestFirstQueue.ActiveGoal) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Aesop.BestFirstQueue.ActiveGoal.ofGoalRef (gref : Aesop.GoalRef) : BaseIO Aesop.BestFirstQueue.ActiveGoal

Equations

• One or more equations did not get rendered due to their size.

def Aesop.BestFirstQueue : Type

Equations

• Aesop.BestFirstQueue = Std.BinomialHeap Aesop.BestFirstQueue.ActiveGoal Aesop.BestFirstQueue.ActiveGoal.le

def Aesop.BestFirstQueue.init : Aesop.BestFirstQueue

Equations

• Aesop.BestFirstQueue.init = Std.BinomialHeap.empty

def Aesop.BestFirstQueue.addGoals (q : Aesop.BestFirstQueue) (grefs : Array Aesop.GoalRef) : BaseIO Aesop.BestFirstQueue

Equations

• One or more equations did not get rendered due to their size.

def Aesop.BestFirstQueue.popGoal (q : Aesop.BestFirstQueue) : Option Aesop.GoalRef × Aesop.BestFirstQueue

Equations

• Aesop.BestFirstQueue.popGoal q = match Std.BinomialHeap.deleteMin q with | none => (none, q) | some (ag, q) => (some ag.goal, q)

instance Aesop.instQueueBestFirstQueue : Aesop.Queue Aesop.BestFirstQueue

Equations

• Aesop.instQueueBestFirstQueue = { init := pure Aesop.BestFirstQueue.init, addGoals := Aesop.BestFirstQueue.addGoals, popGoal := fun q => pure (Aesop.BestFirstQueue.popGoal q) }

structure Aesop.LIFOQueue : Type

• goals : Array Aesop.GoalRef

def Aesop.LIFOQueue.init : Aesop.LIFOQueue

Equations

• Aesop.LIFOQueue.init = { goals := #[] }

def Aesop.LIFOQueue.addGoals (q : Aesop.LIFOQueue) (grefs : Array Aesop.GoalRef) : Aesop.LIFOQueue

Equations

• Aesop.LIFOQueue.addGoals q grefs = { goals := q.goals ++ Array.reverse grefs }

def Aesop.LIFOQueue.popGoal (q : Aesop.LIFOQueue) : Option Aesop.GoalRef × Aesop.LIFOQueue

Equations

• Aesop.LIFOQueue.popGoal q = match Array.back? q.goals with | some g => (some g, { goals := Array.pop q.goals }) | none => (none, q)

instance Aesop.LIFOQueue.instQueueLIFOQueue : Aesop.Queue Aesop.LIFOQueue

Equations

• One or more equations did not get rendered due to their size.

structure Aesop.FIFOQueue : Type

• goals : Array Aesop.GoalRef
• pos : Nat

def Aesop.FIFOQueue.init : Aesop.FIFOQueue

Equations

• Aesop.FIFOQueue.init = { goals := #[], pos := 0 }

def Aesop.FIFOQueue.addGoals (q : Aesop.FIFOQueue) (grefs : Array Aesop.GoalRef) : Aesop.FIFOQueue

Equations

• Aesop.FIFOQueue.addGoals q grefs = { goals := q.goals ++ grefs, pos := q.pos }

def Aesop.FIFOQueue.popGoal (q : Aesop.FIFOQueue) : Option Aesop.GoalRef × Aesop.FIFOQueue

Equations

• Aesop.FIFOQueue.popGoal q = if h : q.pos < Array.size q.goals then (some q.goals[q.pos], { goals := q.goals, pos := q.pos + 1 }) else (none, q)

instance Aesop.FIFOQueue.instQueueFIFOQueue : Aesop.Queue Aesop.FIFOQueue

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Options.queue (opts : Aesop.Options) : (Q : Type) × Aesop.Queue Q

Equations

• One or more equations did not get rendered due to their size.