Skip to content

Commit

Permalink
doc: Add module docstrings and info about ~q()
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Jul 14, 2024
1 parent a7bfa63 commit 1312e90
Show file tree
Hide file tree
Showing 3 changed files with 116 additions and 1 deletion.
7 changes: 7 additions & 0 deletions Qq/Macro.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,13 @@ import Lean
import Qq.ForLean.ReduceEval
import Qq.ForLean.ToExpr
import Qq.Typ
/-!
# The `q( )` and `Q( )` macros
This file provides the main feature of `Qq`; the `q( )` and `Q( )` macros,
which are available with `open scoped Qq`.
-/

open Lean Meta Std

namespace Qq
Expand Down
83 changes: 82 additions & 1 deletion Qq/Match.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,54 @@ import Qq.Macro
import Qq.MetaM
import Qq.ForLean.Do
import Qq.SortLocalDecls
/-!
# `~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>) ``.
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 `Expr`s
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.
-/

open Lean in
partial def Lean.Syntax.stripPos : Syntax → Syntax
Expand Down Expand Up @@ -274,7 +322,40 @@ section

open Impl

scoped syntax "~q(" term ")" : term
/--
`Qq`s 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`.
-/
scoped syntax (name := matcher) "~q(" term ")" : term

partial def Impl.hasQMatch : Syntax → Bool
| `(~q($_)) => true
Expand Down
27 changes: 27 additions & 0 deletions Qq/MetaM.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,13 @@
import Qq.Macro
import Qq.Delab

/-!
# `Qq`-ified spellings of functions in `Lean.Meta`
This file provides variants of the function in the `Lean.Meta` namespace,
which operate with `Q(_)` instead of `Expr`.
-/

open Lean Elab Term Meta

namespace Qq
Expand Down Expand Up @@ -28,17 +35,35 @@ def elabTermEnsuringTypeQ (stx : Syntax) (expectedType : Q(Sort u))
TermElabM Q($expectedType) := do
elabTermEnsuringType stx (some expectedType) catchExPostpone implicitLambda errorMsgHeader?

/--
A `Qq`-ified version of `Lean.Meta.inferType`
Instead of writing `let α ← inferType e`, this allows writing `let ⟨u, α, e⟩ ← inferTypeQ e`,
which results in a context of
```
e✝ : Expr
u : Level
α : Q(Type u)
e : Q($α)
```
Here, the new `e` is defeq to the old one, but now has `Qq`-ascribed type information.
This is frequently useful when using the `~q` matching from `QQ/Match.lean`,
as it allows an `Expr` to be turned into something that can be matched upon.
-/
def inferTypeQ (e : Expr) : MetaM ((u : Level) × (α : Q(Sort $u)) × Q($α)) := do
let α ← inferType e
let .sort u ← whnf (← inferType α) | throwError "not a type{indentExpr α}"
pure ⟨u, α, e⟩

/-- If `e` is a `ty`, then view it as a term of `Q($ty)`. -/
def checkTypeQ (e : Expr) (ty : Q(Sort $u)) : MetaM (Option Q($ty)) := do
if ← isDefEq (← inferType e) ty then
return some e
else
return none

/-- The result of `Qq.isDefEqQ`; `MaybeDefEq a b` is an optional version of `$a =Q $b`. -/
inductive MaybeDefEq {α : Q(Sort $u)} (a b : Q($α)) where
| defEq : QuotedDefEq a b → MaybeDefEq a b
| notDefEq : MaybeDefEq a b
Expand All @@ -48,12 +73,14 @@ instance : Repr (MaybeDefEq a b) where
| .defEq _, prec => Repr.addAppParen "defEq _" prec
| .notDefEq, _ => "notDefEq"

/-- A version of `Lean.Meta.isDefEq` which returns a strongly-typed witness rather than a bool. -/
def isDefEqQ {α : Q(Sort $u)} (a b : Q($α)) : MetaM (MaybeDefEq a b) := do
if ← isDefEq a b then
return .defEq ⟨⟩
else
return .notDefEq

/-- Like `Qq.isDefEqQ`, but throws an error if not defeq. -/
def assertDefEqQ {α : Q(Sort $u)} (a b : Q($α)) : MetaM (PLift (QuotedDefEq a b)) := do
match ← isDefEqQ a b with
| .defEq witness => return ⟨witness⟩
Expand Down

0 comments on commit 1312e90

Please sign in to comment.