Module ast 

Abstract Syntax Tree types for both logical expressions and imperative statements.

This module defines the core AST types produced by the parser and consumed by the transpiler, interpreter, and verifier. It is split into three submodules:

• logic: First-order logic expressions (predicates, quantifiers, connectives)
• stmt: Imperative statements (let bindings, if/match, loops, function defs)
• theorem: Theorem and proof blocks for the vernacular proof language

Logic Expressions (LogicExpr)

The logical fragment includes:

• Predicates with terms: Predicate { name, args, world }
• Quantifiers: ∀x, ∃x with island tracking for scope
• Connectives: ∧, ∨, →, ↔, ¬
• Modal operators: □, ◇ with Kripke semantics
• Lambda terms: λx.body for compositional semantics
• Neo-Davidsonian events: NeoEvent with thematic roles

Imperative Statements (Stmt)

The imperative fragment (LOGOS mode) includes:

• Let bindings with optional type annotations
• Control flow: if/else, match, while/for
• Function definitions with refinement types
• Assert/require/ensure for specification

Arena Allocation

All AST nodes are arena-allocated using bumpalo for efficient memory management. The 'a lifetime parameter tracks the arena lifetime.

Re-exports

pub use stmt::Stmt;

pub use stmt::Expr;

pub use stmt::Literal;

pub use stmt::Block;

pub use stmt::BinaryOpKind;

pub use stmt::TypeExpr;

pub use stmt::MatchArm;

pub use theorem::TheoremBlock;

pub use theorem::ProofStrategy;

pub use logic::*;

Modules

logic

Logic expression AST types for first-order logic with modal and event extensions.

stmt

Imperative statement AST types for the LOGOS language.

theorem

Theorem and proof block AST types.