Module Beloch.Eval

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.

type snapshot

Opaque incremental-evaluation checkpoint; see snapshot / restore and Session.

type stmt_kind =
  1. | SFold
  2. | SMark
  3. | SBind
  4. | SApply of string
type stmt_log_entry = {
  1. sl_kind : stmt_kind;
  2. sl_span : Error.span;
  3. sl_frame_index : int;
    (*

    Index into frames of the frame this statement's geometry reads against: the just-pushed frame for SFold, the most-recently pushed frame for SMark (marks don't fold anything).

    *)
  4. sl_mark : Fold_state.mark option;
    (*

    The mark AS RECORDED by this statement, captured at record-time: independent of whether it later graduates into a real crease. None for SFold.

    *)
  5. sl_kept : Fold_state.mark list;
    (*

    Marks still dangling (not yet graduated into a real crease) as of immediately after this statement.

    *)
  6. sl_parent : int option;
    (*

    The entry of the apply this statement runs under, None at the top level (ADR 0030).

    *)
}
type free_info = {
  1. fi_t : Num.t;
  2. fi_p0 : Geom.point;
    (*

    t = 0 endpoint (anchor)

    *)
  3. fi_p1 : Geom.point;
    (*

    t = 1 endpoint

    *)
  4. fi_source_line : int;
}
val snapshot : Beloch__.Ctx.ctx -> snapshot
val restore : Beloch__.Ctx.ctx -> snapshot -> unit
type folded = {
  1. state : Fold_state.t;
  2. named_points : (string * Geom.point * int * int option) list;
    (*

    The 0-based creation step (index into frames at bind time) and the index of the statement that binds the point in the `beloch:statements` log. Every statement is logged (ADR 0026), so the index is the binding statement's own. None for a name no statement bound, which the four paper corners are.

    *)
  3. named_lines : (string * Geom.line * int * int option) list;
    (*

    Name, current line, and the same two counters a named point carries: the creation frame and the statement that binds it.

    *)
  4. named_line_cids : (string * int) list;
    (*

    Crease id per name for Material/Mark creases: the identity the line coefficients in named_lines lose (a folded crease's current line can coincide with another crease's line).

    *)
  5. frames : (Fold_state.t * Error.span option) list;
  6. statements : stmt_log_entry list;
  7. references : Beloch__.Ctx.reference list;
    (*

    Every resolved mention of a crease name, in source order: the sourcemap from a bundle back to the places the program names it.

    *)
  8. annotations : Beloch__.Ctx.annot_entry list;
    (*

    every annotation in the order it was read, each with the log entry of the statement it belongs to (ADR 0029)

    *)
  9. trace : Beloch__.Trace.entry list;
    (*

    every construction's candidates in the order they were evaluated (docs/reference/FOLD.md, "The trace")

    *)
  10. sheet : Sheet.t;
    (*

    The sheet the program opened; its unfolded state is the first frame of the output.

    *)
  11. unit_name : string;
    (*

    The unit the file declares, "unit" when it declares none.

    *)
  12. free_points : (string * free_info) list;
    (*

    One entry per `free on` point, recorded at bind time: a running log (like statements), not reconstructed from scope state at finalize.

    *)
}
val eval_program : ?resume:snapshot -> ?on_step:(Beloch__.Ctx.ctx -> unit) -> ?prelude:Ast.shape_def list -> Ast.program -> folded

Evaluate prog. resume restores an incremental-evaluation checkpoint taken after a statement and runs the statements of prog from there; without it the header runs first, the unit, the shapes of prelude (default the standard library, Prelude.shapes) and of prog, and the sheet prog opens. on_step runs after every statement (used by Session to collect a fresh snapshot per statement).

val eval_folded : Ast.program -> folded

eval_program with no resume/on_step.

val run_program : ?prelude:Ast.shape_def list -> Beloch__.Ctx.ctx -> (Beloch__.Ctx.ctx -> unit) -> Ast.program -> unit

Run prog on a fresh ctx: its header, as eval_program does without a checkpoint, then its statements, calling the second argument after each. A failing statement raises Error.Beloch_error with its log entry already written.

val build_output : Beloch__.Ctx.ctx -> Beloch__.Ctx.scope -> folded

The result of the statements run so far, with the root scope the names are read from.