diff --git a/src/Init/Core.lean b/src/Init/Core.lean index fee7d34327..d212ebd6b9 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -96,10 +96,10 @@ An element of `α ⊕ β` is either of the form `.inl a` where `a : α`, or `.inr b` where `b : β`. -/ inductive Sum (α : Type u) (β : Type v) where - | /-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/ - inl (val : α) : Sum α β - | /-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/ - inr (val : β) : Sum α β + /-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/ + | inl (val : α) : Sum α β + /-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/ + | inr (val : β) : Sum α β @[inheritDoc] infixr:30 " ⊕ " => Sum @@ -115,10 +115,10 @@ because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic. `PSum` is usually only used in automation that constructs sums of arbitrary types. -/ inductive PSum (α : Sort u) (β : Sort v) where - | /-- Left injection into the sum type `α ⊕' β`. If `a : α` then `.inl a : α ⊕' β`. -/ - inl (val : α) : PSum α β - | /-- Right injection into the sum type `α ⊕' β`. If `b : β` then `.inr b : α ⊕' β`. -/ - inr (val : β) : PSum α β + /-- Left injection into the sum type `α ⊕' β`. If `a : α` then `.inl a : α ⊕' β`. -/ + | inl (val : α) : PSum α β + /-- Right injection into the sum type `α ⊕' β`. If `b : β` then `.inr b : α ⊕' β`. -/ + | inr (val : β) : PSum α β @[inheritDoc] infixr:30 " ⊕' " => PSum @@ -190,9 +190,9 @@ example (h : ∃ x : Nat, x = x) : True := ``` -/ inductive Exists {α : Sort u} (p : α → Prop) : Prop where - | /-- Existential introduction. If `a : α` and `h : p a`, - then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/ - intro (w : α) (h : p w) : Exists p + /-- Existential introduction. If `a : α` and `h : p a`, + then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/ + | intro (w : α) (h : p w) : Exists p /-- Auxiliary type used to compile `for x in xs` notation. @@ -206,12 +206,12 @@ representing the body of a for loop. It can be: `.done` is produced by calls to `break` or `return` in the loop, -/ inductive ForInStep (α : Type u) where - | /-- `.done a` means that we should early-exit the loop. - `.done` is produced by calls to `break` or `return` in the loop. -/ - done : α → ForInStep α - | /-- `.yield a` means that we should continue the loop. - `.yield` is produced by `continue` and reaching the bottom of the loop body. -/ - yield : α → ForInStep α + /-- `.done a` means that we should early-exit the loop. + `.done` is produced by calls to `break` or `return` in the loop. -/ + | done : α → ForInStep α + /-- `.yield a` means that we should continue the loop. + `.yield` is produced by `continue` and reaching the bottom of the loop body. -/ + | yield : α → ForInStep α deriving Inhabited /-- @@ -276,16 +276,16 @@ block can exit: All cases return a value `s : σ` which bundles all the mutable variables of the do-block. -/ inductive DoResultPRBC (α β σ : Type u) where - | /-- `pure (a : α) s` means that the block exited normally with return value `a` -/ - pure : α → σ → DoResultPRBC α β σ - | /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/ - return : β → σ → DoResultPRBC α β σ - | /-- `break s` means that `break` was called, meaning that we should exit - from the containing loop -/ - break : σ → DoResultPRBC α β σ - | /-- `continue s` means that `continue` was called, meaning that we should continue - to the next iteration of the containing loop -/ - continue : σ → DoResultPRBC α β σ + /-- `pure (a : α) s` means that the block exited normally with return value `a` -/ + | pure : α → σ → DoResultPRBC α β σ + /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/ + | return : β → σ → DoResultPRBC α β σ + /-- `break s` means that `break` was called, meaning that we should exit + from the containing loop -/ + | break : σ → DoResultPRBC α β σ + /-- `continue s` means that `continue` was called, meaning that we should continue + to the next iteration of the containing loop -/ + | continue : σ → DoResultPRBC α β σ /-- Auxiliary type used to compile `do` notation. It is the same as @@ -293,10 +293,10 @@ Auxiliary type used to compile `do` notation. It is the same as because we are not in a loop context. -/ inductive DoResultPR (α β σ : Type u) where - | /-- `pure (a : α) s` means that the block exited normally with return value `a` -/ - pure : α → σ → DoResultPR α β σ - | /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/ - return : β → σ → DoResultPR α β σ + /-- `pure (a : α) s` means that the block exited normally with return value `a` -/ + | pure : α → σ → DoResultPR α β σ + /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/ + | return : β → σ → DoResultPR α β σ /-- Auxiliary type used to compile `do` notation. It is an optimization of @@ -304,12 +304,12 @@ Auxiliary type used to compile `do` notation. It is an optimization of used when neither `pure` nor `return` are possible exit paths. -/ inductive DoResultBC (σ : Type u) where - | /-- `break s` means that `break` was called, meaning that we should exit - from the containing loop -/ - break : σ → DoResultBC σ - | /-- `continue s` means that `continue` was called, meaning that we should continue - to the next iteration of the containing loop -/ - continue : σ → DoResultBC σ + /-- `break s` means that `break` was called, meaning that we should exit + from the containing loop -/ + | break : σ → DoResultBC σ + /-- `continue s` means that `continue` was called, meaning that we should continue + to the next iteration of the containing loop -/ + | continue : σ → DoResultBC σ /-- Auxiliary type used to compile `do` notation. It is an optimization of @@ -317,18 +317,18 @@ either `DoResultPRBC α PEmpty σ` or `DoResultPRBC PEmpty α σ` to remove the impossible case, used when either `pure` or `return` is never used. -/ inductive DoResultSBC (α σ : Type u) where - | /-- This encodes either `pure (a : α)` or `return (a : α)`: - * `pure (a : α) s` means that the block exited normally with return value `a` - * `return (b : β) s` means that the block exited via a `return b` early-exit command + /-- This encodes either `pure (a : α)` or `return (a : α)`: + * `pure (a : α) s` means that the block exited normally with return value `a` + * `return (b : β) s` means that the block exited via a `return b` early-exit command - The one that is actually encoded depends on the context of use. -/ - pureReturn : α → σ → DoResultSBC α σ - | /-- `break s` means that `break` was called, meaning that we should exit - from the containing loop -/ - break : σ → DoResultSBC α σ - | /-- `continue s` means that `continue` was called, meaning that we should continue - to the next iteration of the containing loop -/ - continue : σ → DoResultSBC α σ + The one that is actually encoded depends on the context of use. -/ + | pureReturn : α → σ → DoResultSBC α σ + /-- `break s` means that `break` was called, meaning that we should exit + from the containing loop -/ + | break : σ → DoResultSBC α σ + /-- `continue s` means that `continue` was called, meaning that we should continue + to the next iteration of the containing loop -/ + | continue : σ → DoResultSBC α σ /-- `HasEquiv α` is the typeclass which supports the notation `x ≈ y` where `x y : α`.-/ class HasEquiv (α : Sort u) where @@ -450,8 +450,8 @@ This is the universe-polymorphic version of `PNonScalar`; it is preferred to use `NonScalar` instead where applicable. -/ inductive PNonScalar : Type u where - | /-- You should not use this function -/ - mk (v : Nat) : PNonScalar + /-- You should not use this function -/ + | mk (v : Nat) : PNonScalar @[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl @@ -932,10 +932,10 @@ transitive and contains `r`. `r⁺ a z` if and only if there exists a sequence `a r b r ... r z` of length at least 1 connecting `a` to `z`. -/ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where - | /-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/ - base : ∀ a b, r a b → TC r a b - | /-- The transitive closure is transitive. -/ - trans : ∀ a b c, TC r a b → TC r b c → TC r a c + /-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/ + | base : ∀ a b, r a b → TC r a b + /-- The transitive closure is transitive. -/ + | trans : ∀ a b c, TC r a b → TC r b c → TC r a c /-! # Subtype -/ diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index 908da26326..cfaef5f975 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -36,32 +36,32 @@ open Format in The pretty-printing algorithm is based on Wadler's paper [_A Prettier Printer_](https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf). -/ inductive Format where - | /-- The empty format. -/ - nil : Format - | /-- A position where a newline may be inserted + /-- The empty format. -/ + | nil : Format + /-- A position where a newline may be inserted if the current group does not fit within the allotted column width. -/ - line : Format - | /-- A node containing a plain string. -/ - text : String → Format - | /-- `nest n f` tells the formatter that `f` is nested inside something with length `n` - so that it is pretty-printed with the correct indentation on a line break. - For example, we can define a formatter for list `l : List Format` as: + | line : Format + /-- A node containing a plain string. -/ + | text : String → Format + /-- `nest n f` tells the formatter that `f` is nested inside something with length `n` + so that it is pretty-printed with the correct indentation on a line break. + For example, we can define a formatter for list `l : List Format` as: - ``` - let f := join <| l.intersperse <| ", " ++ Format.line - group (nest 1 <| "[" ++ f ++ "]") - ``` + ``` + let f := join <| l.intersperse <| ", " ++ Format.line + group (nest 1 <| "[" ++ f ++ "]") + ``` - This will be written all on one line, but if the text is too large, - the formatter will put in linebreaks after the commas and indent later lines by 1. - -/ - nest (indent : Int) : Format → Format - | /-- Concatenation of two Formats. -/ - append : Format → Format → Format - | /-- Creates a new flattening group for the given inner format. -/ - group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format - | /-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/ - tag : Nat → Format → Format + This will be written all on one line, but if the text is too large, + the formatter will put in linebreaks after the commas and indent later lines by 1. + -/ + | nest (indent : Int) : Format → Format + /-- Concatenation of two Formats. -/ + | append : Format → Format → Format + /-- Creates a new flattening group for the given inner format. -/ + | group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format + /-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/ + | tag : Nat → Format → Format deriving Inhabited namespace Format diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 3dda518619..1fb2949ceb 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1187,12 +1187,12 @@ inductive TransparencyMode where deriving Inhabited, BEq, Repr inductive EtaStructMode where - | /-- Enable eta for structure and classes. -/ - all - | /-- Enable eta only for structures that are not classes. -/ - notClasses - | /-- Disable eta for structures and classes. -/ - none + /-- Enable eta for structure and classes. -/ + | all + /-- Enable eta only for structures that are not classes. -/ + | notClasses + /-- Disable eta for structures and classes. -/ + | none deriving Inhabited, BEq, Repr namespace DSimp diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 7ac6485c4b..b45809b457 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -107,8 +107,8 @@ This is the universe-polymorphic version of `Unit`; it is preferred to use For more information about universe levels: [Types as objects](https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects) -/ inductive PUnit : Sort u where - | /-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/ - unit : PUnit + /-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/ + | unit : PUnit /-- The unit type, the canonical type with one element, named `unit` or `()`. @@ -177,9 +177,9 @@ In other words, `True` is simply true, and has a canonical proof, `True.intro` For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic) -/ inductive True : Prop where - | /-- `True` is true, and `True.intro` (or more commonly, `trivial`) - is the proof. -/ - intro : True + /-- `True` is true, and `True.intro` (or more commonly, `trivial`) + is the proof. -/ + | intro : True /-- `False` is the empty proposition. Thus, it has no introduction rules. @@ -264,9 +264,9 @@ The triangle in the second presentation is a macro built on top of `Eq.subst` an For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ inductive Eq : α → α → Prop where - | /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the - equality type. See also `rfl`, which is usually used instead. -/ - refl (a : α) : Eq a a + /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the + equality type. See also `rfl`, which is usually used instead. -/ + | refl (a : α) : Eq a a /-- Non-dependent recursor for the equality type. -/ @[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := @@ -444,8 +444,8 @@ and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`. the same type then `a = b` and `HEq a b` ae equivalent. -/ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where - | /-- Reflexivity of heterogeneous equality. -/ - refl (a : α) : HEq a a + /-- Reflexivity of heterogeneous equality. -/ + | refl (a : α) : HEq a a /-- A version of `HEq.refl` with an implicit argument. -/ @[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a := @@ -516,10 +516,10 @@ and you can use `match` or `cases` to destruct an `Or` assumption into the two cases. -/ inductive Or (a b : Prop) : Prop where - | /-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/ - inl (h : a) : Or a b - | /-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/ - inr (h : b) : Or a b + /-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/ + | inl (h : a) : Or a b + /-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/ + | inr (h : b) : Or a b /-- Alias for `Or.inl`. -/ theorem Or.intro_left (b : Prop) (h : a) : Or a b := @@ -546,10 +546,10 @@ code generator, while `Bool` corresponds to the type called `bool` or `boolean` in most programming languages. -/ inductive Bool : Type where - | /-- The boolean value `false`, not to be confused with the proposition `False`. -/ - false : Bool - | /-- The boolean value `true`, not to be confused with the proposition `True`. -/ - true : Bool + /-- The boolean value `false`, not to be confused with the proposition `False`. -/ + | false : Bool + /-- The boolean value `true`, not to be confused with the proposition `True`. -/ + | true : Bool export Bool (false true) @@ -664,8 +664,8 @@ Given `Nonempty α`, you can construct an element of `α` *nonconstructively* using `Classical.choice`. -/ class inductive Nonempty (α : Sort u) : Prop where - | /-- If `val : α`, then `α` is nonempty. -/ - intro (val : α) : Nonempty α + /-- If `val : α`, then `α` is nonempty. -/ + | intro (val : α) : Nonempty α /-- **The axiom of choice**. `Nonempty α` is a proof that `α` has an element, @@ -788,10 +788,10 @@ If a proposition `p` is `Decidable`, then `(by decide : p)` will prove it by evaluating the decidability instance to `isTrue h` and returning `h`. -/ class inductive Decidable (p : Prop) where - | /-- Prove that `p` is decidable by supplying a proof of `¬p` -/ - isFalse (h : Not p) : Decidable p - | /-- Prove that `p` is decidable by supplying a proof of `p` -/ - isTrue (h : p) : Decidable p + /-- Prove that `p` is decidable by supplying a proof of `¬p` -/ + | isFalse (h : Not p) : Decidable p + /-- Prove that `p` is decidable by supplying a proof of `p` -/ + | isTrue (h : p) : Decidable p /-- Convert a decidable proposition into a boolean value. @@ -1012,12 +1012,12 @@ This type is special-cased by both the kernel and the compiler: library (usually [GMP](https://gmplib.org/)). -/ inductive Nat where - | /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number. - This is one of the two constructors of `Nat`. -/ - zero : Nat - | /-- The successor function on natural numbers, `succ n = n + 1`. - This is one of the two constructors of `Nat`. -/ - succ (n : Nat) : Nat + /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number. + This is one of the two constructors of `Nat`. -/ + | zero : Nat + /-- The successor function on natural numbers, `succ n = n + 1`. + This is one of the two constructors of `Nat`. -/ + | succ (n : Nat) : Nat instance : Inhabited Nat where default := Nat.zero @@ -1517,10 +1517,10 @@ An inductive definition of the less-equal relation on natural numbers, characterized as the least relation `≤` such that `n ≤ n` and `n ≤ m → n ≤ m + 1`. -/ protected inductive Nat.le (n : Nat) : Nat → Prop - | /-- Less-equal is reflexive: `n ≤ n` -/ - refl : Nat.le n n - | /-- If `n ≤ m`, then `n ≤ m + 1`. -/ - step {m} : Nat.le n m → Nat.le n (succ m) + /-- Less-equal is reflexive: `n ≤ n` -/ + | refl : Nat.le n n + /-- If `n ≤ m`, then `n ≤ m + 1`. -/ + | step {m} : Nat.le n m → Nat.le n (succ m) instance : LE Nat where le := Nat.le @@ -2097,10 +2097,10 @@ def map (f : α → β) (x : Option α) : Option β := ``` -/ inductive Option (α : Type u) where - | /-- No value. -/ - none : Option α - | /-- Some value of type `α`. -/ - some (val : α) : Option α + /-- No value. -/ + | none : Option α + /-- Some value of type `α`. -/ + | some (val : α) : Option α attribute [unbox] Option @@ -2140,11 +2140,11 @@ It is implemented as a linked list. performance because it can do destructive updates. -/ inductive List (α : Type u) where - | /-- `[]` is the empty list. -/ - nil : List α - | /-- If `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the - list whose first element is `a` and with `l` as the rest of the list. -/ - cons (head : α) (tail : List α) : List α + /-- `[]` is the empty list. -/ + | nil : List α + /-- If `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the + list whose first element is `a` and with `l` as the rest of the list. -/ + | cons (head : α) (tail : List α) : List α instance {α} : Inhabited (List α) where default := List.nil @@ -2746,10 +2746,10 @@ value of type `α`. The error type is listed first because operation returns the first encountered `error`. -/ inductive Except (ε : Type u) (α : Type v) where - | /-- A failure value of type `ε` -/ - error : ε → Except ε α - | /-- A success value of type `α` -/ - ok : α → Except ε α + /-- A failure value of type `ε` -/ + | error : ε → Except ε α + /-- A success value of type `α` -/ + | ok : α → Except ε α attribute [unbox] Except @@ -3070,10 +3070,10 @@ namespace EStateM combined inductive yields a more efficient data representation. -/ inductive Result (ε σ α : Type u) where - | /-- A success value of type `α`, and a new state `σ`. -/ - ok : α → σ → Result ε σ α - | /-- A failure value of type `ε`, and a new state `σ`. -/ - error : ε → σ → Result ε σ α + /-- A success value of type `α`, and a new state `σ`. -/ + | ok : α → σ → Result ε σ α + /-- A failure value of type `ε`, and a new state `σ`. -/ + | error : ε → σ → Result ε σ α variable {ε σ α : Type u} @@ -3276,23 +3276,23 @@ corresponds to a Lean declaration in scope. If the name is not in scope, Lean will report an error. -/ inductive Name where - | /-- The "anonymous" name. -/ - anonymous : Name - | /-- - A string name. The name `Lean.Meta.run` is represented at - ```lean - .str (.str (.str .anonymous "Lean") "Meta") "run" - ``` - -/ - str (pre : Name) (str : String) - | /-- - A numerical name. This kind of name is used, for example, to create hierarchical names for - free variables and metavariables. The identifier `_uniq.231` is represented as - ```lean - .num (.str .anonymous "_uniq") 231 - ``` - -/ - num (pre : Name) (i : Nat) + /-- The "anonymous" name. -/ + | anonymous : Name + /-- + A string name. The name `Lean.Meta.run` is represented at + ```lean + .str (.str (.str .anonymous "Lean") "Meta") "run" + ``` + -/ + | str (pre : Name) (str : String) + /-- + A numerical name. This kind of name is used, for example, to create hierarchical names for + free variables and metavariables. The identifier `_uniq.231` is represented as + ```lean + .num (.str .anonymous "_uniq") 231 + ``` + -/ + | num (pre : Name) (i : Nat) with /-- A hash function for names, which is stored inside the name itself as a computed field. -/ @@ -3361,22 +3361,20 @@ end Name /-- Source information of tokens. -/ inductive SourceInfo where - | /-- - Token from original input with whitespace and position information. - `leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing, - it is not at all clear what the preceding token was, especially with backtracking. - -/ - original (leading : Substring) (pos : String.Pos) (trailing : Substring) (endPos : String.Pos) - | /-- - Synthesized syntax (e.g. from a quotation) annotated with a span from the original source. - In the delaborator, we "misuse" this constructor to store synthetic positions identifying - subterms. - -/ - synthetic (pos : String.Pos) (endPos : String.Pos) - | /-- - Synthesized token without position information. - -/ - protected none + /-- + Token from original input with whitespace and position information. + `leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing, + it is not at all clear what the preceding token was, especially with backtracking. + -/ + | original (leading : Substring) (pos : String.Pos) (trailing : Substring) (endPos : String.Pos) + /-- + Synthesized syntax (e.g. from a quotation) annotated with a span from the original source. + In the delaborator, we "misuse" this constructor to store synthetic positions identifying + subterms. + -/ + | synthetic (pos : String.Pos) (endPos : String.Pos) + /-- Synthesized token without position information. -/ + | protected none instance : Inhabited SourceInfo := ⟨SourceInfo.none⟩ @@ -3411,50 +3409,50 @@ Note: We do not statically know whether a syntax expects a namespace or term nam so a `Syntax.ident` may contain both preresolution kinds. -/ inductive Syntax.Preresolved where - | /-- A potential namespace reference -/ - namespace (ns : Name) - | /-- A potential global constant or section variable reference, with additional field accesses -/ - decl (n : Name) (fields : List String) + /-- A potential namespace reference -/ + | namespace (ns : Name) + /-- A potential global constant or section variable reference, with additional field accesses -/ + | decl (n : Name) (fields : List String) /-- Syntax objects used by the parser, macro expander, delaborator, etc. -/ inductive Syntax where - | /-- A `missing` syntax corresponds to a portion of the syntax tree that is - missing because of a parse error. The indexing operator on Syntax also - returns `missing` for indexing out of bounds. -/ - missing : Syntax - | /-- Node in the syntax tree. + /-- A `missing` syntax corresponds to a portion of the syntax tree that is + missing because of a parse error. The indexing operator on Syntax also + returns `missing` for indexing out of bounds. -/ + | missing : Syntax + /-- Node in the syntax tree. - The `info` field is used by the delaborator to store the position of the - subexpression corresponding to this node. The parser sets the `info` field - to `none`. - The parser sets the `info` field to `none`, with position retrieval continuing recursively. - Nodes created by quotatons use the result from `SourceInfo.fromRef` so that they are marked - as synthetic even when the leading/trailing token is not. - The delaborator uses the `info` field to store the position of the subexpression - corresponding to this node. + The `info` field is used by the delaborator to store the position of the + subexpression corresponding to this node. The parser sets the `info` field + to `none`. + The parser sets the `info` field to `none`, with position retrieval continuing recursively. + Nodes created by quotatons use the result from `SourceInfo.fromRef` so that they are marked + as synthetic even when the leading/trailing token is not. + The delaborator uses the `info` field to store the position of the subexpression + corresponding to this node. - (Remark: the `node` constructor did not have an `info` field in previous - versions. This caused a bug in the interactive widgets, where the popup for - `a + b` was the same as for `a`. The delaborator used to associate - subexpressions with pretty-printed syntax by setting the (string) position - of the first atom/identifier to the (expression) position of the - subexpression. For example, both `a` and `a + b` have the same first - identifier, and so their infos got mixed up.) -/ - node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax - | /-- An `atom` corresponds to a keyword or piece of literal unquoted syntax. - These correspond to quoted strings inside `syntax` declarations. - For example, in `(x + y)`, `"("`, `"+"` and `")"` are `atom` - and `x` and `y` are `ident`. -/ - atom (info : SourceInfo) (val : String) : Syntax - | /-- An `ident` corresponds to an identifier as parsed by the `ident` or - `rawIdent` parsers. - * `rawVal` is the literal substring from the input file - * `val` is the parsed identifier (with hygiene) - * `preresolved` is the list of possible declarations this could refer to - -/ - ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Syntax.Preresolved) : Syntax + (Remark: the `node` constructor did not have an `info` field in previous + versions. This caused a bug in the interactive widgets, where the popup for + `a + b` was the same as for `a`. The delaborator used to associate + subexpressions with pretty-printed syntax by setting the (string) position + of the first atom/identifier to the (expression) position of the + subexpression. For example, both `a` and `a + b` have the same first + identifier, and so their infos got mixed up.) -/ + | node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax + /-- An `atom` corresponds to a keyword or piece of literal unquoted syntax. + These correspond to quoted strings inside `syntax` declarations. + For example, in `(x + y)`, `"("`, `"+"` and `")"` are `atom` + and `x` and `y` are `ident`. -/ + | atom (info : SourceInfo) (val : String) : Syntax + /-- An `ident` corresponds to an identifier as parsed by the `ident` or + `rawIdent` parsers. + * `rawVal` is the literal substring from the input file + * `val` is the parsed identifier (with hygiene) + * `preresolved` is the list of possible declarations this could refer to + -/ + | ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Syntax.Preresolved) : Syntax /-- `SyntaxNodeKinds` is a set of `SyntaxNodeKind` (implemented as a list). -/ def SyntaxNodeKinds := List SyntaxNodeKind @@ -3739,48 +3737,48 @@ A `ParserDescr` is a grammar for parsers. This is used by the `syntax` command to produce parsers without having to `import Lean`. -/ inductive ParserDescr where - | /-- A (named) nullary parser, like `ppSpace` -/ - const (name : Name) - | /-- A (named) unary parser, like `group(p)` -/ - unary (name : Name) (p : ParserDescr) - | /-- A (named) binary parser, like `orelse` or `andthen` - (written as `p1 <|> p2` and `p1 p2` respectively in `syntax`) -/ - binary (name : Name) (p₁ p₂ : ParserDescr) - | /-- Parses using `p`, then pops the stack to create a new node with kind `kind`. - The precedence `prec` is used to determine whether the parser should apply given - the current precedence level. -/ - node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr) - | /-- Like `node` but for trailing parsers (which start with a nonterminal). - Assumes the lhs is already on the stack, and parses using `p`, then pops the - stack including the lhs to create a new node with kind `kind`. - The precedence `prec` and `lhsPrec` are used to determine whether the parser - should apply. -/ - trailingNode (kind : SyntaxNodeKind) (prec lhsPrec : Nat) (p : ParserDescr) - | /-- A literal symbol parser: parses `val` as a literal. - This parser does not work on identifiers, so `symbol` arguments are declared - as "keywords" and cannot be used as identifiers anywhere in the file. -/ - symbol (val : String) - | /-- Like `symbol`, but without reserving `val` as a keyword. - If `includeIdent` is true then `ident` will be reinterpreted as `atom` if it matches. -/ - nonReservedSymbol (val : String) (includeIdent : Bool) - | /-- Parses using the category parser `catName` with right binding power - (i.e. precedence) `rbp`. -/ - cat (catName : Name) (rbp : Nat) - | /-- Parses using another parser `declName`, which can be either - a `Parser` or `ParserDescr`. -/ - parser (declName : Name) - | /-- Like `node`, but also declares that the body can be matched using an antiquotation - with name `name`. For example, `def $id:declId := 1` uses an antiquotation with - name `declId` in the place where a `declId` is expected. -/ - nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr) - | /-- A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`. - `psep` is usually the same as `symbol sep`, but it can be overridden. - `sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`. - `allowTrailingSep` is true if e.g. `a, b,` is also allowed to match. -/ - sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) - | /-- `sepBy1` is just like `sepBy`, except it takes 1 or more instead of - 0 or more occurrences of `p`. -/ - sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) + /-- A (named) nullary parser, like `ppSpace` -/ + | const (name : Name) + /-- A (named) unary parser, like `group(p)` -/ + | unary (name : Name) (p : ParserDescr) + /-- A (named) binary parser, like `orelse` or `andthen` + (written as `p1 <|> p2` and `p1 p2` respectively in `syntax`) -/ + | binary (name : Name) (p₁ p₂ : ParserDescr) + /-- Parses using `p`, then pops the stack to create a new node with kind `kind`. + The precedence `prec` is used to determine whether the parser should apply given + the current precedence level. -/ + | node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr) + /-- Like `node` but for trailing parsers (which start with a nonterminal). + Assumes the lhs is already on the stack, and parses using `p`, then pops the + stack including the lhs to create a new node with kind `kind`. + The precedence `prec` and `lhsPrec` are used to determine whether the parser + should apply. -/ + | trailingNode (kind : SyntaxNodeKind) (prec lhsPrec : Nat) (p : ParserDescr) + /-- A literal symbol parser: parses `val` as a literal. + This parser does not work on identifiers, so `symbol` arguments are declared + as "keywords" and cannot be used as identifiers anywhere in the file. -/ + | symbol (val : String) + /-- Like `symbol`, but without reserving `val` as a keyword. + If `includeIdent` is true then `ident` will be reinterpreted as `atom` if it matches. -/ + | nonReservedSymbol (val : String) (includeIdent : Bool) + /-- Parses using the category parser `catName` with right binding power + (i.e. precedence) `rbp`. -/ + | cat (catName : Name) (rbp : Nat) + /-- Parses using another parser `declName`, which can be either + a `Parser` or `ParserDescr`. -/ + | parser (declName : Name) + /-- Like `node`, but also declares that the body can be matched using an antiquotation + with name `name`. For example, `def $id:declId := 1` uses an antiquotation with + name `declId` in the place where a `declId` is expected. -/ + | nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr) + /-- A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`. + `psep` is usually the same as `symbol sep`, but it can be overridden. + `sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`. + `allowTrailingSep` is true if e.g. `a, b,` is also allowed to match. -/ + | sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) + /-- `sepBy1` is just like `sepBy`, except it takes 1 or more instead of + 0 or more occurrences of `p`. -/ + | sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) instance : Inhabited ParserDescr where default := ParserDescr.symbol "" @@ -4092,12 +4090,12 @@ structure Context where /-- An exception in the `MacroM` monad. -/ inductive Exception where - | /-- A general error, given a message and a span (expressed as a `Syntax`). -/ - error : Syntax → String → Exception - | /-- An unsupported syntax exception. We keep this separate because it is - used for control flow: if one macro does not support a syntax then we try - the next one. -/ - unsupportedSyntax : Exception + /-- A general error, given a message and a span (expressed as a `Syntax`). -/ + | error : Syntax → String → Exception + /-- An unsupported syntax exception. We keep this separate because it is + used for control flow: if one macro does not support a syntax then we try + the next one. -/ + | unsupportedSyntax : Exception /-- The mutable state for the `MacroM` monad. -/ structure State where diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 7f9f8f41c9..c15664726b 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -191,36 +191,36 @@ def CtorInfo.isScalar (info : CtorInfo) : Bool := !info.isRef inductive Expr where - | /-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime. - This instruction is also used to creat `struct` and `union` return values. - For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/ - ctor (i : CtorInfo) (ys : Array Arg) + /-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime. + This instruction is also used to creat `struct` and `union` return values. + For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/ + | ctor (i : CtorInfo) (ys : Array Arg) | reset (n : Nat) (x : VarId) - | /-- `reuse x in ctor_i ys` instruction in the paper. -/ - reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg) - | /-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`. - We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/ - proj (i : Nat) (x : VarId) - | /-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/ - uproj (i : Nat) (x : VarId) - | /-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/ - sproj (n : Nat) (offset : Nat) (x : VarId) - | /-- Full application. -/ - fap (c : FunId) (ys : Array Arg) - | /-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/ - pap (c : FunId) (ys : Array Arg) - | /-- Application. `x` must be a `pap` value. -/ - ap (x : VarId) (ys : Array Arg) - | /-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`. - For small scalar values, the Result is a tagged pointer, and no memory allocation is performed. -/ - box (ty : IRType) (x : VarId) - | /-- Given `x : [t]object`, obtain the scalar value. -/ - unbox (x : VarId) + /-- `reuse x in ctor_i ys` instruction in the paper. -/ + | reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg) + /-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`. + We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/ + | proj (i : Nat) (x : VarId) + /-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/ + | uproj (i : Nat) (x : VarId) + /-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/ + | sproj (n : Nat) (offset : Nat) (x : VarId) + /-- Full application. -/ + | fap (c : FunId) (ys : Array Arg) + /-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/ + | pap (c : FunId) (ys : Array Arg) + /-- Application. `x` must be a `pap` value. -/ + | ap (x : VarId) (ys : Array Arg) + /-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`. + For small scalar values, the Result is a tagged pointer, and no memory allocation is performed. -/ + | box (ty : IRType) (x : VarId) + /-- Given `x : [t]object`, obtain the scalar value. -/ + | unbox (x : VarId) | lit (v : LitVal) - | /-- Return `1 : uint8` Iff `RC(x) > 1` -/ - isShared (x : VarId) - | /-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/ - isTaggedPtr (x : VarId) + /-- Return `1 : uint8` Iff `RC(x) > 1` -/ + | isShared (x : VarId) + /-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/ + | isTaggedPtr (x : VarId) @[export lean_ir_mk_ctor_expr] def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr := Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys @@ -247,31 +247,31 @@ inductive AltCore (FnBody : Type) : Type where | default (b : FnBody) : AltCore FnBody inductive FnBody where - | /-- `let x : ty := e; b` -/ - vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) - | /-- Join point Declaration `block_j (xs) := e; b` -/ - jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) - | /-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. - This operation is not part of λPure is only used during optimization. -/ - set (x : VarId) (i : Nat) (y : Arg) (b : FnBody) + /-- `let x : ty := e; b` -/ + | vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) + /-- Join point Declaration `block_j (xs) := e; b` -/ + | jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) + /-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. + This operation is not part of λPure is only used during optimization. -/ + | set (x : VarId) (i : Nat) (y : Arg) (b : FnBody) | setTag (x : VarId) (cidx : Nat) (b : FnBody) - | /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/ - uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody) - | /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. - `ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/ - sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) - | /-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. - If `persistent == true` then `x` is statically known to be a persistent object. -/ - inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) - | /-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. - If `persistent == true` then `x` is statically known to be a persistent object. -/ - dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) + /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/ + | uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody) + /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. + `ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/ + | sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) + /-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. + If `persistent == true` then `x` is statically known to be a persistent object. -/ + | inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) + /-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. + If `persistent == true` then `x` is statically known to be a persistent object. -/ + | dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) | del (x : VarId) (b : FnBody) | mdata (d : MData) (b : FnBody) | case (tid : Name) (x : VarId) (xType : IRType) (cs : Array (AltCore FnBody)) | ret (x : Arg) - | /-- Jump to join point `j` -/ - jmp (j : JoinPointId) (ys : Array Arg) + /-- Jump to join point `j` -/ + | jmp (j : JoinPointId) (ys : Array Arg) | unreachable instance : Inhabited FnBody := ⟨FnBody.unreachable⟩ diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index e3a0a9ccde..44cab01fd0 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -15,13 +15,13 @@ namespace Lean.Compiler.LCNF The pipeline phase a certain `Pass` is supposed to happen in. -/ inductive Phase where -| /-- Here we still carry most of the original type information, most - of the dependent portion is already (partially) erased though. -/ - base -| /-- In this phase polymorphism has been eliminated. -/ - mono -| /-- In this phase impure stuff such as RC or efficient BaseIO transformations happen. -/ - impure + /-- Here we still carry most of the original type information, most + of the dependent portion is already (partially) erased though. -/ + | base + /-- In this phase polymorphism has been eliminated. -/ + | mono + /-- In this phase impure stuff such as RC or efficient BaseIO transformations happen. -/ + | impure deriving Inhabited /-- diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 2a48399e0b..f402eee2a2 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -50,19 +50,19 @@ a big problem in practice because we run the simplifier multiple times, and this is recomputed from scratch at the beginning of each simplification step. -/ inductive FunDeclInfo where - | /-- - Local function is applied once, and must be inlined. - -/ - once - | /-- - Local function is applied many times, and will only be inlined - if it is small. - -/ - many - | /-- - Function must be inlined. - -/ - mustInline + /-- + Local function is applied once, and must be inlined. + -/ + | once + /-- + Local function is applied many times, and will only be inlined + if it is small. + -/ + | many + /-- + Function must be inlined. + -/ + | mustInline deriving Repr, Inhabited /-- diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 23434382aa..41409a3d58 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -13,31 +13,31 @@ namespace Lean.Compiler.LCNF Each parameter is associated with a `SpecParamInfo`. This information is used by `LCNF/Specialize.lean`. -/ inductive SpecParamInfo where - | /-- - A parameter that is an type class instance (or an arrow that produces a type class instance), - and is fixed in recursive declarations. By default, Lean always specializes this kind of argument. - -/ - fixedInst - | /-- - A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration - with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize - `.fixedHO` arguments in addition to `.fixedInst`. - -/ - fixedHO - | /-- - Computationally irrelevant parameters that are fixed in recursive declarations. - -/ - fixedNeutral - | /-- - An argument that has been specified in the `@[specialize]` attribute. Lean specializes it even if it is - not fixed in recursive declarations. Non-termination can happen, and Lean interrupts it with an error message - based on the stack depth. - -/ - user - | /-- - Parameter is not going to be specialized. - -/ - other + /-- + A parameter that is an type class instance (or an arrow that produces a type class instance), + and is fixed in recursive declarations. By default, Lean always specializes this kind of argument. + -/ + | fixedInst + /-- + A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration + with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize + `.fixedHO` arguments in addition to `.fixedInst`. + -/ + | fixedHO + /-- + Computationally irrelevant parameters that are fixed in recursive declarations. + -/ + | fixedNeutral + /-- + An argument that has been specified in the `@[specialize]` attribute. Lean specializes it even if it is + not fixed in recursive declarations. Non-termination can happen, and Lean interrupts it with an error message + based on the stack depth. + -/ + | user + /-- + Parameter is not going to be specialized. + -/ + | other deriving Inhabited, Repr instance : ToMessageData SpecParamInfo where diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index bc1579f947..ebf8504394 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -37,32 +37,32 @@ instance : ToString RequestID where [JSON-RPC](https://www.jsonrpc.org/specification#error_object) and [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#errorCodes). -/ inductive ErrorCode where - | /-- Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.-/ - parseError - | /-- The JSON sent is not a valid Request object. -/ - invalidRequest - | /-- The method does not exist / is not available. -/ - methodNotFound - | /-- Invalid method parameter(s). -/ - invalidParams - | /-- Internal JSON-RPC error. -/ - internalError - | /-- Error code indicating that a server received a notification or - request before the server has received the `initialize` request. -/ - serverNotInitialized + /-- Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.-/ + | parseError + /-- The JSON sent is not a valid Request object. -/ + | invalidRequest + /-- The method does not exist / is not available. -/ + | methodNotFound + /-- Invalid method parameter(s). -/ + | invalidParams + /-- Internal JSON-RPC error. -/ + | internalError + /-- Error code indicating that a server received a notification or + request before the server has received the `initialize` request. -/ + | serverNotInitialized | unknownErrorCode -- LSP-specific codes below. - | /-- The server detected that the content of a document got - modified outside normal conditions. A server should - NOT send this error code if it detects a content change - in it unprocessed messages. The result even computed - on an older state might still be useful for the client. + /-- The server detected that the content of a document got + modified outside normal conditions. A server should + NOT send this error code if it detects a content change + in it unprocessed messages. The result even computed + on an older state might still be useful for the client. - If a client decides that a result is not of any use anymore - the client should cancel the request. -/ - contentModified - | /-- The client has canceled a request and a server as detected the cancel. -/ - requestCancelled + If a client decides that a result is not of any use anymore + the client should cancel the request. -/ + | contentModified + /-- The client has canceled a request and a server as detected the cancel. -/ + | requestCancelled -- Lean-specific codes below. | rpcNeedsReconnect | workerExited @@ -104,14 +104,14 @@ Uses separate constructors for notifications and errors because client and serve behavior is expected to be wildly different for both. -/ inductive Message where - | /-- A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request. -/ - request (id : RequestID) (method : String) (params? : Option Structured) - | /-- A notification message. A processed notification message must not send a response back. They work like events. -/ - notification (method : String) (params? : Option Structured) - | /-- A Response Message sent as a result of a request. -/ - response (id : RequestID) (result : Json) - | /-- A non-successful response. -/ - responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) + /-- A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request. -/ + | request (id : RequestID) (method : String) (params? : Option Structured) + /-- A notification message. A processed notification message must not send a response back. They work like events. -/ + | notification (method : String) (params? : Option Structured) + /-- A Response Message sent as a result of a request. -/ + | response (id : RequestID) (result : Json) + /-- A non-successful response. -/ + | responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) def Batch := Array Message diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 3d97cc69c5..2754e14db5 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -187,15 +187,15 @@ structure Alt (σ : Type) where inductive Code where | decl (xs : Array Var) (doElem : Syntax) (k : Code) | reassign (xs : Array Var) (doElem : Syntax) (k : Code) - | /-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/ - joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code) + /-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/ + | joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code) | seq (action : Syntax) (k : Code) | action (action : Syntax) | break (ref : Syntax) | continue (ref : Syntax) | return (ref : Syntax) (val : Syntax) - | /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/ - ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) + /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/ + | ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) | match (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code)) | jmp (ref : Syntax) (jpName : Name) (args : Array Syntax) deriving Inhabited diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index f282b120b7..d06c281f7b 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -128,18 +128,18 @@ there is no coercion `Matrix Real 5 4` from `Matrix Real 4 8` and vice-versa, bu -/ private inductive Tree where - | /-- - Leaf of the tree. - We store the `infoTrees` generated when elaborating `val`. These trees become - subtrees of the infotree nodes generated for `op` nodes. - -/ - term (ref : Syntax) (infoTrees : Std.PersistentArray InfoTree) (val : Expr) - | /-- - `ref` is the original syntax that expanded into `binop%`. - `macroName` is the `macro_rule` that produce the expansion. We store this information - here to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator. - -/ - op (ref : Syntax) (macroName : Name) (lazy : Bool) (f : Expr) (lhs rhs : Tree) + /-- + Leaf of the tree. + We store the `infoTrees` generated when elaborating `val`. These trees become + subtrees of the infotree nodes generated for `op` nodes. + -/ + | term (ref : Syntax) (infoTrees : Std.PersistentArray InfoTree) (val : Expr) + /-- + `ref` is the original syntax that expanded into `binop%`. + `macroName` is the `macro_rule` that produce the expansion. We store this information + here to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator. + -/ + | op (ref : Syntax) (macroName : Name) (lazy : Bool) (f : Expr) (lhs rhs : Tree) private partial def toTree (s : Syntax) : TermElabM Tree := do /- diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index d6b8e3e0cf..ab6aa28e46 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -150,12 +150,12 @@ inductive Info where `hole`s which are filled in later in the same way that unassigned metavariables are. -/ inductive InfoTree where - | /-- The context object is created by `liftTermElabM` at `Command.lean` -/ - context (i : ContextInfo) (t : InfoTree) - | /-- The children contain information for nested term elaboration and tactic evaluation -/ - node (i : Info) (children : Std.PersistentArray InfoTree) - | /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/ - hole (mvarId : MVarId) + /-- The context object is created by `liftTermElabM` at `Command.lean` -/ + | context (i : ContextInfo) (t : InfoTree) + /-- The children contain information for nested term elaboration and tactic evaluation -/ + | node (i : Info) (children : Std.PersistentArray InfoTree) + /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/ + | hole (mvarId : MVarId) deriving Inhabited /-- This structure is the state that is being used to build an InfoTree object. diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 9364914659..7c8147b9a0 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -276,35 +276,35 @@ private abbrev Alt := List Term × Term alternative. This datatype describes what kind of check this involves, which helps other patterns decide if they are covered by the same check and don't have to be checked again (see also `MatchResult`). -/ inductive HeadCheck where - | /-- match step that always succeeds: _, x, `($x), ... -/ - unconditional - | /-- match step based on kind and, optionally, arity of discriminant - If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the - same number of new patterns. - We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by - the node kind. - without arity: `($x:k) - with arity: any quotation without an antiquotation head pattern -/ - shape (k : List SyntaxNodeKind) (arity : Option Nat) - | /-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants - for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children. - example: `([$x, $xs,*, $y]) is `slice 2 2` -/ - slice (numPrefix numSuffix : Nat) - | /-- other, complicated match step that will probably only cover identical patterns - example: antiquotation splices `($[...]*) -/ - other (pat : Syntax) + /-- match step that always succeeds: _, x, `($x), ... -/ + | unconditional + /-- match step based on kind and, optionally, arity of discriminant + If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the + same number of new patterns. + We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by + the node kind. + without arity: `($x:k) + with arity: any quotation without an antiquotation head pattern -/ + | shape (k : List SyntaxNodeKind) (arity : Option Nat) + /-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants + for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children. + example: `([$x, $xs,*, $y]) is `slice 2 2` -/ + | slice (numPrefix numSuffix : Nat) + /-- other, complicated match step that will probably only cover identical patterns + example: antiquotation splices `($[...]*) -/ + | other (pat : Syntax) open HeadCheck /-- Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern). -/ inductive MatchResult where - | /-- Pattern agrees with head check, remove and transform remaining alternative. - If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. -/ - covered (f : Alt → TermElabM Alt) (exhaustive : Bool) - | /-- Pattern disagrees with head check, include in "no" branch only -/ - uncovered - | /-- Pattern is not quite sure yet; include unchanged in both branches -/ - undecided + /-- Pattern agrees with head check, remove and transform remaining alternative. + If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. -/ + | covered (f : Alt → TermElabM Alt) (exhaustive : Bool) + /-- Pattern disagrees with head check, include in "no" branch only -/ + | uncovered + /-- Pattern is not quite sure yet; include unchanged in both branches -/ + | undecided open MatchResult diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index f13b473d52..6751f96e81 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -248,8 +248,8 @@ def Field.isSimple {σ} : Field σ → Bool | _ => false inductive Struct where - | /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/ - mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source) + /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/ + | mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source) deriving Inhabited abbrev Fields := List (Field Struct) diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean index 6ae34f3678..51bd35d2b4 100644 --- a/src/Lean/Elab/Tactic/Location.lean +++ b/src/Lean/Elab/Tactic/Location.lean @@ -10,11 +10,11 @@ namespace Lean.Elab.Tactic /-- Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`. -/ inductive Location where - | /-- Apply the tactic everywhere. -/ - wildcard - | /-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to. - If `type` is true, then the tactic should also be applied to the target type. -/ - targets (hypotheses : Array Syntax) (type : Bool) + /-- Apply the tactic everywhere. -/ + | wildcard + /-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to. + If `type` is true, then the tactic should also be applied to the target type. -/ + | targets (hypotheses : Array Syntax) (type : Bool) /- Recall that diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index fd7a34a63a..a9bf02ea7b 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -39,18 +39,18 @@ structure SavedContext where /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/ inductive SyntheticMVarKind where - | /-- Use typeclass resolution to synthesize value for metavariable. -/ - typeClass - | /-- - Similar to `typeClass`, but error messages are different. - if `f?` is `some f`, we produce an application type mismatch error message. - Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` - Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/ - coe (header? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) - | /-- Use tactic to synthesize value for metavariable. -/ - tactic (tacticCode : Syntax) (ctx : SavedContext) - | /-- Metavariable represents a hole whose elaboration has been postponed. -/ - postponed (ctx : SavedContext) + /-- Use typeclass resolution to synthesize value for metavariable. -/ + | typeClass + /-- + Similar to `typeClass`, but error messages are different. + if `f?` is `some f`, we produce an application type mismatch error message. + Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` + Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/ + | coe (header? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) + /-- Use tactic to synthesize value for metavariable. -/ + | tactic (tacticCode : Syntax) (ctx : SavedContext) + /-- Metavariable represents a hole whose elaboration has been postponed. -/ + | postponed (ctx : SavedContext) deriving Inhabited instance : ToString SyntheticMVarKind where @@ -70,12 +70,12 @@ structure SyntheticMVarDecl where We have three different kinds of error context. -/ inductive MVarErrorKind where - | /-- Metavariable for implicit arguments. `ctx` is the parent application. -/ - implicitArg (ctx : Expr) - | /-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/ - hole - | /-- "Custom", `msgData` stores the additional error messages. -/ - custom (msgData : MessageData) + /-- Metavariable for implicit arguments. `ctx` is the parent application. -/ + | implicitArg (ctx : Expr) + /-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/ + | hole + /-- "Custom", `msgData` stores the additional error messages. -/ + | custom (msgData : MessageData) deriving Inhabited instance : ToString MVarErrorKind where @@ -378,9 +378,9 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl -/ inductive LVal where | fieldIdx (ref : Syntax) (i : Nat) - | /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name. - `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/ - fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax) + /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name. + `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/ + | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax) def LVal.getRef : LVal → Syntax | .fieldIdx ref _ => ref diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index ff898eb1af..1a59157eba 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -12,13 +12,13 @@ namespace Lean /-- Exception type used in most Lean monads -/ inductive Exception where - | /-- Error messages that are displayed to users. `ref` is used to provide position information. -/ - error (ref : Syntax) (msg : MessageData) - | /-- - Internal exceptions that are not meant to be seen by users. - Examples: "pospone elaboration", "stuck at universe constraint", etc - -/ - internal (id : InternalExceptionId) (extra : KVMap := {}) + /-- Error messages that are displayed to users. `ref` is used to provide position information. -/ + | error (ref : Syntax) (msg : MessageData) + /-- + Internal exceptions that are not meant to be seen by users. + Examples: "pospone elaboration", "stuck at universe constraint", etc + -/ + | internal (id : InternalExceptionId) (extra : KVMap := {}) /-- Convert exception into a structured message. -/ def Exception.toMessageData : Exception → MessageData diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 33685c5a1f..53f62059ed 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -10,10 +10,10 @@ namespace Lean /-- Literal values for `Expr`. -/ inductive Literal where - | /-- Natural number literal -/ - natVal (val : Nat) - | /-- String literal -/ - strVal (val : String) + /-- Natural number literal -/ + | natVal (val : Nat) + /-- String literal -/ + | strVal (val : String) deriving Inhabited, BEq, Repr protected def Literal.hash : Literal → UInt64 @@ -63,27 +63,27 @@ def bar ⦃x : Nat⦄ : Nat := x See also the Lean manual: https://leanprover.github.io/lean4/doc/expressions.html#implicit-arguments -/ inductive BinderInfo where - | /-- Default binder annotation, e.g. `(x : α)` -/ - default - | /-- Implicit binder annotation, e.g., `{x : α}` -/ - implicit - | /-- Strict implict binder annotation, e.g., `{{ x : α }}` -/ - strictImplicit - | /-- Local instance binder annotataion, e.g., `[Decidable α]` -/ - instImplicit - | /-- - Auxiliary declarations used by Lean when elaborating recursive declarations. - When defining a function such as - ``` - def f : Nat → Nat - | 0 => 1 - | x+1 => (x+1)*f x - ``` - Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`) - with `BinderInfo` set to `auxDecl`. - This local declaration is later removed by the termination checker. - -/ - auxDecl + /-- Default binder annotation, e.g. `(x : α)` -/ + | default + /-- Implicit binder annotation, e.g., `{x : α}` -/ + | implicit + /-- Strict implict binder annotation, e.g., `{{ x : α }}` -/ + | strictImplicit + /-- Local instance binder annotataion, e.g., `[Decidable α]` -/ + | instImplicit + /-- + Auxiliary declarations used by Lean when elaborating recursive declarations. + When defining a function such as + ``` + def f : Nat → Nat + | 0 => 1 + | x+1 => (x+1)*f x + ``` + Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`) + with `BinderInfo` set to `auxDecl`. + This local declaration is later removed by the termination checker. + -/ + | auxDecl deriving Inhabited, BEq, Repr def BinderInfo.hash : BinderInfo → UInt64 @@ -298,134 +298,134 @@ contain metavariables. Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use. -/ inductive Expr where - | /-- - Bound variables. The natural number is the "de Bruijn" index - for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information. - Example, the expression `fun x : Nat => forall y : Nat, x = y` - ```lean - .lam `x (.const `Nat []) - (.forall `y (.const `Nat []) - (.app (.app (.app (.const `Eq [.succ .zero]) - (.const `Nat [])) (.bvar 1)) - (.bvar 0)) - .default) - .default - ``` - -/ - bvar (deBruijnIndex : Nat) - | /-- - Free variable. Lean uses the locally nameless approach. - See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details. - When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables - are converted into free variables using a unique identifier, and their user-facing name, type, - value (for `LetE`), and binder annotation are stored in the `LocalContext`. - -/ - fvar (fvarId : FVarId) - | /-- - Metavariables are used to represent "holes" in expressions, and goals in the - tactic framework. Metavariable declarations are stored in the `MetavarContext`. - Metavariables are used during elaboration, and are not allowed in the kernel, - or in the code generator. - -/ - mvar (mvarId : MVarId) - | /-- - `Type u`, `Sort u`, `Prop`. - - - `Prop` is represented as `.sort .zero`, - - `Sort u` as ``.sort (.param `u)``, and - - `Type u` as ``.sort (.succ (.param `u))`` - -/ - sort (u : Level) - | /-- - A (universe polymorphic) constant. For example, - `@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and - `@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``. - -/ - const (declName : Name) (us : List Level) - | /-- - Function application. `Nat.succ Nat.zero` is represented as - ``` - .app (.const `Nat.succ []) (.const .zero []) - ``` - -/ - app (fn : Expr) (arg : Expr) - | /-- - Lambda abstraction (aka anonymous functions). - - `fun x : Nat => x` is represented as - ``` - .lam `x (.const `Nat []) (.bvar 0) .default - ``` - -/ - lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) - | /-- - A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows. - Examples: - - `forall x : Prop, x ∧ x` is represented as - ``` - .forallE `x - (.sort .zero) - (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) - .default - ``` - - `Nat → Bool` as - ``` - .forallE `a (.const `Nat []) (.const `Bool []) .default - ``` - -/ - forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) - | /-- - Let-expressions. The field `nonDep` is not currently used, but will be used in the future - by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent - or not. + /-- + Bound variables. The natural number is the "de Bruijn" index + for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information. + Example, the expression `fun x : Nat => forall y : Nat, x = y` + ```lean + .lam `x (.const `Nat []) + (.forall `y (.const `Nat []) + (.app (.app (.app (.const `Eq [.succ .zero]) + (.const `Nat [])) (.bvar 1)) + (.bvar 0)) + .default) + .default + ``` + -/ + | bvar (deBruijnIndex : Nat) + /-- + Free variable. Lean uses the locally nameless approach. + See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details. + When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables + are converted into free variables using a unique identifier, and their user-facing name, type, + value (for `LetE`), and binder annotation are stored in the `LocalContext`. + -/ + | fvar (fvarId : FVarId) + /-- + Metavariables are used to represent "holes" in expressions, and goals in the + tactic framework. Metavariable declarations are stored in the `MetavarContext`. + Metavariables are used during elaboration, and are not allowed in the kernel, + or in the code generator. + -/ + | mvar (mvarId : MVarId) + /-- + `Type u`, `Sort u`, `Prop`. - + - `Prop` is represented as `.sort .zero`, + - `Sort u` as ``.sort (.param `u)``, and + - `Type u` as ``.sort (.succ (.param `u))`` + -/ + | sort (u : Level) + /-- + A (universe polymorphic) constant. For example, + `@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and + `@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``. + -/ + | const (declName : Name) (us : List Level) + /-- + Function application. `Nat.succ Nat.zero` is represented as + ``` + .app (.const `Nat.succ []) (.const .zero []) + ``` + -/ + | app (fn : Expr) (arg : Expr) + /-- + Lambda abstraction (aka anonymous functions). + - `fun x : Nat => x` is represented as + ``` + .lam `x (.const `Nat []) (.bvar 0) .default + ``` + -/ + | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) + /-- + A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows. + Examples: + - `forall x : Prop, x ∧ x` is represented as + ``` + .forallE `x + (.sort .zero) + (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) + .default + ``` + - `Nat → Bool` as + ``` + .forallE `a (.const `Nat []) (.const `Bool []) .default + ``` + -/ + | forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) + /-- + Let-expressions. The field `nonDep` is not currently used, but will be used in the future + by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent + or not. - **IMPORTANT**: This flag is for "local" use only. That is, a module should not "trust" its value for any purpose. - In the intended use-case, the compiler will set this flag, and be responsible for maintaining it. - Other modules may not preserve its value while applying transformations. + **IMPORTANT**: This flag is for "local" use only. That is, a module should not "trust" its value for any purpose. + In the intended use-case, the compiler will set this flag, and be responsible for maintaining it. + Other modules may not preserve its value while applying transformations. - Given an environment, metavariable context, and local context, we say a let-expression - `let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`. - Here is an example of a dependent let-expression - `let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but - `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not. - The let-expression `let x : Nat := 2; Nat.succ x` is represented as - ``` - .letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true - ``` - -/ - letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool) - | /-- - Natural number and string literal values. They are not really needed, but provide a more - compact representation in memory for these two kinds of literals, and are used to implement - efficient reduction in the elaborator and kernel. - The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is - definitionally equal to - ``` - .app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero [])) - ``` - -/ - lit : Literal → Expr - | /-- - Metadata (aka annotations). We use annotations to provide hints to the pretty-printer, - store references to `Syntax` nodes, position information, and save information for - elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to - mark `Expr`s that correspond to inaccessible patterns). - Note that `.mdata data e` is definitionally equal to `e`. - -/ - mdata (data : MData) (expr : Expr) - | /-- - Projection-expressions. They are redundant, but are used to create more compact - terms, speedup reduction, and implement eta for structures. - The type of `struct` must be an structure-like inductive type. That is, it has only one - constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators - check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index - is valid (i.e., it is smaller than the numbef of constructor fields). - When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec` - applications. - Example, given `a : Nat x Bool`, `a.1` is represented as - ``` - .proj `Prod 0 a - ``` - -/ - proj (typeName : Name) (idx : Nat) (struct : Expr) + Given an environment, metavariable context, and local context, we say a let-expression + `let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`. + Here is an example of a dependent let-expression + `let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but + `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not. + The let-expression `let x : Nat := 2; Nat.succ x` is represented as + ``` + .letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true + ``` + -/ + | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool) + /-- + Natural number and string literal values. They are not really needed, but provide a more + compact representation in memory for these two kinds of literals, and are used to implement + efficient reduction in the elaborator and kernel. + The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is + definitionally equal to + ``` + .app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero [])) + ``` + -/ + | lit : Literal → Expr + /-- + Metadata (aka annotations). We use annotations to provide hints to the pretty-printer, + store references to `Syntax` nodes, position information, and save information for + elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to + mark `Expr`s that correspond to inaccessible patterns). + Note that `.mdata data e` is definitionally equal to `e`. + -/ + | mdata (data : MData) (expr : Expr) + /-- + Projection-expressions. They are redundant, but are used to create more compact + terms, speedup reduction, and implement eta for structures. + The type of `struct` must be an structure-like inductive type. That is, it has only one + constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators + check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index + is valid (i.e., it is smaller than the numbef of constructor fields). + When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec` + applications. + Example, given `a : Nat x Bool`, `a.1` is represented as + ``` + .proj `Prod 0 a + ``` + -/ + | proj (typeName : Name) (idx : Nat) (struct : Expr) with @[computedField, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"] data : @& Expr → Data diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index cb1090e6a5..5a7f8c2076 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -8,28 +8,28 @@ import Lean.Meta.AppBuilder namespace Lean.Meta inductive CongrArgKind where - | /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/ - fixed - | /-- - It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. - This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ - fixedNoParam - | /-- - The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`. - `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/ - eq - | /-- - The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. - They correspond to arguments that are subsingletons/propositions. -/ - cast - | /-- - The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. - `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ - heq - | /-- - For congr-simp theorems only. Indicates a decidable instance argument. - The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ - subsingletonInst + /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/ + | fixed + /-- + It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. + This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ + | fixedNoParam + /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/ + | eq + /-- + The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. + They correspond to arguments that are subsingletons/propositions. -/ + | cast + /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ + | heq + /-- + For congr-simp theorems only. Indicates a decidable instance argument. + The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ + | subsingletonInst deriving Inhabited structure CongrTheorem where diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index e4107ba760..d1408bf37a 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -143,39 +143,39 @@ private def trySynthPending (e : Expr) : MetaM Bool := do Result type for `isDefEqArgsFirstPass`. -/ inductive DefEqArgsFirstPassResult where - | /-- - Failed to establish that explicit arguments are def-eq. - Remark: higher output parameters, and parameters that depend on them - are postponed. - -/ - failed - | /-- - Succeeded. The array `postponedImplicit` contains the position - of the implicit arguments for which def-eq has been postponed. - `postponedHO` contains the higher order output parameters, and parameters - that depend on them. They should be processed after the implict ones. - `postponedHO` is used to handle applications involving functions that - contain higher order output parameters. Example: - ```lean - getElem : - {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} → - {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] → - (xs : cont) → (i : idx) → (h : dom xs i) → elem - ``` - The argumengs `dom` and `h` must be processed after all implicit arguments - otherwise higher-order unification problems are generated. See issue #1299, - when trying to solve - ``` - getElem ?a ?i ?h =?= getElem a i (Fin.val_lt_of_le i ...) - ``` - we have to solve the constraint - ``` - ?dom a i.val =?= LT.lt i.val (Array.size a) - ``` - by solving after the instance has been synthesized, we reduce this constraint to - a simple check. - -/ - ok (postponedImplicit : Array Nat) (postponedHO : Array Nat) + /-- + Failed to establish that explicit arguments are def-eq. + Remark: higher output parameters, and parameters that depend on them + are postponed. + -/ + | failed + /-- + Succeeded. The array `postponedImplicit` contains the position + of the implicit arguments for which def-eq has been postponed. + `postponedHO` contains the higher order output parameters, and parameters + that depend on them. They should be processed after the implict ones. + `postponedHO` is used to handle applications involving functions that + contain higher order output parameters. Example: + ```lean + getElem : + {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} → + {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] → + (xs : cont) → (i : idx) → (h : dom xs i) → elem + ``` + The argumengs `dom` and `h` must be processed after all implicit arguments + otherwise higher-order unification problems are generated. See issue #1299, + when trying to solve + ``` + getElem ?a ?i ?h =?= getElem a i (Fin.val_lt_of_le i ...) + ``` + we have to solve the constraint + ``` + ?dom a i.val =?= LT.lt i.val (Array.size a) + ``` + by solving after the instance has been synthesized, we reduce this constraint to + a simple check. + -/ + | ok (postponedImplicit : Array Nat) (postponedHO : Array Nat) /-- First pass for `isDefEqArgs`. We unify explicit arguments, *and* easy cases diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index ba00af66de..034cd574ed 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -8,15 +8,15 @@ import Lean.Meta.Basic namespace Lean inductive TransformStep where - | /-- Return expression without visiting any subexpressions. -/ - done (e : Expr) - | /-- Visit expression (which should be different from current expression) instead. -/ - visit (e : Expr) - | /-- - Continue transformation with the given expression (defaults to current expression). - For `pre`, this means visiting the children of the expression. - For `post`, this is equivalent to returning `done`. -/ - continue (e? : Option Expr := none) + /-- Return expression without visiting any subexpressions. -/ + | done (e : Expr) + /-- Visit expression (which should be different from current expression) instead. -/ + | visit (e : Expr) + /-- + Continue transformation with the given expression (defaults to current expression). + For `pre`, this means visiting the children of the expression. + For `post`, this is equivalent to returning `done`. -/ + | continue (e? : Option Expr := none) namespace Core diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 38a29b3a00..86d8318a24 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1582,20 +1582,20 @@ instance : Inhabited PrattParsingTables := ⟨{}⟩ function). -/ inductive LeadingIdentBehavior where - | /-- `LeadingIdentBehavior.default`: if the leading token - is an identifier, then `prattParser` just executes the parsers - associated with the auxiliary token "ident". -/ - default - | /-- `LeadingIdentBehavior.symbol`: if the leading token is - an identifier ``, and there are parsers `P` associated with - the toek ``, then it executes `P`. Otherwise, it executes - only the parsers associated with the auxiliary token "ident". -/ - symbol - | /-- `LeadingIdentBehavior.both`: if the leading token - an identifier ``, the it executes the parsers associated - with token `` and parsers associated with the auxiliary - token "ident". -/ - both + /-- `LeadingIdentBehavior.default`: if the leading token + is an identifier, then `prattParser` just executes the parsers + associated with the auxiliary token "ident". -/ + | default + /-- `LeadingIdentBehavior.symbol`: if the leading token is + an identifier ``, and there are parsers `P` associated with + the toek ``, then it executes `P`. Otherwise, it executes + only the parsers associated with the auxiliary token "ident". -/ + | symbol + /-- `LeadingIdentBehavior.both`: if the leading token + an identifier ``, the it executes the parsers associated + with token `` and parsers associated with the auxiliary + token "ident". -/ + | both deriving Inhabited, BEq, Repr /-- diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index e69c923d6e..98e34eaa7a 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -84,21 +84,21 @@ section Utils /-- Events that worker-specific tasks signal to the main thread. -/ inductive WorkerEvent where - | /-- A synthetic event signalling that the grouped edits should be processed. -/ - processGroupedEdits + /-- A synthetic event signalling that the grouped edits should be processed. -/ + | processGroupedEdits | terminated | crashed (e : IO.Error) | ioError (e : IO.Error) inductive WorkerState where - | /-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker - and when reading a request reply. - In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. - Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. - Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded - to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file - worker arrives. -/ - crashed (queuedMsgs : Array JsonRpc.Message) + /-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker + and when reading a request reply. + In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. + Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. + Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded + to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file + worker arrives. -/ + | crashed (queuedMsgs : Array JsonRpc.Message) | running abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message compare diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index f43a29305c..ef36cd64c9 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -75,9 +75,9 @@ def occurs (e : Expr) (t : Expr) : Bool := Return type for `findExt?` function argument. -/ inductive FindStep where - | /-- Found desired subterm -/ found - | /-- Search subterms -/ visit - | /-- Do not search subterms -/ done + /-- Found desired subterm -/ | found + /-- Search subterms -/ | visit + /-- Do not search subterms -/ | done namespace FindExtImpl diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 01c8078e04..df7c8e5e58 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -56,14 +56,15 @@ private def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPCo } private inductive EmbedFmt - | /-- Tags denote `Info` objects. -/ - expr (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) + /-- Tags denote `Info` objects. -/ + | expr (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId) - | /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow - the user to expand sub-traces interactively. -/ - trace (cls : Name) (msg : Format) (collapsed : Bool) - (children : StrictOrLazy (Array Format) (Array MessageData)) - | /-- Ignore any tags in this subtree. -/ ignoreTags + /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow + the user to expand sub-traces interactively. -/ + | trace (cls : Name) (msg : Format) (collapsed : Bool) + (children : StrictOrLazy (Array Format) (Array MessageData)) + /-- Ignore any tags in this subtree. -/ + | ignoreTags deriving Inhabited private abbrev MsgFmtM := StateT (Array EmbedFmt) IO diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index b97e15348b..62708e82cc 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -15,11 +15,11 @@ Much like Lean 3 [`sf`](https://github.com/leanprover-community/mathlib/blob/bfa but with indentation already stringified. -/ inductive TaggedText (α : Type u) where | text : String → TaggedText α - | /-- Invariants: + /-- Invariants: - non-empty - no adjacent `text` elements (they should be collapsed) - no directly nested `append`s (but `append #[tag _ (append ..)]` is okay) -/ - append : Array (TaggedText α) → TaggedText α + | append : Array (TaggedText α) → TaggedText α | tag : α → TaggedText α → TaggedText α deriving Inhabited, BEq, Repr, FromJson, ToJson diff --git a/src/lake b/src/lake index 6b0abded61..d18b487c4d 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit 6b0abded611a1b4315084d98628e2dda41d40283 +Subproject commit d18b487c4d16385d94322ccdf2b9858ee5a2d9a4 diff --git a/tests/lean/Uri.lean.expected.out b/tests/lean/Uri.lean.expected.out index fe75c80bca..27ba77ddaf 100644 --- a/tests/lean/Uri.lean.expected.out +++ b/tests/lean/Uri.lean.expected.out @@ -1 +1 @@ -true +true diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean index c535470c4a..44f710a63e 100644 --- a/tests/lean/docStr.lean +++ b/tests/lean/docStr.lean @@ -16,8 +16,8 @@ structure Boo (α : Type) where /-- inductive datatype Tree documentation -/ inductive Tree (α : Type) where - | /-- Tree.node documentation -/ node : List (Tree α) → Tree α - | /-- Tree.leaf stores the values -/ leaf : α → Tree α + /-- Tree.node documentation -/ | node : List (Tree α) → Tree α + /-- Tree.leaf stores the values -/ | leaf : α → Tree α namespace Bla diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 7cf32a457d..ac816d1d94 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -95,7 +95,7 @@ "kind": 5, "documentation": {"value": - "`forIn x b f : m β` runs a for-loop in the monad `m` with additional state `β`.\n This traverses over the \"contents\" of `x`, and passes the elements `a : α` to\n `f : α → β → m (ForInStep β)`. `b : β` is the initial state, and the return value\n of `f` is the new state as well as a directive `.done` or `.yield`\n which indicates whether to abort early or continue iteration.\n\n The expression\n ```\n let mut b := ...\n for x in xs do\n b ← foo x b\n ```\n in a `do` block is syntactic sugar for:\n ```\n let b := ...\n let b ← forIn xs b (fun x b => do\n let b ← foo x b\n return .yield b)\n ```\n (Here `b` corresponds to the variables mutated in the loop.) ", + "`forIn x b f : m β` runs a for-loop in the monad `m` with additional state `β`.\nThis traverses over the \"contents\" of `x`, and passes the elements `a : α` to\n`f : α → β → m (ForInStep β)`. `b : β` is the initial state, and the return value\nof `f` is the new state as well as a directive `.done` or `.yield`\nwhich indicates whether to abort early or continue iteration.\n\nThe expression\n```\nlet mut b := ...\nfor x in xs do\n b ← foo x b\n```\nin a `do` block is syntactic sugar for:\n```\nlet b := ...\nlet b ← forIn xs b (fun x b => do\n let b ← foo x b\n return .yield b)\n```\n(Here `b` corresponds to the variables mutated in the loop.) ", "kind": "markdown"}, "detail": "[self : ForIn m ρ α] → {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β"}, diff --git a/tests/lean/interactive/foldingRange.lean b/tests/lean/interactive/foldingRange.lean index 8ace1baca7..68967269e4 100644 --- a/tests/lean/interactive/foldingRange.lean +++ b/tests/lean/interactive/foldingRange.lean @@ -23,12 +23,12 @@ def add (x y : Nat) := x + y inductive InductiveTy -| a -| + | a /-- Another doc comment. This one is not folded. + -/ - b + | b mutual def a := diff --git a/tests/lean/linterMissingDocs.lean b/tests/lean/linterMissingDocs.lean index 42b1f2720c..20c9629a03 100644 --- a/tests/lean/linterMissingDocs.lean +++ b/tests/lean/linterMissingDocs.lean @@ -41,7 +41,7 @@ def lintDoc (x : Nat) := x inductive Ind where | ind1 | ind2 : Ind → Ind - | /-- A doc string -/ doc : Ind + /-- A doc string -/ | doc : Ind with @[computedField] field : Ind → Nat | _ => 1