uor-foundation 0.3.0

// @generated by uor-crate from uor-ontology — do not edit manually

//! `predicate/` namespace — Boolean-valued functions on kernel objects. Formalizes resolver dispatch, reduction guard evaluation, and conditional resolution paths..
//!
//! Space: Kernel

use crate::HostTypes;

/// A total, pure, boolean-valued function on a kernel object. Evaluation terminates for all inputs and produces no side effects.
pub trait Predicate<H: HostTypes> {
    /// The OWL class of objects this predicate accepts as input.
    fn evaluates_over(&self) -> &H::HostString;
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<H>;
    /// The evaluator term that must reduce to a boolean-shaped datum on every input of the declared input type.
    fn evaluator_term(&self) -> &Self::Term;
    /// An IRI or identifier of the proof:Proof / proof:ComputationCertificate attesting that the evaluator halts on all inputs.
    fn termination_witness(&self) -> &H::HostString;
    /// Associated type for `DescentMeasure`.
    type DescentMeasure: crate::kernel::recursion::DescentMeasure<H>;
    /// A termination witness for user-declared predicates. Kernel predicates are total by construction; user-declared predicates must carry a descent measure certifying termination.
    fn bounded_evaluator(&self) -> &[Self::DescentMeasure];
}

/// A predicate over type:TypeDefinition. Used for resolver dispatch.
pub trait TypePredicate<H: HostTypes>: Predicate<H> {}

/// A predicate over state:Context or reduction:ReductionState. Used for reduction step guards.
pub trait StatePredicate<H: HostTypes>: Predicate<H> {}

/// A predicate over partition:SiteIndex. Used for site-level selection in geodesic resolution.
pub trait SitePredicate<H: HostTypes>: Predicate<H> {}

/// A pair (Predicate, Target) where Target is a resolver:Resolver class. The kernel evaluates the predicate; if true, the target resolver is selected.
pub trait DispatchRule<H: HostTypes> {
    /// Associated type for `Predicate`.
    type Predicate: Predicate<H>;
    /// The predicate that triggers this dispatch rule.
    fn dispatch_predicate(&self) -> &Self::Predicate;
    /// The resolver class selected when the predicate is satisfied. Range is the OWL class IRI of a resolver:Resolver subclass; v0.2.1 uses class IRIs so the codegen can construct façade structs.
    fn dispatch_target(&self) -> &H::HostString;
    /// Non-negative integer priority. Lower priority values are evaluated first; ties within a DispatchTable are resolved by declaration order.
    fn dispatch_priority(&self) -> u64;
    /// Position in the dispatch table (evaluation order).
    fn dispatch_index(&self) -> u64;
}

/// An ordered set of DispatchRules for a single dispatch point. Must satisfy exhaustiveness and mutual exclusion.
pub trait DispatchTable<H: HostTypes> {
    /// Associated type for `DispatchRule`.
    type DispatchRule: DispatchRule<H>;
    /// The ordered set of rules in this table.
    fn dispatch_rules(&self) -> &[Self::DispatchRule];
    /// True iff the disjunction of all dispatch predicates is a tautology over the input class.
    fn is_exhaustive(&self) -> bool;
    /// True iff no two dispatch predicates can be simultaneously true for any input.
    fn is_mutually_exclusive(&self) -> bool;
}

/// A triple (StatePredicate, effect:Effect, reduction:ReductionStep). The guard is a StatePredicate; if true, the effect is applied and the reduction advances to the target step.
pub trait GuardedTransition<H: HostTypes> {
    /// Associated type for `StatePredicate`.
    type StatePredicate: StatePredicate<H>;
    /// The guard predicate for this transition.
    fn guard_predicate(&self) -> &Self::StatePredicate;
    /// Associated type for `Effect`.
    type Effect: crate::kernel::effect::Effect<H>;
    /// The effect applied when the guard is satisfied.
    fn guard_effect(&self) -> &Self::Effect;
    /// Associated type for `ReductionStep`.
    type ReductionStep: crate::kernel::reduction::ReductionStep<H>;
    /// The reduction step to advance to.
    fn guard_target(&self) -> &Self::ReductionStep;
}

/// A single case in a pattern match: a Predicate and a result Term. The match evaluates predicates in order and returns the result of the first matching arm.
pub trait MatchArm<H: HostTypes> {
    /// Associated type for `Predicate`.
    type Predicate: Predicate<H>;
    /// The predicate guarding this arm.
    fn arm_predicate(&self) -> &Self::Predicate;
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<H>;
    /// The result term if this arm matches.
    fn arm_result(&self) -> &Self::Term;
    /// Position in the match expression (evaluation order).
    fn arm_index(&self) -> u64;
}

/// A term formed by evaluating a sequence of MatchArms. Extends the term language with deterministic conditional evaluation.
pub trait MatchExpression<H: HostTypes>: crate::kernel::schema::Term<H> {
    /// Associated type for `MatchArm`.
    type MatchArm: MatchArm<H>;
    /// The ordered arms of this match expression.
    fn match_arms(&self) -> &[Self::MatchArm];
}

