Struct Env 

pub struct Env {

    pub terms: HashSet<String>,
    pub assign: HashMap<String, f64>,
    pub symbol_prob: HashMap<String, f64>,
    pub lo: f64,
    pub hi: f64,
    pub valence: u32,
    pub ops: HashMap<String, Op>,
    pub types: HashMap<String, String>,
    pub lambdas: HashMap<String, Lambda>,
    pub templates: HashMap<String, TemplateDecl>,
    pub trace_enabled: bool,
    pub trace_events: Vec<TraceEvent>,
    pub current_span: Option<Span>,
    pub default_span: Span,
    pub namespace: Option<String>,
    pub aliases: HashMap<String, String>,
    pub imported: HashSet<String>,
    pub shadow_diagnostics: Vec<Diagnostic>,
    pub file_namespaces: HashMap<PathBuf, String>,
    pub modes: HashMap<String, Vec<ModeFlag>>,
    pub relations: HashMap<String, Vec<Node>>,
    pub worlds: HashMap<String, Vec<String>>,
    pub inductives: HashMap<String, InductiveDecl>,
    pub definitions: HashMap<String, DefineDecl>,
    pub coinductives: HashMap<String, CoinductiveDecl>,
    pub domain_plugins: HashMap<String, DomainPluginFn>,
    pub automatic_sequence_decisions: HashMap<String, AutomaticSequenceDecision>,
    pub root_constructs: HashMap<String, RootConstructDescriptor>,
    pub foundations: HashMap<String, FoundationDescriptor>,
    pub active_foundation: String,
    pub foundation_stack: Vec<FoundationFrame>,
    pub active_implementations: HashMap<String, ActiveImplementationDescriptor>,
    pub strict_carrier: bool,
    pub carrier: Option<Vec<f64>>,
    pub carrier_label: Option<String>,
    pub proof_rules: HashMap<String, ProofRule>,
    pub proof_assumptions: HashMap<String, ProofAssumption>,
    pub proof_objects: HashMap<String, ProofObject>,
    pub strict_pure_links: bool,
    pub allowed_host_primitives: HashSet<String>,
}

The evaluation environment: holds terms, assignments, operators, and range/valence config.

Fields

terms: HashSet<String>

assign: HashMap<String, f64>

symbol_prob: HashMap<String, f64>

lo: f64

hi: f64

valence: u32

ops: HashMap<String, Op>

types: HashMap<String, String>

lambdas: HashMap<String, Lambda>

templates: HashMap<String, TemplateDecl>

trace_enabled: bool

Tracing state. When trace_enabled is true, key evaluation events (operator resolutions, assignment lookups, top-level reductions) are appended to trace_events. The current top-level form span is stashed on the Env so leaf hooks can attach a location without threading spans through every helper. Mirrors the _tracer/_currentSpan design in js/src/rml-links.mjs.

trace_events: Vec<TraceEvent>

current_span: Option<Span>

default_span: Span

namespace: Option<String>

