Module match_compile 

The equation compiler: surface patterns → the kernel’s positional Match tree.

The kernel’s Term::Match is deliberately primitive. Its cases vector is indexed by CONSTRUCTOR, in the inductive’s registration order, one case per constructor, each case a λ-telescope over that constructor’s value fields. It has no patterns, no nesting, no wildcard and no notion of order among alternatives. That is the right primitive — every extra feature in an eliminator is another thing the trusted base has to be right about — but it is not how mathematics is written. Lean writes

def f : Nat → Nat → Nat
  | 0,      _      => 1
  | _,      0      => 2
  | .succ _, .succ _ => 3

and compiles it. This module is that compiler: Maranget/Augustsson column-based pattern-matrix compilation, with Lean’s top-to-bottom first-match semantics, producing a tree of positional Match nodes the kernel already certifies.

What it guarantees

• Registration order, never source order. A clause is placed in the slot of the constructor it NAMES. Bool is registered true then false; writing the false clause first must not silently compute the other function. For every equal-arity inductive — every enumeration — this is the difference between a correct program and a wrong one that type-checks.
• First match wins. Overlapping equations are split into disjoint constructor cases by specialising the matrix top-to-bottom, which is the only reading under which pick 0 0 is 1 rather than 2.
• Totality. A constructor no clause can reach is an error naming the missing case, not a silently-invented value and not a partial function. The kernel is total; so is its surface — and so is Lean’s: def classify : Nat → Nat | 0 => 0 | Nat.succ (Nat.succ k) => k answers error: missing cases: (Nat.succ Nat.zero) (Lean/Elab/Match.lean:991-992).
• Numerals. When 0: is the unary spelling of 0 in whatever inductive the column has — Lean’s expandNatValuePattern (Lean/Meta/Match/Match.lean:629), except that the zero and the successor are derived from the declaration instead of hard-coded to Nat.
• Nothing is relaxed at the kernel. This is a SURFACE pass. It emits exactly the Term::Match the kernel already accepts, one case per constructor at every node. A hand-written match with the wrong case count is still WrongNumberOfCases.

What it deliberately does not do

The compiled tree is non-dependent: every node’s motive is the CONSTANT λ_:I. T at the same result type T. That is what a surface equation set means (f : A → B, one result type for every branch). A genuinely dependent elimination is written with an explicit motive against Term::Match directly, which this module never touches.

Structs

Clause

One equation: one pattern per column, and the body those patterns’ variables are free in.

CompileReport

What the compiler noticed on the way through, beyond the term itself.

Enums

Pattern

A surface pattern, exactly as a When clause spells it.

Functions

compile_clauses

Compile a clause matrix against a list of scrutinees.

compile_clauses_reporting

compile_clauses, plus what the compiler noticed.

pattern_binder_types

The types a pattern’s binders take when it is matched against a value of disc_ty.