Module tower 

Which values of a program the exact extension reaches: the bindings, function results and parameters that can hold an infinitesimal, a hyperreal, an infinite integer, an algebraic number, a computable real, an ordinal, a residue-dependent value or a provisional answer.

The answer is a fixpoint over the whole program. A value is reached when it is made by a builtin of the extension (infinitesimal, standardPart, tripCount, affinePower, … — every logicaffeine_base::extension::Builtin) or by definedReal, declared with one of the exact types, or computed from a reached value — arithmetic and comparison lift through it, an item, a run of items and a copy of a reached list are reached, and not lifts over it. A binding is reached when anything assigned to it is; a function’s result when anything it returns is; a parameter when any call passes it a reached value. and/or decide their operands, so they reach nothing. A list an item of the extension is stored into is reached; a map or a record stores one under a key and keeps its own kind, as every backend that lowers the bytecode reads it (vm::tower::exact_write).

Every tier that keeps static types reads it: the optimizer leaves alone the integer-only rewrites of a reached value, and a compiled backend holds a reached binding in its exact value model. The answer over-approximates — names are keyed by the function they live in, not by block — which costs a compiled program speed, never meaning: a value model that keeps canonical forms holds a standard integer as one.

Structs

TowerTypes

The reached bindings, results and parameters of a program.

Type Aliases

Scope

Where a name lives: a function’s body, or the program’s root (None).