debugging

python.DebugRun

record DebugRun

A run for the debugger: the machine’s configuration, the nodes it stops at (the program’s statements’), the statement node last entered at each depth of the user’s calls, and the node the last move entered (none when it entered none to stop at).

python.Debugging.internal

def Debugging.internal (name : String) : Bool

Whether a function or a node is the model’s own (CPython runs it in C): model sort, builtin map.<resume>, or one with no name.

python.Debugging.depth

def Debugging.depth (x : Configuration Run Signal Stop) : Nat

How many of the user’s calls the configuration x is in (the state’s depth: the model’s own functions do not count).

python.Debugging.markedWith

def Debugging.markedWith (code : Nat) (label : String) : Bool

Whether a label is marked with a code first.

python.Debugging.forced

def Debugging.forced (label : String) : Bool

Whether a label is marked to always stop (the code 1 first).

python.Debugging.resumed

def Debugging.resumed (label : String) : Bool

Whether a label only tells the statement a resumed generator goes on with (the code 2 first).

python.Debugging.nodeOf

def Debugging.nodeOf (label : String) : String

A label’s node, without the mark.

python.Debugging.lastAt

def Debugging.lastAt (last : List (Nat * String)) (depth : Nat) : Option String

The node last entered at a depth (the remembered nodes are the deepest first, none deeper than it).

python.Debugging.remember

def Debugging.remember (last : List (Nat * String)) (depth : Nat) (node : String) : List (Nat * String)

The remembered nodes last (none deeper than depth) with node as the one at depth.

python.Debugging.atLabel

def Debugging.atLabel (x : Configuration Run Signal Stop) (label : String) : Bool

Whether the configuration x is at label.

python.Debugging.lineOf

def Debugging.lineOf (lines : List (String * Nat)) (n : String) : Option Nat

The line of the node n in the host’s table lines.

python.Debugging.sameLine

def Debugging.sameLine (lines : List (String * Nat)) (a : String) (b : String) : Bool

Whether the nodes a and b are on the same line in the host’s table lines (not when either has none).

python.Debugging.position

def Debugging.position (nodes : List String) (n : String) : Nat

The position of the node n among the program’s statement nodes (in the order of its syntax tree).

python.Debugging.moved

def Debugging.moved (d : DebugRun) (previous : String) (node : String) : Bool

Whether going from the statement previous, last entered at a depth, to the statement node moves to a new line, as CPython’s line event does: without the host’s table of lines in the run d, every other statement does; with it, one on another line, or one before it (a loop going back).

python.Debugging.entering

def Debugging.entering (d : DebugRun) (y : Configuration Run Signal Stop) : DebugRun

The run d after a move to the configuration y: the node y is about to enter, if it is one to stop at. A marked step stops when the move reaches it (not again on the move inside it) and leaves the node remembered at its depth as it was: the statement around it goes on without stopping again. A statement on the line of the one before it is remembered without stopping (Debugging.moved).

python.Debugging.step

def Debugging.step (d : DebugRun) : DebugRun

One move of the run d.

python.Debugging.stoppable

def Debugging.stoppable (p : python.ast.Program) : List String

The nodes the program p stops at: its statements’ (the functions the translation makes of its comprehensions and generator expressions stop only at their marked steps, python.symbols).

python.Debugging.start

def Debugging.start (p : python.ast.Program) (program : Code) (s : Run) : DebugRun

A run of the program p, translated into the code program, from its start in the state s, stopping at its statements.

python.Debugging.state

def Debugging.state (d : DebugRun) : Option Run

The state of the run d (none when it stopped without one).

python.Debugging.atEnd

def Debugging.atEnd (d : DebugRun) : Bool

Whether the last read of the run d reached the end of the input without a whole line.

python.Debugging.blocked

def Debugging.blocked (closed : Bool) (x : DebugRun) (y : DebugRun) : Bool

Whether a move from x to y waits for input: the input is not closed and the move reached its end.

python.Debugging.halt

def Debugging.halt (d : DebugRun) : Option (Halt String Run Raised Run)

How the run d, when finished, ends for the debugger: an uncaught exception, the end, or (what the model cannot do, or a stop) a behavior it does not specify.

python.Debugging.machine

def Debugging.machine : Machine DebugRun Unit String Run Raised Run

The Python model’s machine for the debugger driver.

python.Debugging.stepsFrom

def Debugging.stepsFrom (count : Nat) (fuel : Nat) (d : DebugRun) : List String

The nodes the run d stops at stepping in from its start to its end (at most count stops, each within fuel moves); the input given at the start and closed.

python.Debugging.stopsOf

def Debugging.stopsOf (src : String) (input : String) : List String

The nodes a program stops at, its syntax tree’s JSON src, stepping in from its start with the standard input (one starting with ? when it cannot run).

python.Debugging.lineTable

def Debugging.lineTable (text : String) : List (String * Nat)

A host’s table of the lines of nodes (JSON: an object from a node to its line); empty for text it cannot read.

python.Debugging.stopsWithLines

def Debugging.stopsWithLines (src : String) (input : String) (lines : String) : List String

The nodes a program, its syntax tree’s JSON src, stops at with the host’s table of lines (JSON), stepping in from its start with the standard input.

python.Debugging.stops

def Debugging.stops (src : String) (input : String) : String

The nodes a program, its syntax tree’s JSON src, stops at, stepping in from its start with the standard input, one per line.