logicaffeine-language 0.10.1

//! Imperative statement AST types for the LOGOS language.
//!
//! This module defines statement types for the imperative fragment including:
//!
//! - **[`Stmt`]**: Statement variants (let, if, match, while, for, function defs)
//! - **[`Expr`]**: Imperative expressions (field access, method calls, literals)
//! - **[`TypeExpr`]**: Type annotations with refinements and generics
//! - **[`Literal`]**: Literal values (numbers, strings, booleans)
//! - **[`Block`]**: Statement blocks with optional return expressions
//!
//! The imperative AST is used in LOGOS mode for generating executable Rust code.

use super::axiom::{AxiomBlock, TheoryBlock};
use super::definition::DefinitionBlock;
use super::logic::LogicExpr;
use super::theorem::TheoremBlock;
use logicaffeine_base::Symbol;

/// Type expression for explicit type annotations.
///
/// Represents type syntax like:
/// - `Int` → Primitive(Int)
/// - `User` → Named(User)
/// - `List of Int` → Generic { base: List, params: [Primitive(Int)] }
/// - `List of List of Int` → Generic { base: List, params: [Generic { base: List, params: [Primitive(Int)] }] }
/// - `Result of Int and Text` → Generic { base: Result, params: [Primitive(Int), Primitive(Text)] }
#[derive(Debug, Clone)]
pub enum TypeExpr<'a> {
    /// Primitive type: Int, Nat, Text, Bool
    Primitive(Symbol),
    /// Named type (user-defined): User, Point
    Named(Symbol),
    /// Generic type: List of Int, Option of Text, Result of Int and Text
    Generic {
        base: Symbol,
        params: &'a [TypeExpr<'a>],
    },
    /// Function type: fn(A, B) -> C (for higher-order functions)
    Function {
        inputs: &'a [TypeExpr<'a>],
        output: &'a TypeExpr<'a>,
    },
    /// Refinement type with predicate constraint.
    /// Example: `Int where it > 0`
    Refinement {
        /// The base type being refined
        base: &'a TypeExpr<'a>,
        /// The bound variable (usually "it")
        var: Symbol,
        /// The predicate constraint (from Logic Kernel)
        predicate: &'a LogicExpr<'a>,
    },
    /// Persistent storage wrapper type.
    /// Example: `Persistent Counter`
    /// Semantics: Wraps a Shared type with journal-backed storage
    Persistent {
        /// The inner type (must be a Shared/CRDT type)
        inner: &'a TypeExpr<'a>,
    },
    /// Mutable-parameter marker (Mutable Value Semantics escape hatch).
    /// Example: `## To addItem (items: mutable Seq of Int):` →
    /// `Mutable { inner: Generic { List, [Int] } }`.
    /// Semantics: under value semantics collections pass by value by default; a
    /// `Mutable` parameter passes by reference so the callee's mutations are
    /// visible to the caller (the explicit, opt-in form of the void-mutate
    /// idiom). Carried on the parameter's type so the `(Symbol, &TypeExpr)`
    /// parameter representation is unchanged. For every purpose other than the
    /// parameter-passing convention, `Mutable { inner }` behaves as `inner`.
    Mutable {
        /// The underlying parameter type.
        inner: &'a TypeExpr<'a>,
    },
}

/// Source for Read statements.
#[derive(Debug, Clone, Copy)]
pub enum ReadSource<'a> {
    /// Read from console (stdin)
    Console,
    /// Read from file at given path
    File(&'a Expr<'a>),
}

/// Pattern for loop variable binding.
/// Supports single identifiers and tuple destructuring for Map iteration.
#[derive(Debug, Clone)]
pub enum Pattern {
    /// Single identifier: `Repeat for x in list`
    Identifier(Symbol),
    /// Tuple destructuring: `Repeat for (k, v) in map`
    Tuple(Vec<Symbol>),
}

