feat: terms and structural recursion (#207)

Closes #55

Author: david-christiansen

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

@@ -1,8 +1,7 @@
+APIs
 Abelian
 Kleisli
 Packrat
-accessor
-accessors
 antiquotation
 antiquotation's
 antiquotations
@@ -26,6 +25,9 @@ delaborated
 delaborates
 delaborating
 delaboration
+destructure
+destructured
+destructures
 desugar
 desugar
 desugared
@@ -34,6 +36,8 @@ desugaring
 desugaring
 desugarings
 desugars
+discriminant
+discriminant's
 disjointness
 disjunct
 disjuncts
@@ -66,6 +70,8 @@ letterlike
 lookup
 lookups
 macro_rules
+matcher
+matchers
 memoization
 metaprogram
 metaprogramming
@@ -142,3 +148,4 @@ unexpander
 unexpanders
 uninstantiated
 unparenthesized
+walkthrough

Manual/BasicTypes.lean

@@ -131,7 +131,7 @@ tag := "char-runtime"
 %%%
 
 
-In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a constructor or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed.
+In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a constructor or structure of type {lean}`Char` does not require indirection to access. In polymorphic contexts, characters are boxed.
 
 
 ## API Reference

Manual/Elaboration.lean

@@ -201,13 +201,16 @@ In practice, apparent non-termination is indistinguishable from sufficiently slo
 These metatheoretic properties are a result of having impredicativity, quotient types that compute, definitional proof irrelevance, and propositional extensionality; these features are immensely valuable both to support ordinary mathematical practice and to enable automation.
 
 # Elaboration Results
+%%%
+tag := "elaboration-results"
+%%%
 
 Lean's core type theory does not include pattern matching or recursive definitions.
 Instead, it provides low-level {tech}[recursors] that can be used to implement both case distinction and primitive recursion.
-Thus, the elaborator must translate definitions that use pattern matching and recursion into definitions that use recursors.
+Thus, the elaborator must translate definitions that use pattern matching and recursion into definitions that use recursors.{margin}[More details on the elaboration of recursive definitions is available in the {ref "recursive-definitions"}[dedicated section] on the topic.]
 This translation is additionally a proof that the function terminates for all potential arguments, because all functions that can be translated to recursors also terminate.
 
-The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to auxiliary functions that implement the particular case distinction that occurs in the code.
+The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to {deftech}_auxiliary matching functions_ that implement the particular case distinction that occurs in the code.
 These auxiliary functions are themselves defined using recursors, though they do not make use of the recursors' ability to actually implement recursive behavior.{margin}[They use the `casesOn` construction that is described in the {ref "recursor-elaboration-helpers"}[section on recursors and elaboration].]
 The term elaborator thus returns core-language terms in which pattern matching has been replaced with the use of special functions that implement case distinction, but these terms may still contain recursive occurrences of the function being defined.
 To see auxiliary pattern matching functions in Lean's output, set the option {option}`pp.match` to {lean}`false`.
@@ -251,11 +254,12 @@ This split is for three reasons:
  * The compiler can compile {ref "partial-unsafe"}[`partial` functions] that the kernel treats as opaque constants for the purposes of reasoning.
  * The compiler can also compile {ref "partial-unsafe"}[`unsafe` functions] that bypass the kernel entirely.
  * Translation to recursors does not necessarily preserve the cost model expected by programmers, in particular laziness vs strictness, but compiled code must have predictable performance.
+
 The compiler stores an intermediate representation in an environment extension.
 
 For straightforwardly structurally recursive functions, the translation will use the type's recursor.
 These functions tend to be relatively efficient when run in the kernel, their defining equations hold definitionally, and they are easy to understand.
-Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some measure decreases at each recursive call.
+Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some {deftech}_measure_ decreases at each recursive call.
 Lean can automatically derive many of these cases, but some require manual proofs.
 Well-founded recursion is more flexible, but the resulting functions are often slower to execute in the kernel due to the proof terms that show that a measure decreases, and their defining equations may hold only propositionally.
 To provide a uniform interface to functions defined via structural and well-founded recursion and to check its own correctness, the elaborator proves equational lemmas that relate the function to its original definition.
@@ -377,6 +381,26 @@ A C file is produced for each Lean module; these are then compiled to native cod
 If the `precompileModules` option is set in the build configuration, then this native code can be dynamically loaded and invoked by Lean; otherwise, an interpreter is used.
 For most workloads, the overhead of compilation is larger than the time saved by avoiding the interpreter, but some workloads can be sped up dramatically by pre-compiling tactics, language extensions, or other extensions to Lean.
 
+## Memory Allocation and Reference Counting
+
+:::planned 208
+
+The most important topics related to Lean's reference-counting-based allocator:
+
+ * Overview of {deftech key:="reference count"}_reference counting_
+
+ * Compact regions
+
+ * When are counts incremented and decremented?
+
+ * Tools for debugging uniqueness issues
+
+ * When should C code increment or decrement reference counts?
+
+ * What is the meaning of the borrow annotation (`@&`)?
+
+:::
+
 
 # Initialization
 

Manual/Language.lean

@@ -10,15 +10,19 @@ import Manual.Meta
 import Manual.Language.Classes
 import Manual.Language.Files
 import Manual.Language.Types
+import Manual.Language.RecursiveDefs
 
 import Lean.Parser.Command
 
-open Manual hiding «example»
+open Manual
 open Verso.Genre
 open Verso.Genre.Manual
-open Lean.Parser.Command (declModifiers «example»)
+
+
+open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
 set_option pp.rawOnError true
+set_option maxRecDepth 3000
 
 set_option linter.unusedVariables false
 
@@ -178,6 +182,7 @@ $_
 
 Describe signatures, including the following topics:
  * Explicit, implicit, instance-implicit, and strict implicit parameter binders
+ * {deftech key := "optional parameter"}[Optional] and {deftech}[automatic parameters]
  * {deftech}_Automatic implicit_ parameters
  * Argument names and by-name syntax
  * Which parts can be omitted where? Why?
@@ -193,6 +198,18 @@ The {deftech}[_header_] of a definition or declaration specifies the signature o
 * Mention interaction with autoimplicits
 :::
 
+## Namespaces
+%%%
+tag := "namespaces"
+%%%
+
+:::planned 210
+
+Describe {deftech}[namespaces], aliases, and the semantics of `export` and `open`.
+Which language features are controlled by the currently open namespaces?
+
+:::
+
 ## Section Scopes
 %%%
 tag := "scopes"
@@ -207,7 +224,7 @@ Section scopes track the following:
  * The {deftech}_current namespace_
  * The {deftech key:="open namespace"}_open namespaces_
  * The values of all {deftech}_options_
- * Variable and universe declarations
+ * {deftech}[Section variable] and universe declarations
 
 This section will describe this mechanism.
 
@@ -236,48 +253,11 @@ scoped
 Describe {deftech}_axioms_ in detail
 :::
 
-# Recursive Definitions
-
-## Structural Recursion
-::: planned 55
-This section will describe the specification of the translation to recursors.
-:::
-
-### Mutual Structural Recursion
-
-::: planned 56
-This section will describe the specification of the translation to recursors.
-:::
-
-## Well-Founded Recursion
-%%%
-tag := "well-founded-recursion"
-%%%
+{include 0 Manual.Language.RecursiveDefs}
 
-::: planned 57
-This section will describe the translation of {deftech}[well-founded recursion].
-:::
 
-## Controlling Reduction
 
-:::planned 58
-This section will describe {deftech}_reducibility_: {deftech}[reducible], {deftech}[semi-reducible], and {deftech}[irreducible] definitions.
-:::
 
-## Partial and Unsafe Recursive Definitions
-%%%
-tag := "partial-unsafe"
-%%%
-
-:::planned 59
-This section will describe `partial` and `unsafe` definitions:
-
-
- * Interaction with the kernel and elaborator
- * What guarantees are there, and what aren't there?
- * How to bridge from unsafe to safe code?
-
-:::
 
 # Attributes
 %%%

Manual/Language/Classes/BasicClasses.lean

@@ -37,6 +37,9 @@ Many Lean type classes exist in order to allow built-in notations such as additi
 {docstring LE}
 
 # Decidability
+%%%
+tag := "decidable-propositions"
+%%%
 
 A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index subterm:="decidable"}[proposition]
 The Law of the Excluded Middle means that every proposition is true or false, but it provides no way to check which of the two cases holds, which can often be useful.