logicaffeine_language/ast/

stmt.rs

//! 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::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>,
    },
}

/// 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)]
pub enum BinaryOpKind {
    Add,
    Subtract,
    Multiply,
    Divide,
    Modulo,
    Eq,
    NotEq,
    Lt,
    Gt,
    LtEq,
    GtEq,
    // Logical operators for compound conditions
    And,
    Or,
    /// String concatenation ("X combined with Y")
    Concat,
}

/// 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>,
}

/// 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.
#[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>>,
    },

    /// 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.` (for imperative mode)
    RuntimeAssert {
        condition: &'a Expr<'a>,
    },

    /// 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,
        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>,
    },

    /// 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>,
    },

    /// 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 file path for memory-mapped zones (Mapped zones only)
        source_file: Option<Symbol>,
        /// 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".`
    SendMessage {
        message: &'a Expr<'a>,
        destination: &'a Expr<'a>,
    },

    /// Await response from agent.
    /// `Await response from "agent" into result.`
    AwaitMessage {
        source: &'a Expr<'a>,
        into: Symbol,
    },

    /// 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>,
    },

    /// Connect to remote peer.
    /// `Connect to "/ip4/127.0.0.1/tcp/8000".`
    /// Semantics: Dial peer via libp2p
    ConnectTo {
        address: &'a Expr<'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>),

    /// 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>,
    },

    /// 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>>,
    },
}

/// 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, PartialEq)]
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),
}