Beloch (beloch.Beloch)

val version : string

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

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

type failure = {

f_span : Error.span;
f_message : string;
f_hint : string option;
f_statement : int;
(*
the log entry of the statement that failed
*)

}

The FOLD with its trace (docs/reference/FOLD.md, "The trace"), and the program's failure. A program that fails still yields the file up to the failing statement, with the failure in `beloch:error`. A parse error raises as in fold_string.

val eval_traced : Ast.program -> Eval.folded * failure option

val fold_traced : filename:string -> string -> Yojson.Safe.t * failure option

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 docs/decision/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 Sheet : sig ... end

The sheet a program folds (def-sheet): the unfolded state it starts from and the outline of that state, in paper coordinates.

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 (Kawasaki and Maekawa where the anchor surrounds O, the closure of the paper paths everywhere), moves each face by the creases on its paper path (ADR 0044), 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 docs/decision/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-evaluation, the longest matching key prefix is reused and only the divergent suffix is recomputed.