pub enum Stmt<'a> {
Show 51 variants
Let {
var: Symbol,
ty: Option<&'a TypeExpr<'a>>,
value: &'a Expr<'a>,
mutable: bool,
},
Set {
target: Symbol,
value: &'a Expr<'a>,
},
Call {
function: Symbol,
args: Vec<&'a Expr<'a>>,
},
If {
cond: &'a Expr<'a>,
then_block: Block<'a>,
else_block: Option<Block<'a>>,
},
While {
cond: &'a Expr<'a>,
body: Block<'a>,
decreasing: Option<&'a Expr<'a>>,
},
Repeat {
var: Symbol,
iterable: &'a Expr<'a>,
body: Block<'a>,
},
Return {
value: Option<&'a Expr<'a>>,
},
Assert {
proposition: &'a LogicExpr<'a>,
},
Trust {
proposition: &'a LogicExpr<'a>,
justification: Symbol,
},
RuntimeAssert {
condition: &'a Expr<'a>,
},
Give {
object: &'a Expr<'a>,
recipient: &'a Expr<'a>,
},
Show {
object: &'a Expr<'a>,
recipient: &'a Expr<'a>,
},
SetField {
object: &'a Expr<'a>,
field: Symbol,
value: &'a Expr<'a>,
},
StructDef {
name: Symbol,
fields: Vec<(Symbol, Symbol, bool)>,
is_portable: bool,
},
FunctionDef {
name: Symbol,
params: Vec<(Symbol, &'a TypeExpr<'a>)>,
body: Block<'a>,
return_type: Option<&'a TypeExpr<'a>>,
is_native: bool,
},
Inspect {
target: &'a Expr<'a>,
arms: Vec<MatchArm<'a>>,
has_otherwise: bool,
},
Push {
value: &'a Expr<'a>,
collection: &'a Expr<'a>,
},
Pop {
collection: &'a Expr<'a>,
into: Option<Symbol>,
},
Add {
value: &'a Expr<'a>,
collection: &'a Expr<'a>,
},
Remove {
value: &'a Expr<'a>,
collection: &'a Expr<'a>,
},
SetIndex {
collection: &'a Expr<'a>,
index: &'a Expr<'a>,
value: &'a Expr<'a>,
},
Zone {
name: Symbol,
capacity: Option<usize>,
source_file: Option<Symbol>,
body: Block<'a>,
},
Concurrent {
tasks: Block<'a>,
},
Parallel {
tasks: Block<'a>,
},
ReadFrom {
var: Symbol,
source: ReadSource<'a>,
},
WriteFile {
content: &'a Expr<'a>,
path: &'a Expr<'a>,
},
Spawn {
agent_type: Symbol,
name: Symbol,
},
SendMessage {
message: &'a Expr<'a>,
destination: &'a Expr<'a>,
},
AwaitMessage {
source: &'a Expr<'a>,
into: Symbol,
},
MergeCrdt {
source: &'a Expr<'a>,
target: &'a Expr<'a>,
},
IncreaseCrdt {
object: &'a Expr<'a>,
field: Symbol,
amount: &'a Expr<'a>,
},
DecreaseCrdt {
object: &'a Expr<'a>,
field: Symbol,
amount: &'a Expr<'a>,
},
AppendToSequence {
sequence: &'a Expr<'a>,
value: &'a Expr<'a>,
},
ResolveConflict {
object: &'a Expr<'a>,
field: Symbol,
value: &'a Expr<'a>,
},
Check {
subject: Symbol,
predicate: Symbol,
is_capability: bool,
object: Option<Symbol>,
source_text: String,
span: Span,
},
Listen {
address: &'a Expr<'a>,
},
ConnectTo {
address: &'a Expr<'a>,
},
LetPeerAgent {
var: Symbol,
address: &'a Expr<'a>,
},
Sleep {
milliseconds: &'a Expr<'a>,
},
Sync {
var: Symbol,
topic: &'a Expr<'a>,
},
Mount {
var: Symbol,
path: &'a Expr<'a>,
},
LaunchTask {
function: Symbol,
args: Vec<&'a Expr<'a>>,
},
LaunchTaskWithHandle {
handle: Symbol,
function: Symbol,
args: Vec<&'a Expr<'a>>,
},
CreatePipe {
var: Symbol,
element_type: Symbol,
capacity: Option<u32>,
},
SendPipe {
value: &'a Expr<'a>,
pipe: &'a Expr<'a>,
},
ReceivePipe {
var: Symbol,
pipe: &'a Expr<'a>,
},
TrySendPipe {
value: &'a Expr<'a>,
pipe: &'a Expr<'a>,
result: Option<Symbol>,
},
TryReceivePipe {
var: Symbol,
pipe: &'a Expr<'a>,
},
StopTask {
handle: &'a Expr<'a>,
},
Select {
branches: Vec<SelectBranch<'a>>,
},
Theorem(TheoremBlock<'a>),
}Expand description
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.
Variants§
Let
Variable binding: Let x be 5. or Let x: Int be 5.
Set
Mutation: Set x to 10.
Call
Function call as statement: Call process with data.
If
Conditional: If condition: ... Otherwise: ...
While
Loop: While condition: ... or While condition (decreasing expr): ...
Fields
Repeat
Iteration: Repeat for x in list: ... or Repeat for i from 1 to 10: ...
Return
Return: Return x. or Return.
Assert
Bridge to Logic Kernel: Assert that P.
Trust
Documented assertion with justification.
Trust that P because "reason".
Semantics: Documented runtime check that could be verified statically.
RuntimeAssert
Runtime assertion with imperative condition
Assert that condition. (for imperative mode)
Give
Ownership transfer (move): Give x to processor.
Semantics: Move ownership of object to recipient.
Show
Immutable borrow: Show x to console.
Semantics: Immutable borrow of object passed to recipient.
SetField
Field mutation: Set p's x to 10.
StructDef
Struct definition for codegen.
FunctionDef
Function definition.
Fields
Inspect
Pattern matching on sum types.
Push
Push to collection: Push x to items.
Pop
Pop from collection: Pop from items. or Pop from items into y.
Add
Add to set: Add x to set.
Remove
Remove from set: Remove x from set.
SetIndex
Index assignment: Set item N of X to Y.
Zone
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’:”
Fields
Concurrent
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
Parallel
Parallel execution block (CPU-bound). “Simultaneously:” Semantics: True parallelism via rayon::join or thread::spawn Best for: computation, data processing, number crunching
ReadFrom
Read from console or file.
Read input from the console. or Read data from file "path.txt".
WriteFile
Write to file.
Write "content" to file "output.txt".
Spawn
Spawn an agent.
Spawn a Worker called "w1".
SendMessage
Send message to agent.
Send Ping to "agent".
AwaitMessage
Await response from agent.
Await response from "agent" into result.
MergeCrdt
Merge CRDT state.
Merge remote into local. or Merge remote's field into local's field.
IncreaseCrdt
Increment GCounter.
Increase local's points by 10.
DecreaseCrdt
Decrement PNCounter (Tally).
Decrease game's score by 5.
AppendToSequence
Append to SharedSequence (RGA).
Append "Hello" to doc's lines.
ResolveConflict
Resolve MVRegister conflicts.
Resolve page's title to "Final".
Check
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.
Fields
Listen
Listen on network address.
Listen on "/ip4/127.0.0.1/tcp/8000".
Semantics: Bind to address, start accepting connections via libp2p
ConnectTo
Connect to remote peer.
Connect to "/ip4/127.0.0.1/tcp/8000".
Semantics: Dial peer via libp2p
LetPeerAgent
Create PeerAgent remote handle.
Let remote be a PeerAgent at "/ip4/127.0.0.1/tcp/8000".
Semantics: Create handle for remote agent communication
Sleep
Sleep for milliseconds.
Sleep 1000. or Sleep delay.
Semantics: Pause execution for N milliseconds (async)
Sync
Sync CRDT variable on topic.
Sync x on "topic".
Semantics: Subscribe to GossipSub topic, auto-publish on mutation, auto-merge on receive
Mount
Mount persistent CRDT from journal file.
Mount counter at "data/counter.journal".
Semantics: Load or create journal, replay operations to reconstruct state
Fields
LaunchTask
Launch a fire-and-forget task (green thread).
Launch a task to process(data).
Semantics: tokio::spawn with no handle capture
LaunchTaskWithHandle
Launch a task with handle for control.
Let worker be Launch a task to process(data).
Semantics: tokio::spawn returning JoinHandle
Fields
CreatePipe
Create a bounded channel (pipe).
Let jobs be a new Pipe of Int.
Semantics: tokio::sync::mpsc::channel(32)
Fields
SendPipe
Blocking send into pipe.
Send value into pipe.
Semantics: pipe_tx.send(value).await
ReceivePipe
Blocking receive from pipe.
Receive x from pipe.
Semantics: let x = pipe_rx.recv().await
TrySendPipe
Non-blocking send (try).
Try to send value into pipe.
Semantics: pipe_tx.try_send(value) - returns immediately
Fields
TryReceivePipe
Non-blocking receive (try).
Try to receive x from pipe.
Semantics: pipe_rx.try_recv() - returns Option
Fields
StopTask
Cancel a spawned task.
Stop worker.
Semantics: handle.abort()
Select
Select on multiple channels/timeouts.
Await the first of:
Receive x from ch:
...
After 5 seconds:
...
Semantics: tokio::select! with auto-cancel
Fields
branches: Vec<SelectBranch<'a>>The branches to select from
Theorem(TheoremBlock<'a>)
Theorem block.
## Theorem: Name
Given: Premise.
Prove: Goal.
Proof: Auto.