symbols

python.Scope

record Scope

What a scope itself has (not going into nested functions and lambdas): the names it binds, the names it reads, the ones it declares global and nonlocal, whether it yields.

python.Scope.empty

def Scope.empty : Scope

A scope with nothing.

python.Scope.join

def Scope.join (a : Scope) (b : Scope) : Scope

The contents of the scopes a and b together.

python.Scope.all

def Scope.all (scopes : List Scope) : Scope

The contents of scopes together.

python.Scope.binding

def Scope.binding (names : List String) : Scope

Binding names.

python.Scope.reading

def Scope.reading (name : String) : Scope

Reading a name.

python.Scope.yielding

def Scope.yielding : Scope

A yield.

python.Names.without

def Names.without (names : List String) (out : List String) : List String

names without the ones in out.

python.Names.has

def Names.has (names : List String) (x : String) : Bool

Whether x is among names.

python.Symbols.imported

def Symbols.imported (a : python.ast.Alias) : String

The name the import alias a binds: the as name, else the first part of the module’s name.

python.Symbols.comprehensionNames

def Symbols.comprehensionNames (gs : List python.ast.Comprehension) : List String

The variables a comprehension’s fors, gs, bind.

python.Symbols.capturing

def Symbols.capturing (gs : List python.ast.Comprehension) (elt : python.ast.Expr) (value : python.ast.Expr) : Bool

Whether a comprehension is a function of its own: a lambda in it captures its variables. It has the fors gs, the item elt (a dict comprehension’s key) and value (a dict comprehension’s value, the item again otherwise).

python.Symbols.firstIterable

def Symbols.firstIterable (gs : List python.ast.Comprehension) : Option python.ast.Expr

The iterable of the first of a comprehension’s fors, gs, which is read where the expression is (the rest of a generator expression or a capturing comprehension is its own scope).

python.Body

data Body

A function’s body: statements, or a lambda’s expression.

python.Body.scope

def Body.scope (b : Body) : Scope

What the body b adds to its scope.

python.Symbols.firstParameter

def Symbols.firstParameter : python.ast.Arguments

The parameters of a function made from a generator expression or a capturing comprehension: .0, its first iterable.

python.Symbols.alwaysStop

def Symbols.alwaysStop (n : String) : python.ast.Stmt

A stop the debugger always takes at the node n (its label marked with code 1): where a comprehension’s loop goes back.

python.Symbols.filters

def Symbols.filters (n : String) (ifs : List python.ast.Expr) (inner : List python.ast.Stmt) : List python.ast.Stmt

A comprehension’s filters ifs around the statements inner, at the node n.

python.Symbols.comprehensionLoops

def Symbols.comprehensionLoops (n : String) (inner : python.ast.Stmt) (gs : List python.ast.Comprehension) (first : Bool) : List python.ast.Stmt

A comprehension’s loops over its fors gs around the statement inner (the outermost over .0 when first), with a stop at the end of each round, at the node n.

python.Symbols.generatorBody

def Symbols.generatorBody (n : String) (elt : python.ast.Expr) (gs : List python.ast.Comprehension) : List python.ast.Stmt

A generator expression’s body at the node n: a stop at its start and the loops over its fors gs yielding each item elt (CPython stops where the generator starts and where each loop goes back).

python.Symbols.comprehensionSteps

def Symbols.comprehensionSteps (n : String) (kind : Nat) (elt : python.ast.Expr) (value : python.ast.Expr) (gs : List python.ast.Comprehension) : List python.ast.Stmt

A comprehension’s statements at the node n (kind 0 a list, 1 a set, 2 a dict): the items elt (a dict’s keys, with their value) collected in .acc over the fors gs, the first loop over .0.

python.Symbols.comprehensionBody

def Symbols.comprehensionBody (n : String) (kind : Nat) (elt : python.ast.Expr) (value : python.ast.Expr) (gs : List python.ast.Comprehension) : List python.ast.Stmt

A capturing comprehension as a function’s body at the node n: its statements (Symbols.comprehensionSteps of kind, elt, value and gs), then .acc returned.

python.Discovered

record Discovered

A function found while collecting: its number, name, enclosing function, node, parameters, body, whether it is a lambda.

python.Collected

record Collected

What collecting has so far: the next number and the functions found, in order.

python.Collected.add

def Collected.add (c : Collected) (f : Discovered) : Collected

c with the function f added under the next number.

python.Collected.function

def Collected.function (c : Collected) (name : String) (parent : Option Nat) (node : String) (a : python.ast.Arguments) (b : Body) (lambda : Bool) : Collected

c with the function name found at node added, numbered next: inside the function numbered parent, with the parameters a and the body b, a lambda when lambda.

python.Symbols.argumentName

def Symbols.argumentName (x : python.ast.Arg) : String

The name of the parameter x.

python.Symbols.parameterNames

def Symbols.parameterNames (a : python.ast.Arguments) : List String

The names of the parameters a: positional-only, positional, *args, keyword-only, **kwargs.

python.Part

record Part

A function after its own scope is known (its free names not yet): its locals (parameters and bound names, not global or nonlocal), its global and nonlocal names, the names it reads, whether it is a generator.

python.Symbols.part

def Symbols.part (f : Discovered) : Part

The own scope of the function f found while collecting.

python.Symbols.find

def Symbols.find (parts : List Part) (k : Nat) : Option Part

The function numbered k among parts.

python.Symbols.enclosingHas

def Symbols.enclosingHas (parts : List Part) (p : Option Nat) (x : String) (fuel : Nat) : Bool

Whether the function numbered p or one around it (within fuel levels) has the name x as a local, looked up among parts.

python.Symbols.childFrees

def Symbols.childFrees (parts : List Part) (frees : List (Nat * List String)) (k : Nat) : List String

The free names of the functions among parts directly inside the function numbered k, from the ones already known in frees (by function number).

python.Symbols.freeOf

def Symbols.freeOf (parts : List Part) (frees : List (Nat * List String)) (x : Part) : List String

The free names of the function x: the ones it reads or declares nonlocal and its children’s free ones (known in frees), not its own locals or globals, that an enclosing function among parts has.

python.Symbols.frees

def Symbols.frees (parts : List Part) (rest : List Part) (known : List (Nat * List String)) : List (Nat * List String)

The free names of the functions rest, from the last function to the first (a function’s children are after it), added to the ones known; parts are all the functions.

python.Symbol

record Symbol

One function of the program, after the symbol table is built.

python.Symbols.finished

def Symbols.finished (parts : List Part) (frees : List (Nat * List String)) (x : Part) : Symbol

The symbol of the function x from its own scope and the free names known in frees, its cells from its children among parts.

python.Symbols.of

def Symbols.of (p : python.ast.Program) : List Symbol

The symbol table of the program p: every function of the program, numbered in order of appearance.