From d95163641a6bda2fe5cedeadf5eeebfe11ce942f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jul 2022 22:36:55 -0400 Subject: [PATCH] chore: indent docstrings --- src/Init/Prelude.lean | 60 ++++++------ src/Lean/Expr.lean | 218 +++++++++++++++++++++--------------------- 2 files changed, 140 insertions(+), 138 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 4f94473177..8e27b7745a 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1844,20 +1844,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. --/ + 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 token (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. --/ + Synthesized token (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. --/ + Synthesized token without position information. + -/ protected none instance : Inhabited SourceInfo := ⟨SourceInfo.none⟩ @@ -1882,25 +1882,26 @@ Syntax objects used by the parser, macro expander, delaborator, etc. inductive Syntax where | missing : Syntax | /-- -Node in the syntax tree. + 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 `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`. -(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 + (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 | atom (info : SourceInfo) (val : String) : Syntax | ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax @@ -2144,10 +2145,11 @@ def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax := introduced symbol, which results in better error positions than not applying any position. -/ class MonadQuotation (m : Type → Type) extends MonadRef m where - -- Get the fresh scope of the current macro invocation + /-- Get the fresh scope of the current macro invocation -/ getCurrMacroScope : m MacroScope getMainModule : m Name - /- Execute action in a new macro invocation context. This transformer should be + /-- + Execute action in a new macro invocation context. This transformer should be used at all places that morally qualify as the beginning of a "macro call", e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it can also be used internally inside a "macro" if identifiers introduced by diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 084f093ed6..2947ebbdc0 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -53,7 +53,7 @@ This can be set to The difference between implicit `{}` and strict-implicit `⦃⦄` is how implicit arguments are treated that are *not* followed by explicit arguments. `{}` arguments are applied eagerly, while `⦃⦄` arguments are left partially applied: -```lean +```lean4 def foo {x : Nat} : Nat := x def bar ⦃x : Nat⦄ : Nat := x #check foo -- foo : Nat @@ -72,17 +72,17 @@ inductive BinderInfo where | /-- 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. --/ + 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 @@ -297,127 +297,127 @@ Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keyword 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 -``` --/ + 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`. --/ + 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. + 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))`` --/ + `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]``. --/ + 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 -```lean -.app (.const `Nat.succ []) (.const .zero []) -``` --/ + Function application. `Nat.succ Nat.zero` is represented as + ```lean4 + .app (.const `Nat.succ []) (.const .zero []) + ``` + -/ app (fn : Expr) (arg : Expr) | /-- -Lambda abstraction (aka anonymous functions). -- `fun x : Nat => x` is represented as -```lean -.lam `x (.const `Nat []) (.bvar 0) .default -``` --/ + Lambda abstraction (aka anonymous functions). + - `fun x : Nat => x` is represented as + ```lean4 + .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: + A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows. + Examples: -- `forall x : Prop, x ∧ x` is represented as -```lean -.forallE `x - (.sort .zero) - (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) - .default -``` -- `Nat → Bool` as -```lean -.forallE `a (.const `Nat []) (.const `Bool []) .default -``` --/ + - `forall x : Prop, x ∧ x` is represented as + ```lean4 + .forallE `x + (.sort .zero) + (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) + .default + ``` + - `Nat → Bool` as + ```lean4 + .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. 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 -``` --/ + 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. 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 [])) -``` --/ + 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 + ```lean4 + .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`. --/ + 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 -``` --/ + 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 + ```lean4 + .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*))"]