printing

python.Printing.natural

def Printing.natural (n : Nat) : Codes

The decimal digits of the natural n.

python.Printing.integer

def Printing.integer (n : Int) : Codes

The decimal text of the int n.

python.Printing.join

def Printing.join (separator : Codes) (pieces : List Codes) : Codes

The pieces joined with separator between them.

python.Printing.hexDigit

def Printing.hexDigit (d : Nat) : Nat

The digit d (0-15) in lowercase hexadecimal.

python.Printing.hexWithin

def Printing.hexWithin (fuel : Nat) (n : Nat) (after : Codes) : Codes

The natural n in lowercase hexadecimal, within fuel digits (the digits so far, after, after it).

python.Printing.hex

def Printing.hex (n : Nat) : Codes

The natural n in lowercase hexadecimal.

python.Printing.address

def Printing.address (a : Nat) : Codes

The address an object without a repr of its own shows: 0x and its heap position, spaced like CPython’s.

python.Printing.trimmedWithin

def Printing.trimmedWithin (fuel : Nat) (digits : Nat) (last : Int) : Nat * Int

Significant digits without trailing zeros, the exponent of the last digit raised to match (within fuel).

python.Printing.shortestWithin

def Printing.shortestWithin (fuel : Nat) (count : Nat) (v : Float) : Nat * Int

The fewest significant digits (from count up to 17) that read back to the finite float v exactly, trying at most fuel more counts: the digits and the exponent of the last one.

python.Printing.zeros

def Printing.zeros (n : Nat) : Codes

Zeros, n of them.

python.Printing.exponent

def Printing.exponent (x : Int) : Codes

The decimal exponent x with at least two digits and its sign (e+05, e-10).

python.Printing.layout

def Printing.layout (digits : Codes) (first : Int) : Codes

The digits laid out with first, the power of ten of the first digit: fixed point when it is from -4 to 15, otherwise scientific.

python.Printing.float

def Printing.float (v : Float) : Codes

repr of the float v.

python.Printing.escape

def Printing.escape (q : Nat) (c : Nat) : Codes

The code point c in a str’s repr between the quote q: backslash, the quote and control characters escaped.

python.Printing.text

def Printing.text (cs : Codes) : Codes

repr of the str cs: single quotes, or double quotes when it has a single quote and no double quote.

python.Printing.functionName

def Printing.functionName (name : Codes) : Codes

A function’s name as shown (up to the code point 1, which separates a nested function’s own name).

python.Printing.nameOf

def Printing.nameOf (f : Value) : Codes

The name of the function value f (none for anything else).

python.Printing.range

def Printing.range (start : Int) (stop : Int) (step : Int) : Codes

repr of the range from start up to stop by step.

python.Printing.exception

def Printing.exception (type : Codes) (message : Codes) : Codes

repr of a built-in exception value: its type and its message (KeyError’s message is already its argument’s repr).

python.Printing.builtinName

def Printing.builtinName (name : Codes) : Codes

A built-in function’s name as its repr, __name__ and __qualname__ show it: without its module’s (math.sqrt is sqrt; the messages of a call name it with its module).

python.Printing.function

def Printing.function (name : Codes) : Codes

repr of the function value named name.

python.Printing.exceptionBase

def Printing.exceptionBase (h : Heap) (c : Value) : Codes

The built-in exception class the class c derives from (empty when none), looking up a user’s class on the heap h.

python.Printing.ownAttribute

def Printing.ownAttribute (attributes : List (Codes * Value)) (name : String) : Option Value

The attribute name among the attributes an object holds itself (not looked up through its class).

python.Printing.arguments

def Printing.arguments (h : Heap) (v : Value) : List Value

The arguments of the exception instance v on the heap h: its args attribute’s items.

python.Hidden

data Hidden

What repr leaves out, to tell what its text depends on: nothing (the text itself), objects’ addresses (the model’s allocation rule, which CPython’s memory does not follow), or the user’s functions (CPython shows a function’s address, which a function value of the model does not have).

python.Printing.addressOr

def Printing.addressOr (hidden : Hidden) (a : Nat) : Codes

The address the object at a shows, or nothing while hidden hides addresses.

python.Printing.functionOr

def Printing.functionOr (hidden : Hidden) (name : Codes) : Codes

repr of the function value named name, or nothing for a user’s function while hidden hides functions.

python.Printing.wrapper

def Printing.wrapper (hidden : Hidden) (kind : Codes) (a : Nat) : Codes

repr of the staticmethod, classmethod or property object (its type name kind) at a, its address left out while hidden hides addresses.

python.Printing.depth

def Printing.depth (h : Heap) : Nat

How deep repr may follow references: one more than the size of the heap h (each object is shown at most once on a path, so this is never reached by a finite value).

python.Printing.reprHiding

