Pattern Matching

Pattern matching with switch expressions lets you inspect variant tags, options, tuples, and literals while making every case visible to the type checker and verifier.

Basic Syntax

The switch expression evaluates a scrutinee and matches it against a list of cases:

switch (value) {
  case (pattern1) expr1;
  case (pattern2) expr2;
  case (pattern3) expr3;
}

Each case starts with a pattern that describes what values match, followed by an expression to evaluate when matched. The switch is an expression that returns the value of the matched case.

switch-basic.sr9

// Basic switch expressions
persistent actor {
  type Color = { #red; #green; #blue };

  // Switch is an expression that returns a value
  public func colorValue(c : Color) : async Nat
    ensures switch (c) {
      case (#red) result == 0;
      case (#green) result == 1;
      case (#blue) result == 2;
    };
  {
    switch (c) {
      case (#red) 0;
      case (#green) 1;
      case (#blue) 2;
    }
  };

  // Assign switch result to variable
  public func describe(c : Color) : async Nat {
    let code = switch (c) {
      case (#red) 100;
      case (#green) 200;
      case (#blue) 300;
    };
    code
  };
}

Key points:

• Cases are evaluated in order, top to bottom
• The first matching case executes; remaining cases are skipped
• All cases must be covered (exhaustiveness is checked at compile time)
• The result type is the common supertype of all case expressions

Pattern Types

Tag Patterns

Match variant tags with #tagName:

case (#pending) ...   // matches the #pending tag
case (#approved) ...  // matches the #approved tag

Payload Binding

Bind payloads to variables by adding a name after the tag:

case (#ok n) ...           // n binds to the Nat payload
case (#err msg) ...        // msg binds to the Text payload
case (#coords (x, y)) ...  // destructure tuple payload

switch-payload.sr9

// Extracting payloads from variants
persistent actor {
  type Shape = { #circle : Nat; #rect : (Nat, Nat); #point };

  // Bind payload to variable
  public func area(s : Shape) : async Nat
    ensures switch (s) {
      case (#circle r) result == r * r;
      case (#rect (w, h)) result == w * h;
      case (#point) result == 0;
    };
  {
    switch (s) {
      case (#circle r) r * r;         // r binds to payload
      case (#rect (w, h)) w * h;      // tuple destructuring
      case (#point) 0;                // no payload
    }
  };

  // Ignore payload with wildcard
  public func hasSize(s : Shape) : async Bool
    ensures switch (s) {
      case (#point) result == false;
      case (_) result == true;
    };
  {
    switch (s) {
      case (#circle _) true;   // ignore the radius
      case (#rect _) true;     // ignore dimensions
      case (#point) false;
    }
  };
}

Payload patterns:

Pattern	Syntax	Binds
No payload	case (#tag)	Nothing
Single value	case (#tag x)	x to payload
Tuple payload	case (#tag (a, b))	a and b to tuple elements
Ignored	case (#tag _)	Nothing (discards payload)

Wildcard Patterns

Use _ to match any value without binding:

case (_) ...     // matches anything
case (#ok _) ... // matches #ok with any payload

switch-wildcard.sr9

// Wildcard patterns in switch
persistent actor {
  type Status = { #pending; #approved; #rejected; #cancelled };

  // Wildcard catches all remaining cases
  public func isActive(s : Status) : async Bool
    ensures s == #pending ==> result == true;
    ensures s != #pending ==> result == false;
  {
    switch (s) {
      case (#pending) true;
      case (_) false;  // matches #approved, #rejected, #cancelled
    }
  };

  // Multiple specific cases before wildcard
  public func priority(s : Status) : async Nat
    ensures switch (s) {
      case (#pending) result == 1;
      case (#approved) result == 2;
      case (_) result == 0;
    };
  {
    switch (s) {
      case (#pending) 1;
      case (#approved) 2;
      case (_) 0;  // matches #rejected and #cancelled
    }
  };
}

Wildcards are useful for:

• Catching all remaining cases
• Ignoring payloads you don't need
• Simplifying switches when you only care about specific cases

Option Patterns

Match option types with null and ?:

case null { ... }    // matches null/None
case (?v) { ... }    // matches Some, binds v to the value

option-switch.sr9

// Pattern matching on options
persistent actor {
  transient var stored : ?Nat = null;

  // Basic switch pattern
  public func getOrDefault(default : Nat) : async Nat
    reads stored
    ensures stored == null ==> result == default;
  {
    switch (stored) {
      case null { default };
      case (?v) { v };
    }
  };

  // Transform option value
  public func double() : async ?Nat
    reads stored
    ensures switch (stored, result) {
      case (null, null) true;
      case (?n, ?m) m == n * 2;
      case (_, _) false;
    };
  {
    switch (stored) {
      case null { null };
      case (?v) { ?(v * 2) };
    }
  };

  // Switch extracting to local variable
  public func process() : async Nat
    reads stored
  {
    let x = switch (stored) {
      case null { 0 };
      case (?v) { v + 1 };
    };
    x
  };
}

Literal Patterns

Match specific values:

case (0) ...   // matches zero
case (1) ...   // matches one
case (_) ...   // matches everything else

Literal patterns work with Nat, Int, Bool, and Char types.

Nested Switches

Switches can be nested for multi-dimensional matching:

switch-nested.sr9

// Nested switch expressions
persistent actor {
  type Color = { #red; #blue };
  type Size = { #small; #large };

  // Nested switches for multiple dimensions
  public func code(c : Color, s : Size) : async Nat
    ensures switch (c) {
      case (#red) switch (s) {
        case (#small) result == 1;
        case (#large) result == 2;
      };
      case (#blue) switch (s) {
        case (#small) result == 3;
        case (#large) result == 4;
      };
    };
  {
    switch (c) {
      case (#red) {
        switch (s) {
          case (#small) 1;
          case (#large) 2;
        }
      };
      case (#blue) {
        switch (s) {
          case (#small) 3;
          case (#large) 4;
        }
      };
    }
  };
}

For complex multi-way decisions, nested switches are clearer than deeply nested if/else chains.

Switch in Contracts

Use switch in postconditions to specify per-case behavior:

public func process(r : Result) : async Nat
  ensures switch (r) {
    case (#ok n) result == n;
    case (#err _) result == 0;
  };
{
  switch (r) {
    case (#ok n) n;
    case (#err _) 0;
  }
}

The verifier translates switch expressions in contracts to nested conditionals with discriminator functions:

isResult$ok(r) ? (result == getResult$ok$0(r)) : (result == 0)

Tuple Patterns in Contracts

Match input and output together:

ensures switch (input, result) {
  case (null, null) true;
  case (?n, ?m) m == n + 1;
  case (_, _) false;
};

This pattern is useful when the relationship between input and output depends on the input's structure. The same technique works with old(...) when the postcondition compares pre-state and post-state variants.

Exhaustiveness

All cases must be covered. Missing cases cause compile error M0145:

type Status = { #pending; #approved; #rejected };

switch (s) {
  case (#pending) 0;
  case (#approved) 1;
  // ERROR M0145: pattern does not cover value #rejected
}

Fix by adding the missing case or using a wildcard:

switch (s) {
  case (#pending) 0;
  case (#approved) 1;
  case (#rejected) 2;  // explicit
}

// Or use wildcard
switch (s) {
  case (#pending) 0;
  case (_) 1;  // matches #approved and #rejected
}

Unreachable cases trigger warning M0146:

switch (s) {
  case (_) 0;          // matches everything
  case (#pending) 1;   // WARNING M0146: this pattern is never matched
}

Verification Behavior

The verifier handles pattern matching by generating:

1. Discriminator functions: isStatus$pending(s) returns true if s has tag #pending
2. Getter functions: getResult$ok$0(r) extracts the first payload field from #ok
3. Exhaustiveness axioms: Exactly one tag is active at any time
4. Reconstructor axioms: A value equals its constructor applied to its extracted fields

This encoding means the verifier can reason precisely about which case applies and what values are bound. When a branch mutates actor state, the method still needs matching modifies clauses and must preserve actor invariants.

Restrictions

No Or-Patterns

Combining patterns with or is not supported:

// NOT SUPPORTED
case (0 or 1) ...
case (#red or #blue) ...

List cases separately or use a wildcard:

case (0) 1;
case (1) 1;
case (_) 0;

No Signed Literal Patterns

Negative literals in patterns are not supported:

// NOT SUPPORTED
case (-1) ...

Use guards or comparisons in the body instead.

Let Pattern Restrictions

In let bindings, patterns must be irrefutable (always match):

// Supported - tuple patterns are irrefutable
let (a, b) = (1, 2);

// Supported - record patterns are irrefutable when the fields exist
let { x } = record;

// NOT SUPPORTED - literal pattern is refutable
let (0, y) = pair;

// NOT SUPPORTED - option pattern is refutable
let (?x, y) = pair;

Use switch for refutable patterns, or a let ... else form when the language construct you are using explicitly supports a failure branch:

switch (pair) {
  case (0, y) { /* use y */ };
  case _ { /* handle other cases */ };
};

For-In Pattern Restrictions

Loop patterns must be simple identifiers:

// Supported
for (x in arr.values()) { ... }

// NOT SUPPORTED - option patterns
for (?x in optArr.values()) { ... }

// NOT SUPPORTED - literal patterns
for (0 in arr.values()) { ... }

Iterator Requirements

In verification mode, for-in loops accept iterators whose next() method has a function type contract: next : () -> ?T contract { ... }. Built-in iterators like arr.values(), arr.keys(), blob.values(), and text.chars() satisfy this; arbitrary iterator-like objects must expose the same contracted shape.

These are rejected because next() is missing a contract:

type Iter<T> = { next : () -> ?T };  // Missing contract

let it : Iter<Nat> = object { public func next() : ?Nat { null } };
for (x in it) { ... }  // Rejected

Common Patterns

Result Handling

type Result<T, E> = { #ok : T; #err : E };

switch (result) {
  case (#ok value) { /* use value */ };
  case (#err error) { /* handle error */ };
};

State Machine Transitions

type State = { #idle; #running : Nat; #done };

public func step() : async ()
  modifies state
  entry_requires switch (state) { case (#running _) true; case _ false };
  requires switch (state) { case (#running _) true; case _ false };
{
  switch (state) {
    case (#running n) {
      if (n == 0) { state := #done }
      else { state := #running(n - 1) }
    };
    case _ { assert false };
  }
};

Default Value Extraction

public func getOrDefault(opt : ?Nat, default : Nat) : Nat {
  switch (opt) {
    case null { default };
    case (?v) { v };
  }
};

Error Codes

Code	Meaning
M0110	Literal pattern cannot consume expected type
M0112	Tuple pattern has wrong number of components
M0115	Option pattern cannot consume expected type
M0116	Variant pattern cannot consume expected type
M0145	Pattern does not cover all cases
M0146	Pattern is never matched (unreachable)
M0189	Or-pattern alternatives bind different variables

Summary

• switch expressions match values against patterns and return the matched case's result
• Pattern types: tags (#name), payloads (#name x), tuples ((a, b)), options (?v / null), wildcards (_), literals
• All cases must be covered (exhaustiveness checked at compile time)
• Use switch in postconditions for per-case specifications
• Or-patterns and signed literals are not supported
• Let bindings require irrefutable patterns; use switch for refutable ones
• For-in loops only support simple identifier patterns

Related Topics

• Variants for defining tagged state
• Options for null and ?value cases
• Protocol state machines for verified transitions over variants