pr4xis 0.6.0

Prove your domain is correct — ontology-driven rule enforcement with category theory, logical composition, and runtime state machines
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

use crate::category::Category;
use crate::logic::Axiom;

use super::property::Quality;

/// An ontology: what exists, how things relate, and what rules govern them.
///
/// An `Ontology` ties together:
/// - A category (individuals + relations with composition)
/// - Qualities on individuals (attributes, capabilities)
/// - Axioms: structural (auto-generated) + domain (user-provided)
///
/// Users implement `domain_axioms()` to declare domain-specific constraints.
/// Structural axioms (NoCycles, Antisymmetric, etc.) are generated by
/// `define_ontology!` and merged automatically via monoidal composition
/// (Vec concatenation). Users never see or touch structural axioms.
///
/// The ontology validates itself — if it compiles and passes validation,
/// the domain model is mathematically sound.
pub trait Ontology {
    /// The underlying category (individuals + relations).
    type Cat: Category;

    /// Qualities that individuals can have.
    type Qual: Quality<Individual = <Self::Cat as Category>::Object>;

    /// Structural axioms — auto-generated by `define_ontology!`.
    /// Users do NOT implement this. The macro provides it.
    /// Default: empty (for ontologies not using the macro).
    fn structural_axioms() -> Vec<Box<dyn Axiom>> {
        Vec::new()
    }

    /// Domain-specific axioms — the ONLY thing the user provides.
    /// These are constraints that require domain knowledge to express.
    /// Default: empty.
    fn domain_axioms() -> Vec<Box<dyn Axiom>> {
        Vec::new()
    }

    /// All axioms: structural ⊕ domain (monoidal composition under Vec concatenation).
    /// Users do NOT override this.
    fn axioms() -> Vec<Box<dyn Axiom>> {
        let mut all = Self::structural_axioms();
        all.extend(Self::domain_axioms());
        all
    }

    /// Validate the entire ontology: category laws + all axioms.
    fn validate() -> Result<(), Vec<String>>
    where
        <Self::Cat as Category>::Morphism: PartialEq,
    {
        let mut errors = Vec::new();

        // Category laws
        if let Err(e) = crate::category::validate::check_identity_law::<Self::Cat>() {
            errors.push(e);
        }
        if let Err(e) = crate::category::validate::check_associativity::<Self::Cat>() {
            errors.push(e);
        }
        if let Err(e) = crate::category::validate::check_closure::<Self::Cat>() {
            errors.push(e);
        }

        // All axioms (structural ⊕ domain)
        for axiom in Self::axioms() {
            if !axiom.holds() {
                errors.push(format!("axiom violated: {}", axiom.description()));
            }
        }

        if errors.is_empty() {
            Ok(())
        } else {
            Err(errors)
        }
    }
}