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.

Instances For
    Equations
    • x.fvarTy = match x with | { ty := none, fvarId := fvarId, userName := userName } => q(Lean.Level) | { ty := some val, fvarId := fvarId, userName := userName } => q(Lean.Expr)
    Instances For
      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
      Instances For
        Equations
        Instances For
          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»)
          Instances For
            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
            Instances For
              Equations
              Instances For
                Equations
                Instances For
                  def Qq.Impl.mkInstantiateMVars (decls : List Qq.Impl.PatVarDecl) :
                  List Qq.Impl.PatVarDeclLean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))
                  Instances For
                    def Qq.Impl.mkIsDefEqCore (decls : List Qq.Impl.PatVarDecl) (pat : Q(Lean.Expr)) (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.
                    Instances For
                      def Qq.Impl.mkIsDefEq (decls : List Qq.Impl.PatVarDecl) (pat : Q(Lean.Expr)) (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
                      Instances For
                        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(«$γ»)
                        Instances For
                          Equations
                          Instances For
                            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 : Q(Q(«$$ty»))) (discr : Q(Q(«$$ty»))) (alt : Q(«$m» «$γ»)) (expectedType : Lean.Expr) (k : Lean.ExprLean.Elab.TermElabM Q(«$m» «$γ»)) :
                            Lean.Elab.TermElabM Q(«$m» «$γ»)
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                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.
                                                Instances For

                                                  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.
                                                  Instances For
                                                    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