logicaffeine_language/ast/
stmt.rs

1//! Imperative statement AST types for the LOGOS language.
2//!
3//! This module defines statement types for the imperative fragment including:
4//!
5//! - **[`Stmt`]**: Statement variants (let, if, match, while, for, function defs)
6//! - **[`Expr`]**: Imperative expressions (field access, method calls, literals)
7//! - **[`TypeExpr`]**: Type annotations with refinements and generics
8//! - **[`Literal`]**: Literal values (numbers, strings, booleans)
9//! - **[`Block`]**: Statement blocks with optional return expressions
10//!
11//! The imperative AST is used in LOGOS mode for generating executable Rust code.
12
13use super::logic::LogicExpr;
14use super::theorem::TheoremBlock;
15use logicaffeine_base::Symbol;
16
17/// Type expression for explicit type annotations.
18///
19/// Represents type syntax like:
20/// - `Int` → Primitive(Int)
21/// - `User` → Named(User)
22/// - `List of Int` → Generic { base: List, params: [Primitive(Int)] }
23/// - `List of List of Int` → Generic { base: List, params: [Generic { base: List, params: [Primitive(Int)] }] }
24/// - `Result of Int and Text` → Generic { base: Result, params: [Primitive(Int), Primitive(Text)] }
25#[derive(Debug, Clone)]
26pub enum TypeExpr<'a> {
27    /// Primitive type: Int, Nat, Text, Bool
28    Primitive(Symbol),
29    /// Named type (user-defined): User, Point
30    Named(Symbol),
31    /// Generic type: List of Int, Option of Text, Result of Int and Text
32    Generic {
33        base: Symbol,
34        params: &'a [TypeExpr<'a>],
35    },
36    /// Function type: fn(A, B) -> C (for higher-order functions)
37    Function {
38        inputs: &'a [TypeExpr<'a>],
39        output: &'a TypeExpr<'a>,
40    },
41    /// Refinement type with predicate constraint.
42    /// Example: `Int where it > 0`
43    Refinement {
44        /// The base type being refined
45        base: &'a TypeExpr<'a>,
46        /// The bound variable (usually "it")
47        var: Symbol,
48        /// The predicate constraint (from Logic Kernel)
49        predicate: &'a LogicExpr<'a>,
50    },
51    /// Persistent storage wrapper type.
52    /// Example: `Persistent Counter`
53    /// Semantics: Wraps a Shared type with journal-backed storage
54    Persistent {
55        /// The inner type (must be a Shared/CRDT type)
56        inner: &'a TypeExpr<'a>,
57    },
58}
59
60/// Source for Read statements.
61#[derive(Debug, Clone, Copy)]
62pub enum ReadSource<'a> {
63    /// Read from console (stdin)
64    Console,
65    /// Read from file at given path
66    File(&'a Expr<'a>),
67}
68
69/// Binary operation kinds for imperative expressions.
70#[derive(Debug, Clone, Copy, PartialEq, Eq)]
71pub enum BinaryOpKind {
72    Add,
73    Subtract,
74    Multiply,
75    Divide,
76    Modulo,
77    Eq,
78    NotEq,
79    Lt,
80    Gt,
81    LtEq,
82    GtEq,
83    // Logical operators for compound conditions
84    And,
85    Or,
86    /// String concatenation ("X combined with Y")
87    Concat,
88}
89
90/// Block is a sequence of statements.
91pub type Block<'a> = &'a [Stmt<'a>];
92
93/// Match arm for pattern matching in Inspect statements.
94#[derive(Debug)]
95pub struct MatchArm<'a> {
96    pub enum_name: Option<Symbol>,          // The enum type (e.g., Shape)
97    pub variant: Option<Symbol>,            // None = Otherwise (wildcard)
98    pub bindings: Vec<(Symbol, Symbol)>,    // (field_name, binding_name)
99    pub body: Block<'a>,
100}
101
102/// Imperative statement AST (LOGOS §15.0.0).
103///
104/// Stmt is the primary AST node for imperative code blocks like `## Main`
105/// and function bodies. The Assert variant bridges to the Logic Kernel.
106#[derive(Debug)]
107pub enum Stmt<'a> {
108    /// Variable binding: `Let x be 5.` or `Let x: Int be 5.`
109    Let {
110        var: Symbol,
111        ty: Option<&'a TypeExpr<'a>>,
112        value: &'a Expr<'a>,
113        mutable: bool,
114    },
115
116    /// Mutation: `Set x to 10.`
117    Set {
118        target: Symbol,
119        value: &'a Expr<'a>,
120    },
121
122    /// Function call as statement: `Call process with data.`
123    Call {
124        function: Symbol,
125        args: Vec<&'a Expr<'a>>,
126    },
127
128    /// Conditional: `If condition: ... Otherwise: ...`
129    If {
130        cond: &'a Expr<'a>,
131        then_block: Block<'a>,
132        else_block: Option<Block<'a>>,
133    },
134
135    /// Loop: `While condition: ...` or `While condition (decreasing expr): ...`
136    While {
137        cond: &'a Expr<'a>,
138        body: Block<'a>,
139        /// Optional decreasing variant for termination proof.
140        decreasing: Option<&'a Expr<'a>>,
141    },
142
143    /// Iteration: `Repeat for x in list: ...` or `Repeat for i from 1 to 10: ...`
144    Repeat {
145        var: Symbol,
146        iterable: &'a Expr<'a>,
147        body: Block<'a>,
148    },
149
150    /// Return: `Return x.` or `Return.`
151    Return {
152        value: Option<&'a Expr<'a>>,
153    },
154
155    /// Bridge to Logic Kernel: `Assert that P.`
156    Assert {
157        proposition: &'a LogicExpr<'a>,
158    },
159
160    /// Documented assertion with justification.
161    /// `Trust that P because "reason".`
162    /// Semantics: Documented runtime check that could be verified statically.
163    Trust {
164        proposition: &'a LogicExpr<'a>,
165        justification: Symbol,
166    },
167
168    /// Runtime assertion with imperative condition
169    /// `Assert that condition.` (for imperative mode)
170    RuntimeAssert {
171        condition: &'a Expr<'a>,
172    },
173
174    /// Ownership transfer (move): `Give x to processor.`
175    /// Semantics: Move ownership of `object` to `recipient`.
176    Give {
177        object: &'a Expr<'a>,
178        recipient: &'a Expr<'a>,
179    },
180
181    /// Immutable borrow: `Show x to console.`
182    /// Semantics: Immutable borrow of `object` passed to `recipient`.
183    Show {
184        object: &'a Expr<'a>,
185        recipient: &'a Expr<'a>,
186    },
187
188    /// Field mutation: `Set p's x to 10.`
189    SetField {
190        object: &'a Expr<'a>,
191        field: Symbol,
192        value: &'a Expr<'a>,
193    },
194
195    /// Struct definition for codegen.
196    StructDef {
197        name: Symbol,
198        fields: Vec<(Symbol, Symbol, bool)>, // (name, type_name, is_public)
199        is_portable: bool,                    // Derives Serialize/Deserialize
200    },
201
202    /// Function definition.
203    FunctionDef {
204        name: Symbol,
205        params: Vec<(Symbol, &'a TypeExpr<'a>)>,
206        body: Block<'a>,
207        return_type: Option<&'a TypeExpr<'a>>,
208        is_native: bool,
209    },
210
211    /// Pattern matching on sum types.
212    Inspect {
213        target: &'a Expr<'a>,
214        arms: Vec<MatchArm<'a>>,
215        has_otherwise: bool,            // For exhaustiveness tracking
216    },
217
218    /// Push to collection: `Push x to items.`
219    Push {
220        value: &'a Expr<'a>,
221        collection: &'a Expr<'a>,
222    },
223
224    /// Pop from collection: `Pop from items.` or `Pop from items into y.`
225    Pop {
226        collection: &'a Expr<'a>,
227        into: Option<Symbol>,
228    },
229
230    /// Add to set: `Add x to set.`
231    Add {
232        value: &'a Expr<'a>,
233        collection: &'a Expr<'a>,
234    },
235
236    /// Remove from set: `Remove x from set.`
237    Remove {
238        value: &'a Expr<'a>,
239        collection: &'a Expr<'a>,
240    },
241
242    /// Index assignment: `Set item N of X to Y.`
243    SetIndex {
244        collection: &'a Expr<'a>,
245        index: &'a Expr<'a>,
246        value: &'a Expr<'a>,
247    },
248
249    /// Memory arena block (Zone).
250    /// "Inside a new zone called 'Scratch':"
251    /// "Inside a zone called 'Buffer' of size 1 MB:"
252    /// "Inside a zone called 'Data' mapped from 'file.bin':"
253    Zone {
254        /// The variable name for the arena handle (e.g., "Scratch")
255        name: Symbol,
256        /// Optional pre-allocated capacity in bytes (Heap zones only)
257        capacity: Option<usize>,
258        /// Optional file path for memory-mapped zones (Mapped zones only)
259        source_file: Option<Symbol>,
260        /// The code block executed within this memory context
261        body: Block<'a>,
262    },
263
264    /// Concurrent execution block (async, I/O-bound).
265    /// "Attempt all of the following:"
266    /// Semantics: All tasks run concurrently via tokio::join!
267    /// Best for: network requests, file I/O, waiting operations
268    Concurrent {
269        /// The statements to execute concurrently
270        tasks: Block<'a>,
271    },
272
273    /// Parallel execution block (CPU-bound).
274    /// "Simultaneously:"
275    /// Semantics: True parallelism via rayon::join or thread::spawn
276    /// Best for: computation, data processing, number crunching
277    Parallel {
278        /// The statements to execute in parallel
279        tasks: Block<'a>,
280    },
281
282    /// Read from console or file.
283    /// `Read input from the console.` or `Read data from file "path.txt".`
284    ReadFrom {
285        var: Symbol,
286        source: ReadSource<'a>,
287    },
288
289    /// Write to file.
290    /// `Write "content" to file "output.txt".`
291    WriteFile {
292        content: &'a Expr<'a>,
293        path: &'a Expr<'a>,
294    },
295
296    /// Spawn an agent.
297    /// `Spawn a Worker called "w1".`
298    Spawn {
299        agent_type: Symbol,
300        name: Symbol,
301    },
302
303    /// Send message to agent.
304    /// `Send Ping to "agent".`
305    SendMessage {
306        message: &'a Expr<'a>,
307        destination: &'a Expr<'a>,
308    },
309
310    /// Await response from agent.
311    /// `Await response from "agent" into result.`
312    AwaitMessage {
313        source: &'a Expr<'a>,
314        into: Symbol,
315    },
316
317    /// Merge CRDT state.
318    /// `Merge remote into local.` or `Merge remote's field into local's field.`
319    MergeCrdt {
320        source: &'a Expr<'a>,
321        target: &'a Expr<'a>,
322    },
323
324    /// Increment GCounter.
325    /// `Increase local's points by 10.`
326    IncreaseCrdt {
327        object: &'a Expr<'a>,
328        field: Symbol,
329        amount: &'a Expr<'a>,
330    },
331
332    /// Decrement PNCounter (Tally).
333    /// `Decrease game's score by 5.`
334    DecreaseCrdt {
335        object: &'a Expr<'a>,
336        field: Symbol,
337        amount: &'a Expr<'a>,
338    },
339
340    /// Append to SharedSequence (RGA).
341    /// `Append "Hello" to doc's lines.`
342    AppendToSequence {
343        sequence: &'a Expr<'a>,
344        value: &'a Expr<'a>,
345    },
346
347    /// Resolve MVRegister conflicts.
348    /// `Resolve page's title to "Final".`
349    ResolveConflict {
350        object: &'a Expr<'a>,
351        field: Symbol,
352        value: &'a Expr<'a>,
353    },
354
355    /// Security check - mandatory runtime guard.
356    /// `Check that user is admin.`
357    /// `Check that user can publish the document.`
358    /// Semantics: NEVER optimized out. Panics if condition is false.
359    Check {
360        /// The subject being checked (e.g., "user")
361        subject: Symbol,
362        /// The predicate name (e.g., "admin") or action (e.g., "publish")
363        predicate: Symbol,
364        /// True if this is a capability check (`can [action]`)
365        is_capability: bool,
366        /// For capabilities: the object being acted on (e.g., "document")
367        object: Option<Symbol>,
368        /// Original English text for error message
369        source_text: String,
370        /// Source location for error reporting
371        span: crate::token::Span,
372    },
373
374    /// Listen on network address.
375    /// `Listen on "/ip4/127.0.0.1/tcp/8000".`
376    /// Semantics: Bind to address, start accepting connections via libp2p
377    Listen {
378        address: &'a Expr<'a>,
379    },
380
381    /// Connect to remote peer.
382    /// `Connect to "/ip4/127.0.0.1/tcp/8000".`
383    /// Semantics: Dial peer via libp2p
384    ConnectTo {
385        address: &'a Expr<'a>,
386    },
387
388    /// Create PeerAgent remote handle.
389    /// `Let remote be a PeerAgent at "/ip4/127.0.0.1/tcp/8000".`
390    /// Semantics: Create handle for remote agent communication
391    LetPeerAgent {
392        var: Symbol,
393        address: &'a Expr<'a>,
394    },
395
396    /// Sleep for milliseconds.
397    /// `Sleep 1000.` or `Sleep delay.`
398    /// Semantics: Pause execution for N milliseconds (async)
399    Sleep {
400        milliseconds: &'a Expr<'a>,
401    },
402
403    /// Sync CRDT variable on topic.
404    /// `Sync x on "topic".`
405    /// Semantics: Subscribe to GossipSub topic, auto-publish on mutation, auto-merge on receive
406    Sync {
407        var: Symbol,
408        topic: &'a Expr<'a>,
409    },
410
411    /// Mount persistent CRDT from journal file.
412    /// `Mount counter at "data/counter.journal".`
413    /// Semantics: Load or create journal, replay operations to reconstruct state
414    Mount {
415        /// The variable name for the mounted value
416        var: Symbol,
417        /// The path expression for the journal file
418        path: &'a Expr<'a>,
419    },
420
421    // =========================================================================
422    // Go-like Concurrency (Green Threads, Channels, Select)
423    // =========================================================================
424
425    /// Launch a fire-and-forget task (green thread).
426    /// `Launch a task to process(data).`
427    /// Semantics: tokio::spawn with no handle capture
428    LaunchTask {
429        /// The function to call
430        function: Symbol,
431        /// Arguments to pass
432        args: Vec<&'a Expr<'a>>,
433    },
434
435    /// Launch a task with handle for control.
436    /// `Let worker be Launch a task to process(data).`
437    /// Semantics: tokio::spawn returning JoinHandle
438    LaunchTaskWithHandle {
439        /// Variable to bind the handle
440        handle: Symbol,
441        /// The function to call
442        function: Symbol,
443        /// Arguments to pass
444        args: Vec<&'a Expr<'a>>,
445    },
446
447    /// Create a bounded channel (pipe).
448    /// `Let jobs be a new Pipe of Int.`
449    /// Semantics: tokio::sync::mpsc::channel(32)
450    CreatePipe {
451        /// Variable for the pipe
452        var: Symbol,
453        /// Type of values in the pipe
454        element_type: Symbol,
455        /// Optional capacity (defaults to 32)
456        capacity: Option<u32>,
457    },
458
459    /// Blocking send into pipe.
460    /// `Send value into pipe.`
461    /// Semantics: pipe_tx.send(value).await
462    SendPipe {
463        /// The value to send
464        value: &'a Expr<'a>,
465        /// The pipe to send into
466        pipe: &'a Expr<'a>,
467    },
468
469    /// Blocking receive from pipe.
470    /// `Receive x from pipe.`
471    /// Semantics: let x = pipe_rx.recv().await
472    ReceivePipe {
473        /// Variable to bind the received value
474        var: Symbol,
475        /// The pipe to receive from
476        pipe: &'a Expr<'a>,
477    },
478
479    /// Non-blocking send (try).
480    /// `Try to send value into pipe.`
481    /// Semantics: pipe_tx.try_send(value) - returns immediately
482    TrySendPipe {
483        /// The value to send
484        value: &'a Expr<'a>,
485        /// The pipe to send into
486        pipe: &'a Expr<'a>,
487        /// Variable to bind the result (true/false)
488        result: Option<Symbol>,
489    },
490
491    /// Non-blocking receive (try).
492    /// `Try to receive x from pipe.`
493    /// Semantics: pipe_rx.try_recv() - returns Option
494    TryReceivePipe {
495        /// Variable to bind the received value (if any)
496        var: Symbol,
497        /// The pipe to receive from
498        pipe: &'a Expr<'a>,
499    },
500
501    /// Cancel a spawned task.
502    /// `Stop worker.`
503    /// Semantics: handle.abort()
504    StopTask {
505        /// The handle to cancel
506        handle: &'a Expr<'a>,
507    },
508
509    /// Select on multiple channels/timeouts.
510    /// `Await the first of:`
511    ///     `Receive x from ch:`
512    ///         `...`
513    ///     `After 5 seconds:`
514    ///         `...`
515    /// Semantics: tokio::select! with auto-cancel
516    Select {
517        /// The branches to select from
518        branches: Vec<SelectBranch<'a>>,
519    },
520
521    /// Theorem block.
522    /// `## Theorem: Name`
523    /// `Given: Premise.`
524    /// `Prove: Goal.`
525    /// `Proof: Auto.`
526    Theorem(TheoremBlock<'a>),
527}
528
529/// A branch in a Select statement.
530#[derive(Debug)]
531pub enum SelectBranch<'a> {
532    /// Receive from a pipe: `Receive x from ch:`
533    Receive {
534        var: Symbol,
535        pipe: &'a Expr<'a>,
536        body: Block<'a>,
537    },
538    /// Timeout: `After N seconds:` or `After N milliseconds:`
539    Timeout {
540        milliseconds: &'a Expr<'a>,
541        body: Block<'a>,
542    },
543}
544
545/// Shared expression type for pure computations (LOGOS §15.0.0).
546///
547/// Expr is used by both LogicExpr (as terms) and Stmt (as values).
548/// These are pure computations without side effects.
549#[derive(Debug)]
550pub enum Expr<'a> {
551    /// Literal value: 42, "hello", true, nothing
552    Literal(Literal),
553
554    /// Variable reference: x
555    Identifier(Symbol),
556
557    /// Binary operation: x plus y
558    BinaryOp {
559        op: BinaryOpKind,
560        left: &'a Expr<'a>,
561        right: &'a Expr<'a>,
562    },
563
564    /// Function call as expression: f(x, y)
565    Call {
566        function: Symbol,
567        args: Vec<&'a Expr<'a>>,
568    },
569
570    /// Dynamic index access: `items at i` (1-indexed).
571    Index {
572        collection: &'a Expr<'a>,
573        index: &'a Expr<'a>,
574    },
575
576    /// Dynamic slice access: `items 1 through mid` (1-indexed, inclusive).
577    Slice {
578        collection: &'a Expr<'a>,
579        start: &'a Expr<'a>,
580        end: &'a Expr<'a>,
581    },
582
583    /// Copy expression: `copy of slice` → slice.to_vec().
584    Copy {
585        expr: &'a Expr<'a>,
586    },
587
588    /// Length expression: `length of items` → items.len().
589    Length {
590        collection: &'a Expr<'a>,
591    },
592
593    /// Set contains: `set contains x` or `x in set`
594    Contains {
595        collection: &'a Expr<'a>,
596        value: &'a Expr<'a>,
597    },
598
599    /// Set union: `a union b`
600    Union {
601        left: &'a Expr<'a>,
602        right: &'a Expr<'a>,
603    },
604
605    /// Set intersection: `a intersection b`
606    Intersection {
607        left: &'a Expr<'a>,
608        right: &'a Expr<'a>,
609    },
610
611    /// Get manifest of a zone.
612    /// `the manifest of Zone` → FileSipper::from_zone(&zone).manifest()
613    ManifestOf {
614        zone: &'a Expr<'a>,
615    },
616
617    /// Get chunk at index from a zone.
618    /// `the chunk at N in Zone` → FileSipper::from_zone(&zone).get_chunk(N)
619    ChunkAt {
620        index: &'a Expr<'a>,
621        zone: &'a Expr<'a>,
622    },
623
624    /// List literal: [1, 2, 3]
625    List(Vec<&'a Expr<'a>>),
626
627    /// Tuple literal: (1, "hello", true)
628    Tuple(Vec<&'a Expr<'a>>),
629
630    /// Range: 1 to 10 (inclusive)
631    Range {
632        start: &'a Expr<'a>,
633        end: &'a Expr<'a>,
634    },
635
636    /// Field access: `p's x` or `the x of p`.
637    FieldAccess {
638        object: &'a Expr<'a>,
639        field: Symbol,
640    },
641
642    /// Constructor: `a new Point` or `a new Point with x 10 and y 20`.
643    /// Supports generics: `a new Box of Int`
644    New {
645        type_name: Symbol,
646        type_args: Vec<Symbol>,  // Empty for non-generic types
647        init_fields: Vec<(Symbol, &'a Expr<'a>)>,  // Optional field initialization
648    },
649
650    /// Enum variant constructor: `a new Circle with radius 10`.
651    NewVariant {
652        enum_name: Symbol,                      // Shape (resolved from registry)
653        variant: Symbol,                        // Circle
654        fields: Vec<(Symbol, &'a Expr<'a>)>,    // [(radius, 10)]
655    },
656}
657
658/// Literal values in LOGOS.
659#[derive(Debug, Clone, PartialEq)]
660pub enum Literal {
661    /// Integer literal
662    Number(i64),
663    /// Float literal
664    Float(f64),
665    /// Text literal
666    Text(Symbol),
667    /// Boolean literal
668    Boolean(bool),
669    /// The nothing literal (unit type)
670    Nothing,
671    /// Character literal
672    Char(char),
673}
logicaffeine_language/ast/stmt.rs

logicaffeine_language/ast/
stmt.rs
