Beloch (beloch.Beloch)

val version : string

val parse : filename:string -> string -> Ast.program

val fold_string : filename:string -> string -> Yojson.Safe.t

module Num : sig ... end

Exact real algebraic numbers. A value is an exact rational Rat q (fast path: axioms 1–4 never leave ℚ), an element of a single extension of degree ≤ field_degree_cap Field {gen; coords} = coords(α) with α the root of the monic irreducible gen.mu isolated in (gen.lo, gen.hi) (fast path for axiom-5/6/7 roots, bpr2006 §12.4), or a general real algebraic number Qq backed by FLINT's qqbar (canonical minimal polynomial + certified ball; cross-field arithmetic, composite extensions). Invariant: Qq is irrational — rationals collapse to Rat. to_float is the only float, output-only. See decisions/0013-flint-qqbar-backend.md.

module Error : sig ... end

Source spans and the single error type used across the evaluator.

module Geom : sig ... end

Exact constructible-real plane geometry. A line a*x + b*y = c with a,b,c in Num (the v0.3 constructible reals; rational on the fast-path).

module Isometry : sig ... end

Exact 2D isometry: an orthogonal 2×2 matrix (det ±1) plus a translation, all in Num. Used to place each face of the paper onto the table.

module Isometry3 : sig ... end

Exact 3D rigid motion: a 3×3 orthogonal matrix (det ±1) plus a translation, all in Num. Places a face of the paper into 3-space. Flat folds use only half_turn_about_line; general rotation-by-θ (θ = rπ) is Stage B.

module Fold_state : sig ... end

The 3D-native folded-state core (issue #48, spec 2026-07-15-fold-state-3d-rewrite). t is abstract: a folded state exists only via make, which enforces the state invariants — so a value of type t IS a legal folded state. Flat-first: hinge angles (dihedral/π) are restricted to

module Ast : sig ... end

Abstract syntax for Beloch. Spans point into the source for diagnostics.

module Lexer : sig ... end

module Parser : sig ... end

module Parse : sig ... end

Source-to-AST parsing, shared by Beloch and Session.

module State : sig ... end

Provenance carried on each crease: which axiom produced it, its source inputs, the source span, the bound crease name (if any), and the index of the statement that scored it.

module Eval : sig ... end

Evaluate a program, resolving names and applying axioms. Geometry is exact; preconditions are reported as Error.Beloch_error. This is the public surface of the core evaluator: consumed by Fold_emit, Session, Beloch, the test suites and packages/www/public/beloch/beloch-eval.js.

module Fold_emit : sig ... end

Serialize a folded state to FOLD (https://github.com/edemaine/fold).

module Collapse : sig ... end

Single-vertex collapse: fold along n >= 4 material crease segments sharing one interior endpoint O — the flat end state of a multi-crease move (rabbit ear hull2020, Thm 8.5). Skips the 3D intermediate entirely: checks the end state exists (reflection closure = Kawasaki, Maekawa), assigns per-sector isometries, enumerates valid layer orders.

module Flatten : sig ... end

The generator half of the flatten solver. Given a set of material creases ("rays") sharing one interior vertex O, an ODD ray count means one emergent ray is part of the solution space; candidates generates the geometric completions that could close the vertex — same-direction filter, per-line dedup, two-tier (`LineNew`/`OppositeRay`) preference tag. It does NOT check feasibility or M/V and does NOT pick a winner.

module Poly : sig ... end

module Mpoly : sig ... end

Sparse multivariate polynomials over ℚ in a fixed number of variables (indices 0 .. nvars-1). Built for Num.real_roots: it manufactures, by Sylvester-resultant elimination of each algebraic coefficient's generator, a ℚ-polynomial in the root variable whose real roots are a SUPERSET of the true roots (spurious conjugate roots are removed later by exact evaluation). Only the root set matters, so sign/constant factors are not tracked. The Sylvester resultant is computed by evaluation + interpolation: each specialized Sylvester determinant is a numeric Gaussian elimination over ℚ (Poly.det), and the multivariate result is recovered by Lagrange interpolation. Algorithms: bpr2006 §4.2.

module Qqbar : sig ... end

Exact real algebraic numbers backed by FLINT 3's qqbar (Calcium): canonical minimal-polynomial representation with Arb ball certification. Values are immutable; the C finalizer frees the FLINT struct. ℚ crosses the FFI as strings. See decisions/0013-flint-qqbar-backend.md.

module Diagnostic : sig ... end

Render a Beloch_error as a rustc-style source-context block, with the hint as a help line under the caret when there is one. Pure: source text + span + message + hint -> string. Uses whatever span the error carries.

module Field_merge : sig ... end

Primitive-element merge for real_roots: express algebraic coefficients over one generator γ of the field they span (compositum of independent folds), and form the ℚt superset polynomial via a single resultant. The tier this sits in, and the gate that reaches it, are in Num.real_roots.

module Spine : sig ... end

Per-statement hash chain for the incremental evaluation cache.

module Session : sig ... end

Incremental evaluation session. Memoizes one Eval.snapshot per statement along Spine's prefix-stable hash chain: on re-eval, the longest matching key prefix is reused and only the divergent suffix is recomputed.