Crate implicit_predicates_gen

Expand description

Code generator for exact geometric predicates.

Turns the definition of a predicate or of a point type into specialized Rust code for the implicit-predicates crates.

Status: early development. generate takes the definitions of a .pred file and returns, for each predicate, the Rust module of its stages: a floating-point filter, exact stages on floating-point expansions, and the chain that runs them (see generate for the items of the module), and the module of its checks for tests: an exact evaluator and inputs at the edge of the error bound of the filter. The implicit-predicates-gen command line tool writes those modules for a directory of definitions, formatted with rustfmt, or checks with --check that the files are up to date; its README gives the command that regenerates the code of the implicit-predicates crate.

The steps of the generation are public as well. parse takes a .pred file, written in a small subset of Rust, and returns each Predicate as an expression Graph in which equal subexpressions share a node. Mistakes in the file are reported as an Error that carries the position of the offending token.

A definition is a function over Point3 parameters returning Sign. Its body holds let bindings and a final expression built from +, - (binary and unary), *, parentheses, integer literals, the coordinates p.x, p.y, p.z of a parameter and the names of earlier bindings. A second function with the same name and parameters, marked #[exact], gives the form used for exact evaluation. Comments cost nothing; doc comments (///, //!, /** */, /*! */) are rejected, and so are predicate names that cannot name a module, such as keywords.

A .pred file may also declare point types, which parse_points reads and parse skips: the word point, a name, parameters of type F64x3 or f64, =, an expression and ;, as in point Lnc(p: F64x3, q: F64x3, t: f64) = q + t*(p - q) where 0 <= t, t <= 1;. The expression uses +, -, *, parentheses, integer literals and the parameters; operations on an F64x3 are per coordinate, a product has at least one f64 factor, and the value is an F64x3. The optional where clause is a list of comparisons <= between sums of f64 parameters and integers. A PointType holds the three coordinates as one PointGraph of f64 operations in which equal subexpressions share a node, and the clause as a list of Constraints. The limit on brackets and the guarantee of never panicking are those of parse. generate_points emits the module of the point types of a file, with their constructors, their error bounds and their exact coordinates; error_bound derives the rule of the error bound of each coordinate, and documents why it is an upper bound. generate_points has budgets too: MAX_ROUNDS roundings on a chain of operations, and MAX_POINT_NODES distinct operations and inputs in the coordinates of a point, which bounds the size of the emitted code.

The only limit of parse is the nesting of brackets, at most 32 deep, which keeps the stack small: sums, products and runs of unary minus are read in loops, so parse cannot panic or overflow the stack of the calling thread, even in a debug build with a 1 MiB stack, and it accepts a sum of any length. The later steps have budgets instead: a sum written as one chain of more than about 1,560 terms is rejected by filter_bound, because the exact coefficients of its error bound grow with the length of the chain, an expression too large to expand is rejected by canonical, and generate rejects main forms of more than 256 distinct subexpressions, for which the search of the edge cases of the checks would be slow. Each reports the limit it hit, before doing the work; the work section of generate lists every budget.

Two analyses work on the graphs. check_same_polynomial expands the main and the exact form of a predicate with canonical and requires them to be the same, nonzero polynomial. difference_graph checks that a form is homogeneous in differences of point coordinates, that is, built from differences of one coordinate of two points, combined by sums of terms of equal degree and by products, and returns it as a DiffGraph with the degree of every node.

filter_bound derives, in exact arithmetic, the error bound of evaluating a DiffGraph in f64: with D the largest computed difference plus the two largest errors of the points, and E the sum of those two errors, the computed value differs from the exact one by at most (epsilon * D + kappa * E) * D^(k - 1), where k is the degree. FilterBound::constants gives epsilon and kappa rounded up to f64, and the range of D, between two powers of two, in which overflow and underflow cannot invalidate the bound. filter_form chooses the per-axis form instead when every term has the same degree in each axis (DiffGraph::axis_degrees): an AxisBound keeps one size and one uncertainty per axis, with the same epsilon, one kappa per axis that add up to the global kappa, and the same range for each axis.

