variables

python.Variables.user

def Variables.user (name : String) : Bool

Whether a name is the user’s (the translation’s own names start with a dot or a space).

python.Variables.maybe

def Variables.maybe (x : Option String) : List String

The optional name x as a list of names.

python.Variables.at

def Variables.at (n : String) (names : List String) : List (String * String)

The names bound at the node n.

python.Variables.parameterBinds

def Variables.parameterBinds (a : python.ast.Arguments) : List (String * String)

A function’s parameters a with their nodes.

python.Variables.functionBinds

def Variables.functionBinds (f : Symbol) : List (String * String)

The binding nodes of the function f: its parameters’, then its body’s.

python.Variables.declOf

def Variables.declOf (binds : List (String * String)) (name : String) : String

The first binding node of name among binds (empty when it has none).

python.Shown

record Shown

A function as the debugger shows it: its name in the program’s table, its name shown, its locals’ places, its own locals (not its free names), its captured locals and its binding nodes.

python.Variables.path

def Variables.path (methods : List (String * String)) (infos : List Symbol) (fuel : Nat) (f : Symbol) : String

The name shown of the function f among the program’s functions infos (within fuel levels): a nested function’s after its enclosing ones, a method’s after its class (the class each method belongs to in methods).

python.Variables.display

def Variables.display (methods : List (String * String)) (infos : List Symbol) (f : Symbol) : String

The name shown of the function f, made unique among the program’s functions infos (the class each method belongs to in methods): one shown like an earlier function’s gets a mark (code 1) and its number.

python.Variables.shown

def Variables.shown (methods : List (String * String)) (infos : List Symbol) (f : Symbol) : Shown

The function f as the debugger shows it, among the program’s functions infos (the class each method belongs to in methods).

python.Shows

record Shows

What the debugger shows of a program: the module’s names with their slots and declaration nodes, and its functions.

python.Variables.moduleDecl

def Variables.moduleDecl (body : List python.ast.Stmt) (infos : List Symbol) (name : String) : String

The declaration node of the module’s name: its first binding in the module’s body, else where a function among infos declaring it global binds it.

python.Variables.of

def Variables.of (p : python.ast.Program) : Shows

What the debugger shows of the program p (its module’s slots as Lowering.program lays them out).

python.Shows.function

def Shows.function (x : Shows) (table : String) : Option Shown

The function among those x shows whose name in the program’s table is table (a generator’s continuation is its function’s).

python.Variables.generatorState

def Variables.generatorState (g : Suspended) : String

The state of the generator g as CPython’s inspect.getgeneratorstate names it.

python.Variables.shownValue

def Variables.shownValue (h : Heap) (captured : Bool) (v : Option Value) : Option Value

The value a variable holding v shows: a captured one’s is in its cell on the heap h.

python.Variables.slot

def Variables.slot (p : Place) : Nat

The slot of the place p.

python.Variables.captured

def Variables.captured (p : Place) : Bool

Whether the place p holds a cell.

python.Variables.moduleName

def Variables.moduleName (v : Value) : Option Codes

A module’s name, when v is one (the model holds import math as a class named module math).

python.Variables.typeOf

def Variables.typeOf (h : Heap) (v : Value) : String

The type name of v as the debugger shows it (a module’s is module), read from the heap h.

python.Variables.reprOf

def Variables.reprOf (h : Heap) (v : Value) : String

The repr of v on the heap h as the debugger shows it (a module’s is <module 'name'>, without where CPython found it).

python.Variables.plain

def Variables.plain (h : Heap) (id : String) (name : String) (decl : String) (v : Option Value) : List (String * Json)

A variable’s fields as JSON: its id, name, the type and repr of its value v on the heap h (null while unbound), its declaration node decl.

python.Variables.saved

def Variables.saved (h : Heap) (owner : String) (f : Shown) (locals : List (Option Value)) : List Json

A suspended generator’s own local variables that are bound, from its kept locals on the heap h (each shown plainly): those of its function f, their ids under the generator variable’s id owner.

python.Variables.generatorFields

def Variables.generatorFields (x : Shows) (h : Heap) (owner : String) (g : Suspended) : List (String * Json)

The state of the generator g, and its local variables unless it is running or done: its function looked up in what x shows, values on the heap h, ids under the generator variable’s id owner.

python.Variables.json

def Variables.json (x : Shows) (h : Heap) (id : String) (name : String) (decl : String) (v : Option Value) : Json

The variable name with the id id, the declaration node decl and the value v on the heap h, as JSON (a generator’s with its state and frame, its function looked up in what x shows).

python.Variables.globals

def Variables.globals (x : Shows) (s : Run) : String

The globals of the run s as JSON: the module’s names x shows, in the order of their slots.

python.Variables.locals

def Variables.locals (x : Shows) (h : Heap) (f : Shown) (locals : Array (Option Value)) : Json

The own local variables of a call of the function f as JSON, read from its locals on the heap h (a generator’s function looked up in what x shows).

python.Variables.call

def Variables.call (x : Shows) (h : Heap) (function : String) (at : String) (locals : Array (Option Value)) : Json

One shown call, as x shows it: its function (a name in the program’s table; a class body’s is its class’s name, the module’s is empty), the node it is at, its variables read from its locals on the heap h (the module’s and a class body’s have none).

python.Variables.statementAt

def Variables.statementAt (last : List (Nat * String)) (depth : Nat) : Option String

The statement last entered at a depth of calls (none when there is none).

python.Variables.calls

def Variables.calls (x : Shows) (h : Heap) (last : List (Nat * String)) (depth : Nat) (at : String) (locals : Array (Option Value)) (frames : List (Frame Run Signal Stop)) : List Json

The calls of a run as x shows them, innermost first, from the node it is at, its locals and its depth of calls, values on the heap h: a call’s frame (in frames) says whose they are, and holds the caller’s state; a caller is at the statement it last entered at its depth (else the call); the model’s own calls are passed over; the module’s comes last.

python.Variables.frames

def Variables.frames (x : Shows) (last : List (Nat * String)) (at : String) (c : Configuration Run Signal Stop) : String

The calls of the run c stopped at the node at, as JSON as x shows them, innermost first (with the statements last entered at each depth of calls and the depth it is at).

python.Variables.literal

def Variables.literal (text : String) : Either String Value

The Python literal text a variable is set from: a number, a string in quotes, True, False or None.

python.Variables.setLocal

def Variables.setLocal (f : Shown) (id : String) (v : Value) (locals : Locals) : Option (Either String Locals)

locals with the own variable id of a call of the function f set to v: none when the call has no such variable; an error for a captured one.

python.Locals

def Locals : Type

A call’s locals.

python.Change

data Change

Where a variable is set: in the locals of a call below (the frames rebuilt with them), or in the globals.

python.Variables.change

def Variables.change (x : Shows) (n : Nat) (id : String) (v : Value) (locals : Array (Option Value)) (frames : List (Frame Run Signal Stop)) : Either String Change

The variable id of the n-th call x shows set to v, from the locals of the call the frames say (innermost first; the model’s own calls are not counted): the frames rebuilt with the caller’s locals changed.

python.Variables.setGlobal

def Variables.setGlobal (x : Shows) (id : String) (v : Value) (s : Run) : Either String Run

The module variable named id (among those x shows) set to v in the globals of the run s.

python.Variables.set

def Variables.set (x : Shows) (n : Nat) (id : String) (text : String) (c : Configuration Run Signal Stop) : Either String (Configuration Run Signal Stop)

The run c with the variable id of the n-th call x shows (innermost first) set from the Python literal text.