debugger

machine.Halt

data Halt (W : Type) (S : Type) (E : Type) (O : Type)

How a halted run ends, as the language classifies it.

machine.Stop

data Stop (C : Type) (W : Type) (S : Type) (E : Type) (O : Type)

Why the driver stopped (Stop.kind numbers them for the host). A divergence stops at the boundary before the move that noted it: before is the configuration the move started from (what the stop reports: output, variables) and configuration the one after it (its notes; the run goes on from there, without taking the move again).

machine.Stop.kind

def Stop.kind {C : Type} {W : Type} {S : Type} {E : Type} {O : Type} (s : Stop C W S E O) : Nat

Which kind of stop it is, as the debugging host reads it (the stopKind export): 0 breakpoint, 1 step, 2 fuel spent, 3 awaiting input, 4 undefined behavior, 5 terminated, 6 exited, 7 unspecified behavior, 8 diverged. A host reads this instead of the value’s constructor, which a module wrapping its stops in its own type does not keep.

machine.Machine

record Machine (C : Type) (M : Type) (W : Type) (S : Type) (E : Type) (O : Type)

A language’s machine as the driver sees it: C configurations, M the memory carried between moves.

machine.StepMode

data StepMode

What a step asks for: run to a breakpoint, stop at the next node, stop at the next node no deeper, or shallower.

machine.StepMode.wants

def StepMode.wants (request : StepMode) (depth : Nat) : Bool

Whether a step asked for by request stops at a node at call depth depth.

machine.Stop.ofHalt

def Stop.ofHalt {C : Type} {W : Type} {S : Type} {E : Type} {O : Type} (h : Halt W S E O) : Stop C W S E O

The stop for a run that halted as h.

machine.Visits

def Visits : Type

How many times a run entered each node, by the node’s label.

machine.Visits.none

def Visits.none : Visits

No node entered yet.

machine.Visits.add

def Visits.add (v : Visits) (node : String) : Visits

The counts v with one more entry into node.

machine.Visits.merge

def Visits.merge (a : Visits) (b : Visits) : Visits

The counts a and b of two runs together.

machine.Visits.json

def Visits.json (v : Visits) : String

The counts v as JSON, {"<node>": n} by the nodes’ order.

machine.Stop.isBreakpoint

def Stop.isBreakpoint (node : String) (breakpoints : List String) : Bool

Whether a node is one of the breakpoints.

machine.Machine.after

def Machine.after {C : Type} {M : Type} {W : Type} {S : Type} {E : Type} {O : Type} (m : Machine C M W S E O) (closed : Bool) (breakpoints : List String) (request : StepMode) (fuel : Nat) (memory : M) (visits : Visits) (x : C) (y : C) : Stop C W S E O * Visits

After the machine m moves from x to y: halted, diverged, quiet, at one of the breakpoints, at the stop the step request asks for, or on to the next move with fuel moves left. memory is what m carries between moves, closed whether the input is closed, and a node the move enters is added to visits whether or not the run stops there.

machine.Machine.runTo

def Machine.runTo {C : Type} {M : Type} {W : Type} {S : Type} {E : Type} {O : Type} (m : Machine C M W S E O) (closed : Bool) (breakpoints : List String) (request : StepMode) (fuel : Nat) (memory : M) (visits : Visits) (x : C) : Stop C W S E O * Visits

Runs the machine m from x to the next stop, at most fuel moves, counting the nodes entered on top of visits; breakpoints, request and memory are as in Machine.after. A move that m says would wait for input (given whether the input is closed) is not taken.

machine.Machine.debugRunCounted

def Machine.debugRunCounted {C : Type} {M : Type} {W : Type} {S : Type} {E : Type} {O : Type} (m : Machine C M W S E O) (kind : Nat) (closed : Bool) (breakpoints : List String) (fuel : Nat) (memory : M) (x : C) : Stop C W S E O * Visits

Runs the machine m from x by the host’s kind of request (0 continue, 1 step in, 2 step over, 3 step out), with the breakpoints, at most fuel moves, starting from memory, the input closed or not: the stop and how many times the run entered each node.

machine.Machine.debugRun

def Machine.debugRun {C : Type} {M : Type} {W : Type} {S : Type} {E : Type} {O : Type} (m : Machine C M W S E O) (kind : Nat) (closed : Bool) (breakpoints : List String) (fuel : Nat) (memory : M) (x : C) : Stop C W S E O

Runs m from x as Machine.debugRunCounted does with the same kind, closed, breakpoints, fuel and memory: the stop alone.

machine.Stop.resumeFrom

def Stop.resumeFrom {C : Type} {W : Type} {S : Type} {E : Type} {O : Type} (d : C) (s : Stop C W S E O) : C

The configuration the stop s can resume from, or d when the run cannot continue.

machine.Stop.node

def Stop.node {C : Type} {W : Type} {S : Type} {E : Type} {O : Type} (s : Stop C W S E O) : String

The node the stop s is at (empty when it has none).