Skip to main content

Module typed

Module typed 

Source
Expand description

Typed oracle gate.

Wraps the structural super::evaluate_rule, super::evaluate_fixpoint, and super::evaluate_scc_fixpoint oracles with a relation-schema-driven type gate. For each rule:

  1. Walk positive body atoms; for each Term::Variable whose predicate is present in base_relations, look up relation.schema[position] and unify into a per-rule BTreeMap<String, ScalarType>. Cross-atom disagreement is a RefEvalError::ConflictingVariableType.
  2. Run super::analyze_typed with that map. Any Boundary::UnsupportedKeyType for a join-key vertex becomes an RefEvalError::Ineligible.
  3. Delegate to the structural evaluator.

§Locked policy: unknowable-after-inference ≠ unsupported

A “missing vertex type” means not derivable from base relation schemas AND not derivable from PR 8 transitive SCC type inference, not “supported.” The typed gate rejects only known-unsupported join-key types.

For the single-rule entry point (evaluate_rule_typed), types come from base_relations only — there is no group context for inference. A self-referencing or recursive rule used through this path therefore retains the original “unknown ≠ unsupported” behavior on its recursive body atoms; callers needing inference-aware typing should drive evaluate_fixpoint_typed or evaluate_scc_fixpoint_typed.

For the group-aware entry points (evaluate_fixpoint_typed, evaluate_scc_fixpoint_typed), PR 8 inference runs at entry and feeds inferred SCC predicate schemas alongside base_relations into per-rule type derivation. Cyclic-only predicates (no base anchor anywhere in the rule graph) produce all-None inferred schemas and pass the gate; this is the narrowed policy now locked by cyclic_only_predicate_still_passes_typed_gate_locked_policy.

§Why a separate module

The structural evaluators (PR 2/3/4) take no type map. Wiring type derivation into each evaluator’s signature would either (a) force callers to pre-compute the map even when they want the structural-only behavior or (b) introduce a parallel “with-types” code path inside each evaluator. Keeping the gate as a thin orchestration layer above the existing oracles preserves the structural API and makes the typed contract testable in one place.

Functions§

evaluate_fixpoint_typed
Evaluate a recursive fixpoint with typed gating applied to every rule against base_relations at function entry.
evaluate_rule_typed
Evaluate a single rule with relation-schema-driven type gating.
evaluate_scc_fixpoint_typed
Evaluate a multi-predicate SCC fixpoint with typed gating applied to every rule against base_relations at function entry.