querying

python.Querying.heap

def Querying.heap : Heap

The heap the representative values are on: an empty list at 0, an empty dict at 1, an empty set at 2.

python.Querying.representative

def Querying.representative (t : String) : Option Value

A value of the type t to try operations on (none for a type that has none).

python.Tried

data Tried

What trying an operation gave: the result’s type, a TypeError’s message, or something else (an exception that depends on the values).

python.Querying.outcome

def Querying.outcome (h : Heap) (o : Outcome) : Tried

What the outcome o on the representatives’ heap h tried.

python.Querying.evaluated

def Querying.evaluated (e : Expression) : Tried

What the expression e on the representatives tried.

python.Querying.changed

def Querying.changed (c : Changed) : Tried

What the change of the heap c tried.

python.HolePlace

data HolePlace

Where a hole is: an operand (the operation decides whether a type fits), a place any type fits, or elsewhere (it depends on values at run time).

python.Seen

record Seen

What walking a scope knows: the names’ types it sees, the built-in names there, the holes’ assumed types, the module’s types and built-in names, the enclosing functions’ locals (free names inside, of unknown type), the names some function changes with nonlocal.

python.Findings

record Findings

What walking finds: the nodes’ types, the type errors, the operations whose operands’ types are unknown, and the holes’ places (each list newest first).

python.Findings.empty

def Findings.empty : Findings

Nothing found.

python.Findings.node

def Findings.node (a : Findings) (n : String) (t : Option String) : Findings

The findings a with the type t of the node n added, when it is known.

python.Findings.error

def Findings.error (a : Findings) (n : String) (message : String) : Findings

The findings a with a type error at the node n, with its message, added.

python.Findings.undecided

def Findings.undecided (a : Findings) (n : String) : Findings

The findings a with the operation at the node n, whose operands’ types are not known, added.

python.Findings.hole

def Findings.hole (a : Findings) (label : String) (p : HolePlace) : Findings

The findings a with the place p of the hole labelled label added.

python.Querying.lookup

def Querying.lookup (x : String) (types : List (String * String)) : Option String

The type of the name x in the list of names’ types.

python.Querying.without

def Querying.without (xs : List String) (names : List String) : List String

The names without those in xs.

python.Seen.forget

def Seen.forget (c : Seen) (xs : List String) : Seen

The scope c without the names xs (they are its own, of unknown type).

python.Querying.builtinResults

def Querying.builtinResults : List (String * String)

The built-ins’ result types (whatever the arguments; a call that raises has no result).

python.Querying.same

def Querying.same (x : Option String) (y : Option String) : Option String

The types x and y when they are the same.

python.Querying.both

def Querying.both (left : Option String) (right : Option String) : Option (Value * Value)

The representatives of the types left and right, when both have one.

python.Querying.binary

def Querying.binary (n : String) (op : python.ast.BinOp) (augmented : Bool) (left : Option String) (right : Option String) (a : Findings) : Findings * Option String

x op y (or x op= y when augmented) at the node n, with its operands’ types left and right, added to the findings a: str % x formats (whether it fails depends on the format); else the operation tried on representatives.

python.Querying.unary

def Querying.unary (n : String) (op : python.ast.UnaryOp) (t : Option String) (a : Findings) : Findings * Option String

op x at the node n, with its operand’s type t, added to the findings a (not is always a bool).

python.Querying.comparison

def Querying.comparison (op : python.ast.CmpOp) (x : Value) (y : Value) : Tried

One comparison x op y tried on representatives.

python.Querying.compare

def Querying.compare (n : String) (ops : List python.ast.CmpOp) (types : List (Option String)) (first : Bool) (a : Findings) : Findings * Bool

x < y < z at the node n, its operators ops and its operands’ types, added to the findings a (first while at the first pair): only the first pair is always compared (the rest may be cut short); the result is a bool when all of them can be compared.

python.Querying.constant

def Querying.constant (v : python.ast.Constant) : Option String

The type of the constant v.

python.Querying.allSame

def Querying.allSame (ts : List (Option String)) : Option String

The type of all of some values, from their types ts, when they have the same.

python.Querying.builtin

def Querying.builtin (c : Seen) (x : String) (f : python.ast.Expr) : Bool

Whether the callee f is the name x and, in the scope c, a built-in’s.

python.Querying.called

def Querying.called (c : Seen) (f : python.ast.Expr) : Option String

