feat: macros and notations (#147)

Closes #69, #70, #71

Author: david-christiansen

.vale/scripts/rewrite_html.py

@@ -27,6 +27,8 @@ def process_html_file(filepath, output_filepath):
         if code_tag.next_sibling and code_tag.next_sibling.string and code_tag.next_sibling.string.startswith('th'):
             # Replace <code>XYZ</code>th with '5th'
             code_tag.replace_with("5")
+        elif code_tag.attrs and 'class' in code_tag.attrs and 'hl' in code_tag['class'] and 'lean' in code_tag['class']:
+            code_tag.decompose()
 
     # Delete docstring content (for now)
     for element in soup.find_all(class_="namedocs"):

.vale/styles/Lean/TechnicalTerms.yml

@@ -2,6 +2,7 @@ extends: substitution
 message: Use '%s' instead of '%s'
 level: error
 ignorecase: true
+capitalize: true
 swap:
   'typeclass': 'type class'
   'typeclasses': 'type classes'
@@ -19,3 +20,8 @@ swap:
   'semireducible': 'semi-reducible'
   '\b(.+)\b simps': 'non-terminal simps'
   '\babelian\b': 'Abelian'
+  'context free grammar': 'context-free grammar'
+  'left associative': 'left-associative'
+  'right associative': 'right-associative'
+  'pretty-printer': 'pretty printer'
+  'pretty printed': 'pretty-printed'

.vale/styles/config/ignore/terms.txt

@@ -2,6 +2,10 @@ Abelian
 Packrat
 accessor
 accessors
+antiquotation
+antiquotation's
+antiquotations
+antiquotations'
 bitvector
 bitvectors
 bitwise
@@ -15,6 +19,11 @@ cumulative
 cumulativity
 declaratively
 definitionally
+delaborate
+delaborated
+delaborates
+delaborating
+delaboration
 desugar
 desugared
 desugaring
@@ -28,6 +37,9 @@ enum
 equational
 extensional
 extensionality
+functor
+functor's
+functors
 guillemet
 guillemets
 hoc
@@ -38,6 +50,7 @@ initializers
 injectivity
 interoperate
 interoperates
+interrobang
 iterator
 iterator's
 iterators
@@ -53,21 +66,33 @@ metatheoretic
 metavariable
 metavariable's
 metavariables
+mixfix
 monoid
 monomorphic
 monomorphism
 multiset
 multisets
 namespace
 namespaces
+nonterminal
+nonterminals
 nullary
 parameters'
+parenthesization
+parenthesizer
+parenthesizers
+parser's
 polymorphic
 polymorphically
+postfix
 predicative
 predicativity
 prepending
 propositionally
+quasiquotation
+quasiquotations
+quasiquote
+quasiquoted
 recursor
 recursor's
 recursors
@@ -77,9 +102,9 @@ se
 semigroup
 semireducible
 simp
-simps
 simproc
 simprocs
+simps
 subgoal
 subgoals
 subproblem
@@ -100,4 +125,7 @@ toolchain's
 toolchains
 unary
 unescaped
+unexpander
+unexpanders
 uninstantiated
+unparenthesized

Manual.lean

@@ -44,6 +44,7 @@ tag := "monads-and-do"
 
 :::planned 102
 This chapter will describe `do`-notation in Lean:
+ * Overview of {deftech}[monads]
  * Desugaring of `do` and its associated control structures
  * Comprehensive description of the syntax of `do`-notation
  * Definition of being in the "same `do`-block"
@@ -85,6 +86,14 @@ Describe {name}`Option`, including the default coercions and its API.
 
 {include 0 Manual.NotationsMacros}
 
+# Output from Lean
+
+:::planned 122
+ * {deftech}[Unexpanders]
+ * {deftech key:="delaborate"}[Delaboration]
+ * {deftech}[Pretty printing]
+ * Parenthesizers
+:::
 
 # Elan
 %%%

Manual/Elaboration.lean

@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Manual.Meta
+import Manual.Papers
 
 open Verso.Genre Manual
 
@@ -14,27 +15,6 @@ set_option pp.rawOnError true
 open Lean (Syntax SourceInfo)
 
 
-def pratt73 : InProceedings where
-  title := .concat (inlines!"Top down operator precedence")
-  authors := #[.concat (inlines!"Vaughan Pratt")]
-  year := 1973
-  booktitle := .concat (inlines!"Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages")
-
-def carneiro19 : Thesis where
-  title := .concat (inlines!"The Type Theory of Lean")
-  author := .concat (inlines!"Mario Carneiro")
-  year := 2019
-  university := .concat (inlines!"Carnegie Mellon University")
-  url := some "https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf"
-  degree := .concat (inlines!"Masters thesis")
-
-def ullrich23 : Thesis where
-  title := .concat (inlines!"An Extensible Theorem Proving Frontend")
-  author := .concat (inlines!"Sebastian Ullrich")
-  year := 2023
-  university := .concat (inlines!"Karlsruhe Institute of Technology")
-  url := some "https://www.lean-lang.org/papers/thesis-sebastian.pdf"
-  degree := .concat (inlines!"Dr. Ing. dissertation")
 
 #doc (Manual) "Elaboration and Compilation" =>
 %%%
@@ -92,7 +72,7 @@ tag := "parser"
 Lean's parser is a recursive-descent parser that uses dynamic tables based on Pratt parsing{citep pratt73}[] to resolve operator precedence and associativity.
 When grammars are unambiguous, the parser does not need to backtrack; in the case of ambiguous grammars, a memoization table similar to that used in Packrat parsing avoids exponential blowup.
 Parsers are highly extensible: users may define new syntax in any command, and that syntax becomes available in the next command.
-The open namespaces in the current {tech}[scope] also influences which parsing rules are used, because parser extensions may be set to be active only when a given namespace is open.
+The open namespaces in the current {tech}[section scope] also influence which parsing rules are used, because parser extensions may be set to be active only when a given namespace is open.
 
 When ambiguity is encountered, the longest matching parse is selected.
 If there is no unique longest match, then both matching parses are saved in the syntax tree in a {deftech}[choice node] to be resolved later by the elaborator.
@@ -127,7 +107,7 @@ Elaboration of both commands and terms may be recursive, both because of command
 Command and term elaboration have different capabilities.
 Command elaboration may have side effects on an environment, and it has access to run arbitrary computations in {lean}`IO`.
 Lean environments contain the usual mapping from names to definitions along with additional data defined in {deftech}[environment extensions], which are additional tables associated with an environment; environment extensions are used to track most other information about Lean code, including {tactic}`simp` lemmas, custom pretty printers, and internals such as the compiler's intermediate representations.
-Command elaboration also maintains a message log with the contents of the compiler's informational output, warnings, and errors, a set of {tech}[info trees] that associate metadata with the original syntax (used for interactive features such as displaying proof states, identifier completion, and showing documentation), accumulated debugging traces, the open {tech}[scopes], and some internal state related to macro expansion.
+Command elaboration also maintains a message log with the contents of the compiler's informational output, warnings, and errors, a set of {tech}[info trees] that associate metadata with the original syntax (used for interactive features such as displaying proof states, identifier completion, and showing documentation), accumulated debugging traces, the open {tech}[section scopes], and some internal state related to macro expansion.
 Term elaboration may modify all of these fields except the open scopes.
 Additionally, it has access to all the machinery needed to create fully-explicit terms in the core language from Lean's terse, friendly syntax, including unification, type class instance synthesis, and type checking.
 

Manual/Intro.lean

@@ -153,6 +153,17 @@ skip
 
 Identifiers in code examples are hyperlinked to their documentation.
 
+Examples of code with syntax errors are shown with an indicator of where the parser stopped, along with the error message:
+```syntaxError intro
+def f : Option Nat → Type
+  | some 0 => Unit
+  | => Option (f t)
+  | none => Empty
+```
+```leanOutput intro
+<example>:3:4: expected term
+```
+
 ## Examples
 %%%
 tag := "example-boxes"

Manual/Language.lean

@@ -468,7 +468,7 @@ unknown universe level 'v'
 ```
 :::
 
-In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[scope] using the `universe` command.
+In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[section scope] using the `universe` command.
 
 :::syntax Lean.Parser.Command.universe
 ```grammar
@@ -712,19 +712,36 @@ tag := "scopes"
 
 ::: planned 54
 
-Many commands have an effect for the current {deftech key:="scope"}[_section scope_] (sometimes just called "scope" when clear).
+Many commands have an effect for the current {deftech}[_section scope_] (sometimes just called "scope" when clear).
 A section scope ends when a namespace ends, a section ends, or a file ends.
 They can also be anonymously and locally created via `in`.
 Section scopes track the following:
  * The {deftech}_current namespace_
- * The {deftech}_open namespaces_
+ * The {deftech key:="open namespace"}_open namespaces_
  * The values of all {deftech}_options_
  * Variable and universe declarations
 
 This section will describe this mechanism.
 
 :::
 
+:::syntax attrKind (open := false)
+Globally-scoped declarations (the default) are in effect whenever the {tech}[module] in which they're established is transitively imported.
+They are indicated by the absence of another scope modifier.
+```grammar
+```
+
+Locally-scoped declarations are in effect only for the extent of the {tech}[section scope] in which they are established.
+```grammar
+local
+```
+
+Scoped declarations are in effect whenever the {tech key:="open namespace"}[namespace] in which they are established is opened.
+```grammar
+scoped
+```
+:::
+
 # Axioms
 
 :::planned 78
@@ -774,6 +791,18 @@ This section will describe `partial` and `unsafe` definitions:
 
 :::
 
+# Attributes
+%%%
+tag := "attributes"
+%%%
+
+:::planned 144
+ * Concrete syntax of {deftech}[attributes]
+ * Use cases
+ * Scope
+ * When can they be added?
+:::
+
 {include 0 Manual.Language.Classes}
 
 # Dynamic Typing
@@ -785,3 +814,15 @@ This section will describe `partial` and `unsafe` definitions:
 {docstring Dynamic.mk}
 
 {docstring Dynamic.get?}
+
+# Coercions
+%%%
+tag := "coercions"
+%%%
+
+:::planned 146
+ * {deftech}[Coercions]
+ * When they are inserted
+ * Varieties of coercions
+ * When should each be used?
+:::

Manual/Language/Classes.lean

@@ -82,7 +82,7 @@ Here are some typical use cases for type classes:
  * A type class can represent a relation between two types that allows them to be used together in some novel way by a library.
    The {lean}`Coe` class represents automatically-inserted coercions from one type to another, and {lean}`MonadLift` represents a way to run operations with one kind of effect in a context that expects another kind.
  * Type classes can represent a framework of type-driven code generation, where instances for polymorphic types each contribute some portion of a final program.
-    The {name}`Repr` class defines a canonical pretty-printer for a type, and polymorphic types end up with polymorphic {name}`Repr` instances.
+    The {name}`Repr` class defines a canonical pretty printer for a type, and polymorphic types end up with polymorphic {name}`Repr` instances.
     When pretty printing is finally invoked on an expression with a known concrete type, such as {lean}`List (Nat × (String ⊕ Int))`, the resulting pretty printer contains code assembled from the {name}`Repr` instances for {name}`List`, {name}`Prod`, {name}`Nat`, {name}`Sum`, {name}`String`, and {name}`Int`.
 
 # Class Declarations
@@ -285,7 +285,6 @@ The problem is that a heap constructed with one {name}`Ord` instance may later b
 
 One way to correct this is to making the heap type depend on the selected `Ord` instance:
 ```lean
-
 structure Heap' (α : Type u) [Ord α] where
   contents : Array α
 

Manual/Language/Classes/InstanceSynth.lean

@@ -7,17 +7,14 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Manual.Meta
+import Manual.Papers
 
 
 open Manual
 open Verso.Genre
 open Verso.Genre.Manual
 
-def tabledRes : ArXiv where
-  title := .concat (inlines!"Tabled typeclass resolution")
-  authors := #[.concat (inlines!"Daniel Selsam"), .concat (inlines!"Sebastian Ullrich"), .concat (inlines!"Leonardo de Moura")]
-  year := 2020
-  id := "2001.04301"
+
 
 #doc (Manual) "Instance Synthesis" =>
 %%%

Manual/Language/Files.lean

@@ -87,7 +87,7 @@ tag := "keywords-and-identifiers"
 %%%
 
 
-An {deftech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier]
+An {tech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier]
 
 {deftech}[Identifier components] consist of a letter or letter-like character or an underscore (`'_'`), followed by zero or more identifier continuation characters.
 Letters are English letters, upper- or lowercase, and the letter-like characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, as well as the members of the Unicode letter-like symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations.