Skip to main content

Module codegen

Module codegen 

Source
Available on crate feature codegen only.
Expand description

Code generation from LOGOS AST to Rust source code.

This module transforms the parsed and type-checked LOGOS program into idiomatic Rust code. The generated code uses logicaffeine_data types for runtime values and integrates with the kernel for proof verification.

§Pipeline Position

┌─────────────────────────────────────────────────────────┐
│  LOGOS Source → Lexer → Parser → AST → Analysis → HERE │
└─────────────────────────────────────────────────────────┘
                                                     ↓
                                              Rust Source

§Code Generation Rules

LOGOS StatementRust Output
Let x be 5.let x = 5;
Set x to 10.x = 10;
Give x to y.let y = x; (move)
Show x to show.println!("{}", x);
If x > 0 then...if x > 0 { ... }
Repeat while x > 0...while x > 0 { ... }
Zone "name"...{ /* zone scope */ }
Mount x at "path".x.mount(vfs, "path").await;
Sync x on "topic".x.subscribe("topic").await;

§Key Features

  • Refinement Types: Generates debug_assert! for type predicates
  • Policy Enforcement: Emits capability checks for access control
  • Zone Safety: Translates memory zones to Rust scopes
  • CRDT Mutability: Uses .set() for LWWRegister/MVRegister fields
  • Async Detection: Adds #[tokio::main] when async operations are present
  • VFS Detection: Injects NativeVfs::new() for file operations
  • Mount+Sync Detection: Uses Distributed<T> for combined persistence/sync

§Refinement Context

The RefinementContext tracks type predicates across scopes:

Let x: { it: Int | it > 0 } be 5.   ←  Register constraint
     ↓
debug_assert!(5 > 0);               ←  Check at definition
     ↓
Set x to 10.                        ←  Re-check on mutation
     ↓
debug_assert!(10 > 0);              ←  Re-emit assertion
  • When a variable with a refinement type is defined, its constraint is registered
  • When that variable is mutated, the assertion is re-emitted
  • Variable types are tracked for capability resolution

§Entry Point

The main entry point is codegen_program, which generates a complete Rust program from a list of statements.

Structs§

RefinementContext
Tracks refinement type constraints across scopes for mutation enforcement.
VariableCapabilities
Tracks which variables have Mount and/or Sync statements.

Enums§

CAbiClass
Classification of a LOGOS type for C ABI boundary crossing.

Functions§

codegen_assertion
Converts a LogicExpr to a Rust boolean expression for debug_assert!(). Uses RustFormatter to unify all logic-to-Rust translation.
codegen_expr
codegen_expr_with_async
Phase 54+: Codegen expression with async function tracking. Adds .await to async function calls at the expression level, handling nested calls.
codegen_program
Generate a complete Rust program from LOGOS statements.
codegen_stmt
codegen_term
collect_async_functions
Phase 54: Collect function names that are async. Used by LaunchTask codegen to determine if .await is needed.
collect_pipe_sender_params
Phase 54: Collect parameters that are used as pipe senders in function body. If a param appears in SendPipe { pipe: Expr::Identifier(param) }, it’s a sender.
collect_pipe_vars
Phase 54: Collect variables that are pipe declarations (created with CreatePipe). These have _tx/_rx suffixes, while pipe parameters don’t.
empty_var_caps
Helper to create an empty VariableCapabilities map (for tests).
generate_c_header
Generate the C header (.h) content for all C-exported functions.
generate_python_bindings
Generate Python ctypes bindings for all C-exported functions.
generate_typescript_bindings
Generate TypeScript type declarations (.d.ts) and FFI bindings (.js).