Sorted Linked List State

Sorted Linked list internal state is the same as Unordered, i.e, we keep an unsorted list as internal state.

Actions are the same as in Unsorted lists (but safe) plus insertion.

inductive MOList.State.Actions (α : Type) : Type

• ModifyData {α : Type} : Tokens.Elem.TId → α → Actions α
• SafePrepend {α : Type} (key : MUList.State.Key) (data : α) (root : Tokens.Elem.TId) : Actions α
• SafeAppend {α : Type} (key : MUList.State.Key) (data : α) (last : Tokens.Elem.TId) : Actions α
• Insert {α : Type} (key : MUList.State.Key) (data : α) (anchor : Tokens.Elem.TId) : Actions α
• Remove {α : Type} (removed_node anchor_node : Tokens.Elem.TId) : Actions α

instance MOList.State.instReprActions {α✝ : Type} [Repr α✝] : Repr (Actions α✝)

Equations

• MOList.State.instReprActions = { reprPrec := MOList.State.instReprActions.repr }

def MOList.State.instReprActions.repr {α✝ : Type} [Repr α✝] : Actions α✝ → ℕ → Std.Format

Equations

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

Operations

Sorted lists provide the same operations plus verifiable /non_membership/. Since a node is a range in itself, we know there is no element between a node's key and the key it links to.

Sorted lists accept same operations as Unsorted plus /parallel/ insertion.

def MOList.Operations.non_member_lower (k1 : Option MUList.State.Key) (k2 : MUList.State.Key) : Bool

Equations

• MOList.Operations.non_member_lower none k2 = false
• MOList.Operations.non_member_lower (some k) k2 = decide (k < k2)

def MOList.Operations.non_member_upper (k1 : MUList.State.Key) (k2 : Option MUList.State.Key) : Bool

Equations

• MOList.Operations.non_member_upper k1 none = false
• MOList.Operations.non_member_upper k1 (some k) = decide (k1 < k)

def MOList.Operations.midgard_is_non_member {α : Type} (mkey : Option MUList.State.Key) (nd : MUList.State.ListToken α) : Bool

Equations

• One or more equations did not get rendered due to their size.
• MOList.Operations.midgard_is_non_member none nd = false

def MOList.Operations.is_non_member {α : Type} (mkey : Option MUList.State.Key) (tid : Tokens.Elem.TId) (s : MUList.State.ListST α) : Bool

Equations

• MOList.Operations.is_non_member mkey tid s = match Tokens.State.Tokens.get tid s with | none => false | some nd => MOList.Operations.midgard_is_non_member mkey nd