/// Binary operation kinds for imperative expressions.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum BinaryOpKind {
    Add,
    Subtract,
    Multiply,
    /// `a ** b` — exponentiation. Integer power is EXACT (promotes to BigInt on
    /// overflow); a Float operand uses `powf`; a negative integer exponent is a
    /// loud error. Binds tighter than `* / %`, right-associative.
    Pow,
    Divide,
    /// EXACT division — the type-directed sibling of [`BinaryOpKind::Divide`].
    /// `Divide` floors (`7 / 2 → 3`, the integer default); `ExactDivide` keeps the
    /// quotient exact (`7 / 2 → 7/2`, a `Rational`). The `resolve_divisions` pass
    /// rewrites `Divide → ExactDivide` only where the result flows into a `Rational`
    /// context, so existing (floor) code is untouched.
    ExactDivide,
    /// `a // b` — FLOOR division, rounding toward negative infinity (`-7 // 2 → -4`).
    /// Distinct from [`BinaryOpKind::Divide`], which truncates toward zero (`-7 / 2 →
    /// -3`); the two agree when the operands share a sign. Exact (promotes to BigInt),
    /// integer-producing, and immune to the `resolve_divisions` Rational rewrite — the
    /// explicit spelling for "give me the floored integer quotient."
    FloorDivide,
    Modulo,
    Eq,
    NotEq,
    Lt,
    Gt,
    LtEq,
    GtEq,
    // Logical/bitwise operators — type-aware in codegen (&&/|| for Bool, &/| for Int)
    And,
    Or,
    /// String concatenation ("X combined with Y")
    Concat,
    /// Sequence concatenation ("A followed by B") — merge two sequences into one.
    SeqConcat,
    /// Tolerant float comparison ("a is approximately b") — Python-isclose
    /// semantics (rel 1e-9, abs floor 1e-12). `==` stays IEEE bit-exact;
    /// this is the EXPLICIT spelling for near-equality.
    ApproxEq,
    /// Bitwise XOR: `x ^ y` (the word `xor` is the English spelling); on
    /// Sets, symmetric difference.
    BitXor,
    /// Bitwise AND: `x & y`; on Sets, intersection.
    BitAnd,
    /// Bitwise OR: `x | y`; on Sets, union.
    BitOr,
    /// Left shift: "x shifted left by y" → `x << y`
    Shl,
    /// Right shift: "x shifted right by y" → `x >> y`
    Shr,
}

/// Block is a sequence of statements.
pub type Block<'a> = &'a [Stmt<'a>];

/// Match arm for pattern matching in Inspect statements.
#[derive(Debug, Clone)]
pub struct MatchArm<'a> {
    pub enum_name: Option<Symbol>,          // The enum type (e.g., Shape)
    pub variant: Option<Symbol>,            // None = Otherwise (wildcard)
    pub bindings: Vec<(Symbol, Symbol)>,    // (field_name, binding_name)
    pub body: Block<'a>,
}

/// The wire compression codec a `Send compressed [with <codec>]` selects. The
/// transpiler maps this to the runtime's wire codec; bare `compressed` = `Deflate`.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum CompressionCodec {
    /// DEFLATE — the balanced default (bare `Send compressed`).
    Deflate,
    /// LZ4 — near-memcpy speed, lighter ratio.
    Lz4,
    /// Zstandard — the best ratio.
    Zstd,
}

/// 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.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum SendLayout {
    /// `compact` / `small` — smallest wire (LEB128 varint). For a bandwidth-bound link
    /// (mobile, WAN, metered). This is also the default when no layout word is given.
    Compact,
    /// `fast` / `quickly` — fastest decode (fixed-width memcpy, zero parse). For a
    /// latency-bound / fat link (LAN, datacenter, RDMA).
    Fast,
    /// `packed` — varint size with SIMD group-varint decode; the balanced middle.
    Packed,
    /// `smallest` / `best` — turn on the per-column compression menu (delta /
    /// delta-of-delta / frame-of-reference / run-length / dictionary), auto-selecting
    /// each column's smallest form and never exceeding plain varint. For a
    /// bandwidth-bound link where CPU is cheap relative to bytes.
    Smallest,
    /// `redundant` / `tough` — forward error correction: the message is split into
    /// Reed-Solomon shards and each is published as its own packet, so a receiver
    /// reconstructs the exact message from any K even after some are lost. For a lossy
    /// / one-way link (UDP, multicast, BLE, LoRa) where retransmit is impossible.
    Redundant,
}

/// Backing-file source for a memory-mapped zone (`… mapped from <here>`).
/// `Inside a zone called "D" mapped from "f.bin"` is [`ZoneSource::Literal`];
/// `… mapped from path` (a runtime `Text` variable) is [`ZoneSource::Variable`].
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ZoneSource {
    /// A string-literal path baked into the source.
    Literal(Symbol),
    /// A variable holding the path, resolved at runtime.
    Variable(Symbol),
}

/// Imperative statement AST (LOGOS §15.0.0).
///
/// Stmt is the primary AST node for imperative code blocks like `## Main`
/// and function bodies. The Assert variant bridges to the Logic Kernel.
/// Which end of the shared pad this peer draws from, for the PNP one-time-pad tier.
/// `as initiator` sends on the first directional half; `as responder` sends on the second.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SecureRole {
    /// Draws the send pad from the first directional half (`i2r`).
    Initiator,
    /// Draws the send pad from the second directional half (`r2i`).
    Responder,
}

/// 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`.
#[derive(Debug, Clone, Copy)]
pub struct SecurePad<'a> {
    /// The pad file path (a string-literal or variable expression).
    pub pad: &'a Expr<'a>,
    /// Which directional half this peer sends on.
    pub role: SecureRole,
}

