Interpretation (-r, -i)

Run programs for development and testing without producing WebAssembly.

The -r (run) and -i (interactive) flags interpret Sector9 programs directly, bypassing the WebAssembly compilation step. This enables rapid testing of logic during development, debugging with print statements, and interactive exploration of your code.

Basic Usage

Run Mode (-r)

Execute a program and exit:

sector9 -r file.sr9

The program runs to completion, printing output to stdout. The command exits with code 0 on success or 1 on runtime error (assertion failure, trap, etc.).

Interactive Mode (-i)

Start an interactive REPL (Read-Eval-Print Loop):

sector9 -i file.sr9

This loads your file, then enters an interactive session where you can type expressions and declarations at the > prompt. The REPL maintains state across inputs, so you can build up definitions incrementally.

What Interpretation Does

The interpretation pipeline performs these steps:

1. Parsing - Tokenizes and parses source code
2. Import resolution - Loads library dependencies
3. Type checking - Full type inference and validation
4. Desugaring - Converts to intermediate representation
5. Execution - Runs the program in the abstract interpreter

This uses the normal frontend type checking, followed by direct execution. If the program imports local packages such as mo:core/..., pass the same --package flags you use for checking.

What Interpretation Does NOT Do

• Does not compile to WebAssembly
• Does not invoke the SMT solver for verification
• Does not prove contracts (runtime assertions only)
• Does not deploy to the Internet Computer

For formal verification, use --verify. For deployment, use -c to compile.

-r vs -i

Aspect	-r	-i
Execution mode	Batch	Interactive
Input source	Files only	Files, then stdin
State after run	Exits	Preserved in REPL
Banner printed	No	Yes (version info)
Use case	Testing, scripts	Exploration, debugging

Interpreting Ghost Code

Ghost declarations are still visible to the source interpreter:

ghost var count : Nat = 0;

public func increment() {
  ghost { count := count + 1 };
};

When you run this with -r, the ghost variable updates in the interpreter. This differs from compilation and runtime projection, where ghost code is erased.

Assertion Behavior

The interpreter distinguishes assertion types:

Assertion	Behavior
assert expr	Static verification assertion; not a deployed runtime check
runtime:assert expr	Evaluated; traps if false
trap expr	Evaluated; traps if true

Runtime assertions execute and can cause traps. Static assertions are skipped entirely.

Exit Codes

Code	Meaning
0	Success - program completed normally
1	Failure - runtime error, assertion failure, or trap
2	Invalid arguments - missing files or conflicting flags

Common Flags

Verbose Output

Show phase timings and intermediate steps:

sector9 -r -v file.sr9

Tracing

Enable trace output for debugging:

sector9 -r -t file.sr9

Print Depth

Control how deeply nested values are printed:

# Set print depth to 10 levels
sector9 -r -p 10 file.sr9

Hide Warnings

Suppress warning messages:

sector9 -r --hide-warnings file.sr9

Interactive REPL Features

Multi-line Input

When entering incomplete expressions, the REPL continues reading with a (two-space) prompt:

> let record = {
    name = "Alice";
    age = 30
  };
record : {age : Nat; name : Text} = {age = 30; name = "Alice"}

State Preservation

The REPL preserves state across syntax and type errors:

> let x = 42;
x : Nat = 42
> let x = "invalid" *;
stdin:1.16: syntax error [M0001], unexpected token ';', expected one of token or <phrase> sequence...
> runtime:assert (x == 42);
() : ()

After the syntax error, x still holds 42.

Importing Modules

Import modules interactively:

> import Prim "mo:⛔";
> Prim.natToText(42);
"42" : Text

Evaluating Expressions

Type expressions directly to see their values:

> 1 + 2 * 3;
7 : Nat
> #Monday;
#Monday : \{#Monday}
> [1, 2, 3];
[1, 2, 3] : [Nat]

Limitations

Declaration-Only Functions

Functions without bodies (verification-only declarations) cannot be interpreted:

// This will fail with M0336
func spec_only(x : Nat) : Nat
  ensures result > x;

Error: declaration-only functions are verification-only; add a body before compiling or running

Add a body to run:

func spec_only(x : Nat) : Nat
  ensures result > x;
{
  x + 1
}

Actor Imports

IDL-based actor imports are not supported in the interpreter:

// This will trap: "actor import"
import SomeActor "canister:some_actor";

Mixins

Include directives (mixins) are not yet supported:

// This will trap: "Mixins are not yet supported in the interpreter"
include SomeMixin;

Actor Class Configuration

Only basic actor class instantiation works. Advanced configuration is unsupported:

// Only "new" with default settings works
// Custom settings will trap

Runtime Errors

Assertion Failure

file.sr9:10.4-10.25: execution error, assertion failure

A runtime:assert evaluated to false.

Pattern Match Failure

file.sr9:15.4-15.30: execution error, switch value #Unknown does not match any case

A switch expression had no matching case.

Array Index Out of Bounds

file.sr9:8.4-8.15: execution error, array index out of bounds

Accessed an array with an invalid index.

Arithmetic Overflow

file.sr9:12.4-12.20: execution error, arithmetic overflow

A fixed-width integer operation overflowed.

IR Interpretation (-iR)

For debugging compiler transformations, interpret the lowered IR:

sector9 -r -iR file.sr9

This runs the program after applying IR lowering passes (async/await transformations, tailcall optimization). Combine with other flags:

# IR interpretation without await lowering
sector9 -r -iR -no-await file.sr9

# IR interpretation without async lowering
sector9 -r -iR -no-async file.sr9

This is primarily useful for compiler development and debugging.

Interpretation vs Verification

Aspect	Interpretation (-r)	Verification (--verify)
Execution	Concrete runtime	Symbolic analysis
Assertions	runtime:assert executes	All become proof obligations
Ghost code	Executes at runtime	Drives verification
Paths explored	Single execution	All possible paths
Speed	Fast	Slower (SMT solving)
Guarantees	This run worked	All inputs satisfy contracts

Typical Workflow

# 1. Quick testing during development
sector9 --package core ./core/src -r my_module.sr9

# 2. Interactive exploration
sector9 --package core ./core/src -i my_module.sr9

# 3. Type checking when ready
sector9 --package core ./core/src --check my_module.sr9

# 4. Full verification before deployment
sector9 --package core ./core/src --verify my_module.sr9

Summary

• -r executes programs in batch mode for testing
• -i provides an interactive REPL for exploration
• Ghost code executes at runtime (unlike compilation)
• Only runtime:assert runs; static assert is skipped
• State persists across errors in interactive mode
• Declaration-only functions require bodies to run
• Use -iR for debugging compiler IR transformations
• Add --package <name> <path> when interpreted files import local packages