max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: metaprogramming-arith: deduplicate

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-03 18:37:32 +02:00
parent 87431da7b1
commit f6e74c677e
1 changed files with 14 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
doc/metaprogramming-arith.md
View file

@ -15,12 +15,7 @@ building an arithmetic AST.
Here's the AST that we will be parsing:
```lean,ignore
-- example on parsing arith language via macros
inductive Arith : Type where
| add : Arith → Arith → Arith -- e + f
| mul : Arith → Arith → Arith -- e * f
| int : Int → Arith -- constant
| symbol : String → Arith -- variable
{{#include metaprogramming-arith.lean:1:5}}
```
We declare a syntax category to describe the grammar that we will be parsing.
@ -29,12 +24,7 @@ indicating that multiplication binds tighter than addition (higher the number, t
This allows us to declare _precedence_ when defining new syntax.
```lean,ignore
declare_syntax_cat arith
syntax num : arith -- int for Arith.int
syntax str : arith -- strings for Arith.symbol
syntax:60 arith:60 "+" arith:61 : arith -- Arith.add
syntax:70 arith:70 "*" arith:71 : arith -- Arith.mul
syntax "(" arith ")" : arith -- bracketed expressions
{{#include metaprogramming-arith.lean:7:13}}
```
Further, if we look at `syntax:60 arith:60 "+" arith:61 : arith`, the
@ -72,82 +62,48 @@ a precedence of `70` to `(a * b)`. This is compatible with addition which expect
**at least `60` ** (`70` is greater than `60`). Thus, the string `a * b + c` is parsed as `(a * b) + c`.
For more details, please look at the [Lean manual on syntax extensions](../syntax.md#notations-and-precedence).
To go from strings into `Arith`, We define a macro to
To go from strings into `Arith`, we define a macro to
translate the syntax category `arith` into an `Arith` inductive value that
lives in `term`:
```lean,ignore
-- auxiliary notation for translating `arith` into `term`
syntax "`[Arith| " arith "]" : term
{{#include metaprogramming-arith.lean:15:16}}
```
Our macro rules perform the "obvious" translation:
```lean,ignore
macro_rules
| `(`[Arith| $s:strLit ]) => `(Arith.symbol $s)
| `(`[Arith| $num:numLit ]) => `(Arith.int $num)
| `(`[Arith| $x:arith + $y:arith ]) => `(Arith.add `[Arith| $x] `[Arith| $y])
| `(`[Arith| $x:arith * $y:arith ]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
| `(`[Arith| ($x:arith) ]) => `(`[Arith| $x ])
{{#include metaprogramming-arith.lean:18:23}}
```
And some examples:
```lean,ignore
#check `[Arith| "x" * "y"] -- Arith.mul (Arith.symbol "x") (Arith.symbol "y") : Arith
#check `[Arith| "x" + "y"] -- add
-- Arith.add (Arith.symbol "x") (Arith.symbol "y")
#check `[Arith| "x" + 20] -- symbol + int
-- Arith.add (Arith.symbol "x") (Arith.int 20)
#check `[Arith| "x" + "y" * "z" ] -- precedence
Arith.add (Arith.symbol "x") (Arith.mul (Arith.symbol "y") (Arith.symbol "z"))
--
#check `[Arith| "x" * "y" + "z"] -- precedence
-- Arith.add (Arith.mul (Arith.symbol "x") (Arith.symbol "y")) (Arith.symbol "z")
#check `[Arith| ("x" + "y") * "z"] -- brackets
-- Arith.mul (Arith.add (Arith.symbol "x") (Arith.symbol "y")) (Arith.symbol "z")
{{#include metaprogramming-arith.lean:25:41}}
```
Writing variables as strings, such as `"x"` gets old; Wouldn't it be so much
Writing variables as strings, such as `"x"` gets old; wouldn't it be so much
prettier if we could write `x * y`, and have the macro translate this into `Arith.mul (Arith.Symbol "x") (Arith.mul "y")`?
We can do this, and this will be our first taste of manipulating macro variables --- we'll use `x.getId` instead of directly evaluating `$x`.
We also write a macro rule for `Arith|` that translates an identifier into
a string, using `$(Lean.quote (toString x.getId))`. (TODO: explain what
`Lean.quote` does):
a string, using `$(Lean.quote (toString x.getId))`:
```lean,ignore
syntax ident : arith
macro_rules
| `(`[Arith| $x:ident]) => `(Arith.symbol $(Lean.quote (toString x.getId)))
{{#include metaprogramming-arith.lean:43:46}}
```
Let's test and see that we can now write expressions such as `x * y` directly instead of having to write `"x" * "y"`:
```lean,ignore
#check `[Arith| x ] -- Arith.symbol "x"
def xPlusY := `[Arith| x + y]
#check xPlusY -- Arith.add (Arith.symbol "x") (Arith.symbol "y")
{{#include metaprogramming-arith.lean:48:51}}
```
We now show an unfortunate consequence of the above definitions. Suppose we want to build `(x + y) + z`.
Since we already have defined `xPlusY` as `x + y`, perhaps we should reuse it! Let's try:
```lean,ignore
#check `[Arith| xPlusY + z] -- Arith.add (Arith.symbol "xPlusY") (Arith.symbol "z")
#check `[Arith| xPlusY + z] -- Arith.add (Arith.symbol "xPlusY") (Arith.symbol "z")
```
Whoops, that didn't work! What happened? Lean treats `xPlusY` _itself_ as an identifier! So we need to add some syntax
@ -155,16 +111,13 @@ to be able to "escape" the `Arith|` context. Let's use the syntax `<[ $e:term ]>
not an identifier. The macro looks like follows:
```lean,ignore
syntax "<[" term "]>" : arith -- escape for embedding terms into `Arith`
macro_rules
| `(`[Arith| <[ $e:term ]> ]) => e
{{#include metaprogramming-arith.lean:53:56}}
```
Let's try our previous example:
```lean,ignore
#check `[Arith| <[ xPlusY ]> + z] -- Arith.add xPlusY (Arith.symbol "z")
{{#include metaprogramming-arith.lean:58:58}}
```
Perfect!