vyre-conform 0.1.0

//! Loader and validator for embedded `.formal` law specifications.

use std::collections::BTreeSet;

use crate::proof::algebra::formal::spec::FormalLawSpec;
use crate::spec::law::LAW_CATALOG;

/// One embedded formal spec file.
#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub struct FormalSpecFile {
    /// Relative source path for diagnostics.
    pub path: &'static str,
    /// File contents.
    pub contents: &'static str,
}

/// Loader error for formal algebraic-law specs.
#[derive(Debug, thiserror::Error)]
pub enum FormalSpecError {
    /// TOML parsing failed.
    #[error("{path}: invalid .formal TOML: {source}. Fix: use the documented TOML schema.")]
    Parse {
        /// File path.
        path: &'static str,
        /// Parser error.
        source: toml::de::Error,
    },
    /// A required field was empty.
    #[error("{path}: {field} is empty. Fix: provide a non-empty value.")]
    EmptyField {
        /// File path.
        path: &'static str,
        /// Field name.
        field: &'static str,
    },
    /// Schema version is unsupported.
    #[error(
        "{path}: unsupported schema_version {version}. Fix: use schema_version = 1 or update the loader."
    )]
    UnsupportedSchema {
        /// File path.
        path: &'static str,
        /// Version in the file.
        version: u16,
    },
    /// A variable or parameter has an invalid field.
    #[error("{path}: invalid {item} `{name}`: {message}. Fix: make every field explicit.")]
    InvalidItem {
        /// File path.
        path: &'static str,
        /// Item kind.
        item: &'static str,
        /// Item name.
        name: String,
        /// Diagnostic.
        message: String,
    },
    /// A law is duplicated across files.
    #[error(
        "{path}: duplicate formal spec for law `{law}`. Fix: keep exactly one .formal file per AlgebraicLaw variant."
    )]
    DuplicateLaw {
        /// File path.
        path: &'static str,
        /// Law name.
        law: String,
    },
    /// A file names a law that is not in `LAW_CATALOG`.
    #[error(
        "{path}: unknown law `{law}`. Fix: use a canonical AlgebraicLaw name from LAW_CATALOG."
    )]
    UnknownLaw {
        /// File path.
        path: &'static str,
        /// Law name.
        law: String,
    },
    /// At least one `AlgebraicLaw` variant has no formal spec.
    #[error(
        "missing formal specs for {laws:?}. Fix: add conform/src/algebra/formal/<law>.formal files."
    )]
    MissingLaws {
        /// Missing law names.
        laws: Vec<String>,
    },
}

macro_rules! formal_file {
    ($name:literal) => {
        FormalSpecFile {
            path: concat!("conform/src/algebra/formal/", $name, ".formal"),
            contents: include_str!(concat!($name, ".formal")),
        }
    };
}

const FORMAL_SPEC_FILES: &[FormalSpecFile] = &[
    formal_file!("absorbing"),
    formal_file!("associative"),
    formal_file!("bounded"),
    formal_file!("commutative"),
    formal_file!("complement"),
    formal_file!("custom"),
    formal_file!("de-morgan"),
    formal_file!("distributive"),
    formal_file!("identity"),
    formal_file!("idempotent"),
    formal_file!("inverse-of"),
    formal_file!("involution"),
    formal_file!("lattice-absorption"),
    formal_file!("left-absorbing"),
    formal_file!("left-identity"),
    formal_file!("monotone"),
    formal_file!("monotonic"),
    formal_file!("right-absorbing"),
    formal_file!("right-identity"),
    formal_file!("self-inverse"),
    formal_file!("trichotomy"),
    formal_file!("zero-product"),
];

/// Parse and validate every embedded `.formal` law specification.
#[inline]
pub fn load_catalog() -> Result<Vec<FormalLawSpec>, FormalSpecError> {
    load_catalog_from_files(FORMAL_SPEC_FILES)
}

/// Parse and validate the supplied formal spec files.
#[inline]
pub fn load_catalog_from_files(
    files: &[FormalSpecFile],
) -> Result<Vec<FormalLawSpec>, FormalSpecError> {
    let known: BTreeSet<&str> = LAW_CATALOG.iter().copied().collect();
    let mut seen = BTreeSet::new();
    let mut specs = Vec::with_capacity(files.len());

    for file in files {
        let spec: FormalLawSpec =
            toml::from_str(file.contents).map_err(|source| FormalSpecError::Parse {
                path: file.path,
                source,
            })?;
        validate_spec(file.path, &spec, &known)?;
        if !seen.insert(spec.law.clone()) {
            return Err(FormalSpecError::DuplicateLaw {
                path: file.path,
                law: spec.law,
            });
        }
        specs.push(spec);
    }

    let missing = LAW_CATALOG
        .iter()
        .filter(|law| !seen.contains(**law))
        .map(|law| (*law).to_string())
        .collect::<Vec<_>>();
    if !missing.is_empty() {
        return Err(FormalSpecError::MissingLaws { laws: missing });
    }

    specs.sort_by(|left, right| left.law.cmp(&right.law));
    Ok(specs)
}

fn validate_spec(
    path: &'static str,
    spec: &FormalLawSpec,
    known: &BTreeSet<&str>,
) -> Result<(), FormalSpecError> {
    if spec.schema_version != 1 {
        return Err(FormalSpecError::UnsupportedSchema {
            path,
            version: spec.schema_version,
        });
    }
    reject_empty(path, "law", &spec.law)?;
    reject_empty(path, "variant", &spec.variant)?;
    reject_empty(path, "natural_language", &spec.natural_language)?;
    reject_empty(path, "mathematical_statement", &spec.mathematical_statement)?;
    reject_empty(path, "postcondition", &spec.postcondition)?;
    reject_empty(path, "citation", &spec.citation)?;

    if !known.contains(spec.law.as_str()) {
        return Err(FormalSpecError::UnknownLaw {
            path,
            law: spec.law.clone(),
        });
    }
    if spec.variables.is_empty() && spec.parameters.is_empty() {
        return Err(FormalSpecError::EmptyField {
            path,
            field: "variables or parameters",
        });
    }
    if spec.preconditions.is_empty() {
        return Err(FormalSpecError::EmptyField {
            path,
            field: "preconditions",
        });
    }
    for variable in &spec.variables {
        validate_item(
            path,
            "variable",
            &variable.name,
            &variable.ty,
            &variable.role,
        )?;
    }
    for parameter in &spec.parameters {
        validate_item(
            path,
            "parameter",
            &parameter.name,
            &parameter.ty,
            &parameter.source,
        )?;
    }
    Ok(())
}

fn reject_empty(
    path: &'static str,
    field: &'static str,
    value: &str,
) -> Result<(), FormalSpecError> {
    if value.trim().is_empty() {
        return Err(FormalSpecError::EmptyField { path, field });
    }
    Ok(())
}

fn validate_item(
    path: &'static str,
    item: &'static str,
    name: &str,
    ty: &str,
    detail: &str,
) -> Result<(), FormalSpecError> {
    if name.trim().is_empty() {
        return Err(FormalSpecError::InvalidItem {
            path,
            item,
            name: name.to_string(),
            message: "empty name".to_string(),
        });
    }
    if ty.trim().is_empty() || detail.trim().is_empty() {
        return Err(FormalSpecError::InvalidItem {
            path,
            item,
            name: name.to_string(),
            message: "empty type or source/role".to_string(),
        });
    }
    Ok(())
}