~q() matching

This file extends the syntax of match and let to permit matching terms of type Q(α) using ~q(<pattern>), just as terms of type Syntax can be matched with `(<pattern>). Compare to the builtin match_expr and let_expr, ~q() matching:

• is type-safe, and so helps avoid many mistakes in match patterns
• matches by definitional equality, rather than expression equality
• supports compound expressions, not just a single application

See Qq.matcher for a brief syntax summary.

Matching typeclass instances

For a more complete example, consider

def isCanonicalAdd {u : Level} {α : Q(Type u)} (inst : Q(Add $α)) (x : Q($α)) :
    MetaM <| Option (Q($α) × Q($α)) := do
  match x with
  | ~q($a + $b) => return some (a, b)
  | _ => return none

Here, the ~q($a + $b) match is specifically matching the addition against the provided inst instance, as this is what is being used to elaborate the +.

If the intent is to match an arbitrary Add α instance in x, then you must match this with a $inst antiquotation:

def isAdd {u : Level} {α : Q(Type u)} (x : Q($α)) :
    MetaM <| Option (Q(Add $α) × Q($α) × Q($α)) := do
  match x with
  | ~q(@HAdd.hAdd _ _ _ (@instHAdd _ $inst) $a $b) => return some (inst, a, b)
  | _ => return none

Matching Exprs

By itself, ~q() can only match against terms of the form Q($α). To match an Expr, it must first be converted to Qq with Qq.inferTypeQ.

For instance, to match an arbitrary expression for n + 37 where n : Nat, we can write

def isAdd37 (e : Expr) : MetaM (Option Q(Nat)) := do
  let ⟨1, ~q(Nat), ~q($n + 37)⟩ ← inferTypeQ e | return none
  return some n

This is performing three sequential matches: first that e is in Sort 1, then that the type of e is Nat, then finally that e is of the right form. This syntax can be used in match too.

def Qq.Impl.mkInstantiateMVars (decls a✝ : List PatVarDecl) : Lean.MetaM (have a := mkIsDefEqType decls; Q(Lean.MetaM «$a»))

def Qq.Impl.mkIsDefEqCore (decls : List PatVarDecl) (pat discr : Q(Lean.Expr)) : List PatVarDecl → Lean.MetaM (have a := mkIsDefEqType decls; Q(Lean.MetaM «$a»))

def Qq.Impl.mkIsDefEq (decls : List PatVarDecl) (pat discr : Q(Lean.Expr)) : Lean.MetaM (have a := mkIsDefEqType decls; Q(Lean.MetaM «$a»))

def Qq.Impl.mkQqLets {γ : Q(Type)} (decls : List PatVarDecl) : (have a := mkIsDefEqType decls; Q(«$a»)) → Lean.Elab.TermElabM Q(«$γ») → Lean.Elab.TermElabM Q(«$γ»)

def Qq.Impl.replaceTempExprsByQVars : List PatVarDecl → Lean.Expr → Lean.Expr

def Qq.Impl.makeMatchCode {v : Lean.Level} {γ : Q(Type)} {m : Q(Type → Type v)} (_instLift : Q(MonadLiftT Lean.MetaM «$m»)) (_instBind : Q(Bind «$m»)) (decls : List PatVarDecl) (uTy : Q(Lean.Level)) (ty : Q(Q(Sort «$uTy»))) (pat discr : Q(Q(«$$ty»))) (alt : Q(«$m» «$γ»)) (expectedType : Lean.Expr) (k : Lean.Expr → Lean.Elab.TermElabM Q(«$m» «$γ»)) : Lean.Elab.TermElabM Q(«$m» «$γ»)

def Qq.Impl.unquoteForMatch (et : Lean.Expr) : UnquoteM (Lean.LocalContext × Lean.LocalInstances × Lean.Expr)

def Qq.Impl.mkNAryFunctionType : Nat → Lean.MetaM Lean.Expr

structure Qq.Impl.PatternVar : Type

• name : Lean.Name
• arity : Nat

  Pattern variables can be functions; if so, this is their arity.

• mvar : Lean.Expr
• stx : Lean.Term

partial def Qq.Impl.getPatVars (pat : Lean.Term) : StateT (Array PatternVar) Lean.Elab.TermElabM Lean.Term

def Qq.Impl.elabPat (pat : Lean.Term) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (ty : Lean.Expr) (levelNames : List Lean.Name) : Lean.Elab.TermElabM (Lean.Expr × Array Lean.LocalDecl × Array Lean.Name)

def Qq.Impl.«term_qq_match_←_|_In_» : Lean.ParserDescr

def Qq.Impl.«term_qq_match_:=_|_» : Lean.ParserDescr

partial def Qq.Impl.isIrrefutablePattern : Lean.Term → Bool

def Qq.Impl.term_comefrom_Do_In_ : Lean.ParserDescr

def Qq.Impl.term_comefrom_Do_ : Lean.ParserDescr

def Qq.Impl.doElemComefrom_Do_ : Lean.ParserDescr

def Qq.Impl.mkLetDoSeqItem {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (pat : Lean.Term) (rhs : Lean.TSyntax `term) (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) : m (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem))

def Qq.matcher : Lean.ParserDescr

Qqs expression matching in MetaM, up to reducible defeq.

This syntax is valid in match, let, and if let, but not fun.

The usage is very similar to the builtin Syntax-matching that uses `(<pattern>) notation. As an example, consider matching against a n : Q(ℕ), which can be written

• With a match expression,

  match n with
  | ~q(Nat.gcd $x $y) => handleGcd x y
  | ~q($x + $y) => handleAdd x y
  | _ => throwError "no match"
  

• With a let expression (if there is a single match)

  let ~q(Nat.gcd $x $y) := n | throwError "no match"
  handleGcd x y
  

• With an if let statement

  if let ~q(Nat.gcd $x $y) := n then
    handleGcd x y
  else if let ~q($x + $y) := n then
    handleAdd x y
  else
    throwError "no match"
  

In addition to the obvious x and y captures, in the example above ~q also inserts into the context a term of type $n =Q Nat.gcd $x $y.

partial def Qq.Impl.hasQMatch : Lean.Syntax → Bool

partial def Qq.Impl.floatQMatch (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) : Lean.Term → StateT (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem)) Lean.MacroM Lean.Term

partial def Qq.unpackParensIdent : Lean.Syntax → Option Lean.Syntax