csw_derive/

type_system.rs

//! Type system representation.
//!
//! This module defines the data structures that represent a derived type system,
//! including type constructors, term constructors, typing rules, and reduction rules.

#[cfg(feature = "serde")]
use serde::{Deserialize, Serialize};

/// A complete derived type system.
///
/// This is the main output of the derivation process.
#[derive(Clone, Debug, Default)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct TypeSystem {
    /// Name of the type system
    pub name: String,

    /// Type constructors (how to form types)
    pub type_constructors: Vec<TypeConstructor>,

    /// Term constructors (how to form terms)
    pub term_constructors: Vec<TermConstructor>,

    /// Typing rules
    pub typing_rules: Vec<TypingRule>,

    /// Reduction rules (β-reduction)
    pub reduction_rules: Vec<ReductionRule>,

    /// Equivalence rules (η-expansion)
    pub equivalence_rules: Vec<EquivalenceRule>,

    /// Structural rules available
    pub structural: StructuralRules,
}

/// A type constructor in the derived type system.
#[derive(Clone, Debug)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct TypeConstructor {
    /// Internal name
    pub name: String,

    /// Display symbol (e.g., "×", "→", "⊗")
    pub symbol: String,

    /// Number of type arguments
    pub arity: usize,

    /// Kind of type constructor
    pub kind: TypeConstructorKind,
}

/// The kind of a type constructor.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum TypeConstructorKind {
    /// Base/primitive type
    Base,
    /// Unit type (terminal object)
    Unit,
    /// Empty type (initial object)
    Empty,
    /// Product type (A × B)
    Product,
    /// Coproduct/sum type (A + B)
    Coproduct,
    /// Function type (A → B)
    Exponential,
    /// Tensor product (A ⊗ B)
    Tensor,
    /// Linear function (A ⊸ B)
    LinearHom,
}

/// A term constructor in the derived type system.
#[derive(Clone, Debug)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct TermConstructor {
    /// Internal name
    pub name: String,

    /// Display symbol or template
    pub symbol: String,

    /// Kind of term constructor
    pub kind: TermConstructorKind,
}

/// The kind of a term constructor.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum TermConstructorKind {
    /// Variable reference
    Variable,
    /// Unit value introduction
    UnitIntro,
    /// Pair introduction
    PairIntro,
    /// First projection
    PairElimFst,
    /// Second projection
    PairElimSnd,
    /// Lambda abstraction
    Abstraction,
    /// Function application
    Application,
    /// Left injection (sum types)
    InjLeft,
    /// Right injection (sum types)
    InjRight,
    /// Case analysis (sum types)
    Case,
    /// Absurd elimination (empty type)
    Absurd,
    /// Let binding for pairs
    LetPair,
}

/// A typing rule in the type system.
#[derive(Clone, Debug)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct TypingRule {
    /// Name of the rule (e.g., "abs-intro", "app-elim")
    pub name: String,

    /// Premises (judgments above the line)
    pub premises: Vec<String>,

    /// Conclusion (judgment below the line)
    pub conclusion: String,

    /// Side conditions
    pub side_conditions: Vec<String>,
}

/// A reduction rule (β-reduction).
#[derive(Clone, Debug)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct ReductionRule {
    /// Name of the rule (e.g., "beta", "fst-beta")
    pub name: String,

    /// Left-hand side (redex)
    pub lhs: String,

    /// Right-hand side (reduct)
    pub rhs: String,
}

/// An equivalence rule (η-expansion).
#[derive(Clone, Debug)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct EquivalenceRule {
    /// Name of the rule
    pub name: String,

    /// Left-hand side
    pub lhs: String,

    /// Right-hand side
    pub rhs: String,

    /// Type condition (when this rule applies)
    pub condition: Option<String>,
}

/// Structural rules available in the type system.
#[derive(Clone, Debug, Default)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct StructuralRules {
    /// Weakening: can ignore variables
    pub weakening: bool,

    /// Contraction: can use variables multiple times
    pub contraction: bool,

    /// Exchange: variable order doesn't matter
    pub exchange: bool,
}

impl std::fmt::Display for TypeSystem {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        writeln!(f, "# {} Type System", self.name)?;
        writeln!(f)?;

        // Types
        writeln!(f, "## Types")?;
        writeln!(f)?;
        for tc in &self.type_constructors {
            writeln!(f, "  {} ({})", tc.symbol, tc.name)?;
        }
        writeln!(f)?;

        // Terms
        writeln!(f, "## Terms")?;
        writeln!(f)?;
        for tc in &self.term_constructors {
            writeln!(f, "  {} ({})", tc.symbol, tc.name)?;
        }
        writeln!(f)?;

        // Typing Rules
        writeln!(f, "## Typing Rules")?;
        writeln!(f)?;
        for rule in &self.typing_rules {
            writeln!(f, "### {}", rule.name)?;
            for premise in &rule.premises {
                writeln!(f, "  {}", premise)?;
            }
            if !rule.premises.is_empty() {
                writeln!(f, "  ────────────────────")?;
            }
            writeln!(f, "  {}", rule.conclusion)?;
            writeln!(f)?;
        }

        // Reduction Rules
        writeln!(f, "## Reduction Rules")?;
        writeln!(f)?;
        for rule in &self.reduction_rules {
            writeln!(f, "  {} → {}  ({})", rule.lhs, rule.rhs, rule.name)?;
        }
        writeln!(f)?;

        // Structural Rules
        writeln!(f, "## Structural Rules")?;
        writeln!(f)?;
        writeln!(f, "  Weakening:   {}", if self.structural.weakening { "✓" } else { "✗" })?;
        writeln!(f, "  Contraction: {}", if self.structural.contraction { "✓" } else { "✗" })?;
        writeln!(f, "  Exchange:    {}", if self.structural.exchange { "✓" } else { "✗" })?;

        Ok(())
    }
}