Documentation

Qq.Match

~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:

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.

Equations
  • { ty := none, fvarId := fvarId, userName := userName }.fvarTy = q(Lean.Level)
  • { ty := some val, fvarId := fvarId, userName := userName }.fvarTy = q(Lean.Expr)
def Qq.Impl.PatVarDecl.fvar (decl : Qq.Impl.PatVarDecl) :
let a := decl.fvarTy; let match_1_1 := match decl with | { ty := none, fvarId := fvarId, userName := userName } => q(Lean.Level) | { ty := some val, fvarId := fvarId, userName := userName } => q(Lean.Expr); Q(«$match_1_1»)
Equations
Equations
def Qq.Impl.mkIsDefEqResult (val : Bool) (decls : List Qq.Impl.PatVarDecl) :
let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»)
def Qq.Impl.mkIsDefEqResultVal (decls : List Qq.Impl.PatVarDecl) :
(let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»))Q(Bool)
Equations
Equations
def Qq.Impl.mkLet' (n : Lean.Name) (fvar ty val body : Lean.Expr) :
Equations
def Qq.Impl.mkInstantiateMVars (decls a✝ : List Qq.Impl.PatVarDecl) :
Lean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))
def Qq.Impl.mkIsDefEqCore (decls : List Qq.Impl.PatVarDecl) (pat discr : Q(Lean.Expr)) :
List Qq.Impl.PatVarDeclLean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))
Equations
  • One or more equations did not get rendered due to their size.
def Qq.Impl.mkIsDefEq (decls : List Qq.Impl.PatVarDecl) (pat discr : Q(Lean.Expr)) :
Lean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))
Equations
def Qq.Impl.mkQqLets {γ : Q(Type)} (decls : List Qq.Impl.PatVarDecl) :
(let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»))Lean.Elab.TermElabM Q(«$γ»)Lean.Elab.TermElabM Q(«$γ»)
Equations
def Qq.Impl.makeMatchCode {v : Lean.Level} {γ : Q(Type)} {m : Q(TypeType v)} (_instLift : Q(MonadLiftT Lean.MetaM «$m»)) (_instBind : Q(Bind «$m»)) (decls : List Qq.Impl.PatVarDecl) (uTy : Q(Lean.Level)) (ty : Q(Q(Sort «$uTy»))) (pat discr : Q(Q(«$$ty»))) (alt : Q(«$m» «$γ»)) (expectedType : Lean.Expr) (k : Lean.ExprLean.Elab.TermElabM Q(«$m» «$γ»)) :
Lean.Elab.TermElabM Q(«$m» «$γ»)
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Qq.Impl.mkLetDoSeqItem {m : TypeType} [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))
Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.
partial def Qq.Impl.floatQMatch (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) :
Lean.TermStateT (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem)) Lean.MacroM Lean.Term