Exception Postcondition Stack Notation

A monad transformer stack carries one exception postcondition for each transformer that throws. A stack of postconditions is a right-nested × chain with the marker type EStackEnd as its last component. EStack⟨Nat → σ → Prop, String → σ → Prop⟩ is the stack of ExceptT Nat (ExceptT String (StateM σ)), and estack⟨e₁, e₂⟩ is a value of it. The notation hides the nesting and the markers. EStackEnd and EStackEnd.mk are abbreviations of Unit and (), so the unexpanders can recognize a stack while every Unit instance still applies.

A base monad has one exception postcondition and no stack, so it does not use the notation: Except ε carries a bare ε → Prop.

Any other type of exception postconditions can declare a ToEStack instance, and vcgen then weakens its values one stack component at a time.

@[reducible, inline]

abbrev Std.WP.EStackEnd : Type

The last component of an exception postcondition stack. It reduces to Unit, so every Unit instance applies. It is a named constant, so only a stack prints as EStack⟨…⟩.

Equations

• EStack⟨⟩ = Unit

@[reducible, inline]

abbrev Std.WP.EStackEnd.mk : EStack⟨⟩

The value of the last stack component. It reduces to (). It is a named constant, so only a stack value prints as estack⟨…⟩.

Equations

• estack⟨⟩ = ()

def Std.WP.«termEStack⟨_⟩» : Lean.ParserDescr

Exception postcondition stack type: EStack⟨ε₁ → l, ε₂ → l⟩ is (ε₁ → l) × (ε₂ → l) × EStack⟨⟩.

Equations

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

def Std.WP.«termEstack⟨_⟩» : Lean.ParserDescr

Exception postcondition stack value: estack⟨e₁, e₂⟩ is (e₁, e₂, ()).

Equations

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

def Std.WP.unexpandEStackEnd : Lean.PrettyPrinter.Unexpander

Prints EStackEnd as EStack⟨⟩.

Equations

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

def Std.WP.unexpandEStack : Lean.PrettyPrinter.Unexpander

Prints a product that ends in EStack⟨⟩ as EStack⟨e₁, e₂, …⟩.

Equations

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

def Std.WP.unexpandEStackEndMk : Lean.PrettyPrinter.Unexpander

Prints EStackEnd.mk as estack⟨⟩.

Equations

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

def Std.WP.unexpandEStackMk : Lean.PrettyPrinter.Unexpander

Prints a tuple that ends in estack⟨⟩ as estack⟨e₁, e₂, …⟩.

Equations

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

theorem Std.WP.EStackEnd.bot_eq [Lean.Order.CCPO EStack⟨⟩] : Lean.Order.bot = estack⟨⟩

⊥ at the end of an exception postcondition stack is the empty stack value.

class Std.WP.ToEStack (E : Type u) (T : outParam (Type u)) [Assertion E] [Assertion T] : Type u

toEStack exposes the exception postconditions E as a stack. Example: Thrown with the field onThrow : String → Prop has toEStack t = estack⟨t.onThrow⟩, and vcgen weakens onThrow.

• toEStack : E → T

  The stack that E converts to.

• le_of_toEStack_le {x y : E} : Lean.Order.PartialOrder.rel (toEStack x) (toEStack y) → Lean.Order.PartialOrder.rel x y

  An entailment between the stacks is an entailment between the originals.