monist_core/
ast.rs

1/// Represents a variable in the logical formula.
2/// Variables can either be freely named (`Free`) or bound to a De Bruijn index (`Bound`).
3#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
4pub enum Var {
5    /// A free variable represented by its name.
6    Free(String),
7    /// A bound variable represented by its De Bruijn index.
8    Bound(usize),
9}
10
11/// Represents atomic propositions in the logic system.
12/// This includes fundamental set-theoretic and topological relations.
13#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
14pub enum Atomic {
15    /// Equality between two variables (`v1 = v2`).
16    Eq(Var, Var),
17    /// Set membership between two variables (`v1 ∈ v2`).
18    Mem(Var, Var),
19    /// Less-than relation, used for stratifications (`v1 < v2`).
20    Lt(Var, Var),
21    /// Quine pair constructor.
22    QPair,
23    /// Quine pair first projection.
24    QProj1,
25    /// Quine pair second projection.
26    QProj2,
27    /// Application for interaction nets.
28    App,
29    /// Lambda abstraction for interaction nets.
30    Lam,
31}
32
33/// Represents a recursive logical formula in the Abstract Syntax Tree (AST).
34/// 
35/// The structure forms a directed acyclic graph when mapped to `FormulaArena`.
36#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
37pub enum Formula {
38    /// An atomic proposition.
39    Atom(Atomic),
40    /// Logical negation of an inner formula.
41    Neg(usize),
42    /// Logical conjunction (AND) of two formulas.
43    Conj(usize, usize),
44    /// Logical disjunction (OR) of two formulas.
45    Disj(usize, usize),
46    /// Logical implication (=>) between two formulas.
47    Impl(usize, usize),
48    /// Universal quantification (∀) over a variable name in an inner formula.
49    Univ(usize, String, usize),
50    /// Existential quantification (∃) over a variable name in an inner formula.
51    Exist(usize, String, usize),
52    /// Set comprehension ({x | P(x)}), defining a new set based on a predicate.
53    Comp(usize, String, usize),
54}
55
56/// An arena-based allocator for managing the `Formula` abstract syntax tree.
57/// 
58/// By storing `Formula` nodes in a flat vector and referencing them by `usize` indices, 
59/// the system builds a Graph Reduction representation of the AST suitable for the 
60/// CPU Geometry Layer. This approach ensures locality and prevents deeply recursive structures.
61#[derive(Debug, Clone, Default, serde::Serialize, serde::Deserialize)]
62pub struct FormulaArena {
63    nodes: Vec<Formula>,
64}
65
66impl FormulaArena {
67    /// Creates a new, empty `FormulaArena`.
68    pub fn new() -> Self {
69        Self::default()
70    }
71
72    /// Adds a new `Formula` node to the arena and returns its index.
73    /// 
74    /// This index acts as a pointer to the formula and can be used in parent nodes.
75    pub fn add(&mut self, formula: Formula) -> usize {
76        let index = self.nodes.len();
77        self.nodes.push(formula);
78        index
79    }
80
81    /// Retrieves a reference to a `Formula` by its index in the arena.
82    /// Returns `None` if the index is out of bounds.
83    pub fn get(&self, index: usize) -> Option<&Formula> {
84        self.nodes.get(index)
85    }
86}
monist_core/ast.rs

monist_core/
ast.rs
