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.

Modules

axiom

AST nodes for the formal-logic vernacular: ## Axiom and ## Theory blocks.

definition

## Define block AST — a vernacular-logic predicate definition (Rung 0a).

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.

Structs

AxiomBlock

A ## Axiom block: a named first-order axiom in formal notation.

CategoricalData

Aristotelian categorical proposition data.

DefinitionBlock

A ## Define block: <definiendum>(params) if and only if <definiens>.

MatchArm

Match arm for pattern matching in Inspect statements.

ModalVector

Modal operator parameters for Kripke semantics (Kratzer-style).

NeoEventData

Neo-Davidsonian event structure with thematic roles.

NounPhrase

Parsed noun phrase structure for compositional interpretation.

RelationData

Simple subject-verb-object relation data.

SecurePad

The with pad "<path>" as <role> binding on a Connect/Listen — activate the PNP one-time-pad session over the pad file at pad, with this peer taking role.

TheoremBlock

A theorem block containing premises, goal, and proof strategy.

TheoryBlock

A ## Theory block: a named development that groups the axioms and theorems that follow it (## Theory Tarski). Its body is the formal development text — a sequence of Axiom … and Theorem … declarations parsed downstream.

Enums

AspectOperator

Grammatical aspect operators for event structure.

BinaryOpKind

Binary operation kinds for imperative expressions.

BinaryTemporalOp

Binary temporal operators (LTL).

ComparisonRelation

Degree-comparison relation for LogicExpr::Comparative.

CompressionCodec

The wire compression codec a Send compressed [with <codec>] selects. The transpiler maps this to the runtime’s wire codec; bare compressed = Deflate.

Dimension

Physical dimension for degree semantics and unit tracking.

Expr

Shared expression type for pure computations (LOGOS §15.0.0).

Literal

Literal values in LOGOS.

LogicExpr

First-order logic expression with modal, temporal, and event extensions.

LogicalType

Montague semantic types for compositional interpretation.

ModalDomain

Modal logic domain classification.

ModalFlavor

Modal flavor affecting scope interpretation.

NumberKind

Numeric literal representation for degree semantics.

ProofStrategy

Proof strategies for theorem verification.

QuantifierKind

Quantifier types for first-order and generalized quantifiers.

SecureRole

Imperative statement AST (LOGOS §15.0.0).

SendLayout

The wire LAYOUT a Send modifier picks — the size↔speed dial the sender chooses for their link. The transpiler maps this to the runtime’s numeric codec. The sender knows their use case; this lets them express it in one word.

Stmt

TemporalOperator

Temporal logic operators.

Term

First-order logic term representing entities or values.

ThematicRole

Neo-Davidsonian thematic roles for event semantics.

TypeExpr

Type expression for explicit type annotations.

UnaryOpKind

Unary logical operators.

VoiceOperator

Grammatical voice operators.

Type Aliases

Block

Block is a sequence of statements.