logicaffeine_language/ast/
mod.rs

1//! Abstract Syntax Tree types for both logical expressions and imperative statements.
2//!
3//! This module defines the core AST types produced by the parser and consumed by
4//! the transpiler, interpreter, and verifier. It is split into three submodules:
5//!
6//! - [`logic`]: First-order logic expressions (predicates, quantifiers, connectives)
7//! - [`stmt`]: Imperative statements (let bindings, if/match, loops, function defs)
8//! - [`theorem`]: Theorem and proof blocks for the vernacular proof language
9//!
10//! # Logic Expressions ([`LogicExpr`])
11//!
12//! The logical fragment includes:
13//! - Predicates with terms: `Predicate { name, args, world }`
14//! - Quantifiers: `∀x`, `∃x` with island tracking for scope
15//! - Connectives: `∧`, `∨`, `→`, `↔`, `¬`
16//! - Modal operators: `□`, `◇` with Kripke semantics
17//! - Lambda terms: `λx.body` for compositional semantics
18//! - Neo-Davidsonian events: `NeoEvent` with thematic roles
19//!
20//! # Imperative Statements ([`Stmt`])
21//!
22//! The imperative fragment (LOGOS mode) includes:
23//! - Let bindings with optional type annotations
24//! - Control flow: if/else, match, while/for
25//! - Function definitions with refinement types
26//! - Assert/require/ensure for specification
27//!
28//! # Arena Allocation
29//!
30//! All AST nodes are arena-allocated using `bumpalo` for efficient memory management.
31//! The `'a` lifetime parameter tracks the arena lifetime.
32
33pub mod axiom;
34pub mod definition;
35pub mod logic;
36pub mod stmt;
37pub mod theorem;
38
39pub use axiom::{AxiomBlock, TheoryBlock};
40pub use definition::DefinitionBlock;
41pub use logic::*;
42pub use stmt::{Stmt, Expr, Literal, Block, BinaryOpKind, CompressionCodec, SendLayout, TypeExpr, MatchArm, SecurePad, SecureRole};
43pub use theorem::{TheoremBlock, ProofStrategy};
logicaffeine_language/ast/mod.rs

logicaffeine_language/ast/
mod.rs