#[derive(Debug, Clone)]
pub enum Stmt<'a> {
    /// Variable binding: `Let x be 5.` or `Let x: Int be 5.`
    Let {
        var: Symbol,
        ty: Option<&'a TypeExpr<'a>>,
        value: &'a Expr<'a>,
        mutable: bool,
    },

    /// Mutation: `Set x to 10.`
    Set {
        target: Symbol,
        value: &'a Expr<'a>,
    },

    /// Function call as statement: `Call process with data.`
    Call {
        function: Symbol,
        args: Vec<&'a Expr<'a>>,
    },

    /// Conditional: `If condition: ... Otherwise: ...`
    If {
        cond: &'a Expr<'a>,
        then_block: Block<'a>,
        else_block: Option<Block<'a>>,
    },

    /// Loop: `While condition: ...` or `While condition (decreasing expr): ...`
    While {
        cond: &'a Expr<'a>,
        body: Block<'a>,
        /// Optional decreasing variant for termination proof.
        decreasing: Option<&'a Expr<'a>>,
    },

    /// Iteration: `Repeat for x in list: ...` or `Repeat for i from 1 to 10: ...`
    Repeat {
        pattern: Pattern,  // Changed from `var: Symbol` to support tuple destructuring
        iterable: &'a Expr<'a>,
        body: Block<'a>,
    },

    /// Return: `Return x.` or `Return.`
    Return {
        value: Option<&'a Expr<'a>>,
    },

    /// Break: `Break.` — exits the innermost while loop.
    Break,

    /// Bridge to Logic Kernel: `Assert that P.`
    Assert {
        proposition: &'a LogicExpr<'a>,
    },

    /// Documented assertion with justification.
    /// `Trust that P because "reason".`
    /// Semantics: Documented runtime check that could be verified statically.
    Trust {
        proposition: &'a LogicExpr<'a>,
        justification: Symbol,
    },

    /// Runtime assertion with imperative condition.
    /// `Assert that condition.` (`hard: false` → `debug_assert!`, a development check)
    /// `Require that condition.` (`hard: true` → `assert!`, an enforced invariant that
    /// survives release — the form a proven property lowers to).
    RuntimeAssert {
        condition: &'a Expr<'a>,
        hard: bool,
    },

    /// Ownership transfer (move): `Give x to processor.`
    /// Semantics: Move ownership of `object` to `recipient`.
    Give {
        object: &'a Expr<'a>,
        recipient: &'a Expr<'a>,
    },

    /// Immutable borrow: `Show x to console.`
    /// Semantics: Immutable borrow of `object` passed to `recipient`.
    Show {
        object: &'a Expr<'a>,
        recipient: &'a Expr<'a>,
    },

    /// Field mutation: `Set p's x to 10.`
    SetField {
        object: &'a Expr<'a>,
        field: Symbol,
        value: &'a Expr<'a>,
    },

    /// Struct definition for codegen.
    StructDef {
        name: Symbol,
        fields: Vec<(Symbol, Symbol, bool)>, // (name, type_name, is_public)
        is_portable: bool,                    // Derives Serialize/Deserialize
    },

    /// Function definition.
    FunctionDef {
        name: Symbol,
        /// Generic type parameters: empty for monomorphic functions, e.g. `[T, U]` for polymorphic.
        generics: Vec<Symbol>,
        params: Vec<(Symbol, &'a TypeExpr<'a>)>,
        body: Block<'a>,
        return_type: Option<&'a TypeExpr<'a>>,
        is_native: bool,
        /// Rust path for user-defined native functions (e.g., "reqwest::blocking::get").
        /// None for system native functions (read, write, etc.) which use map_native_function().
        native_path: Option<Symbol>,
        /// Whether this function is exported for FFI (C ABI or WASM).
        is_exported: bool,
        /// Export target: None = C ABI (#\[no_mangle\] extern "C"), Some("wasm") = #\[wasm_bindgen\].
        export_target: Option<Symbol>,
        /// Per-function optimization config: each `## No <X>` annotation clears
        /// that optimization's bit (default: all enabled).
        opt_flags: crate::optimization::OptimizationConfig,
    },

    /// Pattern matching on sum types.
    Inspect {
        target: &'a Expr<'a>,
        arms: Vec<MatchArm<'a>>,
        has_otherwise: bool,            // For exhaustiveness tracking
    },

    /// Push to collection: `Push x to items.`
    Push {
        value: &'a Expr<'a>,
        collection: &'a Expr<'a>,
    },

    /// Pop from collection: `Pop from items.` or `Pop from items into y.`
    Pop {
        collection: &'a Expr<'a>,
        into: Option<Symbol>,
    },

    /// Add to set: `Add x to set.`
    Add {
        value: &'a Expr<'a>,
        collection: &'a Expr<'a>,
    },

    /// Remove from set: `Remove x from set.`
    Remove {
        value: &'a Expr<'a>,
        collection: &'a Expr<'a>,
    },

    /// Index assignment: `Set item N of X to Y.`
    SetIndex {
        collection: &'a Expr<'a>,
        index: &'a Expr<'a>,
        value: &'a Expr<'a>,
    },

    /// A SCOPE-TRANSPARENT statement sequence — parser-desugar output, never
    /// written by users. One surface statement can lower to several primitive
    /// statements (a nested place-write `Set item j of (item i of grid) to v`
    /// becomes read → copy-on-write element write → write-back; a multi-push
    /// `Push a, b, c to xs` becomes one Push per element). The body runs in
    /// the ENCLOSING scope with no block of its own: temporaries inside are
    /// gensym'd (`__place_*`), so they can never collide with user names, and
    /// engines that execute blocks with scoping must NOT scope this one.
    Splice {
        body: Block<'a>,
    },

    /// Memory arena block (Zone).
    /// "Inside a new zone called 'Scratch':"
    /// "Inside a zone called 'Buffer' of size 1 MB:"
    /// "Inside a zone called 'Data' mapped from 'file.bin':"
    Zone {
        /// The variable name for the arena handle (e.g., "Scratch")
        name: Symbol,
        /// Optional pre-allocated capacity in bytes (Heap zones only)
        capacity: Option<usize>,
        /// Optional backing file for memory-mapped zones (literal path or runtime variable)
        source_file: Option<ZoneSource>,
        /// The code block executed within this memory context
        body: Block<'a>,
    },

    /// Concurrent execution block (async, I/O-bound).
    /// "Attempt all of the following:"
    /// Semantics: All tasks run concurrently via tokio::join!
    /// Best for: network requests, file I/O, waiting operations
    Concurrent {
        /// The statements to execute concurrently
        tasks: Block<'a>,
    },

    /// Parallel execution block (CPU-bound).
    /// "Simultaneously:"
    /// Semantics: True parallelism via rayon::join or thread::spawn
    /// Best for: computation, data processing, number crunching
    Parallel {
        /// The statements to execute in parallel
        tasks: Block<'a>,
    },

    /// Read from console or file.
    /// `Read input from the console.` or `Read data from file "path.txt".`
    ReadFrom {
        var: Symbol,
        source: ReadSource<'a>,
    },

    /// Write to file.
    /// `Write "content" to file "output.txt".`
    WriteFile {
        content: &'a Expr<'a>,
        path: &'a Expr<'a>,
    },

    /// Spawn an agent.
    /// `Spawn a Worker called "w1".`
    Spawn {
        agent_type: Symbol,
        name: Symbol,
    },

    /// Send message to agent.
    /// `Send Ping to "agent".`, `Send compressed Ping to "agent".`,
    /// `Send cached Point to "agent".`, or `Send cached compressed Report to "agent".`
    SendMessage {
        message: &'a Expr<'a>,
        destination: &'a Expr<'a>,
        /// The wire compression codec. `None` for a plain `Send`; `Some(codec)` for
        /// `Send compressed [with <codec>]` (bare `compressed` = deflate). Kept only
        /// if it actually shrinks the body.
        compression: Option<CompressionCodec>,
        /// `Send cached …` — use the connection's schema dictionary, so a struct
        /// schema is transmitted once and referenced thereafter (content-addressed,
        /// footgun-free). `false` for a plain `Send`.
        cached: bool,
        /// `Send unchecked …` — drop the wire integrity checksum for the fastest path
        /// (latency↔safety dial). `false` keeps the default checksum.
        unchecked: bool,
        /// `Send fast|compact|packed …` — the wire LAYOUT (size↔speed dial). `None` is
        /// the default (compact / varint). The sender picks for their link.
        layout: Option<SendLayout>,
        /// `Send shared …` — OPT-IN type-id elision: drop struct/enum NAMES off the wire
        /// (ship a small registry id both ends derive from their shared program type
        /// defs). Only safe when the receiver runs the same program, so it is OFF by
        /// default — the default `Send` stays self-describing for any peer / relay.
        shared: bool,
        /// `Send computed f …` — COMPUTE-SHIPPING: when the message is a pure single-arg
        /// function, lower it to a sandboxed generator and ship the COMPUTATION, not data.
        /// The receiver evaluates it in the bounded sandbox (never arbitrary code). OFF by
        /// default; a non-lowerable function under `computed` is rejected at send.
        computed: bool,
        /// `Send indexed …` (alias `addressable`) — encode a record list in the random-access
        /// struct-view LAYOUT (row + field offset tables), so the receiver reaches any
        /// (row, field) in O(1) without decoding the rest — Cap'n Proto's home turf. Composes
        /// with the other knobs (`compressed`, `cached`, `shared`, `unchecked`). OFF by default
        /// (the dense columnar form is smaller); opt in when the peer does random field reads.
        indexed: bool,
        /// `Send deduped …` — Rc-DEDUP: a subtree the same value reaches more than once ships ONCE
        /// (the first occurrence) plus a tiny backref for every repeat, and the receiver rebuilds the
        /// SHARING (one aliased value, not N copies). OFF by default; opt in when the message has
        /// shared sub-structure (a lookup table referenced by many records, one object aliased
        /// across the payload). Self-describing by tag, so any peer decodes it.
        deduped: bool,
    },

    /// Await response from agent.
    /// `Await response from "agent" into result.`
    AwaitMessage {
        source: &'a Expr<'a>,
        into: Symbol,
        /// `Await view from …`: hold a received record-list LAZILY (the zero-copy receive —
        /// decode-on-touch, no rows materialized until a field is read) instead of fully decoding
        /// it. Ignored for non-record-list shapes, which always decode eagerly.
        view: bool,
        /// `Await stream from …`: receive a batch STREAM message and deframe it into a list (the
        /// values a peer `Stream`ed), rather than a single message.
        stream: bool,
    },

    /// Stream a batch of values to a peer in one framed message.
    /// `Stream readings to "sink".` — frames each element of `values` length-delimited so the
    /// receiver (`Await stream from …`) deframes them incrementally; one relay publish ships the
    /// whole batch (Kafka-style streaming that amortizes per-message overhead).
    StreamMessage {
        values: &'a Expr<'a>,
        destination: &'a Expr<'a>,
    },

    /// Merge CRDT state.
    /// `Merge remote into local.` or `Merge remote's field into local's field.`
    MergeCrdt {
        source: &'a Expr<'a>,
        target: &'a Expr<'a>,
    },

    /// Increment GCounter.
    /// `Increase local's points by 10.`
    IncreaseCrdt {
        object: &'a Expr<'a>,
        field: Symbol,
        amount: &'a Expr<'a>,
    },

    /// Decrement PNCounter (Tally).
    /// `Decrease game's score by 5.`
    DecreaseCrdt {
        object: &'a Expr<'a>,
        field: Symbol,
        amount: &'a Expr<'a>,
    },

    /// Append to SharedSequence (RGA).
    /// `Append "Hello" to doc's lines.`
    AppendToSequence {
        sequence: &'a Expr<'a>,
        value: &'a Expr<'a>,
    },

    /// Resolve MVRegister conflicts.
    /// `Resolve page's title to "Final".`
    ResolveConflict {
        object: &'a Expr<'a>,
        field: Symbol,
        value: &'a Expr<'a>,
    },

    /// Security check - mandatory runtime guard.
    /// `Check that user is admin.`
    /// `Check that user can publish the document.`
    /// Semantics: NEVER optimized out. Panics if condition is false.
    Check {
        /// The subject being checked (e.g., "user")
        subject: Symbol,
        /// The predicate name (e.g., "admin") or action (e.g., "publish")
        predicate: Symbol,
        /// True if this is a capability check (`can [action]`)
        is_capability: bool,
        /// For capabilities: the object being acted on (e.g., "document")
        object: Option<Symbol>,
        /// Original English text for error message
        source_text: String,
        /// Source location for error reporting
        span: crate::token::Span,
    },

    /// Listen on network address.
    /// `Listen on "/ip4/127.0.0.1/tcp/8000".`
    /// Semantics: Bind to address, start accepting connections via libp2p
    Listen {
        address: &'a Expr<'a>,
        /// Optional PNP one-time-pad binding: `with pad "<path>" as initiator|responder`.
        secure: Option<SecurePad<'a>>,
    },

    /// Connect to remote peer.
    /// `Connect to "/ip4/127.0.0.1/tcp/8000".`
    /// Semantics: Dial peer via libp2p
    ConnectTo {
        address: &'a Expr<'a>,
        /// Optional PNP one-time-pad binding: `with pad "<path>" as initiator|responder`.
        secure: Option<SecurePad<'a>>,
    },

    /// Create PeerAgent remote handle.
    /// `Let remote be a PeerAgent at "/ip4/127.0.0.1/tcp/8000".`
    /// Semantics: Create handle for remote agent communication
    LetPeerAgent {
        var: Symbol,
        address: &'a Expr<'a>,
    },

    /// Sleep for milliseconds.
    /// `Sleep 1000.` or `Sleep delay.`
    /// Semantics: Pause execution for N milliseconds (async)
    Sleep {
        milliseconds: &'a Expr<'a>,
    },

    /// Sync CRDT variable on topic.
    /// `Sync x on "topic".`
    /// Semantics: Subscribe to GossipSub topic, auto-publish on mutation, auto-merge on receive
    Sync {
        var: Symbol,
        topic: &'a Expr<'a>,
    },

    /// Mount persistent CRDT from journal file.
    /// `Mount counter at "data/counter.journal".`
    /// Semantics: Load or create journal, replay operations to reconstruct state
    Mount {
        /// The variable name for the mounted value
        var: Symbol,
        /// The path expression for the journal file
        path: &'a Expr<'a>,
    },

    // =========================================================================
    // Go-like Concurrency (Green Threads, Channels, Select)
    // =========================================================================

    /// Launch a fire-and-forget task (green thread).
    /// `Launch a task to process(data).`
    /// Semantics: tokio::spawn with no handle capture
    LaunchTask {
        /// The function to call
        function: Symbol,
        /// Arguments to pass
        args: Vec<&'a Expr<'a>>,
    },

    /// Launch a task with handle for control.
    /// `Let worker be Launch a task to process(data).`
    /// Semantics: tokio::spawn returning JoinHandle
    LaunchTaskWithHandle {
        /// Variable to bind the handle
        handle: Symbol,
        /// The function to call
        function: Symbol,
        /// Arguments to pass
        args: Vec<&'a Expr<'a>>,
    },

    /// Create a bounded channel (pipe).
    /// `Let jobs be a new Pipe of Int.`
    /// Semantics: tokio::sync::mpsc::channel(32)
    CreatePipe {
        /// Variable for the pipe
        var: Symbol,
        /// Type of values in the pipe
        element_type: Symbol,
        /// Optional capacity (defaults to 32)
        capacity: Option<u32>,
    },

    /// Blocking send into pipe.
    /// `Send value into pipe.`
    /// Semantics: pipe_tx.send(value).await
    SendPipe {
        /// The value to send
        value: &'a Expr<'a>,
        /// The pipe to send into
        pipe: &'a Expr<'a>,
    },

    /// Blocking receive from pipe.
    /// `Receive x from pipe.`
    /// Semantics: let x = pipe_rx.recv().await
    ReceivePipe {
        /// Variable to bind the received value
        var: Symbol,
        /// The pipe to receive from
        pipe: &'a Expr<'a>,
    },

    /// Non-blocking send (try).
    /// `Try to send value into pipe.`
    /// Semantics: pipe_tx.try_send(value) - returns immediately
    TrySendPipe {
        /// The value to send
        value: &'a Expr<'a>,
        /// The pipe to send into
        pipe: &'a Expr<'a>,
        /// Variable to bind the result (true/false)
        result: Option<Symbol>,
    },

    /// Non-blocking receive (try).
    /// `Try to receive x from pipe.`
    /// Semantics: pipe_rx.try_recv() - returns Option
    TryReceivePipe {
        /// Variable to bind the received value (if any)
        var: Symbol,
        /// The pipe to receive from
        pipe: &'a Expr<'a>,
    },

    /// Cancel a spawned task.
    /// `Stop worker.`
    /// Semantics: handle.abort()
    StopTask {
        /// The handle to cancel
        handle: &'a Expr<'a>,
    },

    /// Select on multiple channels/timeouts.
    /// `Await the first of:`
    ///     `Receive x from ch:`
    ///         `...`
    ///     `After 5 seconds:`
    ///         `...`
    /// Semantics: tokio::select! with auto-cancel
    Select {
        /// The branches to select from
        branches: Vec<SelectBranch<'a>>,
    },

    /// Theorem block.
    /// `## Theorem: Name`
    /// `Given: Premise.`
    /// `Prove: Goal.`
    /// `Proof: Auto.`
    Theorem(TheoremBlock<'a>),

    /// `## Define` block — a vernacular-logic predicate definition (Rung 0a).
    /// `x is a bachelor if and only if x is unmarried and x is a man.`
    /// Non-executable: like [`Stmt::Theorem`], it is a declaration the proof
    /// layer consumes, not code the VM/AOT runs.
    Definition(DefinitionBlock<'a>),

    /// `## Axiom` block — a named first-order axiom in formal notation. Registers a
    /// shared premise for later theorems (the seam for an axiomatic base like Tarski).
    Axiom(AxiomBlock),

    /// `## Theory` block — a named development grouping formal axioms and theorems.
    Theory(TheoryBlock),

    /// Escape hatch: embed raw foreign code.
    /// `Escape to Rust:` followed by an indented block of raw code.
    ///
    /// Variables from the enclosing LOGOS scope are available in the
    /// escape block as their generated Rust types. The raw code is
    /// emitted verbatim inside a `{ ... }` block in the generated Rust.
    Escape {
        /// Target language ("Rust" for now, forward-compatible with "Python", "WGSL", etc.)
        language: Symbol,
        /// Raw foreign code, captured verbatim with base indentation stripped.
        code: Symbol,
        /// Source span covering the entire escape block (header + body).
        span: crate::token::Span,
    },

    /// Dependency declaration from `## Requires` block.
    /// The "serde" crate version "1.0" with features "derive".
    Require {
        crate_name: Symbol,
        version: Symbol,
        features: Vec<Symbol>,
        span: crate::token::Span,
    },
}

/// A branch in a Select statement.
#[derive(Debug, Clone)]
pub enum SelectBranch<'a> {
    /// Receive from a pipe: `Receive x from ch:`
    Receive {
        var: Symbol,
        pipe: &'a Expr<'a>,
        body: Block<'a>,
    },
    /// Timeout: `After N seconds:` or `After N milliseconds:`
    Timeout {
        milliseconds: &'a Expr<'a>,
        body: Block<'a>,
    },
}