The type of a call of f in the scope c: a built-in’s result.

python.Querying.typed

def Querying.typed (found : Findings) (n : String) (t : String) : Findings * Option String

An expression at the node n whose type t is known, added to what walking found.

python.Binding

data Binding

A plain binding of a name: x = e (and x: T = e), or x op= e.

python.Querying.named

def Querying.named (v : python.ast.Expr) (t : python.ast.Expr) : List (String * Binding)

A plain binding of the value v to the target t, when it is a name.

python.Querying.walrus

def Querying.walrus (e : python.ast.Expr) : List String

The names the expression e binds with :=.

python.Querying.walrusOf

def Querying.walrusOf (m : Option python.ast.Expr) : List String

The names the optional expression m binds with :=.

python.Querying.otherTargets

def Querying.otherTargets (t : python.ast.Expr) : List String

The names the target t binds when it is not a plain name (a.b, a[i], a, b).

python.Querying.argumentsBound

def Querying.argumentsBound (decorators : List python.ast.Expr) (arguments : python.ast.Arguments) : List String

The names a def’s decorators and the defaults of its arguments bind with :=.

python.Querying.bindingsOf

def Querying.bindingsOf (x : String) (plain : List (String * Binding)) : List Binding

The plain bindings of the name x among the block’s plain bindings.

python.Gives

data Gives

What a binding gives: a known type, never a value (its outermost operation always raises TypeError), or not known.

python.Findings.errorAt

def Findings.errorAt (a : Findings) (n : String) : Bool

Whether walking found, in the findings a, a type error at the node n.

python.Querying.gives

def Querying.gives (c : Seen) (x : String) (b : Binding) : Gives

What the binding b of the name x gives in the scope c.

python.Querying.seed

def Querying.seed (c : Seen) (x : String) (bs : List Binding) : Option String

The type the first plain assignment among the bindings bs of the name x that gives one gives in the scope c: the name’s candidate type.

python.Querying.keeps

def Querying.keeps (g : Gives) (t : String) : Bool

Whether a binding that gives g keeps the type t.

python.Querying.candidate

def Querying.candidate (c : Seen) (known : List (String * String)) (plain : List (String * Binding)) (x : String) : List (String * String)

The type of the name x when every binding of it among the block’s plain bindings keeps its candidate type (assuming the name has it, as x = x + 1 needs), in the scope c given the names known so far.

python.Querying.rounds

def Querying.rounds (c : Seen) (candidates : List String) (plain : List (String * Binding)) (fuel : Nat) (known : List (String * String)) : List (String * String)

The types of the candidates known after fuel rounds from those known, by the block’s plain bindings in the scope c (knowing more names only makes more bindings known, so as many rounds as names reach the fixed point).

python.Querying.scopeTypes

def Querying.scopeTypes (c : Seen) (unknown : List String) (body : List python.ast.Stmt) : List (String * String)

The types of the names the body of a scope binds, before those it sees from outside, the scope c; unknown are names whose type cannot be known (its parameters, names changed elsewhere).

python.Seen.function

def Seen.function (c : Seen) (arguments : python.ast.Arguments) (body : List python.ast.Stmt) : Seen

The scope of a function with arguments and body, defined in the scope c: its own locals are known by its own bindings; a name that is not local is the enclosing function’s (free, of unknown type) or else the module’s.

python.Seen.classBody

def Seen.classBody (c : Seen) (body : List python.ast.Stmt) : Seen

The scope of a class body in the scope c: the names it binds are the class’s attributes (not followed); its functions see the module.

python.Seen.module

def Seen.module (p : python.ast.Program) (holes : List (String * String)) : Seen

The scope of the module p (with the holes’ assumed types): a name some function declares global is not known.

python.Querying.target

def Querying.target (c : Seen) (a : Findings) (t : python.ast.Expr) : Findings

The assignment target t walked in the scope c, added to the findings a (a name’s binding is not an expression; a.b and a[i] are).

python.Querying.targets

def Querying.targets (c : Seen) (a : Findings) (ts : List python.ast.Expr) : Findings

The assignment targets ts walked in the scope c, added to the findings a.

python.Querying.analyze

def Querying.analyze (p : python.ast.Program) (holes : List (String * String)) : Findings

What walking the program p finds (the holes assumed of some types).

python.Fit

data Fit

How a candidate type fits a hole.

python.Querying.newError

