checked

machine.Checked

data Checked (R : Type) (A : Type)

A value of type A, or a stop with a reason of type R.

machine.Checked.bind

def Checked.bind {R : Type} {A : Type} {B : Type} (x : Checked R A) (next : A -> Checked R B) : Checked R B

Continues with next applied to the value of x, or keeps the stop of x.

machine.Checked.map

def Checked.map {R : Type} {A : Type} {B : Type} (f : A -> B) (x : Checked R A) : Checked R B

Applies f to the value of x; a stop is kept.

machine.Checked.fold

def Checked.fold {R : Type} {A : Type} {X : Type} (x : Checked R A) (onValue : A -> X) (onStop : R -> X) : X

Handles both outcomes of x: onValue receives the value, onStop the reason of a stop.

machine.Checked.require

def Checked.require {R : Type} {A : Type} (reason : R) (pre : Bool) (operation : pre = true -> Checked R A) : Checked R A

Runs operation when the precondition pre holds, handing it the proof; otherwise stops with reason.

machine.Checked.and

def Checked.and {R : Type} (a : Checked R Bool) (b : Checked R Bool) : Checked R Bool

Short-circuit and: the right side b is evaluated only when the left side a is true.

machine.Checked.or

def Checked.or {R : Type} (a : Checked R Bool) (b : Checked R Bool) : Checked R Bool

Short-circuit or: the right side b is evaluated only when the left side a is false.

machine.Checked.ifThen

def Checked.ifThen {R : Type} {A : Type} (c : Checked R Bool) (yes : Checked R A) (no : Checked R A) : Checked R A

Conditional on c: only the chosen branch, yes or no, is evaluated.

machine.Checked.bindProceed

def Checked.bindProceed {R : Type} {A : Type} {B : Type} (a : A) (next : A -> Checked R B) : Checked.bind (proceed a) next = next a

Binding a value a continues with next applied to it.

machine.Checked.requireTrue

def Checked.requireTrue {R : Type} {A : Type} (reason : R) (operation : true = true -> Checked R A) : Checked.require reason true operation = operation refl

A met precondition runs operation; reason is not used.

machine.Checked.requireFalse

def Checked.requireFalse {R : Type} {A : Type} (reason : R) (operation : false = true -> Checked R A) : Checked.require reason false operation = halt reason

A failed precondition stops with reason; operation is never run.