Slots of the exception postconditions

EPostSlot EPosts ε EPred locates the slot for exceptions of type ε inside exception postconditions of type EPosts, and EPostSlot.set fills that slot. The throws clause of a def contract builds its exception postconditions with it: for ExceptT ε₁ (ExceptT ε₂ (StateM σ)) and a clause on ε₂, the term EPostSlot.set R ⊥ simplifies to (⊥, R, estack⟨⟩).

Instance search dispatches on the exception type in the manner of MonadExceptOf: an unconstrained ε lands in the outermost slot.

class Std.WP.EPostSlot (EPosts : Type w) (ε : Type u) (EPred : outParam (Type v)) : Type (max (max u v) w)

Locates the slot for exceptions of type ε inside exception postconditions of type EPosts. The slot holds assertions of type ε → EPred.

• set (R : ε → EPred) (eposts : EPosts) : EPosts

  Fills the ε slot of eposts with R. Example: set R (R₁, R₂) = (R₁, R) for ε in the second slot.

@[instance_reducible]

instance Std.WP.instEPostSlotFun {ε : Type u} {EPred : Type v} : EPostSlot (ε → EPred) ε EPred

A bare exception postcondition such as Except ε's ε → Prop is its own slot.

Equations

• Std.WP.instEPostSlotFun = { set := fun (R x : ε → EPred) => R }

@[instance_reducible]

instance Std.WP.instEPostSlotHead {ε : Type u} {EPred : Type v} {EPosts : Type w} : EPostSlot ((ε → EPred) × EPosts) ε EPred

The slot at the head of an exception postcondition stack.

Equations

• Std.WP.instEPostSlotHead = { set := fun (R : ε → EPred) (eposts : (ε → EPred) × EPosts) => (R, eposts.snd) }

@[instance_reducible, instance 100]

instance Std.WP.instEPostSlotTail {ε : Type u} {ε' : Type u'} {EPred : Type v} {EPred' : Type v'} {EPosts : Type w} [EPostSlot EPosts ε EPred] : EPostSlot ((ε' → EPred') × EPosts) ε EPred

A slot in the tail of an exception postcondition stack. The head instance is tried first, so an unconstrained ε lands in the outermost slot.

Equations

• Std.WP.instEPostSlotTail = { set := fun (R : ε → EPred) (eposts : (ε' → EPred') × EPosts) => (eposts.fst, Std.WP.EPostSlot.set R eposts.snd) }

theorem Std.WP.EPostSlot.set_fun {ε : Type u} {EPred : Type v} (R eposts : ε → EPred) : set R eposts = R

Unfolds set at a bare exception postcondition.

theorem Std.WP.EPostSlot.set_head {ε : Type u} {EPred : Type v} {EPosts : Type w} (R : ε → EPred) (eposts : (ε → EPred) × EPosts) : set R eposts = (R, eposts.snd)

Unfolds set at the head slot of a stack.

theorem Std.WP.EPostSlot.set_tail {ε : Type u} {ε' : Type u'} {EPred : Type v} {EPred' : Type v'} {EPosts : Type w} [EPostSlot EPosts ε EPred] (R : ε → EPred) (eposts : (ε' → EPred') × EPosts) : set R eposts = (eposts.fst, set R eposts.snd)

Unfolds set at a slot in the tail of a stack.