Struct RefinementContext 

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

Available on crate feature codegen only.

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