Struct RefinementContext 

pub struct RefinementContext<'a> { /* private fields */ }

Tracks refinement type constraints across scopes for mutation enforcement.

When a variable with a refinement type is defined, its constraint is registered in the current scope. When that variable is mutated via Set, the assertion is re-emitted to ensure the invariant is preserved.

Scope Management

The context maintains a stack of scopes to handle nested blocks:

┌─────────────────────────────┐
│ Global Scope               │ ← x: { it > 0 }
│  ┌──────────────────────┐  │
│  │ Zone Scope           │  │ ← y: { it < 100 }
│  │  ┌────────────────┐  │  │
│  │  │ If Block Scope │  │  │ ← z: { it != 0 }
│  │  └────────────────┘  │  │
│  └──────────────────────┘  │
└─────────────────────────────┘

Variable Type Tracking

The context also tracks variable types for capability resolution. This allows statements like Check that user can publish the document to resolve “the document” to a variable named doc of type Document.

Implementations

impl<'a> RefinementContext<'a>

pub fn new() -> Self

pub fn from_type_env(type_env: &TypeEnv) -> Self

Create a RefinementContext seeded from a TypeEnv.

pub fn set_oracle(&mut self, oracle: Rc<OracleFacts>)

Attach the oracle fact table for borrow-hoist distinctness queries.

pub fn oracle(&self) -> Option<&OracleFacts>

The attached oracle facts, if any.

pub fn set_de_rc_vars(&mut self, vars: HashSet<Symbol>)

Set the de-Rc’d Seq variables (emitted as plain Vec<T>).

pub fn set_returns_vec(&mut self, v: bool)

Phase 4: mark that the current function returns an owned Vec<T>.

pub fn set_escaping_vars(&mut self, vars: HashSet<Symbol>)

Set the escaping vars for local Vec optimization.

pub fn var_escapes(&self, sym: &Symbol) -> bool

Check if a variable escapes (and thus must remain LogosSeq).

pub fn register_fn_return(&mut self, fn_sym: Symbol, return_type: String)

Register a function’s return type.

pub fn get_fn_return(&self, fn_sym: &Symbol) -> Option<&String>

Get a function’s return type.

pub fn set_live_vars_after(&mut self, live: HashSet<Symbol>)

Set the live-after set for the next statement about to be generated.

Must be called before each top-level codegen_stmt call in a function body. codegen_stmt will consume this (clearing it to None) so recursive nested calls conservatively clone.

pub fn take_live_vars_after(&mut self) -> Option<HashSet<Symbol>>

Take (and clear) the live-after set. Called once at the start of codegen_stmt.

Returns None when no liveness information was provided (conservative path).