/// Shared expression type for pure computations (LOGOS §15.0.0).
///
/// Expr is used by both LogicExpr (as terms) and Stmt (as values).
/// These are pure computations without side effects.
#[derive(Debug)]
pub enum Expr<'a> {
    /// Literal value: 42, "hello", true, nothing
    Literal(Literal),

    /// Variable reference: x
    Identifier(Symbol),

    /// Binary operation: x plus y
    BinaryOp {
        op: BinaryOpKind,
        left: &'a Expr<'a>,
        right: &'a Expr<'a>,
    },

    /// Unary NOT: "not x" → `!x` (logical for Bool, bitwise for Int)
    Not {
        operand: &'a Expr<'a>,
    },

    /// Function call as expression: f(x, y)
    Call {
        function: Symbol,
        args: Vec<&'a Expr<'a>>,
    },

    /// Dynamic index access: `items at i` (1-indexed).
    Index {
        collection: &'a Expr<'a>,
        index: &'a Expr<'a>,
    },

    /// Dynamic slice access: `items 1 through mid` (1-indexed, inclusive).
    Slice {
        collection: &'a Expr<'a>,
        start: &'a Expr<'a>,
        end: &'a Expr<'a>,
    },

    /// Copy expression: `copy of slice` → slice.to_vec().
    Copy {
        expr: &'a Expr<'a>,
    },

    /// Give expression: `Give x` → transfers ownership, no clone needed.
    /// Used in function calls to explicitly move values.
    Give {
        value: &'a Expr<'a>,
    },

    /// Length expression: `length of items` → items.len().
    Length {
        collection: &'a Expr<'a>,
    },

    /// Set contains: `set contains x` or `x in set`
    Contains {
        collection: &'a Expr<'a>,
        value: &'a Expr<'a>,
    },

    /// Set union: `a union b`
    Union {
        left: &'a Expr<'a>,
        right: &'a Expr<'a>,
    },

    /// Set intersection: `a intersection b`
    Intersection {
        left: &'a Expr<'a>,
        right: &'a Expr<'a>,
    },

    /// Get manifest of a zone.
    /// `the manifest of Zone` → FileSipper::from_zone(&zone).manifest()
    ManifestOf {
        zone: &'a Expr<'a>,
    },

    /// Get chunk at index from a zone.
    /// `the chunk at N in Zone` → FileSipper::from_zone(&zone).get_chunk(N)
    ChunkAt {
        index: &'a Expr<'a>,
        zone: &'a Expr<'a>,
    },

    /// List literal: [1, 2, 3]
    List(Vec<&'a Expr<'a>>),

    /// Tuple literal: (1, "hello", true)
    Tuple(Vec<&'a Expr<'a>>),

    /// Range: 1 to 10 (inclusive)
    Range {
        start: &'a Expr<'a>,
        end: &'a Expr<'a>,
    },

    /// Field access: `p's x` or `the x of p`.
    FieldAccess {
        object: &'a Expr<'a>,
        field: Symbol,
    },

    /// Constructor: `a new Point` or `a new Point with x 10 and y 20`.
    /// Supports generics: `a new Box of Int` and nested types: `a new Seq of (Seq of Int)`
    New {
        type_name: Symbol,
        type_args: Vec<TypeExpr<'a>>,  // Empty for non-generic types - now supports nested types
        init_fields: Vec<(Symbol, &'a Expr<'a>)>,  // Optional field initialization
    },

    /// Enum variant constructor: `a new Circle with radius 10`.
    NewVariant {
        enum_name: Symbol,                      // Shape (resolved from registry)
        variant: Symbol,                        // Circle
        fields: Vec<(Symbol, &'a Expr<'a>)>,    // [(radius, 10)]
    },

    /// Escape hatch expression: raw foreign code that produces a value.
    /// Used in expression position: `Let x: Int be Escape to Rust:`
    Escape {
        language: Symbol,
        code: Symbol,
    },

    /// Option Some: `some 30` → Some(30)
    OptionSome {
        value: &'a Expr<'a>,
    },

    /// Option None: `none` → None
    OptionNone,

    /// Pre-allocation capacity hint wrapping an inner value expression.
    /// `"" with capacity 100` or `a new Seq of Int with capacity n`
    /// Codegen uses with_capacity(); interpreter ignores the hint.
    WithCapacity {
        value: &'a Expr<'a>,
        capacity: &'a Expr<'a>,
    },

    /// Closure expression: `(params) -> body` or `(params) ->:` block body.
    /// Captures variables from the enclosing scope by value (snapshot/clone).
    Closure {
        params: Vec<(Symbol, &'a TypeExpr<'a>)>,
        body: ClosureBody<'a>,
        return_type: Option<&'a TypeExpr<'a>>,
    },

    /// Call an expression that evaluates to a callable value.
    /// `f(x)` where `f` is a variable holding a closure, not a named function.
    CallExpr {
        callee: &'a Expr<'a>,
        args: Vec<&'a Expr<'a>>,
    },

    /// Interpolated string: `"Hello, {name}! Value: {x:.2}"`
    InterpolatedString(Vec<StringPart<'a>>),
}