def Printing.reprHiding (hidden : Hidden) (h : Heap) (v : Value) : Codes

repr(v) on the heap h with what hidden hides left out.

python.Printing.repr

def Printing.repr (h : Heap) (v : Value) : Codes

repr(v), looking up objects on the heap h.

python.Printing.isKeyError

def Printing.isKeyError (h : Heap) (cls : Value) : Bool

Whether the exception instance’s class cls (a user’s on the heap h) derives from KeyError.

python.Printing.strHiding

def Printing.strHiding (hidden : Hidden) (h : Heap) (v : Value) : Codes

str(v) on the heap h with what hidden hides left out.

python.Printing.str

def Printing.str (h : Heap) (v : Value) : Codes

str(v), looking up objects on the heap h.

python.Printing.reprShows

def Printing.reprShows (hidden : Hidden) (h : Heap) (v : Value) : Bool

Whether repr(v) on the heap h shows what hidden hides (its text differs without it).

python.Printing.strShows

def Printing.strShows (hidden : Hidden) (h : Heap) (v : Value) : Bool

Whether str(v) on the heap h shows what hidden hides (its text differs without it).

python.FormatSpec

record FormatSpec

A format specification ([[fill]align][sign][#][0][width][,|_][.precision][type]), each mark as its code point (0 when absent): align one of <, >, ^, =; sign one of -, +, space; # the alternate form (a base’s prefix); grouping , or _.

python.FormatSpec.isAlign

def FormatSpec.isAlign (c : Nat) : Bool

Whether the code point c is an alignment mark.

python.FormatSpec.alignment

def FormatSpec.alignment (cs : Codes) : (Nat * Nat) * Codes

The fill and alignment at the start of the specification text cs, and the rest.

python.FormatSpec.mark

def FormatSpec.mark (marks : List Nat) (absent : Nat) (cs : Codes) : Nat * Codes

The first code point of cs if it is one of the marks (else absent), and the rest.

python.FormatSpec.parse

def FormatSpec.parse (cs : Codes) : FormatSpec

The specification read from its text cs.

python.Printing.grouped

def Printing.grouped (separator : Nat) (digits : Codes) : Codes

The digits with separator every three from the right.

python.Printing.fixed

def Printing.fixed (n : Nat) (d : Nat) (p : Nat) : Codes

The value n / d rounded to p decimal places (ties to even), written in fixed point.

python.Printing.scientific

def Printing.scientific (n : Nat) (d : Nat) (p : Nat) : Codes

The value n / d with p digits after the point in scientific notation (d.ddde+XX).

python.Printing.stripFraction

def Printing.stripFraction (cs : Codes) : Codes

The number text cs with the trailing zeros of its fraction removed, and the point when nothing is left after it.

python.Printing.general

def Printing.general (n : Nat) (d : Nat) (requested : Nat) (keepPoint : Bool) : Codes

The general format (g) of n / d with p significant digits (the requested precision, 0 counting as 1): fixed point when the exponent is from -4 to below p (one less when there is no type and the point must stay, keepPoint), otherwise scientific; trailing zeros removed.

python.Printing.capitals

def Printing.capitals (cs : Codes) : Codes

The code points cs in capitals (ASCII).

python.Printing.floatBody

def Printing.floatBody (type : Nat) (precision : Option Nat) (x : Float) : Codes

The body of the float x without its sign for a type and precision (x is not negative): f F e E g G %, or a precision alone (g keeping the point); NaN and infinity as CPython writes them.

python.Printing.signText

def Printing.signText (spec : FormatSpec) (negative : Bool) : Codes

The sign a number shows: - when negative, else as the specification spec asks.

python.Printing.padded

def Printing.padded (spec : FormatSpec) (rightByDefault : Bool) (sign : Codes) (body : Codes) : Codes

The sign and body padded to the width of spec: aligned as it asks (numbers, rightByDefault, default to the right, text to the left; 0 without an alignment pads with zeros after the sign).

python.Printing.withGrouping

def Printing.withGrouping (spec : FormatSpec) (body : Codes) : Codes

A number’s body with its integer digits grouped when the specification spec asks.

python.Printing.radix

def Printing.radix (type : Nat) (n : Nat) : Codes

The natural n in base 2, 8 or 16 by the conversion type (b, o, x; X in capitals).

python.Printing.inBase

def Printing.inBase (base : Nat) (fuel : Nat) (n : Nat) (after : Codes) : Codes

The digits of the natural n in base, within fuel digits (the digits so far, after, after it).

python.Printing.basePrefix

def Printing.basePrefix (spec : FormatSpec) : Codes

The prefix the alternate form (#) of spec gives an int in a base: 0x, 0X, 0o, 0b.

python.Printing.unknownCode

def Printing.unknownCode (h : Heap) (type : Nat) (v : Value) : Outcome

ValueError for a format type the value v cannot be formatted with (its type name looked up on the heap h).

python.Printing.produce

def Printing.produce (cs : Codes) : Outcome

The text cs as a result.

python.Printing.number

def Printing.number (spec : FormatSpec) (sign : Codes) (body : Codes) : Outcome

A number’s body with its sign, grouped and padded as the specification spec asks, as a str.

python.Printing.formatInt

def Printing.formatInt (h : Heap) (spec : FormatSpec) (original : Value) (n : Int) : Outcome

format(n, spec) of an int (shown as original in errors, its type name looked up on the heap h).

python.Printing.formatFloat

def Printing.formatFloat (h : Heap) (spec : FormatSpec) (x : Float) : Outcome

format(x, spec) of a float (the heap h for the errors’ type names).

python.Printing.formatText

def Printing.formatText (h : Heap) (spec : FormatSpec) (cs : Codes) : Outcome

format(s, spec) of the str cs: truncated to the precision, aligned left by default; grouping is an error (the heap h for the errors’ type names).

python.Printing.format

def Printing.format (h : Heap) (v : Value) (specText : Codes) : Outcome

format(v, spec) with spec read from specText, looking up objects on the heap h: a bool with an empty specification is its str, otherwise an int; a value that is not a number or str only with an empty specification.

python.Printing.hasFlag

def Printing.hasFlag (flags : Codes) (c : Nat) : Bool

Whether the % flags have the flag c.

python.Printing.percentNumber

def Printing.percentNumber (flags : Codes) (width : Codes) (conversion : Nat) (n : Int) : Codes

The int n for the conversion %x, %X or %o, padded to the digits width as printf-style flags ask (- left, 0 zeros after the sign, # the base’s prefix).

python.Printing.truncated

def Printing.truncated (x : Float) : Outcome

%d of the float x: its value truncated, or the error converting infinity or NaN.

python.Outcome.then

def Outcome.then (o : Outcome) (next : Value -> Outcome) : Outcome

The result of the outcome o given to the next step, or the exception passed on.

python.Printing.percentCharacter

def Printing.percentCharacter (h : Heap) (spec : Codes) (v : Value) : Outcome

%c of the value v with the format specification spec: a str of length one, or an int as its code point (the heap h for the errors’ type names).

python.Printing.percentOne

def Printing.percentOne (h : Heap) (flags : Codes) (width : Codes) (precision : Option Nat) (conversion : Nat) (v : Value) : Outcome

One % conversion of the value v on the heap h: its flags, width, precision and the conversion code.

python.PercentScan

data PercentScan

What scanning a % format gives: the text so far and the values left, or an exception.

python.PercentScan.after

def PercentScan.after (o : Outcome) (next : Codes -> PercentScan) : PercentScan

The text of one conversion’s outcome o given to next to add and go on scanning, or its exception.

python.PercentSpec

record PercentSpec

The specification after a %: its flags, width, whether a precision is given and its digits, and the rest.

python.PercentSpec.read

def PercentSpec.read (cs : Codes) : PercentSpec

The specification read from cs, the text after a %.

python.Printing.percentWithin

def Printing.percentWithin (fuel : Nat) (h : Heap) (cs : Codes) (values : List Value) (text : Codes) : PercentScan

Scanning the rest cs of a % format within fuel steps, looking up objects on the heap h: the text so far, the values left.

python.Printing.percent

def Printing.percent (h : Heap) (format : Codes) (argument : Value) : Outcome

fmt % arg of the format text and the argument, looking up objects on the heap h: a tuple’s items one for each conversion, any other value as the only one.

python.Printing.digitLimit

def Printing.digitLimit : Nat

The most decimal digits an int converts to or from (CPython 3.11’s default_max_str_digits).

python.Printing.tooLong

def Printing.tooLong (n : Int) : Bool

Whether the int n has more decimal digits than the limit.

python.Printing.tooLongError

def Printing.tooLongError : Raised

ValueError: an int too long to convert to decimal text.

python.Printing.objectTooLong

def Printing.objectTooLong (fuel : Nat) (h : Heap) (o : Object) : Bool

Whether printing the object o on the heap h would convert an int too long (fuel: references still to follow).

python.Printing.holdsTooLong

def Printing.holdsTooLong (fuel : Nat) (h : Heap) (v : Value) : Bool

Whether printing the value v on the heap h would convert an int too long (as repr, fuel bounds the references followed).

python.Printing.anyTooLong

def Printing.anyTooLong (fuel : Nat) (h : Heap) (vs : List Value) : Bool

Whether printing any of the values vs on the heap h would convert an int too long, within fuel references.

python.Printing.checked

def Printing.checked (h : Heap) (v : Value) : Option Raised

ValueError when repr or str of the value v on the heap h would convert an int too long.