State-indexed values

@[reducible, inline]

abbrev Std.Do.SVal (σs : List Type) (α : Type) : Type

A value indexed by a curried tuple of states.

example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl

Equations

• Std.Do.SVal [] α = α
• Std.Do.SVal (σ :: σs_2) α = (σ → Std.Do.SVal σs_2 α)

def Std.Do.SVal.StateTuple (σs : List Type) : Type

A tuple capturing the whole state of an SVal.

Equations

• Std.Do.SVal.StateTuple [] = Unit
• Std.Do.SVal.StateTuple (σ :: σs_2) = (σ × Std.Do.SVal.StateTuple σs_2)

instance Std.Do.SVal.instInhabitedStateTupleNil : Inhabited (StateTuple [])

Equations

• Std.Do.SVal.instInhabitedStateTupleNil = { default := () }

instance Std.Do.SVal.instInhabitedStateTupleCons {σ : Type} {σs : List Type} [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs))

Equations

• Std.Do.SVal.instInhabitedStateTupleCons = { default := (default, default) }

def Std.Do.SVal.curry {α : Type} {σs : List Type} (f : StateTuple σs → α) : SVal σs α

Curry a function taking a StateTuple into an SVal.

Equations

• Std.Do.SVal.curry f_2 = f_2 ()
• Std.Do.SVal.curry f_2 = fun (s : head) => ⌜f_2 (s, s')⌝

@[simp]

theorem Std.Do.SVal.curry_nil {α : Type} {f : StateTuple [] → α} : curry f = f ()

@[simp]

theorem Std.Do.SVal.curry_cons {α σ : Type} {σs : List Type} {f : StateTuple (σ :: σs) → α} {s : σ} : curry f s = ⌜f (s, s')⌝

def Std.Do.SVal.uncurry {α : Type} {σs : List Type} (f : SVal σs α) : StateTuple σs → α

Uncurry an SVal into a function taking a StateTuple.

Equations

• #f_2 = fun (x : Std.Do.SVal.StateTuple []) => f_2
• #f_2 = fun (x : Std.Do.SVal.StateTuple (head :: tail)) => match x with | (s, t) => #(f_2 s) t

@[simp]

theorem Std.Do.SVal.uncurry_nil {σ : Type} {s : σ} : #s = fun (x : StateTuple []) => s

@[simp]

theorem Std.Do.SVal.uncurry_cons {α σ : Type} {σs : List Type} {f : SVal (σ :: σs) α} {s : σ} {t : StateTuple σs} : #f (s, t) = #(f s) t

@[simp]

theorem Std.Do.SVal.uncurry_curry {α : Type} {σs : List Type} {f : StateTuple σs → α} : #(curry f) = f

@[simp]

theorem Std.Do.SVal.curry_uncurry {α : Type} {σs : List Type} {f : SVal σs α} : curry #f = f

@[reducible, inline]

abbrev Std.Do.SVal.pure {α : Type} {σs : List Type} (a : α) : SVal σs α

Embed a pure value into an SVal.

Equations

• Std.Do.SVal.pure a = ⌜a⌝

instance Std.Do.SVal.instInhabited {α : Type} {σs : List Type} [Inhabited α] : Inhabited (SVal σs α)

Equations

• Std.Do.SVal.instInhabited = { default := Std.Do.SVal.pure default }

class Std.Do.SVal.GetTy (σ : Type) (σs : List Type) : Type

• get : SVal σs σ

instance Std.Do.SVal.instGetTyCons {σ : Type} {σs : List Type} : GetTy σ (σ :: σs)

Equations

• Std.Do.SVal.instGetTyCons = { get := fun (s : σ) => Std.Do.SVal.pure s }

instance Std.Do.SVal.instGetTyCons_1 {σ₁ : Type} {σs : List Type} {σ₂ : Type} [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs)

Equations

• Std.Do.SVal.instGetTyCons_1 = { get := fun (x : σ₂) => Std.Do.SVal.GetTy.get }

def Std.Do.SVal.getThe {σs : List Type} (σ : Type) [GetTy σ σs] : SVal σs σ

Get the top-most state of type σ from an SVal.

Equations

• Std.Do.SVal.getThe σ = Std.Do.SVal.GetTy.get

@[simp]

theorem Std.Do.SVal.getThe_here {σs : List Type} (σ : Type) (s : σ) : getThe σ s = pure s

@[simp]

theorem Std.Do.SVal.getThe_there {σ : Type} {σs : List Type} [GetTy σ σs] (σ' : Type) (s : σ') : getThe σ s = getThe σ