statement

machine.Exit

data Exit (S : Type) (R : Type) (Q : Type)

How a statement ended: normally, by break, by continue, by returning a value, or stopped with a reason.

machine.SwitchLabel

data SwitchLabel

A switch label: a case value, or the default.

machine.Statement

data Statement (S : Type) (R : Type) (Q : Type)

The statements of the machine.

machine.Frame

data Frame (S : Type) (R : Type) (Q : Type)

What to do after the current statement.

machine.Configuration

data Configuration (S : Type) (R : Type) (Q : Type)

A configuration: running a statement with frames on a state, or halted with an exit.

machine.Exit.withState

def Exit.withState {S : Type} {R : Type} {Q : Type} (e : Exit S R Q) (s : S) : Exit S R Q

The exit e with its state replaced by s (a cleanup that finished normally hands its state to the exit it delayed).

machine.Configuration.push

def Configuration.push {S : Type} {R : Type} {Q : Type} (c : Statement S R Q) (frame : Frame S R Q) (frames : List (Frame S R Q)) (s : S) : Configuration S R Q

Runs c next on the state s, with frame pushed on frames.

machine.Configuration.stopWith

def Configuration.stopWith {S : Type} {R : Type} {Q : Type} (q : Q) : Configuration S R Q

Halts on a stop with the reason q.

machine.Configuration.unwindNormal

def Configuration.unwindNormal {S : Type} {R : Type} {Q : Type} (s : S) (frame : Frame S R Q) (rest : List (Frame S R Q)) : Configuration S R Q

Leaving normally with the state s: the nearest frame frame decides (the next statement, the loop’s next check, back to the caller); rest are the frames under it.

machine.Configuration.unwindBreak

def Configuration.unwindBreak {S : Type} {R : Type} {Q : Type} (s : S) (frame : Frame S R Q) (rest : List (Frame S R Q)) : Configuration S R Q

Leaving by break with the state s, frame the nearest frame and rest the ones under it: out of the nearest loop or switch.

machine.Configuration.unwindContinue

def Configuration.unwindContinue {S : Type} {R : Type} {Q : Type} (s : S) (frame : Frame S R Q) (rest : List (Frame S R Q)) : Configuration S R Q

Leaving by continue with the state s, frame the nearest frame and rest the ones under it: back to the nearest loop’s next check (a switch passes it on).

machine.Configuration.unwindReturn

def Configuration.unwindReturn {S : Type} {R : Type} {Q : Type} (v : R) (s : S) (frame : Frame S R Q) (rest : List (Frame S R Q)) : Configuration S R Q

Leaving by returning v with the state s, frame the nearest frame and rest the ones under it: back to the caller, unless the value unwinds through it (an exception) or a try catches it.

machine.Configuration.unwind

def Configuration.unwind {S : Type} {R : Type} {Q : Type} (e : Exit S R Q) (frames : List (Frame S R Q)) : Configuration S R Q

Leaves the current statement with the exit e, frame by frame through frames; with no frames left the machine halts.

machine.Configuration.countedStep

def Configuration.countedStep {S : Type} {R : Type} {Q : Type} (n : Nat) (body : (k : Nat) -> Nat.blt k n = true -> Statement S R Q) (fuel : Nat) (j : Nat) (frames : List (Frame S R Q)) (s : S) : Configuration S R Q

One iteration of a counted loop at index j with bound n: below the bound, run body with the proof of the bound, else leave to frames with the state s; fuel is how many iterations may still run.

machine.Configuration.countedStepAt

def Configuration.countedStepAt {S : Type} {R : Type} {Q : Type} (n : Nat) (body : (k : Nat) -> Nat.blt k n = true -> Statement S R Q) (g : Nat) (j : Nat) (frames : List (Frame S R Q)) (s : S) (b : Bool) (e : Nat.blt j n = b) : Configuration S R Q

A counted-loop iteration at index j with bound n, by the outcome b of the bound check (e its proof): when true, run body at j and come back with g iterations left at the next index, else leave to frames with the state s.

machine.SwitchLabel.isCase

def SwitchLabel.isCase (v : Int) (l : SwitchLabel) : Bool

Whether the switch label l is the case for the value v.

machine.SwitchLabel.isDefault

def SwitchLabel.isDefault (l : SwitchLabel) : Bool

Whether the switch label l is the default.

machine.SwitchLabel.find

def SwitchLabel.find (p : SwitchLabel -> Bool) (labels : Nat -> SwitchLabel) (j : Nat) (r : Nat) : Option Nat

The first block from j among the next r whose label (read from labels) satisfies p.

machine.SwitchLabel.start

def SwitchLabel.start (v : Int) (n : Nat) (labels : Nat -> SwitchLabel) : Option Nat

Where a switch on v over n blocks labeled by labels starts: the matching case, else the default, else nowhere.

machine.Configuration.switchStart

def Configuration.switchStart {S : Type} {R : Type} {Q : Type} (n : Nat) (blocks : Nat -> Statement S R Q) (start : Option Nat) (frames : List (Frame S R Q)) (s : S) : Configuration S R Q

Jumps into a switch of n blocks at start: run the blocks from there in order (fallthrough), inside a frame that absorbs break, above frames and with the state s; with no start the switch is done.

machine.Configuration.stepRun

def Configuration.stepRun {S : Type} {R : Type} {Q : Type} (c : Statement S R Q) (k : List (Frame S R Q)) (s : S) : Configuration S R Q

One move of the current statement c, with the frames k after it, on the state s.

machine.Configuration.step

def Configuration.step {S : Type} {R : Type} {Q : Type} (x : Configuration S R Q) : Configuration S R Q

One move of the machine in the configuration x; a halted machine stays halted.

machine.Configuration.runLeft

def Configuration.runLeft {S : Type} {R : Type} {Q : Type} (fuel : Nat) (x : Configuration S R Q) : Configuration S R Q * Nat

Runs x at most fuel moves: where it got, and the fuel left unused (a halted machine keeps the rest).

machine.Configuration.run

def Configuration.run {S : Type} {R : Type} {Q : Type} (fuel : Nat) (x : Configuration S R Q) : Configuration S R Q

Runs x at most fuel moves (Configuration.runLeft without the fuel left).

machine.Configuration.labelOf

def Configuration.labelOf {S : Type} {R : Type} {Q : Type} (x : Configuration S R Q) : Option String

The outside label of the statement x is about to run, if it is labeled.

machine.Configuration.start

def Configuration.start {S : Type} {R : Type} {Q : Type} (c : Statement S R Q) (s : S) : Configuration S R Q

A machine about to run the statement c on the state s with nothing after it.