Add CoreMatch dialect: surface pattern matching for Strata Core

[julesmt]

Summary

Adds the CoreMatch dialect: a Core extension giving surface-level
pattern matching at both expression and statement positions, with
two recursion styles that lower to identical Core.

• Expression-level match lowers to an application of the
  auto-generated structural eliminator D$Elim. Recursive functions
  written this way carry no termination obligation — the eliminator
  is total by construction.
• Statement-level match lowers to a nested if chain over the
  auto-generated testers D..isCᵢ, with pattern binders prepended
  as var b : T := D..fᵢ(scrut); init statements.
• The arm keyword anchors expression-level arms against ambiguity
  with Core operators.

Two recursion surfaces, one lowering

// Natural style: write the call.
rec function length(xs : List) : int {
  match xs {
    arm Nil()                       => 0;
    arm Cons(hd : int, tl : List)   => 1 + length(tl);
  }
};

// Cata style: bind the precomputed result.
function length(xs : List) : int {
  match xs {
    arm Nil()                                  => 0;
    arm Cons(hd : int, tl : List, lenTl : int) => 1 + lenTl;
  }
};

Both forms compile to the same List$Elim application. The natural
style runs through a small two-pass transformation: tryRecRewrite
swaps each f(field) self-call for a sentinel fvar during body
translation, and desugarNaturalToCata injects rec-result binders,
lifts existing bvars past them, and substitutes the sentinels for
the matching bvars.

What CoreMatch can do today

• Statement-level match with constructor and wildcard arms,
  and any number of pattern binders per constructor.
• Expression-level match with the head arm anchoring the
  result type and the arm keyword on tail arms.
• Datatype declarations with multiple constructors, each with
  zero or more typed fields; constructors can mix recursive and
  non-recursive fields freely.
• Wildcard arms (_ =>) covering one or more uncovered
  constructors; redundancy checker rejects a wildcard that's already
  redundant given the other arms.
• Recursive functions in two surface styles:
  • Natural — f(field) self-calls on recursive constructor fields,
    rewritten internally to rec-result references.
  • Cata — explicit rec-result binders appended to the pattern
    binders, typed as the function's return type.
• Multiple recursive fields per constructor — e.g. binary tree
  DFS with both left and right recursive fields, each producing
  its own auto-injected rec-result binder.
• Mutually recursive function blocks — every function in the
  same rec function … and … block is a valid self-call target.
• Nested matches — an arm body can itself be a match.
• Constructor calls in arm bodies — return a freshly-built
  datatype value from a recursive case (map_inc, filter_pos,
  etc.).
• Heterogeneously typed fields within a single datatype.
• Procedure specs — requires / ensures clauses, with
  free attributes and user-supplied labels, both preserved through
  lowering.
• Full statement repertoire in procedure bodies — assert,
  assume, if/else, non-deterministic if *, labelled blocks,
  var n : T; (no rhs), var n : T := e;, assignments.
• Type breadth — int, bool, string, real, every
  bv{1,8,16,32,64} width, Map K V, Sequence T, arrow types,
  and arbitrarily nested type constructors.
• Diagnostics with source ranges for non-exhaustive match,
  duplicate or unknown constructor in an arm, redundant or multiple
  wildcards, non-structural recursive calls (f(otherList),
  f(reverse(tl)), f as a higher-order value), and wrong arm
  binder counts.

What CoreMatch cannot do today

• Polymorphic datatypes — declarations are monomorphic. The
  translator's toCoreDatatype accepts an empty typeParams list
  only.
• Recursion through type constructors — the natural-style
  rewrite only fires for f(field) where field's type matches the
  scrutinee datatype directly. Children stored in Sequence T or
  Map K T aren't lifted across the type constructor, so sum on
  an n-ary Tree { Node(value : int, children : Sequence Tree) }
  cannot be written structurally.
• Non-structural recursion in general — merge sort, merge,
  Ackermann, gcd, etc. all require either an explicit decreases
  measure or a different fixed-point principle. CoreMatch has no
  surface form for decreases clauses yet; the escape hatch is to
  fall back to Core's procedure-level termination machinery.
• Or-patterns and nested patterns — each arm matches a single
  constructor at depth 1. Nested decomposition needs a nested
  match inside the arm body.
• Guards on arms — no when … or if … guard clause; push
  the predicate into the body.
• Literal patterns — patterns bind constructor field names,
  never literal values. Match Succ(Succ(_)) is not parseable.
• Cross-module / cross-dialect datatypes — every match's
  scrutinee datatype must be cached during the same Translate
  walk. Datatypes from imports aren't visible to the redundancy
  check or natural-style rewrite.
• Match expressions as conditions or arbitrary subterms in
  statements — the only way to lift an expression-level match
  into statement position is via var x := match …;.