diff --git a/Manual/Language.lean b/Manual/Language.lean index ea5accd..753f819 100644 --- a/Manual/Language.lean +++ b/Manual/Language.lean @@ -2,6 +2,7 @@ import VersoManual import Manual.Meta import Manual.Language.Files +import Manual.Language.InductiveTypes open Verso.Genre Manual @@ -15,14 +16,30 @@ set_option linter.unusedVariables false # Types +::: TODO +Basic framework of the type theory goes here. + +{deftech}[Canonical] type formers, definitional equality, types as first-class entities, large elimination +::: + ## Functions +::: TODO +Write this section. + +Topics: + * Dependent vs non-dependent {deftech}[function] types + * Eta equivalence + * Don't talk recursion (that goes in inductive types), but xref to it + * Syntax of anonymous functions with/without pattern matching + * Strictness +::: ## Propositions -Propositions are meaningful statements that admit proof. {index}[proposition] +{deftech}[Propositions] are meaningful statements that admit proof. {index}[proposition] Nonsensical statements are not propositions, but false statements are. -All propositions are classified by `Prop`. +All propositions are classified by {lean}`Prop`. Propositions have the following properties: @@ -45,8 +62,8 @@ Propositions have the following properties: ## Universes -Types are classified by _universes_. {index}[universe] -Each universe has a {deftech (key:="universe level")}[_level_], {index subterm := "of universe"}[level] which is a natural number. +Types are classified by {deftech}_universes_. {index}[universe] +Each universe has a {deftech (key:="universe level")}_level_, {index subterm := "of universe"}[level] which is a natural number. The {lean}`Sort` operator constructs a universe from a given level. {index}[`Sort`] If the level of a universe is smaller than that of another, the universe itself is said to be smaller. With the exception of propositions (described later in this chapter), types in a given universe may only quantify over types in smaller universes. @@ -59,7 +76,7 @@ example : Sort 5 := Sort 4 example : Sort 2 := Sort 1 ``` -On the other hand, `Sort 3` is not an element of `Sort 5`: +On the other hand, {lean}`Sort 3` is not an element of {lean}`Sort 5`: ```lean (error := true) (name := sort3) example : Sort 5 := Sort 3 ``` @@ -73,7 +90,7 @@ but is expected to have type Type 4 : Type 5 ``` -Similarly, because `Unit` is in `Sort 1`, it is not in `Sort 2`: +Similarly, because {lean}`Unit` is in {lean}`Sort 1`, it is not in {lean}`Sort 2`: ```lean example : Sort 1 := Unit ``` @@ -93,7 +110,7 @@ but is expected to have type Because propositions and data are used differently and are governed by different rules, the abbreviations {lean}`Type` and {lean}`Prop` are provided to make the distinction more convenient. {index}[`Type`] {index}[`Prop`] `Type u` is an abbreviation for `Sort (u + 1)`, so {lean}`Type 0` is {lean}`Sort 1` and {lean}`Type 3` is {lean}`Sort 4`. {lean}`Type 0` can also be abbreviated {lean}`Type`, so `Unit : Type` and `Type : Type 1`. -{lean}`Prop` is an abbreviation for `Sort 0`. +{lean}`Prop` is an abbreviation for {lean}`Sort 0`. ### Predicativity @@ -102,20 +119,33 @@ A function type's universe is determined by the universes of its argument and re The specific rules depend on whether the return type of the function is a proposition. Predicates, which are functions that return propositions (that is, where the result type of the function is some type in `Prop`) may have argument types in any universe whatsoever, but the function type itself remains in `Prop`. -In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions. -For example, proof irrelevance can be written as a proposition that quantifies over all propositions: +In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions (and all other types). + +:::example "Impredicativity" +Proof irrelevance can be written as a proposition that quantifies over all propositions: ```lean example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2 ``` +A proposition may also quantify over all types, at any given level: +```lean +example : Prop := ∀ (α : Type), ∀ (x : α), x = x +example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x +``` +::: + For universes at {tech key:="universe level"}[level] `1` and higher (that is, the `Type u` hierarchy), quantification is {deftech}[_predicative_]. {index}[predicative]{index subterm := "predicative"}[quantification] For these universes, the universe of a function type is the least upper bound of the argument and return types' universes. +:::example "Universe levels of function types" +Both of these types are in {lean}`Type 2`: ```lean example (α : Type 1) (β : Type 2) : Type 2 := α → β example (α : Type 2) (β : Type 1) : Type 2 := α → β ``` +::: +:::example "Predicativity of {lean}`Type`" This example is not accepted, because `α`'s level is greater than `1`. In other words, the annotated universe is smaller than the function type's universe: ```lean error := true name:=toosmall example (α : Type 2) (β : Type 1) : Type 1 := α → β @@ -128,8 +158,12 @@ has type but is expected to have type Type 1 : Type 2 ``` +::: + +Lean's universes are not {deftech}[cumulative];{index}[cumulativity] a type in `Type u` is not automatically also in `Type (u + 1)`. +Each type inhabits precisely one universe. -Lean's universes are not cumulative; a type in `Type u` is not automatically also in `Type (u + 1)`. +:::example "No cumulativity" This example is not accepted because the annotated universe is larger than the function type's universe: ```lean error := true name:=toobig example (α : Type 2) (β : Type 1) : Type 3 := α → β @@ -142,23 +176,29 @@ has type but is expected to have type Type 3 : Type 4 ``` +::: ### Polymorphism -Lean supports _universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters]. +Lean supports {deftech}_universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters]. These parameters can then be instantiated with universe levels when the constant is used. Universe parameters are written in curly braces following a dot after a constant name. +:::example "Universe-polymorphic identity function" When fully explicit, the identity function takes a universe parameter `u`. Its signature is: ```signature id.{u} {α : Sort u} (x : α) : α ``` +::: -Universe variables may additionally occur in universe level expressions, which provide specific universe levels in definitions. +Universe variables may additionally occur in {ref "level-expressions"}[universe level expressions], which provide specific universe levels in definitions. When the polymorphic definition is instantiated with concrete levels, these universe level expressions are also evaluated to yield concrete levels. -In this example, a structure is in a universe that is one greater than the universe of the type it contains: -```lean (keep := true) +::::keepEnv +:::example "Universe level expressions" + +In this example, {lean}`Codec` is in a universe that is one greater than the universe of the type it contains: +```lean structure Codec.{u} : Type (u + 1) where type : Type u encode : Array UInt32 → type → Array UInt32 @@ -179,8 +219,13 @@ def Codec.char : Codec where else failure ``` +::: +:::: Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values. + +:::example "Universe polymorhism is not first-class" + This can be seen in the following example, in which `T` is a gratuitously-universe-polymorphic definition that always returns the constructor of the unit type. Both instantiations of `T` have the same value, and both have the same type, but their differing universe instantiations make them incompatible: ```lean (error := true) (name := uniIncomp) (keep := false) @@ -199,14 +244,13 @@ but is expected to have type Eq.{1} T.{u} T.{v} : Prop ``` -```lean (error := false) (name := uniIncomp) (keep := false) +```lean (error := false) (keep := false) (show := false) -- check that the above statement stays true abbrev T : Unit := (fun (α : Type) => ()) Unit -set_option pp.universes true - def test : T = T := rfl ``` +::: Auto-bound implicit arguments are as universe-polymorphic as possible. Defining the identity function as follows: @@ -217,6 +261,8 @@ results in the signature: ```signature id'.{u} {α : Sort u} (x : α) : α ``` + +:::example "Universe monomorphism in auto-bound implicit" On the other hand, because {name}`Nat` is in universe {lean}`Type 0`, this function automatically ends up with a concrete universe level for `α`, because `m` is applied to both {name}`Nat` and `α`, so both must have the same type and thus be in the same universe: ```lean partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do @@ -237,8 +283,12 @@ info: count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool #guard_msgs in #check count ``` +::: #### Level Expressions +%%% +tag := "level-expressions" +%%% Levels that occur in a definition are not restricted to just variables and addition of constants. More complex relationships between universes can be defined using level expressions. @@ -256,29 +306,36 @@ The `imax` operation is defined as follows: $$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}`` -`imax` is used to implement impredicative quantification for {lean}`Prop`. +`imax` is used to implement {tech}[impredicative] quantification for {lean}`Prop`. In particular, if `A : Sort u` and `B : Sort v`, then `(x : A) → B : Sort (imax u v)`. -If `B : Prop`, then the function type is itself a `Prop`; otherwise, the function type's level is the maximum of `u` and `v`. +If `B : Prop`, then the function type is itself a {lean}`Prop`; otherwise, the function type's level is the maximum of `u` and `v`. #### Universe Variable Bindings Universe-polymorphic definitions bind universe variables. These bindings may be either explicit or implicit. -Explicit universe variable binding and instantiaion occurs as a suffix to the definition's name, as in the following declaration of `map`, which declares two universe parameters (`u` and `v`) and instantiates the polymorphic `List` with each in turn: -```lean (keep := false) -def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β - | [] => [] - | x :: xs => f x :: map f xs -``` +Explicit universe variable binding and instantiation occurs as a suffix to the definition's name. +Universe parameters are defined or provided by suffixing the name of a constant with a period (`.`) followed by a comma-separated sequence of universe variables between curly braces. -Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters: -```lean (keep := false) -def map.{u} {α : Type u} {β : Type v} (f : α → β) : List α → List β +::::keepEnv +:::example "Universe-polymorphic `map`" +The following declaration of {lean}`map` declares two universe parameters (`u` and `v`) and instantiates the polymorphic {name}`List` with each in turn: +```lean +def map.{u, v} {α : Type u} {β : Type v} + (f : α → β) : + List.{u} α → List.{v} β | [] => [] | x :: xs => f x :: map f xs ``` +::: +:::: -When the {TODO}[describe this option and add xref] `autoImplicit` option is set, it is not necessary to explicitly bind universe variables: +Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters. +When the {TODO}[describe this option and add xref] `autoImplicit` option is set to {lean}`true` (the default), it is not necessary to explicitly bind universe variables. +When it is set to {lean}`false`, then they must be added explicitly or declared using the `universe` command. {TODO}[xref] + +::: example "Auto-implicits and universe polymorphism" +When `autoImplicit` is {lean}`true` (which is the default setting), this definition is accepted even though it does not bind its universe parameters: ```lean (keep := false) set_option autoImplicit true def map {α : Type u} {β : Type v} (f : α → β) : List α → List β @@ -286,7 +343,7 @@ def map {α : Type u} {β : Type v} (f : α → β) : List α → List β | x :: xs => f x :: map f xs ``` -Without this setting, the definition is rejected because `u` and `v` are not in scope: +When `autoImplicit` is {lean}`false`, the definition is rejected because `u` and `v` are not in scope: ```lean (error := true) (name := uv) set_option autoImplicit false def map {α : Type u} {β : Type v} (f : α → β) : List α → List β @@ -299,6 +356,7 @@ unknown universe level 'u' ```leanOutput uv 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. @@ -309,17 +367,21 @@ universe $x:ident $xs:ident* Declares one or more universe variables for the extent of the current scope. -Just as the `variable` command causes a particular identifier to be treated as a parameter with a paricular type, the `universe` command causes the subsequent identifiers to be treated consistently as universe parameters, even if they are not mentioned in a signature or if the option `autoImplicit` is {lean}`false`. +Just as the `variable` command causes a particular identifier to be treated as a parameter with a particular type, the `universe` command causes the subsequent identifiers to be implicitly quantified as as universe parameters in declarations that mention them, even if the option `autoImplicit` is {lean}`false`. ::: -When `u` is declared to be a universe variable, it can be used as a parameter. +:::example "The `universe` command when `autoImplicit` is `false`" ```lean set_option autoImplicit false universe u def id₃ (α : Type u) (a : α) := a ``` +::: + +Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with `universe` even when `autoImplicit` is `true`. + +:::example "Automatic universe parameters and the `universe` command" -Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declaread with `universe` even when `autoImplicit` is `true`. This definition with an explicit universe parameter is accepted: ```lean (keep := false) def L.{u} := List (Type u) @@ -338,12 +400,14 @@ universe u def L := List (Type u) ``` The resulting definition of `L` is universe-polymorphic, with `u` inserted as a universe parameter. + Declarations in the scope of a `universe` command are not made polymorphic if the universe variables do not occur in them or in other automatically-inserted arguments. ```lean universe u def L := List (Type 0) #check L ``` +::: #### Universe Unification @@ -352,7 +416,7 @@ def L := List (Type 0) * Lack of injectivity ::: -## Inductive Types +{include 2 Language.InductiveTypes} # Organizational Features diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean index dd2a422..40bf9b5 100644 --- a/Manual/Language/Files.lean +++ b/Manual/Language/Files.lean @@ -128,7 +128,7 @@ Such identifier components may contain any character at all, aside from `'»'`, Some potential identifier components may be reserved keywords. The specific set of reserved keywords depends on the set of active syntax extensions, which may depend on the set of imported modules and the currently-opened {TODO}[xref/deftech for namespace] namespaces; it is impossible to enumerate for Lean as a whole. These keywords must also be quoted with guillemets to be used as identifier components in most syntactic contexts. -Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are _raw identifier_ contexts.{index (subterm:="raw")}[identifier] +Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier] Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers]. Hierarchical identifiers are used to represent both module names and names in a namespace. diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean new file mode 100644 index 0000000..52272d5 --- /dev/null +++ b/Manual/Language/InductiveTypes.lean @@ -0,0 +1,1219 @@ +import VersoManual + +import Manual.Meta + +open Verso.Genre Manual + +open Lean.Parser.Command («inductive» «structure» declValEqns computedField) + +#doc (Manual) "Inductive Types" => + +{deftech}_Inductive types_ are the primary means of introducing new types to Lean. +While {tech}[universes] and {tech}[functions] are built-in primitives that could not be added by users, every other {tech}[canonical] {TODO}[Harmonize terminology: "type constructor" is probably better] type former in Lean is an inductive type. +Inductive types are specified by their {deftech}_type constructors_ {index}[type constructor] and their {deftech}_constructors_; {index}[constructor] their other properties are derived from these. +Each inductive type has a single type constructor, which may take both {tech}[universe parameters] and ordinary parameters. +Inductive types may have any number of constructors; these constructors introduce new values whose types are headed by the inductive type's type constructor. + +Based on the type constructor and the constructors for an inductive type, Lean derives a {deftech}_recursor_{index}[recursor]{see "recursor"}[eliminator]. +Logically, recursors represent induction principles or elimination rules; computationally, they represent primitive recursive computations. +The termination of recursive functions is justified by translating them into uses of the recursors, so Lean's kernel only needs to perform type checking of recursor applications, rather than including a separate termination analysis. +Lean additionally produces a number of helper constructions based on the recursor, which are used elsewhere in the system. +{TODO}[Sidebar note: "recursor" is always used, even for non-recursive types] + +_Structures_ are a special case of inductive types that have exactly one constructor. +When a structure is declared, Lean generates helpers that enable additional language features to be used with the new structure. + +This section describes the specific details of the syntax used to specify both inductive types and structures, the new constants and definitions in the environment that result from inductive type declarations, and the run-time representation of inductive types' values in compiled code. + +# Inductive Type Declarations + + +:::syntax command (alias := «inductive») +```grammar +$_:declModifiers +inductive $d:declId $_:optDeclSig where + $[| $_ $c:ident $_]* +$[deriving $[$_ $[with $_]?],*]? +``` + +Declares a new inductive type. {TODO}[xref declmodifier docs] +::: + +After declaring an inductive type, its type constructor, constructors, and recursor are present in the environment. +New inductive types extend Lean's core logic—they are not encoded or represented by some other already-present data. +Inductive type declarations must satisfy a number of well-formedness requirements {TODO}[xref] to ensure that the logic remains consistent. + +The first line of the declaration, from {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`inductive` to {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`, specifies the new {tech}[type constructor]'s name and type. +If a type signature for the type constructor is provided, then its result type must be a {tech}[universe], but the parameters do not need to be types. +If no signature is provided, then Lean will infer a universe that's just big enough to contain the resulting type. + +The constructor specifications follow {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`. +Constructors are not mandatory, as constructorless datatypes such as {lean}`False` and {lean}`Empty` are perfectly sensible. +Each constructor specification begins with a vertical bar (`'|'`, Unicode `'VERTICAL BAR' (U+007c)`), declaration modifiers, and a name. +The name is a {tech}[raw identifier]. +A declaration signature follows the name. +The signature may specify any parameters, modulo the well-formedness requirements for inductive type declarations, but the return type of the signature must be in the inductive type being specified. +If no signature is provided, then the constructor's type is inferred by inserting sufficient implicit parameters to construct a well-formed return type. + +The new inductive type's name is prefixed by the {TODO}[xref] current namespace. +Each constructor's name is prefixed by the current namespace and the inductive type's name. + +## Parameters and Indices + +Type constructors may take two kinds of arguments: {deftech}_parameters_ and {deftech key:="index"}_indices_. +Parameters must be used consistently in the entire definition; all occurrences of the type constructor in each constructor in the declaration must take precisely the same argument. +Indices may vary among the occurrences of the type constructor. +All parameters must precede all indices in the type constructor's signature. + +Parameters that occur prior to the colon (`':'`) in the type constructor's signature are considered parameters to the entire inductive type declaration. +They are always parameters, while those that occur after the colon may by parameters or indices. +The distinction is inferred from the way in which they are used in the specifications of the constructors. + +## Example Inductive Types + +:::example "A constructorless type" +{lean}`Zero` is an empty datatype, equivalent to Lean's {lean}`Empty` type: +```lean +inductive Zero : Type where +``` + +Empty datatypes are not useless; they can be used to indicate unreachable code. +::: + +:::example "A constructorless proposition" +{lean}`No` is a false {tech}[proposition], equivalent to Lean's {lean}`False`: +```lean +inductive No : Prop where +``` + +```lean (show := false) (keep := false) +theorem no_is_false : No = False := by + apply propext + constructor <;> intro h <;> cases h +``` +::: + +:::example "A unit type" +{lean}`One` is equivalent to Lean's {lean}`Unit` type: +```lean +inductive One where + | one +``` +It is an example of an inductive type in which the signatures have been omitted for both the type constructor and the constructor. +Lean assigns {lean}`One` to {lean}`Type`: +```lean (name := OneTy) +#check One +``` +```leanOutput OneTy +One : Type +``` +The constructor is named {lean}`One.one`, because constructor names are the type constructor's namespace. +Because {lean}`One` expects no arguments, the signature inferred for {lean}`One.one` is: +```lean (name := oneTy) +#check One.one +``` +```leanOutput oneTy +One.one : One +``` +::: + + +:::example "A true proposition" +{lean}`Yes` is equivalent to Lean's {lean}`True` proposition: + +```lean +inductive Yes : Prop where + | intro +``` +Unlike {lean}`One`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe. +```lean (name := YesTy) +#check Yes +``` +```leanOutput YesTy +Yes : Prop +``` +The signature inferred for {lean}`Yes.intro` is: +```lean (name := yesTy) +#check Yes.intro +``` +```leanOutput yesTy +Yes.intro : Yes +``` + +```lean (show := false) (keep := false) +theorem yes_is_true : Yes = True := by + apply propext + constructor <;> intros <;> constructor +``` +::: + +::::example "A type with parameter and index" + +:::keepEnv +```lean (show:=false) +universe u +axiom α : Type u +axiom b : Bool +``` + +An {lean}`EvenOddList α b` is a list where {lean}`α` is the type of the data stored in the list and {lean}`b` is {lean}`true` when there are an even number of entries: +::: + +```lean +inductive EvenOddList (α : Type u) : Bool → Type u where + | nil : EvenOddList α true + | cons : α → EvenOddList α isEven → EvenOddList α (not isEven) +``` + +This example is well typed because there are two entries in the list: +```lean +example : EvenOddList String true := + .cons "a" (.cons "b" .nil) +``` + +This example is not well typed because there are three entries in the list: +```lean (error := true) (name := evenOddOops) +example : EvenOddList String true := + .cons "a" (.cons "b" (.cons "c" .nil)) +``` +```leanOutput evenOddOops +type mismatch + EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil)) +has type + EvenOddList String !!!true : Type +but is expected to have type + EvenOddList String true : Type +``` + +:::keepEnv +```lean (show:=false) +universe u +axiom α : Type u +axiom b : Bool +``` + +In this declaration, {lean}`α` is a {tech}[parameter], because it is used consistently in all occurrences of {name}`EvenOddList`. +{lean}`b` is an {tech}[index], because different {lean}`Bool` values are used for it at different occurrences. +::: + + +```lean (show:=false) (keep:=false) +def EvenOddList.length : EvenOddList α b → Nat + | .nil => 0 + | .cons _ xs => xs.length + 1 + +theorem EvenOddList.length_matches_evenness (xs : EvenOddList α b) : b = (xs.length % 2 = 0) := by + induction xs + . simp [length] + next b' _ xs ih => + simp [length] + cases b' <;> simp only [Bool.true_eq_false, false_iff, true_iff] <;> simp at ih <;> omega +``` +:::: + +:::::keepEnv +::::example "Parameters before and after the colon" + +In this example, both parameters are specified before the colon in {name}`Either`'s signature. + +```lean +inductive Either (α : Type u) (β : Type v) : Type (max u v) where + | left : α → Either α β + | right : α → Either α β +``` + +In this version, there are two types named `α` that might not be identical: +```lean (name := Either') (error := true) +inductive Either' (α : Type u) (β : Type v) : Type (max u v) where + | left : {α : Type u} → {β : Type v} → α → Either' α β + | right : α → Either' α β +``` +```leanOutput Either' +inductive datatype parameter mismatch + α +expected + α✝ +``` + +Placing the parameters after the colon results in parameters that can be instantiated by the constructors: +```lean (name := Either'') +inductive Either'' : Type u → Type v → Type (max u v) where + | left : {α : Type u} → {β : Type v} → α → Either'' α β + | right : α → Either'' α β +``` +{name}`Either''.right`'s type parameters are discovered via Lean's ordinary rules for unbound implicit arguments. {TODO}[xref] +:::: +::::: + + +## Anonymous Constructor Syntax + +If an inductive type has just one constructor, then this constructor is eligible for {deftech}_anonymous constructor syntax_. +Instead of writing the constructor's name applied to its arguments, the explicit arguments can be enclosed in angle brackets (`'⟨'` and `'⟩'`, Unicode `MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8)` and `MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)`) and separated with commas. +This works in both pattern and expression contexts. +Providing arguments by name or converting all implicit parameters to explicit with `@` requires using the ordinary constructor syntax. + +::::example "Anonymous constructors" + +:::keepEnv +```lean (show:=false) +axiom α : Type +``` +The type {lean}`AtLeastOne α` is similar to `List α`, except there's always at least one element present: +::: + +```lean +inductive AtLeastOne (α : Type u) : Type u where + | mk : α → Option (AtLeastOne α) → AtLeastOne α +``` + +Anonymous constructor syntax can be used to construct them: +```lean +def oneTwoThree : AtLeastOne Nat := + ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩ +``` +and to match against them: +```lean +def AtLeastOne.head : AtLeastOne α → α + | ⟨x, _⟩ => x +``` + +Equivalently, traditional constructor syntax could have been used: +```lean +def oneTwoThree' : AtLeastOne Nat := + .mk 1 (some (.mk 2 (some (.mk 3 none)))) + +def AtLeastOne.head' : AtLeastOne α → α + | .mk x _ => x +``` +:::: + + +## Deriving Instances + +The optional {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` clause of an inductive type declaration can be used to derive instances of type classes. +Please refer to {TODO}[write it!] the section on instance deriving for more information. + +:::TODO + * Deriving (just xref) + * Interaction with `variable` (xref) +::: + +# Structure Declarations + +:::syntax command +```grammar +$_:declModifiers +structure $d:declId $_:bracketedBinder* + $[extends $_,*]? $[: $_]? where + $[$_:declModifiers $_ ::]? + $_ +$[deriving $[$_ $[with $_]?],*]? +``` + +Declares a new structure type. +::: + +{deftech}[Structures] are non-recursive inductive types that have only a single constructor and no indices. +In exchange for these restrictions, Lean generates code for structures that offers a number of conveniences: accessor functions are generated for each field, an additional constructor syntax based on field names rather than positional arguments is available, a similar syntax may be used to replace the values of certain named fields, and structures may extend other structures. +Structures do not add any expressive power to Lean; all of their features are implemented in terms of code generation. + +```lean (show := false) +-- Test claim about non-recursive above +/-- error: unknown identifier 'RecStruct' -/ +#guard_msgs in +structure RecStruct where + next : Option RecStruct +``` + +## Structure Parameters + +Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe. +Structures may not define indexed families. {TODO}[insert this terminology earlier at the right spot] + +## Fields + +Each field of a structure declaration corresponds to a parameter of the constructor. +Auto-implicit arguments are inserted in each field separately, even if their names coincide, and the fields become constructor parameters that quantify over types. + +:::: example "Auto-implicit parameters in structure fields" + +The structure {lean}`MyStructure` contains a field whose type is an auto-implicit parameter: + +```lean +structure MyStructure where + field1 : α + field2 : α +``` +The type constructor {name}`MyStructure` takes two universe parameters: +```signature +MyStructure.{u, v} : Type (max u v) +``` +The resulting type is in `Type` rather than `Sort` because the constructor fields quantify over types in `Sort`. In particular, both fields in its constructor {name}`MyStructure.mk` take an implicit type parameter: +```signature +MyStructure.mk.{u, v} + (field1 : {α : Sort u} → α) + (field2 : {α : Sort v} → α) + : MyStructure.{u,v} +``` + +:::: + + +For each field, a {deftech}[projection function] is generated that extracts the field's value from the underlying datatype's constructor. +This function is in the structure's name's namespace. +Structure field projections are handled specially by the elaborator (as described in the {ref "structure-inheritance"}[section on structure inheritance]), which performs extra steps beyond looking up a namespace. +When field types depend on prior fields, the types of the dependent projection functions are written in terms of earlier projections, rather than explicit pattern matching. + + +:::: example "Dependent projection types" + +The structure {lean}`ArraySized` contains a field whose type depends on both a structure parameter and an earlier field: +```lean +structure ArraySized (α : Type u) (length : Nat) where + array : Array α + size_eq_length : array.size = length +``` + +The signature of the projection function {name ArraySized.size_eq_length}`size_eq_length` takes the structure type's parameter as an implicit parameter and refers to the earlier field using the corresponding projection: +```signature +ArraySized.size_eq_length.{u} + {α : Type u} {length : Nat} + (self : ArraySized α length) + : self.array.size = length +``` + +:::: + +Structure fields may have default values, specified with `:=`. +These values are used if no explicit value is provided. + + +::: example "Default values" + +An adjacency list representation of a graph can be represented as an array of lists of {lean}`Nat`. +The size of the array indicates the number of vertices, and the outgoing edges from each vertex are stored in the array at the vertex's index. +Because the default value {lean}`#[]` is provided for the field {name Graph.adjacency}`adjacency`, the empty graph {lean}`Graph.empty` can be constructed without providing any field values. +```lean +structure Graph where + adjacency : Array (List Nat) := #[] + +def Graph.empty : Graph := {} +``` +::: + + +Structure fields may additionally be accessed via their index, using dot notation. +Fields are numbered beginning with `1`. + + +## Structure Constructors + +Structure constructors may be explicitly named by providing the constructor name and `::` prior to the fields. +If no name is explicitly provided, then the constructor is named `mk` in the structure type's namespace. +Declaration modifiers {TODO}[xref] may additionally be provided along with an explicit constructor name. + +::: example "Non-default constructor name" +The structure {lean}`Palindrome` contains a string and a proof that the string is the same when reversed: + +```lean +structure Palindrome where + ofString :: + text : String + is_palindrome : text.data.reverse = text.data +``` + +Its constructor is named {name}`Palindrome.ofString`, rather than `Palindrome.mk`. + +::: + +::: example "Modifiers on structure constructor" +The structure {lean}`NatStringBimap` maintains a finite bijection between natural numbers and strings. +It consists of a pair of maps, such that the keys each occur as values exactly once in the other map. +Because the constructor is private, code outside the defining module can't construct new instances and must use the provided API, which maintains the invariants of the datatype. +Additionally, providing the default constructor name explicitly is an opportunity to attach a {TODO}[xref] documentation comment to the constructor. + +```lean +structure NatStringBimap where + /-- Build a finite bijection between some natural numbers and strings -/ + private mk :: + natToString : Std.HashMap Nat String + stringToNat : Std.HashMap String Nat + +def NatStringBimap.insert (nat : Nat) (string : String) (map : NatStringBimap) : Option NatStringBimap := + if map.natToString.contains nat || map.stringToNat.contains string then + none + else + some (NatStringBimap.mk (map.natToString.insert nat string) (map.stringToNat.insert string nat)) +``` +::: + +Because structures are represented by single-constructor inductive types, their constructors can be invoked or matched against using {tech}[anonymous constructor syntax]. +Additionally, structures may be constructed or matched against using the names of the fields together with values for them. + +:::syntax term + +```grammar +{ $_,* + $[: $ty:term]? } +``` + +Constructs a value of a constructor type given values for named fields. +Field specifiers may take two forms: +```grammar (of := Lean.Parser.Term.structInstField) +$x := $y +``` + +```grammar (of := Lean.Parser.Term.structInstFieldAbbrev) +$f:ident +``` + +A `structInstLVal` {TODO}[role for nonterminals] is a field name (an identifier), a field index (a natural number), or a term in square brackets, followed by a sequence of zero or more subfields. +Subfields are either a field name or index preceded by a dot, or a term in square brackets. + +This syntax is elaborated to applications of structure constructors. +The values provided for fields are by name, and they may be provided in any order. +The values provided for subfields are used to initialize fields of constructors of structures that are themselves found in fields. +Terms in square brackets are not allowed when constructing a structure; they are used in structure updates. + +Field specifiers that do not contain `:=` are field abbreviations. +In this context, the identifier `f` is an abbreviation for `f := f`; that is, the value of `f` in the current scope is used to initialize the field `f`. + +Every field that does not have a default value must be provided. +If a tactic is specified as the default argument, then it is run at elaboration time to construct the argument's value. + +In a pattern context, field names are mapped to patterns that match the corresponding projection, and field abbreviations bind a pattern variable that is the field's name. +Default arguments are still present in patterns; if a pattern does not specify a value for a field with a default value, then the pattern only matches the default. + +The optional type annotation allows the structure type to be specified in contexts where it is not otherwise determined. +::: + +:::example "Patterns and default values" +The structure {name}`AugmentedIntList` contains a list together with some extra information, which is empty if omitted: +```lean +structure AugmentedIntList where + list : List Int + augmentation : String := "" +``` + +When testing whether the list is empty, the function {name AugmentedIntList.isEmpty}`isEmpty` is also testing whether the {name AugmentedIntList.augmentation}`augmentation` field is empty, because the omitted field's default value is also used in pattern contexts: +```lean (name := isEmptyDefaults) +def AugmentedIntList.isEmpty : AugmentedIntList → Bool + | {list := []} => true + | _ => false + +#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty +``` +```leanOutput isEmptyDefaults +false +``` +::: + + +:::syntax term +```grammar +{$e:term with + $_,* + $[: $ty:term]?} +``` +Updates a value of a constructor type. +The term that precedes the {keywordOf Lean.Parser.Term.structInst}`with` clause is expected to have a structure type; it is the value that is being updated. +A new instance of the structure is created in which every field not specified is copied from the value that is being updated, and the specified fields are replaced with their new values. +When updating a structure, array values may also be replaced by including the index to be updated in square brackets. +This updating does not require that the index expression be in bounds for the array, and out-of-bounds updates are discarded. +::: + +::::example "Updating arrays" +:::keepEnv +Updating structures may use array indices as well as projection names. +Updates at indices that are out of bounds are ignored: + +```lean name:=arrayUpdate +structure AugmentedIntArray where + array : Array Int + augmentation : String := "" +deriving Repr + +def one : AugmentedIntArray := {array := #[1]} +def two : AugmentedIntArray := {one with array := #[1, 2]} +def two' : AugmentedIntArray := {two with array[0] := 2} +def two'' : AugmentedIntArray := {two with array[99] := 3} +#eval (one, two, two', two'') +``` +```leanOutput arrayUpdate +({ array := #[1], augmentation := "" }, + { array := #[1, 2], augmentation := "" }, + { array := #[2, 2], augmentation := "" }, + { array := #[1, 2], augmentation := "" }) +``` +::: +:::: + +Values of structure types may also be declared using {keywordOf Lean.Parser.Command.declaration (parser:=declValEqns)}`where`, followed by definitions for each field. +This may only be used as part of a definition, not in an expression context. + +::::example "`where` for structures" +:::keepEnv +The product type in Lean is a structure named {name}`Prod`. +Products can be defined using their projections: +```lean +def location : Float × Float where + fst := 22.807 + snd := -13.923 +``` +::: +:::: + +## Structure Inheritance +%%% +tag := "structure-inheritance" +%%% + +Structures may be declared as extending other structures using the optional {keywordOf Lean.Parser.Command.declaration (parser:=«structure»)}`extends` clause. +The resulting structure type has all of the fields of all of the parent structure types. +If the parent structure types have overlapping field names, then all overlapping field names must have the same type. +If the overlapping fields have different default values, then the default value from the last parent structure that includes the field is used. +New default values in the child structure take precedence over default values from the parent structures. + +```lean (show := false) (keep := false) +-- If the overlapping fields have different default values, then the default value from the last parent structure that includes the field is used. +structure Q where + x : Nat := 0 +deriving Repr +structure Q' where + x : Nat := 3 +deriving Repr +structure Q'' extends Q, Q' +deriving Repr +structure Q''' extends Q', Q +deriving Repr + +/-- info: 3 -/ +#guard_msgs in +#eval ({} : Q'').x +/-- info: 0 -/ +#guard_msgs in +#eval ({} : Q''').x +``` + +When the new structure extends existing structures, the new structure's constructor takes the existing structure's information as additional arguments. +Typically, this is in the form of a constructor parameter for each parent structure type. +If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead to prevent duplicating field information. + + +There is no subtyping relation between a parent structure type and its children. +Even if structure `B` extends structure `A`, a function expecting an `A` will not accept a `B`. +However, conversion functions are generated that convert a structure into each of its parents. +These conversion functions are in the child structure's namespace, and their name is the parent structure's name preceded by `to`. + +::: example "Structure type inheritance with overlapping fields" +In this example, a {lean}`Textbook` is a {lean}`Book` that is also an {lean}`AcademicWork`: + +```lean +structure Book where + title : String + author : String + +structure AcademicWork where + author : String + discipline : String + +structure Textbook extends Book, AcademicWork + +#check Textbook.toBook +``` + +Because the field `author` occurs in both {lean}`Book` and {lean}`AcademicWork`, the constructor {name}`Textbook.mk` does not take both parents as arguments. +Its signature is: +```signature +Textbook.mk (toBook : Book) (discipline : String) : Textbook +``` + +The conversion functions are: +```signature +Textbook.toBook (self : Textbook) : Book +``` +```signature +Textbook.toAcademicWork (self : Textbook) : AcademicWork +``` + +The latter combines the `author` field of the included {lean}`Book` with the unbundled `Discipline` field, and is equivalent to: +```lean +def toAcademicWork (self : Textbook) : AcademicWork := + let .mk book discipline := self + let .mk _title author := book + .mk author discipline +``` +```lean (show := false) +-- check claim of equivalence +example : toAcademicWork = Textbook.toAcademicWork := by + funext b + cases b + dsimp [toAcademicWork] +``` + +::: + +The resulting structure's projections can be used as if its fields are simply the union of the parents' fields. +The Lean elaborator automatically generates an appropriate accessor when it encounters a projection. +Likewise, the field-based initialization and structure update notations hide the details of the encoding of inheritance. +The encoding is, however, visible when using the constructor's name, when using {tech}[anonymous constructor syntax], or when referring to fields by their index rather than their name. + +:::: example "Field indices and structure inheritance" + +```lean +structure Pair (α : Type u) where + fst : α + snd : α +deriving Repr + +structure Triple (α : Type u) extends Pair α where + thd : α +deriving Repr + +def coords : Triple Nat := {fst := 17, snd := 2, thd := 95} +``` + +Evaluating the first field index of {name}`coords` yields the underlying {name}`Pair`, rather than the contents of the field `fst`: +```lean name:=coords1 +#eval coords.1 +``` +```leanOutput coords1 +{ fst := 17, snd := 2 } +``` + +The elaborator translates {lean}`coords.fst` into {lean}`coords.toPair.fst`. + +````lean (show := false) (keep := false) +example (t : Triple α) : t.fst = t.toPair.fst := rfl +```` +:::: + +:::: example "No structure subtyping" +:::keepEnv +Given these definitions of even numbers, even prime numbers, and a concrete even prime: +```lean +structure EvenNumber where + val : Nat + isEven : 2 ∣ val := by decide + +structure EvenPrime extends EvenNumber where + notOne : val ≠ 1 := by decide + isPrime : ∀ n, n ≤ val → n ∣ val → n = 1 ∨ n = val + +def two : EvenPrime where + val := 2 + isPrime := by + intros + dsimp only at * + repeat' (cases ‹Nat.le _ _›) + all_goals omega + +def printEven (num : EvenNumber) : IO Unit := + IO.print num.val +``` +it is a type error to apply {name}`printEven` directly to {name}`two`: +```lean (error := true) (name := printTwo) +#check printEven two +``` +```leanOutput printTwo +application type mismatch + printEven two +argument + two +has type + EvenPrime : Type +but is expected to have type + EvenNumber : Type +``` +because values of type {name}`EvenPrime` are not also values of type {name}`EvenNumber`. +::: +:::: + + +```lean (show := false) (keep := false) +structure A where + x : Nat + y : Int +structure A' where + x : Int +structure B where + foo : Nat +structure C extends A where + z : String +/-- info: C.mk (toA : A) (z : String) : C -/ +#guard_msgs in +#check C.mk + +def someC : C where + x := 1 + y := 2 + z := "" + +/-- +error: type mismatch + someC +has type + C : Type +but is expected to have type + A : Type +-/ +#guard_msgs in +#check (someC : A) + +structure D extends A, B where + z : String +/-- info: D.mk (toA : A) (toB : B) (z : String) : D -/ +#guard_msgs in +#check D.mk +structure E extends A, B where + x := 44 + z : String +/-- info: E.mk (toA : A) (toB : B) (z : String) : E -/ +#guard_msgs in +#check E.mk +/-- +error: parent field type mismatch, field 'x' from parent 'A'' has type + Int : Type +but is expected to have type + Nat : Type +-/ +#guard_msgs in +structure F extends A, A' where + + + +``` + +# Logical Model + +## Recursors + +Every inductive type is equipped with a {tech}[recursor]. +The recursor is completely determined by the signatures of the type constructor and the constructors. +Recursors have function types, but they are primitive and are not definable using `fun`. + +### Recursor Types + +The recursor takes the following parameters: +: The inductive type's {tech}[parameters] + + Because parameters are consistent, they can be abstracted over the entire recursor + +: The {deftech}_motive_ + + The motive determines the type of an application of the recursor. The motive is a function whose arguments are the type's indices and an instance of the type with these indices instantiated. The specific universe for the type that the motive determines depends on the inductive type's universe and the specific constructors—see the section on {ref "subsingleton-elimination"}[{tech}[subsingleton] elimination] for details. + +: A case for each constructor + + For each constructor, the recursor expects a function that satisfies the motive for an arbitrary application of the constructor. Each case abstracts over all of the constructor's parameters. If the constructor's parameter's type is the inductive type itself, then the case additionally takes a parameter whose type is the motive applied to that parameter's value—this will receive the result of recursively processing the recursive parameter. + +: The target + + Finally, the recursor takes an instance of the type as an argument, along with any index values. + +The result type of the recursor is the motive applied to these indices and the target. + +:::example "The recursor for {lean}`Bool`" +{lean}`Bool`'s recursor {lean}`Bool.rec` has the following parameters: + + * The motive computes a type in any universe, given a Bool. + * There are cases for both constructors, in which the motive is satisfied for both {lean}`false` and {lean}`true`. + * The target is some {lean}`Bool`. + +The return type is the motive applied to the target. + +```signature +Bool.rec.{u} {motive : Bool → Sort u} + (false : motive false) + (true : motive true) + (t : Bool) : motive t +``` +::: + +::::example "The recursor for {lean}`List`" +{lean}`List`'s recursor {lean}`List.rec` has the following parameters: + +:::keepEnv +```lean (show := false) +axiom α.{u} : Type u +``` + + * The parameter {lean}`α` comes first, because the parameter and the cases need to refer to it + * The motive computes a type in any universe, given a {lean}`List α`. There is no connection between the universe levels `u` and `v`. + * There are cases for both constructors: + - The motive is satisfied for {name}`List.nil` + - The motive should be satisfiable for any application of {name}`List.cons`, given that it is satisfiable for the tail. The extra parameter `motive tail` is because `tail`'s type is a recursive occurrence of {name}`List`. + * The target is some {lean}`List α`. +::: + +Once again, the return type is the motive applied to the target. + +```signature +List.rec.{u, v} {α : Type v} {motive : List α → Sort u} + (nil : motive []) + (cons : (head : α) → (tail : List α) → motive tail → + motive (head :: tail)) + (t : List α) : motive t +``` +:::: + + +::::example "The recursor for {name}`EvenOddList`" +The recursor {name}`EvenOddList.rec` is very similar to that for `List`. +The difference comes from the presence of the index: + * The motive now abstracts over any arbitrary choice of index. + * The case for {name EvenOddList.nil}`nil` applies the motive to {name EvenOddList.nil}`nil`'s index value `true`. + * The case for {name EvenOddList.cons}`cons` abstracts over the index value used in its recursive occurrence, and instantiates the motive with its negation. + * The target additionally abstracts over an arbitrary choice of index. + +```signature +EvenOddList.rec.{u, v} {α : Type v} + {motive : (isEven : Bool) → EvenOddList α isEven → Sort u} + (nil : motive true EvenOddList.nil) + (cons : {isEven : Bool} → + (head : α) → + (tail : EvenOddList α isEven) → motive isEven tail → + motive (!isEven) (EvenOddList.cons head tail)) : + {isEven : Bool} → (t : EvenOddList α isEven) → motive isEven t +``` +:::: + +When using a predicate (that is, a function that returns a {lean}`Prop`) for the motive, recursors express induction. +The cases for non-recursive constructors are the base cases, and the additional arguments supplied to constructors with recursive arguments are the induction hypotheses. + +### Subsingleton Elimination +%%% +tag := "subsingleton-elimination" +%%% + +Proofs in Lean are computationally irrelevant. +In other words, having been provided with *some* proof of a proposition, it should be impossible for a program to check *which* proof it has received. +This is reflected in the types of recursors for inductively defined propositions or predicates. +For these types, if there's more than one potential proof of the theorem then the motive may only return another {lean}`Prop`. +If the type is structured such that there's only at most one proof anyway, then the motive may return a type in any universe. +A proposition that has at most one inhabitant is called a {deftech}_subsingleton_. +Rather than obligating users to _prove_ that there's only one possible proof, a conservative syntactic overapproximation is used to check whether a proposition is a subsingleton. +Propositions that fulfill both of the following requirements are considered to be subsingletons: + * There is at most one constructor. + * Each of the constructor's parameter types is either a {lean}`Prop`, a parameter, or an index. + +:::example "{lean}`True` is a subsingleton" +{lean}`True` is a subsingleton because it has one constructor, and this constructor has no parameters. +Its recursor has the following signature: +```signature +True.rec.{u} {motive : True → Sort u} + (intro : motive True.intro) + (t : True) : motive t +``` +::: + +:::example "{lean}`False` is a subsingleton" +{lean}`False` is a subsingleton because it has no constructors. +Its recursor has the following signature: +```signature +False.rec.{u} (motive : False → Sort u) (t : False) : motive t +``` +Note that the motive is an explicit parameter. +This is because it is not mentioned in any further parameters' types, so it could not be solved by unification. +::: + + +:::example "{name}`And` is a subsingleton" +{lean}`And` is a subsingleton because it has one constructor, and both of the constructor's parameters's types are propositions. +Its recursor has the following signature: +```signature +And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u} + (intro : (left : a) → (right : b) → motive (And.intro left right)) + (t : a ∧ b) : motive t +``` +::: + +:::example "{name}`Or` is not a subsingleton" +{lean}`Or` is not a subsingleton because it has more than one constructor. +Its recursor has the following signature: +```signature +Or.rec {a b : Prop} {motive : a ∨ b → Prop} + (inl : ∀ (h : a), motive (.inl h)) + (inr : ∀ (h : b), motive (.inr h)) + (t : a ∨ b) : motive t +``` +The motive's type indicates that it can only be used to recursor into other propositions. +A proof of a disjunction can be used to prove something else, but there's no way for a program to inspect _which_ of the two disjuncts was true and used for the proof. +::: + +:::example "{name}`Eq` is a subsingleton" +{lean}`Eq` is a subsingleton because it has just one constructor, {name}`Eq.refl`. +This constructor instantiates {lean}`Eq`'s index with a parameter value, so all arguments are parameters: +```signature +Eq.refl.{u} {α : Sort u} (x : α) : Eq x x +``` + +Its recursor has the following signature: +```signature +Eq.rec.{u, v} {α : Sort v} {x : α} + {motive : (y : α) → x = y → Sort u} + (refl : motive x (.refl x)) + {y : α} (t : x = y) : motive y t +``` +This means that proofs of equality can be used to rewrite the types of non-propositions. +::: + +### Reduction + +In addition to adding new constants to the logic, inductive datatype declarations also add new reduction rules. +These rules govern the interaction between recursors and constructors; specifically recursors that have constructors as their targets. +This form of reduction is called {deftech}_ι-reduction_ (iota reduction){index}[ι-reduction]{index (subterm:="ι (iota)")}[reduction]. + +When the recursor's target is a constructor with no recursive parameters, the recursor application reduces to an application of the constructor's case to the constructor's arguments. +If there are recursive parameters, then these arguments to the case are found by applying the recursor to the recursive occurrence. + +## Well-Formedness Requirements + +Inductive datatype declarations are subject to a number of well-formedness requirements. +These requirements ensure that Lean remains consistent as a logic when it is extended with the inductive type's new rules. +They are conservative: there exist potential inductive types that do not undermine consistency, but that these requirements nonetheless reject. + +### Universe Levels + +Type constructors of inductive types must either inhabit a {tech}[universe] or a function type whose return type is a universe. +Each constructor must inhabit a function type that returns a saturated application of the inductive type. +If the inductive type's universe is {lean}`Prop`, then there are no further restrictions on universes. +If the is not {lean}`Prop`, then the following must hold for each parameter to the constructor: + * If the constructor's parameter is a parameter (in the sense of parameters vs indices) of the inductive type, then this parameter's type may be no larger than the type constructor's universe. + * All other constructor parameters must be smaller than the type constructor's universe. + + +::::example "Universes, constructors, and parameters" +{lean}`Either` is in the greater of its arguments' universes, because both are parameters to the inductive type: +```lean +inductive Either (α : Type u) (β : Type v) : Type (max u v) where + | inl : α → Either α β + | inr : β → Either α β +``` + +{lean}`CanRepr` is in a larger universe than the constructor parameter `α`, because `α` is not one of the inductive type's parameters: +```lean +inductive CanRepr : Type (u + 1) where + | mk : (α : Type u) → [Repr α] → CanRepr +``` + +Constructorless inductive types may be in universes smaller than their parameters: +```lean +inductive Spurious (α : Type 5) : Type 0 where +``` +It would, however, be impossible to add a constructor to {name}`Spurious` without changing its levels. +:::: + +### Strict Positivity + +All occurrences of the type being defined in the types of the parameters of the constructors must be in {deftech}_strictly positive_ positions. +A position is strictly positive if it is not in a function's argument type (no matter how many function types are nested around it) and it is not an argument of any expression other than type constructors of inductive types. +This restriction rules out unsound inductive type definitions, at the cost of also ruling out some unproblematic ones. + +::::example "Non-strictly-positive inductive types" +:::keepEnv +The datatype `Bad` would make Lean inconsistent if it were not rejected: +```lean (name := Bad) (error := true) +inductive Bad where + | bad : (Bad → Bad) → Bad +``` +```leanOutput Bad +(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared +``` +This is because it would be possible to write a circular argument that proves `False` under the assumption `Bad`. +`Bad.bad` is rejected because the constructor's parameter has type `Bad → Bad`, which is a function type in which `Bad` occurs as an argument type. + +This declaration of a fixed point operator is rejected, because `Fix` occurs as an argument to `f`: +```lean (name := Fix) (error := true) +inductive Fix (f : Type u → Type u) where + | fix : f (Fix f) → Fix f +``` +```leanOutput Fix +(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared +``` + +`Fix.fix` is rejected because `f` is not a type constructor of an inductive type, but `Fix` itself occurs as an argument to it. +In this case, `Fix` is also sufficient to construct a type equivalent to `Bad`: +```lean (show := false) +axiom Fix : (Type → Type) → Type +``` +```lean +def Bad : Type := Fix fun t => t → t +``` +::: +:::: + + +### Prop vs Type + +:::TODO +Explain this: +```` +invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}" +```` +::: + + +# Constructions for Termination Checking + +In addition to the type constructor, constructors, and recursors that Lean's core type theory prescribes for inductive types, Lean constructs a number of useful helpers. +First, the equation compiler (which translates recursive functions with pattern matching in to applications of recursors) makes use of these additional constructs: + * `recOn` is a version of the recursor in which the target is prior to the cases for each constructor. + * `casesOn` is a version of the recursor in which the target is prior to the cases for each constructor, and recursive arguments do not yield induction hypotheses. It expresses case analysis rather than primitive recursion. + * `below` computes a type that, for some motive, expresses that _all_ inhabitants of the inductive type that are subtrees of the target satisfy the motive. It transforms a motive for induction or primitive recursion into a motive for strong recursion or strong induction. + * `brecOn` is a version of the recursor in which `below` is used to provide access to all subtrees, rather than just immediate recursive parameters. It represents strong induction. + * `noConfusion` is a general statement from which injectivity and disjointness of constructors can be derived. + * `noConfusionType` is the motive used for `noConfusion` that determines what the consequences of two constructors being equal would be. For separate constructors, this is {lean}`False`; if both constructors are the same, then the consequence is the equality of their respective parameters. + + +For well-founded recursion{TODO}[xref], it is frequently useful to have a generic notion of size available. +This is captured in the {name}`SizeOf` class. + +{docstring SizeOf} + + +# Run-Time Representation + +An inductive type's run-time representation depends both on how many constructors it has, how many arguments each constructor takes, and whether these arguments are {tech}[relevant]. + +## Exceptions + +Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler: +:::keepEnv +````lean (show := false) +axiom α : Prop +```` + + * The fixed-width integer types {lean}`UInt8`, ..., {lean}`UInt64`, and {lean}`USize` are represented by the C types `uint8_t`, ..., `uint64_t`, and `size_t`, respectively. + + * {lean}`Char` is represented by `uint32_t` + + * {lean}`Float` is represented by `double` + + * An {deftech}_enum inductive_ type of at least 2 and at most $`2^32` constructors, each of which has no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to assign a unique value to each constructor. For example, the type {lean}`Bool` is represented by `uint8_t`, with values `0` for {lean}`false` and `1` for {lean}`true`. {TODO}[Find out whether this should say "no relevant parameters"] + + * {lean}`Decidable α` is represented the same way as `Bool` {TODO}[Aren't Decidable and Bool just special cases of the rules for trivial constructors and irrelevance?] + + * {lean}`Nat` is represented by `lean_object *`. Its run-time value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is `1` (checked by `lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`). {TODO}[Move these to FFI section or Nat chapter] +::: + +## Relevance + +Types and proofs have no run-time representation. +That is, if an inductive type is a `Prop`, then its values are erased prior to compilation. +Similarly, all theorem statements and types are erased. +Types with run-time representations are called {deftech}_relevant_, while types without run-time representations are called {deftech}_irrelevant_. + +:::example "Types are irrelevant" +Even though {name}`List.cons` has the following signature, which indicates three parameters: +```signature +List.cons.{u} {α : Type u} : α → List α → List α +``` +its run-time representation has only two, because the type argument is run-time irrelevant. +::: + +:::example "Proofs are irrelevant" +Even though {name}`Fin.mk` has the following signature, which indicates three parameters: +```signature +Fin.mk {n : Nat} (val : Nat) : val < n → Fin n +``` +its run-time representation has only two, because the proof is erased. +::: + +In most cases, irrelevant values simply disappear from compiled code. +However, in cases where some representation is required (such as when they are arguments to polymorphic constructors), they are represented by a trivial value. + +## Trivial Wrappers + +If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter. + +:::example "Zero-Overhead Subtypes" +The structure {name}`Subtype` bundles an element of some type with a proof that it satisfies a predicate. +Its constructor takes four arguments, but three of them are irrelevant: +```signature +Subtype.mk.{u} {α : Sort u} {p : α → Prop} + (val : α) (property : p val) : Subtype p +``` +Thus, subtypes impose no runtime overhead in compiled code, and are represented identically to the type of the {name Subtype.val}`val` field. +::: + +## Other Inductive Types + +If an inductive type doesn't fall into one of the categories above, then its representation is determined by its constructors. +Constructors without relevant parameters are represented by their index into the list of constructors, as unboxed unsigned machine integers (scalars). +Constructors with relevant parameters are represented as an object with a header, the constructor's index, an array of pointers to other objects, and then arrays of scalar fields sorted by their types. +The header tracks the object's reference count and other necessary bookkeeping. + +Recursive functions are compiled as they are in most programming languages, rather than by using the inductive type's recursor. +Elaborating recursive functions to recursors serves to provide reliable termination evidence, not executable code. + +### FFI + +From the perspective of C, these other inductive types are represented by `lean_object *`. +Each constructor is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. +A `lean_ctor_object` stores the constructor index in its header, and the fields are stored in the `m_objs` portion of the object. + +The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows: + +* Non-scalar fields stored as `lean_object *` +* Fields of type {lean}`USize` +* Other scalar fields, in decreasing order by size + +Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose. + +* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field. +* To access {lean}`USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind. +* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds. + +For example, a structure such as +```lean +structure S where + ptr_1 : Array Nat + usize_1 : USize + sc64_1 : UInt64 + ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars + sc64_2 : Float -- `Float` is 64 bit + sc8_1 : Bool + sc16_1 : UInt16 + sc8_2 : UInt8 + sc64_3 : UInt64 + usize_2 : USize + ptr_3 : Char -- trivial wrapper around `UInt32` + sc32_1 : UInt32 + sc16_2 : UInt16 +``` +would get re-sorted into the following memory order: + +* {name}`S.ptr_1` - `lean_ctor_get(val, 0)` +* {name}`S.ptr_2` - `lean_ctor_get(val, 1)` +* {name}`S.ptr_3` - `lean_ctor_get(val, 2)` +* {name}`S.usize_1` - `lean_ctor_get_usize(val, 3)` +* {name}`S.usize_2` - `lean_ctor_get_usize(val, 4)` +* {name}`S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)` +* {name}`S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)` +* {name}`S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)` +* {name}`S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)` +* {name}`S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)` +* {name}`S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)` +* {name}`S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)` +* {name}`S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)` + +::: TODO +Figure out how to test/validate/CI these statements +::: + + +# Mutual Inductive Types + +::: TODO +1. Explain syntax + +2. Generalize the following: + * Recursor spec + * Positivity condition + +3. What doesn't change? + * FFI/cost model is the same + +::: diff --git a/Manual/Meta.lean b/Manual/Meta.lean index df05975..74da060 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -11,7 +11,9 @@ import SubVerso.Highlighting import SubVerso.Examples import Manual.Meta.Basic +import Manual.Meta.Example import Manual.Meta.Figure +import Manual.Meta.Lean import Manual.Meta.Syntax open Lean Elab @@ -102,598 +104,6 @@ def versionString : RoleExpander | #[], #[] => do pure #[← ``(Verso.Doc.Inline.text $(quote Lean.versionString))] | _, _ => throwError "Unexpected arguments" -initialize leanOutputs : EnvExtension (NameMap (List (MessageSeverity × String))) ← - registerEnvExtension (pure {}) - -def Block.lean : Block where - name := `Manual.lean - -def Inline.lean : Inline where - name := `Manual.lean - -structure LeanBlockConfig where - «show» : Option Bool := none - keep : Option Bool := none - name : Option Name := none - error : Option Bool := none - -def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig := - LeanBlockConfig.mk <$> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true - -@[code_block_expander lean] -def lean : CodeBlockExpander - | args, str => do - let config ← LeanBlockConfig.parse.run args - - let altStr ← parserInputString str - - let ictx := Parser.mkInputContext altStr (← getFileName) - let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString altStr, tacticCache? := none, snap? := none, cancelTk? := none} - let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}, {header := ""}]} - let mut pstate := {pos := 0, recovering := false} - let mut cmds := #[] - - repeat - let scope := cmdState.scopes.head! - let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } - let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages - cmds := cmds.push cmd - pstate := ps' - cmdState := {cmdState with messages := messages} - - - cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do - match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with - | Except.error e => logError e.toMessageData; return cmdState - | Except.ok ((), s) => return s - - if Parser.isTerminalCommand cmd then break - - let origEnv ← getEnv - try - setEnv cmdState.env - for t in cmdState.infoState.trees do - pushInfoTree t - - - let mut hls := Highlighted.empty - for cmd in cmds do - hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees) - - if config.show.getD true then - pure #[← `(Block.other {Block.lean with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])] - else - pure #[] - finally - if !config.keep.getD true then - setEnv origEnv - - if let some name := config.name then - let msgs ← cmdState.messages.toList.mapM fun msg => do - - let head := if msg.caption != "" then msg.caption ++ ":\n" else "" - let txt := withNewline <| head ++ (← msg.data.toString) - - pure (msg.severity, txt) - modifyEnv (leanOutputs.modifyState · (·.insert name msgs)) - - match config.error with - | none => - for msg in cmdState.messages.toArray do - logMessage msg - | some true => - if cmdState.messages.hasErrors then - for msg in cmdState.messages.errorsToWarnings.toArray do - logMessage msg - else - throwErrorAt str "Error expected in code block, but none occurred" - | some false => - for msg in cmdState.messages.toArray do - logMessage msg - if cmdState.messages.hasErrors then - throwErrorAt str "No error expected in code block, one occurred" -where - withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str - -@[role_expander lean] -def leanInline : RoleExpander - | args, inlines => do - let config ← LeanBlockConfig.parse.run args - let #[arg] := inlines - | throwError "Expected exactly one argument" - let `(inline|code{ $term:str }) := arg - | throwErrorAt arg "Expected code literal with the example name" - let altStr ← parserInputString term - - match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with - | .error e => throwErrorAt term e - | .ok stx => - let (newMsgs, tree) ← withInfoTreeContext (mkInfoTree := mkInfoTree `leanInline (← getRef)) do - let initMsgs ← Core.getMessageLog - try - Core.resetMessageLog - discard <| Elab.Term.elabTerm stx none - Core.getMessageLog - finally - Core.setMessageLog initMsgs - - if let some name := config.name then - let msgs ← newMsgs.toList.mapM fun msg => do - - let head := if msg.caption != "" then msg.caption ++ ":\n" else "" - let txt := withNewline <| head ++ (← msg.data.toString) - - pure (msg.severity, txt) - modifyEnv (leanOutputs.modifyState · (·.insert name msgs)) - - match config.error with - | none => - for msg in newMsgs.toArray do - logMessage msg - | some true => - if newMsgs.hasErrors then - for msg in newMsgs.errorsToWarnings.toArray do - logMessage msg - else - throwErrorAt term "Error expected in code, but none occurred" - | some false => - for msg in newMsgs.toArray do - logMessage msg - if newMsgs.hasErrors then - throwErrorAt term "No error expected in code, one occurred" - - let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) - - if config.show.getD true then - pure #[← `(Inline.other {Inline.lean with data := ToJson.toJson $(quote hls)} #[Inline.code $(quote term.getString)])] - else - pure #[] -where - withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str - mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do - let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees - let ctx := PartialContextInfo.commandCtx { - env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace, - openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen - } - return InfoTree.context ctx tree - - modifyInfoTrees {m} [Monad m] [MonadInfoTree m] (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := - modifyInfoState fun s => { s with trees := f s.trees } - - -- TODO - consider how to upstream this - withInfoTreeContext {m α} [Monad m] [MonadInfoTree m] [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m (α × InfoTree) := do - let treesSaved ← getResetInfoTrees - MonadFinally.tryFinally' x fun _ => do - let st ← getInfoState - let tree ← mkInfoTree st.trees - modifyInfoTrees fun _ => treesSaved.push tree - pure tree - - - -@[block_extension lean] -def lean.descr : BlockDescr where - traverse _ _ _ := do - pure none - toTeX := - some <| fun _ go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code block while rendering HTML: " ++ err - pure .empty - | .ok (hl : Highlighted) => - hl.blockHtml "examples" - - -@[inline_extension lean] -def lean.inlinedescr : InlineDescr where - traverse _ _ _ := do - pure none - toTeX := - some <| fun go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err - pure .empty - | .ok (hl : Highlighted) => - hl.inlineHtml "examples" - - -def Block.signature : Block where - name := `Manual.signature - -declare_syntax_cat signature_spec -syntax ("def" <|> "theorem")? declId declSig : signature_spec - -@[code_block_expander signature] -def signature : CodeBlockExpander - | args, str => do - ArgParse.done.run args - let altStr ← parserInputString str - - match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with - | .error e => throwError e - | .ok stx => - let `(signature_spec|$[$kw]? $name:declId $sig:declSig) := stx - | throwError m!"Didn't understand parsed signature: {indentD stx}" - let cmdCtx : Command.Context := { - fileName := ← getFileName, - fileMap := ← getFileMap, - tacticCache? := none, - snap? := none, - cancelTk? := none - } - let cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, infoState := ← getInfoState} - let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState - setInfoState st'.infoState - - pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])] - -@[block_extension signature] -def signature.descr : BlockDescr where - traverse _ _ _ := do - pure none - toTeX := - some <| fun _ go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML signature: " ++ err ++ "\n" ++ toString data - pure .empty - | .ok (hl : Highlighted) => - hl.blockHtml "examples" - -open Syntax (mkCApp) in -open MessageSeverity in -instance : Quote MessageSeverity where - quote - | .error => mkCApp ``error #[] - | .information => mkCApp ``information #[] - | .warning => mkCApp ``warning #[] - -open Syntax (mkCApp) in -open Position in -instance : Quote Position where - quote - | ⟨line, column⟩ => mkCApp ``Position.mk #[quote line, quote column] - -def Block.syntaxError : Block where - name := `Manual.syntaxError - -structure SyntaxErrorConfig where - name : Name - «show» : Bool := true - category : Name := `command - prec : Nat := 0 - -defmethod ValDesc.nat [Monad m] [MonadError m] : ValDesc m Nat where - description := m!"a name" - get - | .num x => pure x.getNat - | other => throwError "Expected number, got {repr other}" - -def SyntaxErrorConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m SyntaxErrorConfig := - SyntaxErrorConfig.mk <$> - .positional `name .name <*> - ((·.getD true) <$> .named `show .bool true) <*> - ((·.getD `command) <$> .named `category .name true) <*> - ((·.getD 0) <$> .named `precedence .nat true) - -open Lean.Parser in -@[code_block_expander syntaxError] -def syntaxError : CodeBlockExpander - | args, str => do - let config ← SyntaxErrorConfig.parse.run args - let s := str.getString - match runParserCategory (← getEnv) (← getOptions) config.category s with - | .ok stx => - throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}" - | .error es => - let msgs := es.map fun (pos, msg) => - (.error, mkErrorStringWithPos "" pos msg) - modifyEnv (leanOutputs.modifyState · (·.insert config.name msgs)) - return #[← `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)])] - -@[block_extension syntaxError] -def syntaxError.descr : BlockDescr where - traverse _ _ _ := pure none - toTeX := - some <| fun _ go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [ - r" -.syntax-error { - white-space: normal; -} -.syntax-error::before { - counter-reset: linenumber; -} -.syntax-error > .line { - display: block; - white-space: pre; - counter-increment: linenumber; - font-family: var(--verso-code-font-family); -} -.syntax-error > .line::before { - -webkit-user-select: none; - display: inline-block; - content: counter(linenumber); - border-right: 1px solid #ddd; - width: 2em; - padding-right: 0.25em; - margin-right: 0.25em; - font-family: var(--verso-code-font-family); - text-align: right; -} - -:is(.syntax-error > .line):has(.parse-message)::before { - color: red; - font-weight: bold; -} - -.syntax-error .parse-message > code { - display:none; -} -.syntax-error .parse-message { - position: relative; -} -.syntax-error .parse-message::before { - content: '🛑'; - text-decoration: none; - position: absolute; - top: 0; left: 0; - color: red; -} -" - ] - extraJs := [ - highlightingJs - ] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output Html in - some <| fun _ _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err - pure .empty - | .ok (str, (msgs : (List (Position × String)))) => - let mut pos : String.Pos := ⟨0⟩ - let mut out : Array Html := #[] - let mut line : Array Html := #[] - let filemap := FileMap.ofString str - let mut msgs := msgs - for lineNum in [1:filemap.getLastLine] do - pos := filemap.lineStart lineNum - let lineEnd := str.prev (filemap.lineStart (lineNum + 1)) - repeat - match msgs with - | [] => break - | (pos', msg) :: more => - let pos' := filemap.ofPosition pos' - if pos' > lineEnd then break - msgs := more - line := line.push <| str.extract pos pos' - line := line.push {{{{msg}}"\n"}} - pos := pos' - line := line.push <| str.extract pos lineEnd - out := out.push {{{{line}}}} - line := #[] - pos := str.next lineEnd - - pure {{
{{out}}
}} - -def Block.leanOutput : Block where - name := `Manual.leanOutput - -structure LeanOutputConfig where - name : Ident - «show» : Bool := true - severity : Option MessageSeverity - summarize : Bool - whitespace : WhitespaceMode - -def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig := - LeanOutputConfig.mk <$> - .positional `name output <*> - ((·.getD true) <$> .named `show .bool true) <*> - .named `severity sev true <*> - ((·.getD false) <$> .named `summarize .bool true) <*> - ((·.getD .exact) <$> .named `whitespace ws true) -where - output : ValDesc m Ident := { - description := "output name", - get := fun - | .name x => pure x - | other => throwError "Expected output name, got {repr other}" - } - opt {α} (p : ArgParse m α) : ArgParse m (Option α) := (some <$> p) <|> pure none - optDef {α} (fallback : α) (p : ArgParse m α) : ArgParse m α := p <|> pure fallback - sev : ValDesc m MessageSeverity := { - description := open MessageSeverity in m!"The expected severity: '{``error}', '{``warning}', or '{``information}'", - get := open MessageSeverity in fun - | .name b => do - let b' ← realizeGlobalConstNoOverloadWithInfo b - if b' == ``MessageSeverity.error then pure MessageSeverity.error - else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning - else if b' == ``MessageSeverity.information then pure MessageSeverity.information - else throwErrorAt b "Expected '{``error}', '{``warning}', or '{``information}'" - | other => throwError "Expected severity, got {repr other}" - } - ws : ValDesc m WhitespaceMode := { - description := open WhitespaceMode in m!"The expected whitespace mode: '{``exact}', '{``normalized}', or '{``lax}'", - get := open WhitespaceMode in fun - | .name b => do - let b' ← realizeGlobalConstNoOverloadWithInfo b - if b' == ``WhitespaceMode.exact then pure WhitespaceMode.exact - else if b' == ``WhitespaceMode.normalized then pure WhitespaceMode.normalized - else if b' == ``WhitespaceMode.lax then pure WhitespaceMode.lax - else throwErrorAt b "Expected '{``exact}', '{``normalized}', or '{``lax}'" - | other => throwError "Expected whitespace mode, got {repr other}" - } - -defmethod Lean.NameMap.getOrSuggest [Monad m] [MonadInfoTree m] [MonadError m] - (map : NameMap α) (key : Ident) : m α := do - match map.find? key.getId with - | some v => pure v - | none => - for (n, _) in map do - -- TODO once Levenshtein is merged upstream, use it here - if FuzzyMatching.fuzzyMatch key.getId.toString n.toString || FuzzyMatching.fuzzyMatch n.toString key.getId.toString then - Suggestion.saveSuggestion key n.toString n.toString - throwErrorAt key "'{key}' not found - options are {map.toList.map (·.fst)}" - -@[code_block_expander leanOutput] -def leanOutput : CodeBlockExpander - | args, str => do - let config ← LeanOutputConfig.parser.run args - let msgs : List (MessageSeverity × String) ← leanOutputs.getState (← getEnv) |>.getOrSuggest config.name - - for (sev, txt) in msgs do - if mostlyEqual config.whitespace str.getString txt then - if let some s := config.severity then - if s != sev then - throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr sev}" - if config.show then - let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote sev), $(quote txt), $(quote config.summarize))} #[Block.code $(quote str.getString)]) - return #[content] - else return #[] - - for (_, m) in msgs do - Verso.Doc.Suggestion.saveSuggestion str (m.take 30 ++ "…") m - throwErrorAt str "Didn't match - expected one of: {indentD (toMessageData <| msgs.map (·.2))}\nbut got:{indentD (toMessageData str.getString)}" -where - sevStr : MessageSeverity → String - | .error => "error" - | .information => "information" - | .warning => "warning" - - mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool := - ws.apply s1.trim == ws.apply s2.trim - -@[block_extension leanOutput] -def leanOutput.descr : BlockDescr where - traverse _ _ _ := do - pure none - toTeX := - some <| fun _ go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err - pure .empty - | .ok ((sev, txt, summarize) : MessageSeverity × String × Bool) => - let wrap html := - if summarize then {{
"Expand..."{{html}}
}} - else html - pure <| wrap {{
{{txt}}
}} -where - getClass - | .error => "error" - | .information => "information" - | .warning => "warning" - -def Inline.name : Inline where - name := `Manual.name - -structure NameConfig where - full : Option Name - -def NameConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m NameConfig := - NameConfig.mk <$> ((fun _ => none) <$> .done <|> .positional `name ref <|> pure none) -where - ref : ValDesc m (Option Name) := { - description := m!"reference name" - get := fun - | .name x => - some <$> liftM (realizeGlobalConstNoOverloadWithInfo x) - | other => throwError "Expected Boolean, got {repr other}" - } - - -@[role_expander name] -partial def name : RoleExpander - | args, #[arg] => do - let cfg ← NameConfig.parse.run args - let `(inline|code{ $name:str }) := arg - | throwErrorAt arg "Expected code literal with the example name" - let exampleName := name.getString.toName - let identStx := mkIdentFrom arg (cfg.full.getD exampleName) (canonical := true) - let _resolvedName ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) <| realizeGlobalConstNoOverloadWithInfo identStx - - let hl : Highlighted ← constTok (cfg.full.getD exampleName) name.getString - - pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])] - | _, more => - if h : more.size > 0 then - throwErrorAt more[0] "Unexpected contents" - else - throwError "Unexpected arguments" -where - constTok name str := do - let docs ← findDocString? (← getEnv) name - let sig := toString (← (PrettyPrinter.ppSignature name)).1 - pure <| .token ⟨.const name sig docs, str⟩ - -@[inline_extension name] -def name.descr : InlineDescr where - traverse _ _ _ := do - pure none - toTeX := - some <| fun go _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] - extraCss := [highlightingStyle] - extraJs := [highlightingJs] - extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] - extraCssFiles := [("tippy-border.css", tippy.border.css)] - toHtml := - open Verso.Output.Html in - some <| fun _ _ data _ => do - match FromJson.fromJson? data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err - pure .empty - | .ok (hl : Highlighted) => - hl.inlineHtml "examples" - inductive FFIDocType where | function | type diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean new file mode 100644 index 0000000..5a1072d --- /dev/null +++ b/Manual/Meta/Example.lean @@ -0,0 +1,137 @@ +import VersoManual +import Manual.Meta.Figure +import Manual.Meta.Lean +import Lean.Elab.InfoTree.Types + +open Verso Doc Elab +open Verso.Genre Manual +open Verso.ArgParse + +open Lean Elab + +namespace Manual + +def Block.example (name : Option String) : Block where + name := `Manual.example + data := ToJson.toJson (name, (none : Option Tag)) + +structure ExampleConfig where + description : Array Syntax + /-- Name for refs -/ + name : Option String := none + + +def ExampleConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] : ArgParse m ExampleConfig := + ExampleConfig.mk <$> .positional `description .inlinesString <*> .named `name .string true + +def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β) (xs : Array α) : m (Array β) := do + let mut out := #[] + let mut later := #[] + for h:i in [0:xs.size] do + let x := xs[i] + if ← prioritize x then + out := out.push (i, (← act x)) + else later := later.push (i, x) + for (i, x) in later do + out := out.push (i, (← act x)) + out := out.qsort (fun (i, _) (j, _) => i < j) + return out.map (·.2) + +def isLeanBlock : Syntax → CoreM Bool + | ` => do + let name ← realizeGlobalConstNoOverloadWithInfo nameStx + return name == ``lean + | _ => pure false + + +@[directive_expander «example»] +def «example» : DirectiveExpander + | args, contents => do + let cfg ← ExampleConfig.parse.run args + let description ← cfg.description.mapM elabInline + -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them + let blocks ← prioritizedElab (isLeanBlock ·) elabBlock contents + -- Examples are represented using the first block to hold the description. Storing it in the JSON + -- entails repeated (de)serialization. + pure #[← ``(Block.other (Block.example $(quote cfg.name)) #[Block.para #[$description,*], $blocks,*])] + +@[block_extension «example»] +def example.descr : BlockDescr where + traverse id data contents := do + match FromJson.fromJson? data (α := Option String × Option Tag) with + | .error e => logError s!"Error deserializing example tag: {e}"; pure none + | .ok (none, _) => pure none + | .ok (some x, none) => + let path ← (·.path) <$> read + let tag ← Verso.Genre.Manual.externalTag id path x + pure <| some <| Block.other {Block.example none with id := some id, data := toJson (some x, some tag)} contents + | .ok (some _, some _) => pure none + toTeX := + some <| fun _ go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + toHtml := + open Verso.Doc.Html in + open Verso.Output.Html in + some <| fun goI goB id _data blocks => do + if h : blocks.size < 1 then + HtmlT.logError "Malformed example" + pure .empty + else + let .para description := blocks[0] + | HtmlT.logError "Malformed example - description not paragraph"; pure .empty + let (_, _, xref) ← read + let attrs := match xref.externalTags[id]? with + | none => #[] + | some (_, t) => #[("id", t)] + pure {{ +
+ {{← description.mapM goI}} + {{← blocks.extract 1 blocks.size |>.mapM goB}} +
+ }} + extraCss := [ +r#".example { + padding: 1.5em; + border: 1px solid #98B2C0; + border-radius: 0.5em; + margin-bottom: 0.75em; + margin-top: 0.75em; +} +.example p:last-child {margin-bottom:0;} +.example .description::before { + content: "Example: "; +} +.example[open] .description { + margin-bottom: 1em; +} +.example .description { + font-style: italic; + font-family: var(--verso-structure-font-family); +} +"# + ] + + +def Block.keepEnv : Block where + name := `Manual.example + +@[directive_expander keepEnv] +def keepEnv : DirectiveExpander + | args, contents => do + let () ← ArgParse.done.run args + let env ← getEnv + try + contents.mapM elabBlock + finally + modifyEnv fun _ => env + +@[block_extension keepEnv] +def keepEnv.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := none + toHtml := + open Verso.Doc.Html in + open Verso.Output.Html in + some <| fun _ goB _ _ blocks => do + blocks.mapM goB diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean new file mode 100644 index 0000000..1aac506 --- /dev/null +++ b/Manual/Meta/Lean.lean @@ -0,0 +1,615 @@ +import Lean.Elab.Command +import Lean.Elab.InfoTree + +import Verso +import Verso.Doc.ArgParse +import Verso.Doc.Elab.Monad +import VersoManual +import Verso.Code + +import SubVerso.Highlighting +import SubVerso.Examples + +import Manual.Meta.Basic + + +open Lean Elab +open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets +open SubVerso.Highlighting Highlighted + +open Lean.Elab.Tactic.GuardMsgs + +namespace Manual + + +initialize leanOutputs : EnvExtension (NameMap (List (MessageSeverity × String))) ← + registerEnvExtension (pure {}) + +def Block.lean : Block where + name := `Manual.lean + +def Inline.lean : Inline where + name := `Manual.lean + +structure LeanBlockConfig where + «show» : Option Bool := none + keep : Option Bool := none + name : Option Name := none + error : Option Bool := none + +def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig := + LeanBlockConfig.mk <$> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true + +@[code_block_expander lean] +def lean : CodeBlockExpander + | args, str => do + let config ← LeanBlockConfig.parse.run args + + let altStr ← parserInputString str + + let ictx := Parser.mkInputContext altStr (← getFileName) + let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString altStr, tacticCache? := none, snap? := none, cancelTk? := none} + let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}, {header := ""}]} + let mut pstate := {pos := 0, recovering := false} + let mut cmds := #[] + + repeat + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages + cmds := cmds.push cmd + pstate := ps' + cmdState := {cmdState with messages := messages} + + + cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do + match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with + | Except.error e => logError e.toMessageData; return cmdState + | Except.ok ((), s) => return s + + if Parser.isTerminalCommand cmd then break + + let origEnv ← getEnv + try + setEnv cmdState.env + for t in cmdState.infoState.trees do + pushInfoTree t + + + let mut hls := Highlighted.empty + for cmd in cmds do + hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees) + + if config.show.getD true then + pure #[← `(Block.other {Block.lean with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])] + else + pure #[] + finally + if !config.keep.getD true then + setEnv origEnv + + if let some name := config.name then + let msgs ← cmdState.messages.toList.mapM fun msg => do + + let head := if msg.caption != "" then msg.caption ++ ":\n" else "" + let txt := withNewline <| head ++ (← msg.data.toString) + + pure (msg.severity, txt) + modifyEnv (leanOutputs.modifyState · (·.insert name msgs)) + + match config.error with + | none => + for msg in cmdState.messages.toArray do + logMessage msg + | some true => + if cmdState.messages.hasErrors then + for msg in cmdState.messages.errorsToWarnings.toArray do + logMessage msg + else + throwErrorAt str "Error expected in code block, but none occurred" + | some false => + for msg in cmdState.messages.toArray do + logMessage msg + if cmdState.messages.hasErrors then + throwErrorAt str "No error expected in code block, one occurred" +where + withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str + +@[role_expander lean] +def leanInline : RoleExpander + | args, inlines => do + let config ← LeanBlockConfig.parse.run args + let #[arg] := inlines + | throwError "Expected exactly one argument" + let `(inline|code{ $term:str }) := arg + | throwErrorAt arg "Expected code literal with the example name" + let altStr ← parserInputString term + + match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with + | .error e => throwErrorAt term e + | .ok stx => + let (newMsgs, tree) ← withInfoTreeContext (mkInfoTree := mkInfoTree `leanInline (← getRef)) do + let initMsgs ← Core.getMessageLog + try + Core.resetMessageLog + discard <| Elab.Term.elabTerm stx none + Core.getMessageLog + finally + Core.setMessageLog initMsgs + + if let some name := config.name then + let msgs ← newMsgs.toList.mapM fun msg => do + + let head := if msg.caption != "" then msg.caption ++ ":\n" else "" + let txt := withNewline <| head ++ (← msg.data.toString) + + pure (msg.severity, txt) + modifyEnv (leanOutputs.modifyState · (·.insert name msgs)) + + match config.error with + | none => + for msg in newMsgs.toArray do + logMessage msg + | some true => + if newMsgs.hasErrors then + for msg in newMsgs.errorsToWarnings.toArray do + logMessage msg + else + throwErrorAt term "Error expected in code, but none occurred" + | some false => + for msg in newMsgs.toArray do + logMessage msg + if newMsgs.hasErrors then + throwErrorAt term "No error expected in code, one occurred" + + let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) + + if config.show.getD true then + pure #[← `(Inline.other {Inline.lean with data := ToJson.toJson $(quote hls)} #[Inline.code $(quote term.getString)])] + else + pure #[] +where + withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str + mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do + let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + return InfoTree.context ctx tree + + modifyInfoTrees {m} [Monad m] [MonadInfoTree m] (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit := + modifyInfoState fun s => { s with trees := f s.trees } + + -- TODO - consider how to upstream this + withInfoTreeContext {m α} [Monad m] [MonadInfoTree m] [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m (α × InfoTree) := do + let treesSaved ← getResetInfoTrees + MonadFinally.tryFinally' x fun _ => do + let st ← getInfoState + let tree ← mkInfoTree st.trees + modifyInfoTrees fun _ => treesSaved.push tree + pure tree + + + +@[block_extension lean] +def lean.descr : BlockDescr where + traverse _ _ _ := do + pure none + toTeX := + some <| fun _ go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code block while rendering HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.blockHtml "examples" + + +@[inline_extension lean] +def lean.inlinedescr : InlineDescr where + traverse _ _ _ := do + pure none + toTeX := + some <| fun go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.inlineHtml "examples" + + +def Block.signature : Block where + name := `Manual.signature + +declare_syntax_cat signature_spec +syntax ("def" <|> "theorem")? declId declSig : signature_spec + +@[code_block_expander signature] +def signature : CodeBlockExpander + | args, str => do + ArgParse.done.run args + let altStr ← parserInputString str + + match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with + | .error e => throwError e + | .ok stx => + let `(signature_spec|$[$kw]? $name:declId $sig:declSig) := stx + | throwError m!"Didn't understand parsed signature: {indentD stx}" + let cmdCtx : Command.Context := { + fileName := ← getFileName, + fileMap := ← getFileMap, + tacticCache? := none, + snap? := none, + cancelTk? := none + } + let cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, infoState := ← getInfoState} + let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState + setInfoState st'.infoState + + pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])] + +@[block_extension signature] +def signature.descr : BlockDescr where + traverse _ _ _ := do + pure none + toTeX := + some <| fun _ go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML signature: " ++ err ++ "\n" ++ toString data + pure .empty + | .ok (hl : Highlighted) => + hl.blockHtml "examples" + +open Syntax (mkCApp) in +open MessageSeverity in +instance : Quote MessageSeverity where + quote + | .error => mkCApp ``error #[] + | .information => mkCApp ``information #[] + | .warning => mkCApp ``warning #[] + +open Syntax (mkCApp) in +open Position in +instance : Quote Position where + quote + | ⟨line, column⟩ => mkCApp ``Position.mk #[quote line, quote column] + +def Block.syntaxError : Block where + name := `Manual.syntaxError + +structure SyntaxErrorConfig where + name : Name + «show» : Bool := true + category : Name := `command + prec : Nat := 0 + +defmethod ValDesc.nat [Monad m] [MonadError m] : ValDesc m Nat where + description := m!"a name" + get + | .num x => pure x.getNat + | other => throwError "Expected number, got {repr other}" + +def SyntaxErrorConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m SyntaxErrorConfig := + SyntaxErrorConfig.mk <$> + .positional `name .name <*> + ((·.getD true) <$> .named `show .bool true) <*> + ((·.getD `command) <$> .named `category .name true) <*> + ((·.getD 0) <$> .named `precedence .nat true) + +open Lean.Parser in +@[code_block_expander syntaxError] +def syntaxError : CodeBlockExpander + | args, str => do + let config ← SyntaxErrorConfig.parse.run args + let s := str.getString + match runParserCategory (← getEnv) (← getOptions) config.category s with + | .ok stx => + throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}" + | .error es => + let msgs := es.map fun (pos, msg) => + (.error, mkErrorStringWithPos "" pos msg) + modifyEnv (leanOutputs.modifyState · (·.insert config.name msgs)) + return #[← `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)])] + +@[block_extension syntaxError] +def syntaxError.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := + some <| fun _ go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [ + r" +.syntax-error { + white-space: normal; +} +.syntax-error::before { + counter-reset: linenumber; +} +.syntax-error > .line { + display: block; + white-space: pre; + counter-increment: linenumber; + font-family: var(--verso-code-font-family); +} +.syntax-error > .line::before { + -webkit-user-select: none; + display: inline-block; + content: counter(linenumber); + border-right: 1px solid #ddd; + width: 2em; + padding-right: 0.25em; + margin-right: 0.25em; + font-family: var(--verso-code-font-family); + text-align: right; +} + +:is(.syntax-error > .line):has(.parse-message)::before { + color: red; + font-weight: bold; +} + +.syntax-error .parse-message > code { + display:none; +} +.syntax-error .parse-message { + position: relative; +} +.syntax-error .parse-message::before { + content: '🛑'; + text-decoration: none; + position: absolute; + top: 0; left: 0; + color: red; +} +" + ] + extraJs := [ + highlightingJs + ] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err + pure .empty + | .ok (str, (msgs : (List (Position × String)))) => + let mut pos : String.Pos := ⟨0⟩ + let mut out : Array Html := #[] + let mut line : Array Html := #[] + let filemap := FileMap.ofString str + let mut msgs := msgs + for lineNum in [1:filemap.getLastLine] do + pos := filemap.lineStart lineNum + let lineEnd := str.prev (filemap.lineStart (lineNum + 1)) + repeat + match msgs with + | [] => break + | (pos', msg) :: more => + let pos' := filemap.ofPosition pos' + if pos' > lineEnd then break + msgs := more + line := line.push <| str.extract pos pos' + line := line.push {{{{msg}}"\n"}} + pos := pos' + line := line.push <| str.extract pos lineEnd + out := out.push {{{{line}}}} + line := #[] + pos := str.next lineEnd + + pure {{
{{out}}
}} + +def Block.leanOutput : Block where + name := `Manual.leanOutput + +structure LeanOutputConfig where + name : Ident + «show» : Bool := true + severity : Option MessageSeverity + summarize : Bool + whitespace : WhitespaceMode + +def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig := + LeanOutputConfig.mk <$> + .positional `name output <*> + ((·.getD true) <$> .named `show .bool true) <*> + .named `severity sev true <*> + ((·.getD false) <$> .named `summarize .bool true) <*> + ((·.getD .exact) <$> .named `whitespace ws true) +where + output : ValDesc m Ident := { + description := "output name", + get := fun + | .name x => pure x + | other => throwError "Expected output name, got {repr other}" + } + opt {α} (p : ArgParse m α) : ArgParse m (Option α) := (some <$> p) <|> pure none + optDef {α} (fallback : α) (p : ArgParse m α) : ArgParse m α := p <|> pure fallback + sev : ValDesc m MessageSeverity := { + description := open MessageSeverity in m!"The expected severity: '{``error}', '{``warning}', or '{``information}'", + get := open MessageSeverity in fun + | .name b => do + let b' ← realizeGlobalConstNoOverloadWithInfo b + if b' == ``MessageSeverity.error then pure MessageSeverity.error + else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning + else if b' == ``MessageSeverity.information then pure MessageSeverity.information + else throwErrorAt b "Expected '{``error}', '{``warning}', or '{``information}'" + | other => throwError "Expected severity, got {repr other}" + } + ws : ValDesc m WhitespaceMode := { + description := open WhitespaceMode in m!"The expected whitespace mode: '{``exact}', '{``normalized}', or '{``lax}'", + get := open WhitespaceMode in fun + | .name b => do + let b' ← realizeGlobalConstNoOverloadWithInfo b + if b' == ``WhitespaceMode.exact then pure WhitespaceMode.exact + else if b' == ``WhitespaceMode.normalized then pure WhitespaceMode.normalized + else if b' == ``WhitespaceMode.lax then pure WhitespaceMode.lax + else throwErrorAt b "Expected '{``exact}', '{``normalized}', or '{``lax}'" + | other => throwError "Expected whitespace mode, got {repr other}" + } + +defmethod Lean.NameMap.getOrSuggest [Monad m] [MonadInfoTree m] [MonadError m] + (map : NameMap α) (key : Ident) : m α := do + match map.find? key.getId with + | some v => pure v + | none => + for (n, _) in map do + -- TODO once Levenshtein is merged upstream, use it here + if FuzzyMatching.fuzzyMatch key.getId.toString n.toString || FuzzyMatching.fuzzyMatch n.toString key.getId.toString then + Suggestion.saveSuggestion key n.toString n.toString + throwErrorAt key "'{key}' not found - options are {map.toList.map (·.fst)}" + +@[code_block_expander leanOutput] +def leanOutput : CodeBlockExpander + | args, str => do + let config ← LeanOutputConfig.parser.run args + let msgs : List (MessageSeverity × String) ← leanOutputs.getState (← getEnv) |>.getOrSuggest config.name + + for (sev, txt) in msgs do + if mostlyEqual config.whitespace str.getString txt then + if let some s := config.severity then + if s != sev then + throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr sev}" + if config.show then + let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote sev), $(quote txt), $(quote config.summarize))} #[Block.code $(quote str.getString)]) + return #[content] + else return #[] + + for (_, m) in msgs do + Verso.Doc.Suggestion.saveSuggestion str (m.take 30 ++ "…") m + throwErrorAt str "Didn't match - expected one of: {indentD (toMessageData <| msgs.map (·.2))}\nbut got:{indentD (toMessageData str.getString)}" +where + sevStr : MessageSeverity → String + | .error => "error" + | .information => "information" + | .warning => "warning" + + mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool := + ws.apply s1.trim == ws.apply s2.trim + +@[block_extension leanOutput] +def leanOutput.descr : BlockDescr where + traverse _ _ _ := do + pure none + toTeX := + some <| fun _ go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err + pure .empty + | .ok ((sev, txt, summarize) : MessageSeverity × String × Bool) => + let wrap html := + if summarize then {{
"Expand..."{{html}}
}} + else html + pure <| wrap {{
{{txt}}
}} +where + getClass + | .error => "error" + | .information => "information" + | .warning => "warning" + +def Inline.name : Inline where + name := `Manual.name + +structure NameConfig where + full : Option Name + +def NameConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m NameConfig := + NameConfig.mk <$> ((fun _ => none) <$> .done <|> .positional `name ref <|> pure none) +where + ref : ValDesc m (Option Name) := { + description := m!"reference name" + get := fun + | .name x => + some <$> liftM (realizeGlobalConstNoOverloadWithInfo x) + | other => throwError "Expected Boolean, got {repr other}" + } + + +@[role_expander name] +partial def name : RoleExpander + | args, #[arg] => do + let cfg ← NameConfig.parse.run args + let `(inline|code{ $name:str }) := arg + | throwErrorAt arg "Expected code literal with the example name" + let exampleName := name.getString.toName + let identStx := mkIdentFrom arg (cfg.full.getD exampleName) (canonical := true) + let _resolvedName ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) <| realizeGlobalConstNoOverloadWithInfo identStx + + let hl : Highlighted ← constTok (cfg.full.getD exampleName) name.getString + + pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])] + | _, more => + if h : more.size > 0 then + throwErrorAt more[0] "Unexpected contents" + else + throwError "Unexpected arguments" +where + constTok name str := do + let docs ← findDocString? (← getEnv) name + let sig := toString (← (PrettyPrinter.ppSignature name)).1 + pure <| .token ⟨.const name sig docs, str⟩ + +@[inline_extension name] +def name.descr : InlineDescr where + traverse _ _ _ := do + pure none + toTeX := + some <| fun go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output.Html in + some <| fun _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.inlineHtml "examples" diff --git a/Manual/Meta/PPrint.lean b/Manual/Meta/PPrint.lean new file mode 100644 index 0000000..1b54f2f --- /dev/null +++ b/Manual/Meta/PPrint.lean @@ -0,0 +1,96 @@ +import Lean.Data.RBMap +import Lean.Data.Json +import Lean.Widget.TaggedText + +namespace Manual.Meta.PPrint +open Lean (RBMap) +open Std (Format) + +structure FormatWithTags (α : Type u) where + format : Format + tags : RBMap Nat α compare + +structure TagFormatM.State (α) where + nextTag : Nat := 0 + tags : RBMap Nat α compare := {} + +def TagFormatT α m := StateT (TagFormatM.State α) m + +instance [Monad m] : Monad (TagFormatT α m) := inferInstanceAs (Monad (StateT (TagFormatM.State α) m)) + +scoped instance [Monad m] : MonadStateOf (TagFormatM.State α) (TagFormatT α m) := + inferInstanceAs (MonadStateOf (TagFormatM.State α) (StateT (TagFormatM.State α) m)) + + +instance [Functor m] : MonadLift m (TagFormatT α m) where + monadLift act := fun σ => (·, σ) <$> act + +abbrev TagFormatM α := TagFormatT α Id + +def TagFormatT.run [Monad m] (act : TagFormatT α m Format) : m (FormatWithTags α) := do + let (value, ⟨_, tags⟩) ← StateT.run act {} + pure ⟨value, tags⟩ + +def TagFormatM.run (act : TagFormatM α Format) : FormatWithTags α := TagFormatT.run act + +def fresh [Monad m] : TagFormatT α m Nat := + modifyGet fun ⟨i, tags⟩ => (i, ⟨i+1, tags⟩) + +def tag [Monad m] (val : α) (doc : Format) : TagFormatT α m Format := do + let i ← fresh + modify fun σ => {σ with tags := σ.tags.insert i val} + pure <| Format.tag i doc + +open Lean.Widget + +private structure TaggedState (α) where + out : TaggedText α := .text "" + tagStack : List (Nat × TaggedText α) := [] + column : Nat := 0 +deriving Inhabited + +private abbrev RenderM α := (ReaderT (RBMap Nat α compare) (StateM (TaggedState α))) + +instance inst [Inhabited α] : Format.MonadPrettyFormat (RenderM α) where + pushOutput s := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩ + pushNewline indent := modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩ + currColumn := return (←get).column + startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, out) :: ts, col⟩ + endTags n := do + let tagVals ← read + modify fun ⟨out, ts, col⟩ => + let (ended, left) := (ts.take n, ts.drop n) + let out' := ended.foldl (init := out) fun acc (tag, top) => top.appendTag (tagVals.find! tag) acc + ⟨out', left, col⟩ + +def FormatWithTags.render [Inhabited α] (format : FormatWithTags α) (indent := 0) (w : Nat := Std.Format.defWidth) : TaggedText α := + (format.format.prettyM w indent : RenderM α Unit) format.tags {} |>.2.out + +deriving instance Lean.ToJson, Lean.FromJson for TaggedText +deriving instance Lean.ToJson, Lean.FromJson for PUnit + +open Lean Syntax in +partial instance [Quote α] : Quote (TaggedText α) where + quote := go +where + go + | .text s => mkCApp ``TaggedText.text #[quote s] + | .tag x y => mkCApp ``TaggedText.tag #[quote x, go y] + | .append xs => + mkCApp ``TaggedText.append #[arr xs] + + goArr (xs : Array (TaggedText α)) (i : Nat) (args : Array Term) : Term := + if h : i < xs.size then + goArr xs (i+1) (args.push (go xs[i])) + else + Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args + + arr (xs : Array (TaggedText α)) : Term := + if xs.size <= 8 then + goArr xs 0 #[] + else + Syntax.mkCApp ``List.toArray #[lst xs.toList] + + lst : List (TaggedText α) → Term + | [] => mkCIdent ``List.nil + | (x::xs) => Syntax.mkCApp ``List.cons #[go x, lst xs] diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index 949b9e6..b497b8f 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -1,12 +1,19 @@ import VersoManual +import Verso.Code.Highlighted + import Manual.Meta.Basic +import Manual.Meta.PPrint open Verso Doc Elab open Verso.Genre Manual open Verso.ArgParse +open Verso.Code (highlightingJs) +open Verso.Code.Highlighted.WebAssets + open Lean Elab Parser +open Lean.Widget (TaggedText) namespace Manual @@ -18,11 +25,129 @@ namespace Manual def Block.syntax : Block where name := `Manual.syntax +def Block.grammar : Block where + name := `Manual.grammar + +def Inline.keywordOf : Inline where + name := `Manual.keywordOf + structure SyntaxConfig where name : Name «open» : Bool := true - aliases : List Name + aliases : List Name := [] + +structure KeywordOfConfig where + ofSyntax : Ident + parser : Option Ident + +def KeywordOfConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m KeywordOfConfig := + KeywordOfConfig.mk <$> .positional `ofSyntax .ident <*> .named `parser .ident true + +@[role_expander keywordOf] +def keywordOf : RoleExpander + | args, inlines => do + let ⟨kind, parser⟩ ← KeywordOfConfig.parse.run args + let #[inl] := inlines + | throwError "Expected a single code argument" + let `(inline|code{ $kw:str }) := inl + | throwErrorAt inl "Expected code literal with the keyword" + let kindName := kind.getId + let parserName ← parser.mapM (realizeGlobalConstNoOverloadWithInfo ·) + let env ← getEnv + let mut catName := none + for (cat, contents) in (Lean.Parser.parserExtension.getState env).categories do + for (k, ()) in contents.kinds do + if kindName == k then catName := some cat; break + if let some _ := catName then break + let some c := catName + | throwErrorAt kind s!"Unknown syntax kind {kindName}" + let kindDoc ← findDocString? (← getEnv) kindName + return #[← `(Doc.Inline.other {Inline.keywordOf with data := ToJson.toJson (α := (String × Name × Name × Option String)) $(quote (kw.getString, c, parserName.getD kindName, kindDoc))} #[Doc.Inline.code $kw])] + +@[inline_extension keywordOf] +def keywordOf.descr : InlineDescr where + traverse _ _ _ := do + pure none + toTeX := none + toHtml := + open Verso.Output.Html in + some <| fun goI _ info content => do + match FromJson.fromJson? (α := (String × Name × Name × Option String)) info with + | .ok (kw, cat, kind, kindDoc) => + -- TODO: use the presentation of the syntax in the manual to show the kind, rather than + -- leaking the kind name here, which is often horrible. But we need more data to test this + -- with first! Also TODO: we need docs for syntax categories, with human-readable names to + -- show here. Use tactic index data for inspiration. + -- For now, here's the underlying data so we don't have to fill in xrefs later and can debug. + pure {{ + + + {{kind.toString}} " : " {{cat.toString}} + {{if let some doc := kindDoc then + {{ {{doc}}}} + else + .empty + }} + + {{kw}} + + }} + | .error e => + Html.HtmlT.logError s!"Couldn't deserialized keywordOf data: {e}" + content.mapM goI + extraCss := [ +r#".keyword-of .kw { + font-weight: bold; +} +.keyword-of .hover-info { + display: none; +} +.keyword-of .kw:hover { + background-color: #eee; + border-radius: 2px; +} +"# + ] + extraJs := [ + highlightingJs, +r#" +window.addEventListener("load", () => { + tippy('.keyword-of.hl.lean', { + allowHtml: true, + /* DEBUG -- remove the space: * / + onHide(any) { return false; }, + trigger: "click", + // */ + maxWidth: "none", + theme: "lean", + placement: 'bottom-start', + content (tgt) { + const content = document.createElement("span"); + const state = tgt.querySelector(".hover-info").cloneNode(true); + state.style.display = "block"; + content.appendChild(state); + /* Render docstrings - TODO server-side */ + if ('undefined' !== typeof marked) { + for (const d of content.querySelectorAll("code.docstring, pre.docstring")) { + const str = d.innerText; + const html = marked.parse(str); + const rendered = document.createElement("div"); + rendered.classList.add("docstring"); + rendered.innerHTML = html; + d.parentNode.replaceChild(rendered, d); + } + } + content.style.display = "block"; + content.className = "hl lean popup"; + return content; + } + }); +}); +"# + ] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] partial def many [Inhabited (f (List α))] [Applicative f] [Alternative f] (x : f α) : f (List α) := ((· :: ·) <$> x <*> many x) <|> pure [] @@ -31,8 +156,27 @@ def SyntaxConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEn SyntaxConfig.mk <$> .positional `name .name <*> ((·.getD true) <$> (.named `open .bool true)) <*> - (many (.named `alias .name false) <* .done) + (many (.named `alias .resolvedName false) <* .done) +inductive GrammarTag where + | keyword + | nonterminal (name : Name) (docstring? : Option String) + | fromNonterminal (name : Name) (docstring? : Option String) + | error + | bnf +deriving Repr, FromJson, ToJson, Inhabited + +open Lean.Syntax in +open GrammarTag in +instance : Quote GrammarTag where + quote + | keyword => mkCApp ``keyword #[] + | nonterminal x d => mkCApp ``nonterminal #[quote x, quote d] + | fromNonterminal x d => mkCApp ``fromNonterminal #[quote x, quote d] + | GrammarTag.error => mkCApp ``GrammarTag.error #[] + | bnf => mkCApp ``bnf #[] + +open Manual.Meta.PPrint in @[directive_expander «syntax»] partial def «syntax» : DirectiveExpander | args, blocks => do @@ -61,22 +205,83 @@ where nonTerm : Name → String | .str x "pseudo" => nonTerm x - | .str _ x => s!"⟨{x.toUpper}⟩" - | x => s!"⟨{x.toString.toUpper}⟩" - - production : Syntax → String - | .atom _ str => s!"“{str}”" - | .missing => "" - | .ident _ _ x _ => - match x with - | .str x' "pseudo" => x'.toString - | _ => x.toString - | .node _ k args => - match k, antiquoteOf k, args with - | `many.antiquot_suffix_splice, _, #[stx, star] => "{" ++ production stx ++ "}" - | _, some k', #[a, b, c, d] => - nonTerm k' - | _, _, _ => args.map production |>.toList |> String.intercalate " " + | .str _ x => x + | x => x.toString + + empty : Syntax → Bool + | .node _ _ #[] => true + | _ => false + + kleeneLike (mod : String) : Syntax → Format → TagFormatT GrammarTag DocElabM Format + | .atom .., f + | .ident .., f + | .missing, f => do return f ++ (← tag .bnf mod) + | .node _ _ args, f => do + let nonempty := args.filter (!empty ·) + if h : nonempty.size = 1 then + kleeneLike mod nonempty[0] f + else + return (← tag .bnf "(") ++ f ++ (← tag .bnf s!"){mod}") + + kleene := kleeneLike "*" + + perhaps := kleeneLike "?" + + + production (stx : Syntax) : TagFormatT GrammarTag DocElabM Format := do + match stx with + | .atom info str => infoWrap info <$> tag .keyword str + | .missing => tag .error "" + | .ident info _ x _ => + let d? ← findDocString? (← getEnv) x + -- TODO render markdown + let tok ← + tag (.nonterminal x d?) <| + match x with + | .str x' "pseudo" => x'.toString + | _ => x.toString + return infoWrap info tok + | .node info k args => do + infoWrap info <$> + match k, antiquoteOf k, args with + | `many.antiquot_suffix_splice, _, #[starred, star] => + infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleene starred) + | `optional.antiquot_suffix_splice, _, #[starred, star] => + infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= perhaps starred) + | `sepBy.antiquot_suffix_splice, _, #[starred, star] => + infoWrap2 starred.getHeadInfo star.getTailInfo <$> (production starred >>= kleeneLike ",*" starred) + | `many.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info star] => + infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleene contents) + | `optional.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] => + infoWrap2 dollar.getHeadInfo info <$> (production contents >>= perhaps contents) + | `sepBy.antiquot_scope, _, #[dollar, _null, _brack, contents, _brack2, .atom info _star] => + infoWrap2 dollar.getHeadInfo info <$> (production contents >>= kleeneLike ",*" contents) + | `choice, _, opts => do + return (← tag .bnf "(") ++ (" " ++ (← tag .bnf "|") ++ " ").joinSep (← opts.toList.mapM production) ++ (← tag .bnf ")") + | _, some k', #[a, b, c, d] => do + let doc? ← findDocString? (← getEnv) k' + let last := + if let .node _ _ #[] := d then c else d + infoWrap2 a.getHeadInfo last.getTailInfo <$> tag (.nonterminal k' doc?) (nonTerm k') + | _, _, _ => do -- return ((← args.mapM production) |>.toList |> (Format.joinSep · " ")) + let mut out := Format.nil + for a in args do + out := out ++ (← production a) + let doc? ← findDocString? (← getEnv) k + tag (.fromNonterminal k doc?) out + + lined (ws : String) : Format := + Format.line.joinSep (ws.splitOn "\n") + + infoWrap (info : SourceInfo) (doc : Format) : Format := + if let .original leading _ trailing _ := info then + lined leading.toString ++ doc ++ lined trailing.toString + else doc + + infoWrap2 (info1 : SourceInfo) (info2 : SourceInfo) (doc : Format) : Format := + let pre := if let .original leading _ _ _ := info1 then lined leading.toString else .nil + let post := if let .original _ _ trailing _ := info2 then lined trailing.toString else .nil + pre ++ doc ++ post categoryOf (env : Environment) (kind : Name) : Option Name := do for (catName, contents) in (Lean.Parser.parserExtension.getState env).categories do @@ -86,25 +291,36 @@ where elabGrammar config isFirst howMany (argsStx : Array Syntax) (str : TSyntax `str) col «open» i info close := do let args ← parseArgs <| argsStx.map (⟨·⟩) - let #[] := args - | throwErrorAt str "Expected 0 arguments" + let config ← + if let #[] := args then pure config + else if let #[.named _ ⟨.ident _ _ `of _⟩ (.name n)] := args then pure {name := n.getId, «open» := false} + else throwErrorAt str "Expected optional 'of' to specify alternate nonterminal" let altStr ← parserInputString str let p := andthen ⟨{}, whitespace⟩ <| andthen {fn := (fun _ => (·.pushSyntax (mkIdent config.name)))} (parserOfStack 0) match runParser (← getEnv) (← getOptions) p altStr (← getFileName) with | .ok stx => - let mut bnf := s!"{nonTerm ((categoryOf (← getEnv) config.name).getD config.name)} ::=" - bnf := bnf ++ if config.open || (!config.open && !isFirst) then " ...\n" else if howMany = 1 then "" else "\n" - bnf := bnf ++ if !config.open && isFirst then - if howMany != 1 then " " else " " - else " | " - bnf := bnf ++ production stx - - elabBlock ` + let bnf ← getBnf config isFirst howMany stx + `(Block.other {Block.grammar with data := ToJson.toJson ($(quote bnf) : TaggedText GrammarTag)} #[]) | .error es => for (pos, msg) in es do log (severity := .error) (mkErrorStringWithPos "" pos msg) - `(asldfkj) + `(sorry) + getBnf config isFirst howMany (stx : Syntax) : DocElabM (TaggedText GrammarTag) := do + return (← renderBnf config isFirst howMany stx |>.run).render (w := 5) + + renderBnf config isFirst howMany (stx : Syntax) : TagFormatT GrammarTag DocElabM Format := do + let cat := (categoryOf (← getEnv) config.name).getD config.name + let d? ← findDocString? (← getEnv) cat + let mut bnf : Format := (← tag (.nonterminal cat d?) s!"{nonTerm cat}") ++ " " ++ (← tag .bnf "::=") + if config.open || (!config.open && !isFirst) then + bnf := bnf ++ (" ..." : Format) + bnf := bnf ++ .line + let bar := (← tag .bnf "|") ++ " " + bnf := bnf ++ (← if !config.open && isFirst then production stx else do return bar ++ .nest 2 (← production stx)) + return .nest 4 bnf -- ++ .line ++ repr stx + +def grammar := () @[block_extension «syntax»] def syntax.descr : BlockDescr where @@ -120,3 +336,116 @@ def syntax.descr : BlockDescr where {{← content.mapM goB}} }} + +@[block_extension grammar] +partial def grammar.descr : BlockDescr where + traverse _ _ _ := do + pure none + toTeX := none + toHtml := + open Verso.Output.Html in + some <| fun _ goB _ info _ => do + match FromJson.fromJson? (α := TaggedText GrammarTag) info with + | .ok bnf => + pure {{ + 
+            {{ bnfHtml bnf }}
+
+ }} + | .error e => + Html.HtmlT.logError s!"Couldn't deserialize BNF: {e}" + pure .empty + extraCss := [ +r#"pre.grammar .keyword { + font-weight: bold; +} +pre.grammar .nonterminal { + font-style: italic; +} +pre.grammar .nonterminal > .hover-info, pre.grammar .from-nonterminal > .hover-info { + display: none; +} +pre.grammar .active { + background-color: #eee; + border-radius: 2px; +} +"# + ] + extraJs := [ + highlightingJs, +r#" +window.addEventListener("load", () => { + const innerProps = { + onShow(inst) { console.log(inst); }, + onHide(inst) { console.log(inst); }, + content(tgt) { + const content = document.createElement("span"); + const state = tgt.querySelector(".hover-info").cloneNode(true); + state.style.display = "block"; + content.appendChild(state); + /* Render docstrings - TODO server-side */ + if ('undefined' !== typeof marked) { + for (const d of content.querySelectorAll("code.docstring, pre.docstring")) { + const str = d.innerText; + const html = marked.parse(str); + const rendered = document.createElement("div"); + rendered.classList.add("docstring"); + rendered.innerHTML = html; + d.parentNode.replaceChild(rendered, d); + } + } + content.style.display = "block"; + content.className = "hl lean popup"; + return content; + } + }; + const outerProps = { + allowHtml: true, + theme: "lean", + placement: 'bottom-start', + maxWidth: "none", + delay: 100, + moveTransition: 'transform 0.2s ease-out', + onTrigger(inst, event) { + const ref = event.currentTarget; + const block = ref.closest('.hl.lean'); + block.querySelectorAll('.active').forEach((i) => i.classList.remove('active')); + ref.classList.add("active"); + }, + onUntrigger(inst, event) { + const ref = event.currentTarget; + const block = ref.closest('.hl.lean'); + block.querySelectorAll('.active').forEach((i) => i.classList.remove('active')); + } + }; + tippy.createSingleton(tippy('pre.grammar.hl.lean .nonterminal.documented, pre.grammar.hl.lean .from-nonterminal.documented', innerProps), outerProps); +}); +"# + ] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] +where + bnfHtml : TaggedText GrammarTag → Verso.Output.Html + | .text str => .text true str + | .tag t txt => tagHtml t (bnfHtml txt) + | .append txts => .seq (txts.map bnfHtml) + tagHtml (t : GrammarTag) : Verso.Output.Html → Verso.Output.Html := + open Verso.Output.Html in + match t with + | .bnf => ({{{{·}}}}) + | .error => ({{{{·}}}}) + | .keyword => ({{{{·}}}}) + | .nonterminal k none => ({{{{·}}}}) + | .fromNonterminal k none => ({{{{·}}}}) + | .nonterminal k (some doc) => ({{ + + {{doc}} + {{·}} + + }}) + | .fromNonterminal k (some doc) => ({{ + + {{doc}} + {{·}} + + }}) diff --git a/lake-manifest.json b/lake-manifest.json index 5d45296..397965b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "cf37277bfbb40c333987112af17c342503fcfba7", + "rev": "11903e639bac684b76273287c3293fe4d665f53d", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main",