/// True on every Datum. Match-arm default catch-all.
pub mod always {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// False on every Datum. Disabled-arm marker.
pub mod never {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff the Datum is the additive identity of its ring.
pub mod is_zero {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff the Datum is the multiplicative identity.
pub mod is_unit {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff the Datum parity bit is 1.
pub mod is_odd {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff the Datum parity bit is 0.
pub mod is_even {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff op(op(x)) = x for the bound op.
pub mod is_involution {
    /// `evaluatesOver` -> `Datum`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/schema/Datum";
}

/// True iff the named site coordinate is currently pinned.
pub mod site_pinned {
    /// `evaluatesOver` -> `SiteIndex`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/partition/SiteIndex";
}

/// True iff the named site coordinate is currently free.
pub mod site_free {
    /// `evaluatesOver` -> `SiteIndex`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/partition/SiteIndex";
}

/// True iff the resolver has entered a ContradictionBoundary.
pub mod contradiction_reached {
    /// `evaluatesOver` -> `ContradictionBoundary`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/state/ContradictionBoundary";
}

/// True iff the FreeRank deficit is zero.
pub mod budget_exhausted {
    /// `evaluatesOver` -> `FreeRank`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/partition/FreeRank";
}

/// True iff the reduction fixpoint has been reached.
pub mod reduction_converged {
    /// `evaluatesOver` -> `ReductionState`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/reduction/ReductionState";
}

/// True on ConstrainedType instances whose constraint nerve contains only disjunctions of width ≤ 2.
pub mod is2_sat_shape {
    /// `evaluatesOver` -> `ConstrainedType`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/type/ConstrainedType";
}

/// True on ConstrainedType instances whose disjunctions each contain at most one positive literal.
pub mod is_horn_shape {
    /// `evaluatesOver` -> `ConstrainedType`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/type/ConstrainedType";
}

/// Default (catch-all) predicate. True on ConstrainedType instances not classified by Is2SatShape or IsHornShape.
pub mod is_residual_fragment {
    /// `evaluatesOver` -> `ConstrainedType`
    pub const EVALUATES_OVER: &str = "https://uor.foundation/type/ConstrainedType";
}

/// The predicate:DispatchTable governing resolver:InhabitanceResolver. Three rules form a partition of type:ConstrainedType: Is2SatShape → TwoSatDecider (priority 0), IsHornShape → HornSatDecider (priority 1), IsResidualFragment → ResidualVerdictResolver (priority 2, catch-all). Total coverage is enforced by reduction:DispatchCoverageCheck; DispatchMiss is unreachable for this table.
pub mod inhabitance_dispatch_table {
    /// `isExhaustive`
    pub const IS_EXHAUSTIVE: bool = true;
    /// `isMutuallyExclusive`
    pub const IS_MUTUALLY_EXCLUSIVE: bool = true;
}

/// Dispatch rule 1 of InhabitanceDispatchTable: Is2SatShape → TwoSatDecider at priority 0.
pub mod inhabitance_rule_2sat {
    /// `dispatchPredicate` -> `Is2SatShape`
    pub const DISPATCH_PREDICATE: &str = "https://uor.foundation/predicate/Is2SatShape";
    /// `dispatchPriority`
    pub const DISPATCH_PRIORITY: i64 = 0;
    /// `dispatchTarget` -> `TwoSatDecider`
    pub const DISPATCH_TARGET: &str = "https://uor.foundation/resolver/TwoSatDecider";
}

/// Dispatch rule 2 of InhabitanceDispatchTable: IsHornShape → HornSatDecider at priority 1.
pub mod inhabitance_rule_horn {
    /// `dispatchPredicate` -> `IsHornShape`
    pub const DISPATCH_PREDICATE: &str = "https://uor.foundation/predicate/IsHornShape";
    /// `dispatchPriority`
    pub const DISPATCH_PRIORITY: i64 = 1;
    /// `dispatchTarget` -> `HornSatDecider`
    pub const DISPATCH_TARGET: &str = "https://uor.foundation/resolver/HornSatDecider";
}

/// Dispatch rule 3 (catch-all) of InhabitanceDispatchTable: IsResidualFragment → ResidualVerdictResolver at priority 2. Ensures total coverage.
pub mod inhabitance_rule_residual {
    /// `dispatchPredicate` -> `IsResidualFragment`
    pub const DISPATCH_PREDICATE: &str = "https://uor.foundation/predicate/IsResidualFragment";
    /// `dispatchPriority`
    pub const DISPATCH_PRIORITY: i64 = 2;
    /// `dispatchTarget` -> `ResidualVerdictResolver`
    pub const DISPATCH_TARGET: &str = "https://uor.foundation/resolver/ResidualVerdictResolver";
}