uor-foundation 0.2.0

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

//! `derivation/` namespace — Computation witnesses recording term rewriting sequences from original terms to their canonical forms..
//!
//! Space: Bridge

use crate::enums::RewriteRule;
use crate::Primitives;

/// A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form.
pub trait Derivation<P: Primitives> {
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<P>;
    /// The term at the start of the derivation, before any rewriting.
    fn original_term(&self) -> &Self::Term;
    /// The canonical form produced at the end of the derivation.
    fn canonical_term(&self) -> &Self::Term;
    /// Associated type for `Datum`.
    type Datum: crate::kernel::schema::Datum<P>;
    /// The datum value obtained by evaluating the canonical term.
    fn result(&self) -> &Self::Datum;
    /// Associated type for `RewriteStep`.
    type RewriteStep: RewriteStep<P>;
    /// A rewrite step in this derivation.
    fn step(&self) -> &[Self::RewriteStep];
    /// Associated type for `TermMetrics`.
    type TermMetrics: TermMetrics<P>;
    /// Metrics for the canonical term produced by this derivation.
    fn term_metrics(&self) -> &Self::TermMetrics;
}

/// An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement).
pub trait DerivationStep<P: Primitives> {}

/// A single rewrite step in a derivation: the application of one rewrite rule to transform a term.
pub trait RewriteStep<P: Primitives>: DerivationStep<P> {
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<P>;
    /// The term before this rewrite step.
    fn from(&self) -> &Self::Term;
    /// The term after this rewrite step.
    fn to(&self) -> &Self::Term;
    /// The typed rewrite rule applied in this step. Provides a structured reference to a named RewriteRule individual, complementing the string-valued derivation:rule property.
    fn has_rewrite_rule(&self) -> RewriteRule;
}

/// A type-level refinement step: the application of a constraint to narrow a type, pinning additional site coordinates. Complements RewriteStep (term-level) in the derivation hierarchy.
pub trait RefinementStep<P: Primitives>: DerivationStep<P> {
    /// Associated type for `TypeDefinition`.
    type TypeDefinition: crate::user::type_::TypeDefinition<P>;
    /// The type before this refinement step was applied.
    fn previous_type(&self) -> &Self::TypeDefinition;
    /// Associated type for `Constraint`.
    type Constraint: crate::user::type_::Constraint<P>;
    /// The constraint that was applied in this refinement step.
    fn applied_constraint(&self) -> &Self::Constraint;
    /// The type after this refinement step was applied.
    fn refined_type(&self) -> &Self::TypeDefinition;
    /// The number of site coordinates pinned by this refinement step.
    fn sites_closed(&self) -> P::NonNegativeInteger;
}

/// Metrics describing the size and complexity of a term.
pub trait TermMetrics<P: Primitives> {
    /// The total number of rewrite steps in this derivation.
    fn step_count(&self) -> P::NonNegativeInteger;
    /// The number of nodes in the canonical term's syntax tree.
    fn term_size(&self) -> P::NonNegativeInteger;
}

/// A single step in the construction of a SynthesizedType: one constraint added to the synthesis candidate and the resulting change in the constraint nerve's topological signature. Ordered by derivation:stepIndex. Analogous to derivation:RewriteStep in the forward pipeline.
pub trait SynthesisStep<P: Primitives> {
    /// Zero-based sequential index of this step within the synthesis derivation.
    fn step_index(&self) -> P::NonNegativeInteger;
    /// Associated type for `Constraint`.
    type Constraint: crate::user::type_::Constraint<P>;
    /// The constraint added in this synthesis step.
    fn added_constraint(&self) -> &Self::Constraint;
    /// Associated type for `SynthesisSignature`.
    type SynthesisSignature: crate::bridge::observable::SynthesisSignature<P>;
    /// The constraint nerve signature before this synthesis step.
    fn signature_before(&self) -> &Self::SynthesisSignature;
    /// The constraint nerve signature after this synthesis step.
    fn signature_after(&self) -> &Self::SynthesisSignature;
}

/// A persistent snapshot of a ConstraintSearchState at a specific SynthesisStep, allowing a TypeSynthesisResolver to resume exploration after interruption. Essential at Q1+ scale where exhaustive synthesis is computationally significant.
pub trait SynthesisCheckpoint<P: Primitives> {
    /// Associated type for `SynthesisStep`.
    type SynthesisStep: SynthesisStep<P>;
    /// The SynthesisStep at which this checkpoint was taken.
    fn checkpoint_step(&self) -> &Self::SynthesisStep;
    /// Associated type for `ConstraintSearchState`.
    type ConstraintSearchState: crate::bridge::resolver::ConstraintSearchState<P>;
    /// The ConstraintSearchState snapshot captured by this checkpoint.
    fn checkpoint_state(&self) -> &Self::ConstraintSearchState;
}

/// The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity.
pub mod critical_identity_rule {
    /// `groundedIn` -> `criticalIdentity`
    pub const GROUNDED_IN: &str = "https://uor.foundation/op/criticalIdentity";
}

/// The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f.
pub mod involution_rule {}

/// The rewrite rule applying associativity to re-bracket nested binary operations.
pub mod associativity_rule {}

/// The rewrite rule applying commutativity to reorder operands of commutative operations.
pub mod commutativity_rule {}

/// The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x.
pub mod identity_element_rule {}

/// The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address).
pub mod normalization_rule {}