From 84cc167f952f00080db33962ccc4b8fc463abcc8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 Apr 2022 19:05:43 +0200 Subject: [PATCH] doc: fix example code & style --- doc/SUMMARY.md | 2 +- doc/metaprogramming-arith.lean | 59 +++++++++++++++ doc/{tutorial => }/metaprogramming-arith.md | 80 +++------------------ 3 files changed, 68 insertions(+), 73 deletions(-) create mode 100644 doc/metaprogramming-arith.lean rename doc/{tutorial => }/metaprogramming-arith.md (70%) diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 10260b43b3..1aa45b0022 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -37,7 +37,7 @@ - [Macro Overview](./macro_overview.md) - [Examples](./syntax_examples.md) - [Parenthesized Terms](./syntax_example.md) - - [Arithmetic DSL](./tutorial/metaprogramming-arith.md) + - [Arithmetic DSL](./metaprogramming-arith.md) - [Declaring New Types](./decltypes.md) - [Enumerated Types](./enum.md) - [Inductive Types](./inductive.md) diff --git a/doc/metaprogramming-arith.lean b/doc/metaprogramming-arith.lean new file mode 100644 index 0000000000..6447300d63 --- /dev/null +++ b/doc/metaprogramming-arith.lean @@ -0,0 +1,59 @@ +-- example on parsing arith language via macros +inductive Arith : Type + | add : Arith → Arith → Arith -- e + f + | mul : Arith → Arith → Arith -- e * f + | int : Int → Arith -- constant + | symbol : String → Arith -- variable + +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 + +-- auxiliary notation for translating `arith` into `term` +syntax "`[Arith| " arith "]" : term + +macro_rules + | `(`[Arith| $s:str]) => `(Arith.symbol $s) + | `(`[Arith| $num:num]) => `(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]) + +#check `[Arith| "x" * "y"] -- mul +-- Arith.mul (Arith.symbol "x") (Arith.symbol "y") + +#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") + +syntax ident : arith + +macro_rules + | `(`[Arith| $x:ident]) => `(Arith.symbol $(Lean.quote (toString x.getId))) + +#check `[Arith| x] -- Arith.symbol "x" +def xPlusY := `[Arith| x + y] +#print xPlusY -- def xPlusY : Arith := Arith.add (Arith.symbol "x") (Arith.symbol "y") + +syntax "<[" term "]>" : arith -- escape for embedding terms into `Arith` + +macro_rules + | `(`[Arith| <[ $e:term ]>]) => pure e + + +#check `[Arith| <[ xPlusY ]> + z] -- Arith.add xPlusY (Arith.symbol "z") diff --git a/doc/tutorial/metaprogramming-arith.md b/doc/metaprogramming-arith.md similarity index 70% rename from doc/tutorial/metaprogramming-arith.md rename to doc/metaprogramming-arith.md index ed399b8873..db48ef8fd2 100644 --- a/doc/tutorial/metaprogramming-arith.md +++ b/doc/metaprogramming-arith.md @@ -139,17 +139,18 @@ Let's test and see that we can now write expressions such as `x * y` directly in ```lean,ignore #check `[Arith| x ] -- Arith.symbol "x" -#check `[Arith| x + y] -- Arith.add (Arith.symbol "x") (Arith.symbol "y") +def xPlusY := `[Arith| x + y] +#check xPlusY -- Arith.add (Arith.symbol "x") (Arith.symbol "y") ``` -We now show an unfortunate consequence of the above definitions. Suppose we want to build `(x + y) + z)`. -Since we already have defined `x_plus_y` as `x + y`, perhaps we should reuse it! Let's try: +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| x_plus_y + z] --Arith.add (Arith.symbol "x_plus_y") (Arith.symbol "z") +#check `[Arith| xPlusY + z] -- Arith.add (Arith.symbol "xPlusY") (Arith.symbol "z") ``` -Whoops, that didn't work! What happened? Lean treats `x_plus_y` _itself_ as an identifier! So we need to add some syntax +Whoops, that didn't work! What happened? Lean treats `xPlusY` _itself_ as an identifier! So we need to add some syntax to be able to "escape" the `Arith|` context. Let's use the syntax `<[ $e:term ]>` to mean: evaluate `$e` as a real term, not an identifier. The macro looks like follows: @@ -163,7 +164,7 @@ macro_rules Let's try our previous example: ```lean,ignore -#check `[Arith| <[ x_plus_y ]>] -- x_plus_y +#check `[Arith| <[ xPlusY ]> + z] -- Arith.add xPlusY (Arith.symbol "z") ``` Perfect! @@ -175,71 +176,6 @@ within a macro, and how to provide an escape from within the macro context. #### Full code listing ```lean --- example on parsing arith language via macros -inductive Arith: Type - | add : Arith → Arith → Arith -- e + f - | mul : Arith → Arith → Arith -- e * f - | int : Int → Arith -- constant - | symbol : String → Arith -- variable - -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 - --- auxiliary notation for translating `arith` into `term` -syntax "`[Arith| " arith "]" : term - -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 ]) - -def foo := -#check `[Arith| "x" * "y" ] -- mul --- Arith.mul (Arith.symbol "x") (Arith.symbol "y") - -def bar := -#check `[Arith| "x" + "y"] -- add --- Arith.add (Arith.symbol "x") (Arith.symbol "y") - -def baz := -#check `[Arith| "x" + 20] -- symbol + int --- Arith.add (Arith.symbol "x") (Arith.int 20) - -def quux_left := -#check `[Arith| "x" + "y" * "z" ] -- precedence --- Arith.add (Arith.symbol "x") (Arith.mul (Arith.symbol "y") (Arith.symbol "z")) - -def quux_right := -#check `[Arith| "x" * "y" + "z"] -- precedence --- Arith.add (Arith.mul (Arith.symbol "x") (Arith.symbol "y")) (Arith.symbol "z") - - -def quuz := -#check `[Arith| ("x" + "y") * "z"] -- brackets --- Arith.mul (Arith.add (Arith.symbol "x") (Arith.symbol "y")) (Arith.symbol "z") - -syntax ident : arith - -macro_rules - | `(`[Arith| $x:ident]) => `(Arith.symbol $(Lean.quote (toString x.getId))) - -#check `[Arith| x ] -- Arith.symbol "x" -#check `[Arith| x + y] -- Arith.add (Arith.symbol "x") (Arith.symbol "y") -#check `[Arith| x_plus_y + z] -- Arith.add (Arith.symbol "x_plus_y") (Arith.symbol "z") - -syntax "<[" term "]>" : arith -- escape for embedding terms into `Arith` - -macro_rules - | `(`[Arith| <[ $e:term ]> ]) => e - - -#check `[Arith| <[ x_plus_y ]>] -- x_plus_y +{{#include metaprogramming-arith.lean}} ```