/// A segment of an interpolated string.
#[derive(Debug, Clone)]
pub enum StringPart<'a> {
    /// Literal text segment
    Literal(Symbol),
    /// Expression with optional format specifier
    Expr {
        value: &'a Expr<'a>,
        format_spec: Option<Symbol>,
        /// Self-documenting debug format: `{var=}` → `"var=42"`
        debug: bool,
    },
}

/// Body of a closure expression.
#[derive(Debug, Clone)]
pub enum ClosureBody<'a> {
    /// Single expression: `(n: Int) -> n * 2`
    Expression(&'a Expr<'a>),
    /// Block of statements: `(n: Int) ->:` followed by indented body
    Block(Block<'a>),
}

/// Literal values in LOGOS.
#[derive(Debug, Clone)]
pub enum Literal {
    /// Integer literal
    Number(i64),
    /// Float literal
    Float(f64),
    /// Text literal
    Text(Symbol),
    /// Boolean literal
    Boolean(bool),
    /// The nothing literal (unit type)
    Nothing,
    /// Character literal
    Char(char),
    /// Duration literal (nanoseconds, signed for negative offsets like "5 minutes early")
    Duration(i64),
    /// Date literal (days since Unix epoch 1970-01-01)
    Date(i32),
    /// Moment literal (nanoseconds since Unix epoch)
    Moment(i64),
    /// Calendar span (months, days) - NOT flattened to seconds
    /// Months and days are kept separate because they're incommensurable.
    Span { months: i32, days: i32 },
    /// Time-of-day literal (nanoseconds from midnight)
    /// Range: 0 to 86_399_999_999_999 (just under 24 hours)
    Time(i64),
}

