State-indexed values

@[reducible, inline]

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

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 u)) : Type u

A tuple capturing the whole state of an SVal.

Equations

• Std.Do.SVal.StateTuple [] = PUnit
• 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 u_1} {σs : List (Type u_1)} [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs))

Equations

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

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

Curry a function taking a StateTuple into an SVal.

Equations

• Std.Do.SVal.curry f_2 = f_2 PUnit.unit
• Std.Do.SVal.curry f_2 = fun (s : head) => Std.Do.SVal.curry fun (s' : Std.Do.SVal.StateTuple tail) => f_2 (s, s')

@[simp]

theorem Std.Do.SVal.curry_nil {α : Type u_1} {f : StateTuple [] → α} : curry f = f PUnit.unit

@[simp]

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

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

Uncurry an SVal into a function taking a StateTuple.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Do.SVal.curry_uncurry {α : Type u} {σs : List (Type u)} {f : SVal σs α} : curry f.uncurry = f

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

Equations

• Std.Do.SVal.instInhabited = { default := Std.Do.SVal.curry fun (x : Std.Do.SVal.StateTuple σs) => default }

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

• get : SVal σs σ

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

Equations

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

instance Std.Do.SVal.instGetTyCons_1 {σ₁ : Type u_1} {σs : List (Type u_1)} {σ₂ : Type u_1} [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 u)} (σ : Type u) [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 u)} (σ : Type u) (s : σ) : getThe σ s = curry fun (x : StateTuple σs) => s

@[simp]

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