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

partial def Lean.Syntax.stripPos : Syntax → Syntax

structure Qq.Impl.PatVarDecl : Type

• ty : Option Q(Lean.Expr)
• fvarId : Lean.FVarId
• userName : Lean.Name

def Qq.Impl.PatVarDecl.fvarTy : PatVarDecl → Q(Type)

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 : PatVarDecl) : have a := decl.fvarTy; Q(«$a»)

Equations

• decl.fvar = Lean.Expr.fvar decl.fvarId

def Qq.Impl.mkIsDefEqType : List PatVarDecl → Q(Type)

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkIsDefEqType [] = q(Bool)

def Qq.Impl.mkIsDefEqResult (val : Bool) (decls : List PatVarDecl) : have a := mkIsDefEqType decls; Q(«$a»)

def Qq.Impl.mkIsDefEqResultVal (decls : List PatVarDecl) : (have a := mkIsDefEqType decls; Q(«$a»)) → Q(Bool)

Equations

• Qq.Impl.mkIsDefEqResultVal [] val = q(«$val»)
• Qq.Impl.mkIsDefEqResultVal ({ ty := none, fvarId := fvarId, userName := userName } :: decls) val = Qq.Impl.mkIsDefEqResultVal decls q(«$val».snd)
• Qq.Impl.mkIsDefEqResultVal ({ ty := some val_1, fvarId := fvarId, userName := userName } :: decls) val = Qq.Impl.mkIsDefEqResultVal decls q(«$val».snd)

def Qq.Impl.mkLambda' (n : Lean.Name) (fvar ty body : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Qq.Impl.mkLambda' n fvar ty body = do let __do_lift ← body.abstractM #[fvar] pure (Lean.mkLambda n Lean.BinderInfo.default ty __do_lift)

def Qq.Impl.mkLet' (n : Lean.Name) (fvar ty val body : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Qq.Impl.mkLet' n fvar ty val body = do let __do_lift ← body.abstractM #[fvar] pure (Lean.mkLet n ty val __do_lift)

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

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkInstantiateMVars decls [] = pure (have a := Qq.Impl.mkIsDefEqResult true decls; q(pure «$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»))

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Qq.Impl.mkIsDefEq decls pat discr = do let __do_lift ← Qq.Impl.mkIsDefEqCore decls pat discr decls pure (have a := __do_lift; q(Lean.Meta.withNewMCtxDepth «$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

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.replaceTempExprsByQVars [] x✝ = x✝
• Qq.Impl.replaceTempExprsByQVars ({ ty := none, fvarId := fvarId, userName := userName } :: decls) x✝ = Qq.Impl.replaceTempExprsByQVars decls x✝

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkNAryFunctionType 0 = Lean.Meta.mkFreshTypeMVar

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.getPatVars.isPatVar (fn : Lean.Syntax) : Bool

Equations

• Qq.Impl.getPatVars.isPatVar fn = (fn.isAntiquot && !fn.isEscapedAntiquot && fn.getAntiquotTerm.isIdent && fn.getAntiquotTerm.getId.isAtomic)

partial def Qq.Impl.getPatVars.mkMVar (fn : Lean.Syntax) (args : Array 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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

def Qq.Impl.term_comefrom_Do_In_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.term_comefrom_Do_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.doElemComefrom_Do_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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))

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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