exact_plan_raw and exact_plan_differences derive, for each exact stage, the range of input magnitudes for which every exact product of the arithmetic core stays in its domain and no value overflows, and the worst-case length of every temporary; generate sizes the stack buffers of the emitted stages from them. exact_plan_spans_translated and exact_plan_spans_untranslated derive the same for the stages over arena spans, whose leaves are expansions of up to MAX_COORD_COMPONENTS components: the range bounds every nonzero component, so it does not depend on the type of the points.

Structs§

AxisBound: The exact per-axis error bound of the f64 evaluation of a multihomogeneous difference form.
AxisConstants: The constants of the per-axis filter of a predicate, as f64.
Constraint: A comparison lhs <= rhs of the where clause of a point type.
DiffGraph: An expression graph homogeneous in differences of point coordinates.
Error: An error found in a definition file, with the position of the offending token.
ErrorBound: The error bound of the coordinates of a point type, as derived by error_bound.
ExactPlan: What an exact stage needs: the range of its leaves and the size of its temporaries.
ExactRange: The magnitudes of leaves for which an exact stage is valid: every nonzero leaf x must satisfy min <= |x| <= max. Both are powers of two.
FilterBound: The exact error bound of the f64 evaluation of a difference form.
FilterConstants: The constants of the filter of a predicate, as f64.
Generated: The code generated for one predicate.
Graph: A polynomial expression as a graph in which equal subexpressions share a node.
LinearSum: A sum of f64 parameters and an integer constant: the side of a Constraint.
PointGraph: The three coordinates of a point as one graph of f64 operations in which equal subexpressions share a node.
PointParam: A parameter of a point type.
PointType: A point type read from a definition file.
Polynomial: An expanded polynomial over the input coordinates, with integer coefficients. Terms with a zero coefficient are never stored.
Position: A position in a definition file.
Predicate: A predicate read from a definition file.

Enums§

DiffNode: One node of a DiffGraph.
FilterForm: The form of the error bound of the filter of a predicate.
Leaves: The components of each leaf of a difference form.
Node: One node of an expression graph.
ParamType: The type of a parameter of a point type.
PointNode: A node of a PointGraph: an operation on f64 values.

Constants§

MAX_COORD_COMPONENTS: The most components of a coordinate that the exact stages over spans accept, which covers every point type of the library.
MAX_POINT_NODES: The most nodes that the PointGraph of a point type may have for generate_points to emit it: distinct operations and inputs, counted once each over the three coordinates.
MAX_ROUNDS: The largest rounding count error_bound accepts: it keeps the exact derivation of the slack factor small.

Functions§

canonical: Expands graph into its canonical polynomial.
canonical_of_differences: Expands a DiffGraph into its canonical polynomial over the input coordinates: a leaf is the minuend coordinate minus the subtrahend coordinate and a negation is 0 - x.
check_same_polynomial: Checks that the main form of predicate is a nonzero polynomial and, if the predicate has an exact form, that both forms are the same polynomial.
difference_graph: Rewrites graph over differences of coordinates, checking that every sum and difference combines nodes of the same degree.
error_bound: Derives the error bound of the approximate coordinates of point.
exact_plan_differences: Derives the exact stage of a difference form whose leaves have the given number of components, for the product domain [operand_min, operand_max].
exact_plan_raw: Derives the exact stage of the raw form, whose leaves are the input coordinates, for the product domain [operand_min, operand_max].
exact_plan_spans_translated: Derives the exact stage over spans of a difference form, each of whose leaves is the difference of two coordinates of up to components components, for the product domain [operand_min, operand_max].
exact_plan_spans_untranslated: Derives the exact stage over spans of a raw form, whose leaves are coordinates of up to components components, for the product domain [operand_min, operand_max].
filter_bound: Derives the error bound of the f64 evaluation of graph.
filter_form: Derives the error bound of the f64 evaluation of graph: the per-axis form when every term has the same degree in each axis, and the global form of filter_bound otherwise.
generate: Generates the code of every predicate defined in source.
generate_points: Generates the module of the point types declared in source, or None if it declares none. file and regenerate are as for generate.
parse: Reads every predicate defined in source.
parse_points: Reads every point type declared in source.

Type Aliases§

NodeId: Index of a node in Graph::nodes.