Active implementation selected by the current foundation scope for a
construct such as and or not. This is the behaviour-facing counterpart
to the global root-construct descriptor: strict pure-links mode consults
it before falling back to the global registry.
A parsed (coinductive Name (constructor …) …) declaration. Mirrors
InductiveDecl but additionally guarantees the productivity check
(at least one recursive constructor) has succeeded.
Result of evaluate(src): a list of query results (numeric or type) plus
any diagnostics emitted while parsing/evaluating. When tracing is enabled
via evaluate_with_options, trace carries the deterministic sequence of
TraceEvent values recorded during evaluation; otherwise it is empty.
When proof production is enabled (via EvaluateOptions::with_proofs or
any per-query (? expr with proof) keyword), proofs[i] carries a
derivation tree for results[i]; bare queries that did not request a
witness get None so the vec stays index-aligned with results.
Mirrors the JavaScript {results, diagnostics, trace, proofs} shape.
A foundation descriptor. Bundles a coherent set of root-construct
interpretations. Selecting a foundation never silently rewires
behaviour; the host operators always run, but the active-foundation
tag is exposed via the foundation report so users can audit which
foundation they are trusting.
Stack frame pushed when entering a foundation scope. Stores the previous
active foundation name plus a snapshot of any operators the foundation
rebinds, so exit_foundation can restore the prior semantics exactly.
snapshot maps operator name -> previous Op (None if the op did not
exist before). Carrier snapshot fields (issue #97 Section 2) preserve the
strict-carrier state of the enclosing scope so nested (with-foundation ...) bodies roll back cleanly when their inner scope exits.
A concrete derivation that claims to be an instance of a rule. Stored
alongside the rule so (check-proof <name>) can re-validate it on
demand without re-parsing the source.
Per-proof dependency/trust report (issue #97, Phase 13). Built by
Env::proof_report and surfaced as RunResult::Proof so the
trust audit can be performed for an individual proof object instead
of only globally via foundation-report.
A declared rule of inference. Premises and the conclusion are stored as
AST nodes; leaves whose token starts with ? are metavariables that
bind during check_proof_object. Repeated metavariables must
structurally match.
Printed view of a ProofRule for foundation_report(). Patterns are
stringified via key_of so consumers can pretty-print without owning
the AST representation.
A root-construct descriptor. Stored on the Env for the foundation
registry (issue #97). Every field is purely informational: declaring a
descriptor never changes evaluator behaviour. The CLI’s foundation
report and tests inspect these records to verify the trust contract.
A pre-evaluation template declaration (issue #59).
(template (<name> <param>...) <body>) records a reusable link shape;
later (<name> arg...) uses are expanded before they reach eval_node.
Result of validating a proof-object against its declared rule. On success
the substitution map records each metavariable’s witness; on failure the
error string is suitable for surfacing as an E064 diagnostic.
Compose the dependent corecursor type for Name-corec, given the parsed
constructor list. The state parameter binds the symbol _state_type
throughout, and each constructor case parameter binds case_<ctorName>.
Build a [(name, [dep, ...]), ...] listing covering every registered
root-construct in deterministic, sorted order at every level.
Constructs with no dependencies map to an empty vector so the trust
audit can still see them. Complement of Env::dependency_closure(name)
which gives a per-construct slice.
Compose the dependent eliminator type for Name-rec, given the parsed
constructor list. The motive parameter binds the symbol _motive
throughout, and each constructor case parameter binds case_<ctorName>.
Equality-layer classification used by both build_proof and the
per-query provenance walker. Precedence (issue #97): assigned >
structural > definitional > numeric. Returns the rule string verbatim
so JS and Rust emit identical labels.
Decode an anum-encoded string into a Node. Strictly enforces the
[tag payload] shape; any character outside the four-abit alphabet
raises an error. Returns the decoded Node; errors if trailing content
remains after the top-level frame.
Higher-order abstract syntax (issue #51, D7): rewrite the surface keyword
forall to the kernel binder Pi. Both forms share identical structure
(<binder> (Type x) body), so the desugarer walks the AST and rewrites
the head leaf in place. Object-language binders are encoded as
host-language lambda and Pi/forall, letting substitution and
capture-avoidance reuse the kernel primitives without a separate
object-level binder representation.
Return the equality-layer rule for a query whose body is a direct
equality, or None for any other query shape. Composite queries like
((a = true) and (b = true)) are intentionally returned as None: the
per-equality rules still appear in the proof witness, but the surface
provenance describes the query itself.
Read a file from disk and evaluate it, honouring (import "...") directives.
Mirrors evaluate() but takes a path on disk; relative imports inside the
file are resolved against the file’s directory. A missing file is reported
as an E007 diagnostic instead of an OS error.
Like evaluate, but takes structured EvaluateOptions. When
options.trace is true the returned EvaluateResult.trace carries a
deterministic sequence of TraceEvent values (operator resolutions,
assignment lookups, top-level reductions) — one entry per event,
in source order.
Drop the explicit apply keyword on neutral applications, recursively.
(apply f a) whose head is a free constructor-like symbol becomes
(f a) so the printed normal form matches the LiNo surface example
from issue #50: (succ (succ zero)) rather than the explicit
(apply succ (apply succ zero)).
Format a numeric value for trace output — strips trailing zeros so
1.000000 reads as 1 and 0.5 stays 0.5. Mirrors formatTraceValue
in the JavaScript implementation so cross-runtime traces match exactly.
Public coverage checker. Mirrors isCovered in the JavaScript
implementation and returns identical diagnostic shapes so external
tooling sees consistent output across runtimes.
Public termination checker. Returns a TerminationResult with
structured diagnostics; callers can either propagate them as-is or
convert each entry into a Diagnostic for the existing pipeline. The
mirrored JS helper is exported under the same name (isTerminating).
Public totality checker. Returns a TotalityResult with structured
diagnostics; callers can either propagate them as-is or convert each
entry into a Diagnostic for the existing pipeline. The mirrored JS
helper is exported under the same name (isTotal) and produces an
equivalent shape so downstream tools see consistent output.
Public full normal form API (issue #50, D4).
Reduces every redex in term, including those nested under binders and
in argument positions, until the term is in beta-(eta-)normal form. The
result is post-processed by flatten_neutral_applies so it prints in
the surface shape (succ (succ zero)) from the issue.
Parse a (coinductive Name (constructor …) …) form into a
CoinductiveDecl. Panics with Coinductive declaration error: on
a malformed or non-productive declaration so the existing diagnostic
dispatch maps it to E036.
Parse an (inductive Name (constructor …) …) form into an
InductiveDecl. Panics with Inductive declaration error: on a
malformed declaration so the existing diagnostic dispatch maps it to
E033.
Quantize a value to N discrete levels in range [lo, hi].
For N=2 (Boolean): levels are {lo, hi}
For N=3 (ternary): levels are {lo, mid, hi}
For N<2 (continuous/unary): no quantization
See: https://en.wikipedia.org/wiki/Many-valued_logic
Install a coinductive declaration on the environment: register the type,
every constructor, and the generated corecursor together with its
dependent Pi-type. Mirrors registerCoinductive in the JavaScript kernel.
Install an inductive declaration on the environment: register the type,
every constructor, and the generated eliminator together with its
dependent Pi-type. Mirrors registerInductive in the JavaScript kernel.
Walk a queried node and return sorted, deduplicated dependency paths that
end at a host-primitive or host-derived construct and are not covered
by (allow-host-primitive ...).
Weak-head normal form (D4): reduce the spine of node — i.e. unfold the
head as long as there are arguments to apply to it — without descending
into binders or argument positions. Mirrors whnfTerm in the JS runtime
and nf/is_convertible already use normalize_term for the full
version. Substitution may expose a redex inside the residual body, but
that is no longer on the original spine, so this routine returns it
unevaluated; full normalization is the place that descends into those
positions.