def Querying.newError (base : List (String * String)) (errors : List (String * String)) : Option String

The first of the type errors not already among those found without the hole’s type, base.

python.Querying.fit

def Querying.fit (p : python.ast.Program) (base : Findings) (label : String) (place : HolePlace) (t : String) : Fit

How the type t fits the hole labelled label at place in the program p (base what walking it finds without the hole’s type): no when it makes a type error; else exact when the operation the hole is an operand of can be decided (or any type fits there), unknown otherwise.

python.Fit.exact

def Fit.exact (f : Fit) : Bool

Whether the fit f is exact.

python.Fit.unknown

def Fit.unknown (f : Fit) : Bool

Whether the fit f is unknown.

python.Querying.commas

def Querying.commas (xs : List String) : String

The names xs joined with commas.

python.Querying.exactly

def Querying.exactly (fits : List (String * Fit)) : List String

The candidate types that fit exactly, by their fits.

python.Querying.display

def Querying.display (fits : List (String * Fit)) : String

What a hole shows by how the candidate types fit it, fits: the one type it expects, the types it accepts, or why none is known.

python.Querying.expects

def Querying.expects (fits : List (String * Fit)) : Json

The type a hole expects, when exactly one of the fits fits exactly.

python.Fit.json

def Fit.json (f : Fit) : Json

The fit f as JSON.

python.Querying.slot

def Querying.slot (p : python.ast.Program) (base : Findings) (candidates : List String) (h : String * HolePlace) : String * Json

The entry of the hole h (its label and place) in the program p, with what walking finds without it, base: what it shows, the type it expects, how each of the candidates fits.

python.Querying.candidates

def Querying.candidates : List String

The candidate types tried in a hole when none are given.

python.Querying.json

def Querying.json (p : python.ast.Program) (candidates : List String) : String

The types of the program p as JSON, trying the candidates in each hole: {nodes, slots, errors}.

python.Querying.types

def Querying.types (source : String) (candidates : String) : String

The types of a program given as its syntax tree’s JSON, source, for the editor ({nodes, slots, errors}; see the module’s comment); candidates is a JSON list of the type names to try in each hole, empty for the default ones.

python.Observing.below

def Observing.below (n : String) (xs : List String) : List String

The node list xs without its first item when that is the node n (a callee’s own value is not in the table).

python.Observing.superReceiver

def Observing.superReceiver (f : python.ast.Expr) : Bool

Whether the callee f is super().attr: the model looks the method up without making a super object, so super() there has no value in the table.

python.Observing.withoutTraceback

def Observing.withoutTraceback (name : String) (a : python.ast.Arguments) : python.ast.Arguments

A function’s parameters a without the traceback one (the fourth positional) when it is __exit__ (name): the model gives it None, not the traceback CPython gives (Lowering.readsTraceback).

python.Observing.parameters

def Observing.parameters (xs : List python.ast.Arg) : List String

The nodes of the parameters xs.

python.Observing.parameter

def Observing.parameter (a : Option python.ast.Arg) : List String

The node of the parameter a, when there is one.

python.Observing.table

def Observing.table (p : python.ast.Program) : List String

The nodes of the program p in the table of observed types, in order.

python.Observing.ended

def Observing.ended (c : Configuration Run Signal Stop) : Option Run

The state the run c ended in, when it ended (finished, or left by an uncaught exception); none when it stopped or ran out of steps.

python.Observing.verdict

def Observing.verdict (fields : List (String * Json)) : String

The verdict among a verdict’s fields (Lowering.fields).

python.Observing.json

def Observing.json (verdict : String) (table : List String) (seen : List (String * List String)) : String

The table of observed types as JSON: the verdict, then for each node of the table the union of the type texts seen there (nodes, empty when none) and whether it was seen (basis: observed or unreached).

python.Querying.observed

def Querying.observed (source : String) (input : String) (fuel : Nat) : String

The types a run of the program given as its syntax tree’s JSON, source, on the input for at most fuel steps observed, as JSON {verdict, nodes, basis}: each expression’s node (and each name an assignment binds, each parameter) with the union of the types its values had (int|str, in the order first seen; containers with the union of their items’ types, list[?] when empty: Value.typeText), observed; a node the run did not reach has the empty text, unreached. The types hold for this input only. A run that did not end (unknown: out of steps, a construct the model does not take) or a program that is not valid (invalid) gives no nodes.