From f6e74c677e5de4d5b9d4dffd7f2ba270152f0335 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 3 May 2022 18:37:32 +0200
Subject: [PATCH] doc: metaprogramming-arith: deduplicate

---
 doc/metaprogramming-arith.md | 75 +++++++-----------------------------
 1 file changed, 14 insertions(+), 61 deletions(-)

diff --git a/doc/metaprogramming-arith.md b/doc/metaprogramming-arith.md
index db48ef8fd2..de03cac28f 100644
--- a/doc/metaprogramming-arith.md
+++ b/doc/metaprogramming-arith.md
@@ -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!