Namespace state (issue #34): a file can declare (namespace foo), which prefixes every name it subsequently introduces with foo.. Imports can be aliased via (import "x.lino" as a), which records a -> the imported file’s declared namespace so a.name resolves to that name. imported tracks names that came from an import (not declared in the importing file) so we can emit a shadowing warning (E008) when a later top-level definition rebinds them.

aliases: HashMap<String, String>

imported: HashSet<String>

shadow_diagnostics: Vec<Diagnostic>

file_namespaces: HashMap<PathBuf, String>

modes: HashMap<String, Vec<ModeFlag>>

Mode declarations (issue #43, D15): each relation may declare an argument mode pattern via (mode <name> +input -output ...). The map records the per-argument flag list used by the call-site checker to reject mode mismatches.

relations: HashMap<String, Vec<Node>>

Relation declarations (issue #44, D12): the clause list for each declared relation, keyed by relation name. Each clause is the original AST list (name arg1 arg2 ... result). The totality checker reads these clauses to verify structural decrease on recursive calls.

worlds: HashMap<String, Vec<String>>

World declarations (issue #54, D16): each relation may declare a list of constants permitted to appear free in its arguments via (world <name> (<const1> <const2> ...)). The world checker rejects relation calls and clauses whose arguments contain any other free constant. Relations without a recorded world are unconstrained (the feature is opt-in per relation).

inductives: HashMap<String, InductiveDecl>

Inductive declarations (issue #45, D10): a first-class inductive datatype encoded as link signatures plus a generated eliminator. Stored by type name; see InductiveDecl for the full layout.

definitions: HashMap<String, DefineDecl>

Recursive definition declarations (issue #49, D13): each (define <name> [(measure ...)] (case ...) ...) form is recorded here so the termination checker (is_terminating) can verify structural decrease across recursive calls. Stored by definition name; see DefineDecl for the full layout.

coinductives: HashMap<String, CoinductiveDecl>

Coinductive declarations (issue #53, D11): a first-class coinductive datatype dual to the inductive form, encoded as link signatures plus a generated corecursor Name-corec. Each entry stores the type name, the ordered constructors, and the name and Pi-type of the corecursor. The kernel additionally enforces a syntactic productivity check at declaration time: at least one constructor must take a recursive argument so non-productive types (which cannot generate any infinite values) are rejected up front.

domain_plugins: HashMap<String, DomainPluginFn>

Domain plugins (issue #63): domain-specific decision procedures keyed by (domain <name> ...). The default registry ships the automatic-sequences plugin below; callers may register additional function-pointer plugins on their Env instance.

automatic_sequence_decisions: HashMap<String, AutomaticSequenceDecision>

Decisions recorded by the built-in automatic-sequences plugin.

root_constructs: HashMap<String, RootConstructDescriptor>

Root-construct registry (issue #97). Records what every kernel construct depends on and whether the user has overridden it. Data-only: descriptors never alter evaluator behaviour. Consumed by the foundation report ((foundation-report)) and the CLI trust audit.

foundations: HashMap<String, FoundationDescriptor>

Foundation registry (issue #97). A foundation bundles a coherent set of root-construct interpretations. default-rml is preregistered with the host-implemented semantics; user files can register alternative foundations and select them with (with-foundation …). Backward compatibility is preserved by defaulting to default-rml.

active_foundation: String

foundation_stack: Vec<FoundationFrame>

active_implementations: HashMap<String, ActiveImplementationDescriptor>

strict_carrier: bool

Carrier enforcement state (issue #97, Section 2). Off by default so legacy programs are not constrained; flipped on by an enclosing (with-foundation <name>) whose descriptor includes both (carrier ...) and (strict-carrier) clauses.

carrier: Option<Vec<f64>>

carrier_label: Option<String>

proof_rules: HashMap<String, ProofRule>

Proof-object substrate (issue #97, Phase 3 of netkeep80’s punch-list). proof_rules maps a declared rule name to its premise patterns and conclusion pattern (with ?meta leaves as metavariables). The map proof_objects records concrete derivations consumed by (check-proof <name>). Both are data-only: declaring a rule never alters evaluator behaviour. The CLI’s foundation report surfaces them.

proof_assumptions: HashMap<String, ProofAssumption>

proof_objects: HashMap<String, ProofObject>

strict_pure_links: bool

Pure-links strict mode (issue #97, Phase 6 of netkeep80’s punch-list). When strict_pure_links is true, every queried form is audited against the root-construct registry; any operator whose status is host-primitive or host-derived triggers an E065 diagnostic unless the construct is in allowed_host_primitives. Off by default so legacy programs run unchanged.

allowed_host_primitives: HashSet<String>

Implementations

impl Env

pub fn new(options: Option<EnvOptions>) -> Self

pub fn mid(&self) -> f64

Midpoint of the range.

pub fn init_truth_constants(&mut self)

Initialize truth constants based on current range. (false: min(range)), (true: max(range)), (unknown: mid(range)), (undefined: mid(range))

pub fn clamp(&self, x: f64) -> f64

Clamp and optionally quantize a value to the valid range.

pub fn to_num(&self, s: &str) -> f64

Parse a numeric string respecting current range.

pub fn define_op(&mut self, name: &str, op: Op)

pub fn register_domain_plugin(&mut self, name: &str, plugin: DomainPluginFn)

pub fn get_domain_plugin(&self, name: &str) -> Option<DomainPluginFn>

pub fn register_default_foundation(&mut self)

Preregister the default-rml foundation and seed the built-in root-construct descriptors that describe the current host implementation. These are data-only and never change behaviour.

pub fn register_root_construct( &mut self, descriptor: RootConstructDescriptor, ) -> Result<RootConstructDescriptor, String>

pub fn get_root_construct(&self, name: &str) -> Option<&RootConstructDescriptor>

pub fn list_root_constructs(&self) -> Vec<RootConstructDescriptor>

pub fn register_foundation( &mut self, foundation: FoundationDescriptor, ) -> Result<FoundationDescriptor, String>

pub fn get_foundation(&self, name: &str) -> Option<&FoundationDescriptor>

pub fn enter_foundation(&mut self, name: &str) -> Result<(), String>

pub fn exit_foundation(&mut self)

pub fn check_carrier_value(&self, value: f64) -> Option<String>

Check value against the active foundation’s carrier. Returns None when the carrier is inactive or the value is legal, or a human-readable message otherwise (consumed by the caller to build an E063 diagnostic). Mirrors the JS Env.checkCarrierValue helper.

pub fn foundation_report(&self) -> FoundationReport

pub fn proof_report(&self, name: &str) -> ProofReport

Build a per-proof report (issue #97, Phase 13). Walks the proof object tree starting at name, collects the transitive dependencies (proof-objects, axioms, assumptions) and the registered root constructs that appear as leaf operators in the proof’s premises/conclusion and in the rule patterns it transitively applies. Returns the report in all cases — when the proof object is missing, verdict.ok is false.

pub fn dependency_closure(&self, name: &str) -> Option<Vec<String>>

Return the transitive closure of a construct’s dependencies, breadth-first and deterministically sorted at every level. Missing intermediate deps are silently retained (so a downstream caller can detect dangling names by intersecting against root_constructs.keys()). Returns None if the root itself is unknown.

pub fn register_proof_rule(&mut self, rule: ProofRule)

Register a declared rule of inference. Data-only.

pub fn register_proof_assumption(&mut self, assumption: ProofAssumption)

Register an explicit proof assumption/axiom. Data-only; proof objects cite these leaves via (premise-by <name>) or (uses <name>...).

pub fn register_proof_object(&mut self, po: ProofObject)

Register a concrete derivation. Data-only; verification runs lazily when (check-proof <name>) evaluates.

pub fn get_proof_rule(&self, name: &str) -> Option<&ProofRule>

pub fn get_proof_assumption(&self, name: &str) -> Option<&ProofAssumption>

pub fn get_proof_object(&self, name: &str) -> Option<&ProofObject>

pub fn get_op(&self, name: &str) -> Option<&Op>

pub fn has_op(&self, name: &str) -> bool

pub fn qualify_name(&self, name: &str) -> String

Apply the active namespace to a freshly declared name, e.g. inside (namespace classical) the form (and: min) registers classical.and, not and. Names that already contain a . are passed through. Mirrors Env.qualifyName in js/src/rml-links.mjs.

pub fn resolve_qualified(&self, name: &str) -> String

Resolve a possibly-qualified name to its canonical storage key. Order:

1. Alias prefix: cl.foo with alias cl -> classical becomes classical.foo.
2. Active namespace: an unqualified name lives in <ns>.<name>.
3. Bare name: returned unchanged. Used by lookup helpers (operators, symbol probabilities) to find namespaced bindings without forcing every call site to spell them out. Mirrors Env._resolveQualified in js/src/rml-links.mjs.

pub fn set_expr_prob(&mut self, expr_node: &Node, p: f64)

pub fn set_symbol_prob(&mut self, sym: &str, p: f64)

pub fn get_symbol_prob(&self, sym: &str) -> f64

pub fn trace(&mut self, kind: &str, detail: impl Into<String>)

Push a trace event when tracing is enabled. The event’s span is taken from current_span if set, else default_span. Mirrors Env.trace in the JavaScript implementation.

pub fn set_type(&mut self, expr: &str, type_expr: &str)

pub fn get_type(&self, expr: &str) -> Option<&String>

pub fn set_lambda(&mut self, name: &str, lambda: Lambda)

pub fn get_lambda(&self, name: &str) -> Option<&Lambda>

pub fn apply_op(&self, name: &str, vals: &[f64]) -> f64

Apply an operator by name to the given values.

pub fn apply_eq(&mut self, left: &Node, right: &Node) -> f64

Apply equality operator, checking assigned probabilities first. Takes &mut self so it can emit lookup trace events.

pub fn apply_neq(&mut self, left: &Node, right: &Node) -> f64

Apply inequality operator: not(eq(L, R))

pub fn reinit_ops(&mut self)

Reinitialize ops when range changes (resets to defaults for current range).