polydat_core/iteration/comprehension/optimize/

finding.rs

// Copyright 2024-2026 Jonathan Shook
// SPDX-License-Identifier: Apache-2.0

//! `ReducibilityFinding` and related types — comprehension_forms.md
//! §10.10.2.
//!
//! A finding represents either "no rewrite applies" (empty) or
//! "this rule rewrites C into the witness AST C'." Findings
//! also carry a [`ComplexityDelta`] declaring the improvement
//! the rewrite achieves in compute and/or memory complexity.

use serde::{Deserialize, Serialize};

use crate::iteration::comprehension::ast::Comprehension;

/// Identifier for each R-rule in the optimizer catalog
/// (§10.2 + §10.10.3).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum RuleId {
    /// Identity elimination: a singleton combinator or a trivial filter is dropped.
    R0a,
    /// Associativity flattening: nested unions or cartesians of one kind become one n-ary node.
    R0b,
    /// `order(Lex)` is a counter wrapper: it becomes a truncated lexicographic walk.
    R1,
    /// Push-down of a truncated order to an index-addressable child's closed form.
    R2,
    /// An untruncated lexicographic order commutes with a filter.
    R3,
    /// A filter distributes over a union.
    R4,
    /// A per-axis filter pushes down into a cartesian's axes.
    R5,
    /// A chain of filters folds into one.
    R6,
    /// A chain of orders folds into one when the inner is untruncated
    /// and the outer strategy selects from its input's shape.
    R7,
    // The catalog ends at R7 (comprehension_forms.md §14.1); R8–R10
    // name rewrites outside it, which no finding carries.
    /// Range narrowing from a bounded predicate; outside the catalog.
    R8,
    /// Discrete-set substitution from an `in` predicate; outside the
    /// catalog.
    R9,
    /// Monotonic-cutoff truncation; outside the catalog.
    R10,
}

/// Output of the reducibility analyzer (comprehension_forms.md §10.10.2).
#[derive(Debug, Clone, PartialEq)]
pub struct ReducibilityFinding {
    /// `Some` if a rewrite applies; `None` is the empty
    /// finding (no rule fires).
    pub reduction: Option<Reduction>,
    /// Which rule fired (mirrors `reduction.rule` if it's a
    /// Rewrite). Useful for logging / diagnostics.
    pub rule: Option<RuleId>,
    /// Asymptotic improvement of the witness over the input.
    pub improvement: ComplexityDelta,
}

/// The rewrite carried by a non-empty finding.
#[derive(Debug, Clone, PartialEq)]
pub enum Reduction {
    /// Replace the entire AST with `with` (whole-tree swap).
    Replace {
        /// The AST that replaces the whole input.
        with: Comprehension,
    },
    /// Rewrite via a tagged R-rule. The `witness` is the new
    /// AST; `rule` is the catalog identifier.
    Rewrite {
        /// The catalog rule that fired.
        rule: RuleId,
        /// The rewritten AST.
        witness: Comprehension,
    },
}

/// Strict-improvement vector along the (compute, memory)
/// dimensions (comprehension_forms.md §10.10.2 and §10.10.3's catalog
/// table).
///
/// A non-empty finding must have at least one dimension
/// `Less` and the other ≤ `Equal`. The optimizer rejects
/// findings that are `Equal` on both dimensions.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ComplexityDelta {
    /// How the compute cost of the witness compares to the input's.
    pub compute_order: Ordering,
    /// How its memory cost compares.
    pub memory_order: Ordering,
    /// Why the ordering holds.
    pub rationale: &'static str,
}

/// Three-way asymptotic ordering for one complexity dimension.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Ordering {
    /// Asymptotically less.
    Less,
    /// Asymptotically the same.
    Equal,
    /// Asymptotically more.
    Greater,
}

impl ComplexityDelta {
    /// Rule reduces compute, no change to memory.
    pub fn less_compute() -> Self {
        Self {
            compute_order: Ordering::Less,
            memory_order: Ordering::Equal,
            rationale: "strictly less compute",
        }
    }

    /// Rule reduces memory, no change to compute.
    pub fn less_memory() -> Self {
        Self {
            compute_order: Ordering::Equal,
            memory_order: Ordering::Less,
            rationale: "strictly less memory",
        }
    }

    /// Rule reduces both compute and memory.
    pub fn less_both() -> Self {
        Self {
            compute_order: Ordering::Less,
            memory_order: Ordering::Less,
            rationale: "strictly less compute and memory",
        }
    }

    /// No change in either dimension. Used for the empty
    /// finding; the optimizer never produces a `Reduction`
    /// with this delta.
    pub fn equal() -> Self {
        Self {
            compute_order: Ordering::Equal,
            memory_order: Ordering::Equal,
            rationale: "no asymptotic change",
        }
    }

    /// `true` if at least one dimension is strictly Less and
    /// the other is at most Equal. Per comprehension_forms.md §10.10.2 this is
    /// the condition for a non-empty finding to be valid.
    pub fn is_strict_improvement(&self) -> bool {
        matches!(
            (self.compute_order, self.memory_order),
            (Ordering::Less, Ordering::Less)
                | (Ordering::Less, Ordering::Equal)
                | (Ordering::Equal, Ordering::Less)
        )
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn delta_strict_improvement_classifier() {
        assert!(ComplexityDelta::less_compute().is_strict_improvement());
        assert!(ComplexityDelta::less_memory().is_strict_improvement());
        assert!(ComplexityDelta::less_both().is_strict_improvement());
        assert!(!ComplexityDelta::equal().is_strict_improvement());
    }

    #[test]
    fn rule_id_round_trip_serde() {
        let r = RuleId::R5;
        let json = serde_json::to_string(&r).unwrap();
        let back: RuleId = serde_json::from_str(&json).unwrap();
        assert_eq!(r, back);
    }
}