impl PartialEq for Literal {
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (Literal::Number(a), Literal::Number(b)) => a == b,
            (Literal::Float(a), Literal::Float(b)) => a.to_bits() == b.to_bits(),
            (Literal::Text(a), Literal::Text(b)) => a == b,
            (Literal::Boolean(a), Literal::Boolean(b)) => a == b,
            (Literal::Nothing, Literal::Nothing) => true,
            (Literal::Char(a), Literal::Char(b)) => a == b,
            (Literal::Duration(a), Literal::Duration(b)) => a == b,
            (Literal::Date(a), Literal::Date(b)) => a == b,
            (Literal::Moment(a), Literal::Moment(b)) => a == b,
            (Literal::Span { months: m1, days: d1 }, Literal::Span { months: m2, days: d2 }) => m1 == m2 && d1 == d2,
            (Literal::Time(a), Literal::Time(b)) => a == b,
            _ => false,
        }
    }
}

impl Eq for Literal {}

impl std::hash::Hash for Literal {
    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
        std::mem::discriminant(self).hash(state);
        match self {
            Literal::Number(n) => n.hash(state),
            Literal::Float(f) => f.to_bits().hash(state),
            Literal::Text(s) => s.hash(state),
            Literal::Boolean(b) => b.hash(state),
            Literal::Nothing => {}
            Literal::Char(c) => c.hash(state),
            Literal::Duration(d) => d.hash(state),
            Literal::Date(d) => d.hash(state),
            Literal::Moment(m) => m.hash(state),
            Literal::Span { months, days } => {
                months.hash(state);
                days.hash(state);
            }
            Literal::Time(t) => t.hash(state),
        }
    }
}