A stateful query type for Singly Linked Lists

The query type SinglyLinkedList α models the abstract interface for a singly linked list. Its basic interface is identical to that of it's functional programming cousin, a recursively defined list.

structure Algolean.Algorithms.ListState (α : Type u) : Type u

A state type with a single list that is used to internally represent linear data structures like linked lists, stacks, and queues.

• internalList : List α

  The internal list

inductive Algolean.Algorithms.Strategy : Type

Insertion strategy. This can be either last-in-first-out (lifo) or first-in-first-out (fifo)

• lifo : Strategy
• fifo : Strategy

inductive Algolean.Algorithms.ListADT (s : Strategy) (α : Type u) : Type u → Type u

An ADT query type for a stack. Note this is essentially identical to the List query type, but with renamed queries to match the typical names of a stack interface.

• peek {s : Strategy} {α : Type u} : ListADT s α (Option α)
• drop {s : Strategy} {α : Type u} : ListADT s α PUnit.{u + 1}
• insert {s : Strategy} {α : Type u} (data : α) : ListADT s α PUnit.{u + 1}

def Algolean.Algorithms.listModel {α : Type} (s : Strategy) : ModelM (ListADT s α) (StateM (ListState α)) ℕ

A model for the stack query using the ListState to store the stack internally in the state type.

Equations

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

@[simp]

theorem Algolean.Algorithms.listModel_cost {α : Type} (s : Strategy) {α✝ : Type} (x✝ : ListADT s α α✝) : (listModel s).cost x✝ = 1

@[simp]

theorem Algolean.Algorithms.listModel_evalQuery {α : Type} (s : Strategy) {α✝ : Type} (x✝ : ListADT s α α✝) : (listModel s).evalQuery x✝ = match α✝, x✝ with | .(Option α), ListADT.peek => do let iL ← get pure iL.internalList.head? | .(PUnit.{1}), ListADT.drop => do let iL ← get set { internalList := iL.internalList.tail } pure () | .(PUnit.{1}), ListADT.insert x => match s with | Strategy.lifo => modify fun (iL : ListState α) => { internalList := x :: iL.internalList } | Strategy.fifo => modify fun (iL : ListState α) => { internalList := iL.internalList ++ [x] }

@[reducible, inline]

abbrev Algolean.Algorithms.stackModel {α : Type} : ModelM (ListADT Strategy.lifo α) (StateM (ListState α)) ℕ

Interpretation of ListADT as the ADT of a stack

Equations

• Algolean.Algorithms.stackModel = Algolean.Algorithms.listModel Algolean.Algorithms.Strategy.lifo

@[reducible, inline]

abbrev Algolean.Algorithms.queueModel {α : Type} : ModelM (ListADT Strategy.fifo α) (StateM (ListState α)) ℕ

Interpretation of ListADT as the ADT of a queue

Equations

• Algolean.Algorithms.queueModel = Algolean.Algorithms.listModel Algolean.Algorithms.Strategy.fifo