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:
- Walk positive body atoms; for each
Term::Variablewhose predicate is present inbase_relations, look uprelation.schema[position]and unify into a per-ruleBTreeMap<String, ScalarType>. Cross-atom disagreement is aRefEvalError::ConflictingVariableType. - Run
super::analyze_typedwith that map. AnyBoundary::UnsupportedKeyTypefor a join-key vertex becomes anRefEvalError::Ineligible. - 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_relationsat 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_relationsat function entry.