Reference

This is the complete reference for the IRIS language: formal grammar, every primitive opcode, effect tags, and the type system.

Grammar#

The IRIS surface syntax is defined in src/iris-programs/syntax/iris_parser.iris and src/iris-programs/syntax/iris_lowerer.iris, with pre-compiled pipelines in bootstrap/*.json.

Module Structure#

module       ::= capability_decl* item*
item         ::= let_decl | type_decl | import_decl

Capability Declarations#

capability_decl ::= 'allow' '[' cap_entry (',' cap_entry)* ']'
                  | 'deny'  '[' cap_entry (',' cap_entry)* ']'
cap_entry       ::= IDENT STRING_LIT?

Let Declarations#

let_decl     ::= 'let' ['rec'] IDENT param* [':' type] [cost_annot]
                 requires_clause* ensures_clause* '=' expr

param        ::= IDENT
cost_annot   ::= '[' 'cost' ':' cost_expr ']'
requires_clause ::= 'requires' expr
ensures_clause  ::= 'ensures' expr

Type Declarations#

type_decl    ::= 'type' IDENT ['<' IDENT (',' IDENT)* '>'] '=' type
               | 'type' IDENT ['<' IDENT (',' IDENT)* '>'] '=' sum_type
               | 'type' IDENT ['<' IDENT (',' IDENT)* '>'] '=' struct_type

sum_type     ::= variant ('|' variant)*
variant      ::= UPPER_IDENT ['(' type ')']
UPPER_IDENT  ::= [A-Z] [a-zA-Z0-9_]*

struct_type  ::= '{' field (',' field)* '}'
field        ::= IDENT ':' type

Sum type declarations automatically bind constructors. Red in type Color = Red | Green | Blue becomes a value; Some in type Option = Some(Int) | None becomes a function Some : Int -> Option.

Struct type declarations define named-field product types. type Point = { x: Int, y: Int } creates a type where .x resolves to .0 and .y to .1 at compile time. Struct types are sugar over tuples.

Import Declarations#

import_decl  ::= 'import' STRING_LIT 'as' IDENT
               | 'import' HEX_HASH 'as' IDENT
STRING_LIT   ::= '"' [^"]* '"'
HEX_HASH     ::= '#' [0-9a-f]+

Path-based imports use a string literal containing a file path, resolved relative to the importing file. Hash-based imports use a #-prefixed BLAKE3 hash to identify an immutable content-addressed fragment. Both forms bind the imported module’s top-level declarations (including ADT constructors) into the importing scope.

import "stdlib/option.iris" as Opt    -- path-based
import #abc123def456 as math          -- hash-based

Types#

type         ::= 'forall' IDENT '.' type
               | type_atom '->' type
               | type_atom

type_atom    ::= '(' ')'                          -- Unit
               | '(' type (',' type)+ ')'          -- Tuple
               | '(' type ')'                      -- Parenthesized
               | '{' IDENT ':' type '|' expr '}'   -- Refinement
               | '{' field (',' field)* '}'         -- Struct type
               | IDENT '<' type (',' type)* '>'    -- Parameterized
               | IDENT                              -- Named

Cost Expressions#

cost_expr    ::= 'Unknown' | 'Zero'
               | 'Const' '(' INT ')'
               | 'Linear' '(' IDENT ')'
               | 'NLogN' '(' IDENT ')'
               | 'Polynomial' '(' IDENT ',' INT ')'
               | 'Sum' '(' cost_expr ',' cost_expr ')'

See the Type System page for how types, costs, contracts, and effects interact.

Expressions#

Precedence (lowest to highest):

1. let ... in, if ... then ... else, match ... with, \params -> body
2. Pipe: |>
3. Logical OR: ||
4. Logical AND: &&
5. Comparison: ==, !=, <, >, <=, >=
6. Addition: +, -
7. Multiplication: *, /, %
8. Unary: - (negation), ! (logical not)
9. Application: f x y (juxtaposition)
10. Postfix: .0, .1, … (tuple access)
11. Atoms: literals, variables, parenthesized, tuples

expr         ::= 'let' IDENT '=' expr 'in' expr
               | 'if' expr 'then' expr 'else' expr
               | 'match' expr 'with' match_arm+
               | '\' IDENT+ '->' expr
               | pipe_expr

pipe_expr    ::= or_expr ('|>' or_expr)*
or_expr      ::= and_expr ('||' and_expr)*
and_expr     ::= cmp_expr ('&&' cmp_expr)*
cmp_expr     ::= add_expr (cmp_op add_expr)?
add_expr     ::= mul_expr (('+' | '-') mul_expr)*
mul_expr     ::= unary_expr (('*' | '/' | '%') unary_expr)*
unary_expr   ::= '-' unary_expr | '!' unary_expr | app_expr
app_expr     ::= postfix_expr atom_expr*
postfix_expr ::= atom_expr ('.' (INT | IDENT))*

atom_expr    ::= INT | FLOAT | STRING | 'true' | 'false' | IDENT
               | '(' ')'                    -- Unit
               | '(' op ')'                 -- Operator section
               | '(' expr (',' expr)+ ')'   -- Tuple
               | '(' expr ')'               -- Parenthesized
               | '{' field_init (',' field_init)* '}'  -- Struct literal

field_init   ::= IDENT '=' expr

Match Arms#

match_arm    ::= '|' pattern '->' pipe_expr
pattern      ::= '_' | IDENT | INT | 'true' | 'false'
               | UPPER_IDENT ['(' pattern ')']    -- Constructor pattern

Constructor patterns like Some(v) or None destructure sum type values bound by type declarations. Patterns are tried top-to-bottom; the first matching arm is evaluated.

Match expressions work inside any expression context, including lambda bodies. This is essential for fold callbacks and higher-order functions:

let result = fold xs 0 (\acc x ->
  match classify x with
  | Positive(n) -> acc + n
  | Negative(n) -> acc - n
  | Zero -> acc)

Operator Sections#

(+)   -- \a b -> a + b
(*)   -- \a b -> a * b
(==)  -- \a b -> a == b

Lexical Elements#

Keywords#

let  rec  in  val  type  import  as
match  with  if  then  else
forall  true  false
requires  ensures
allow  deny

Operators#

+  -  *  /  %            -- Arithmetic
==  !=  <  >  <=  >=     -- Comparison
&&  ||  !                -- Logical
|>                       -- Pipe
->                       -- Arrow (types and lambdas)
\                        -- Lambda
.                        -- Tuple access

Literals#

Primitive Opcodes#

All primitives are named functions resolved by the IRIS lowerer (src/iris-programs/syntax/iris_lowerer.iris). Each maps to a (opcode, arity) pair.

Arithmetic (0x00–0x09)#

Bitwise (0x10–0x15)#

Comparison (0x20–0x25)#

Higher-Order (0x30–0x32)#

Conversion (0x40–0x44)#

Graph Introspection (0x80–0x8D)#

Meta-Evolution (0xA0)#

String Operations (0xB0–0xC0)#

List/Collection Operations (0xC1–0xCD)#

Data Access / Introspection (0xCF, 0xD2–0xD6)#

Math (0xD8–0xE3)#

Lazy Lists (0xE9–0xEC)#

Time & Bytes (0xE4–0xE8)#

Effect Tags#

Effects are performed through Effect nodes. In surface syntax, effect functions resolve to these tags.

Standard Effects (0x00–0x0D)#

Raw I/O (0x10–0x1F)#

Threading & Atomics (0x20–0x28)#

JIT & FFI (0x29–0x2B)#

Type System#

Primitive Types#

Composite Types#

Algebraic Data Types#

Sum types are declared with type and define constructors that produce tagged values:

type_decl   ::= 'type' IDENT '=' constructor ('|' constructor)*
constructor ::= IDENT '(' type ')' | IDENT

Nullary constructors like None or Red are values. Constructors with a payload like Some(Int) are functions of type Int -> Option. Constructors are first-class: they can be passed to higher-order functions, returned from expressions, and used across import boundaries.

type Option = Some(Int) | None
type Color  = Red | Green | Blue

let colors = (Red, Green, Blue)
let wrapped = map (1, 2, 3) Some   -- (Some(1), Some(2), Some(3))

Struct Types#

Struct types are sugar over product types. A struct declaration assigns field names to tuple positions:

struct_type  ::= '{' field (',' field)* '}'
field        ::= IDENT ':' type

At compile time, struct construction { x = 3, y = 4 } becomes Tuple(3, 4), and field access .x resolves to positional .0. The runtime never sees field names, only tuples and integer projections.

type Point = { x: Int, y: Int }
let p : Point = { x = 10, y = 20 }   -- Tuple(10, 20)
let sum = p.x + p.y                   -- p.0 + p.1 → 30

Runtime Values#