This PR modifies the signature of the functions `Nat.fold`,
`Nat.foldRev`, `Nat.any`, `Nat.all`, so that the function is passed the
upper bound. This allows us to change runtime array bounds checks to
compile time checks in many places.
This PR avoids runtime array bounds checks in places where it can
trivially be done at compile time.
None of these changes are of particular consequence: I mostly wanted to
learn how much we do this, and what the obstacles are to doing it less.
This PR replaces `Array.feraseIdx` and `Array.insertAt` with
`Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat`
argument and a tactic-provided proof that it is in bounds. We also have
`eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the
index is out of bounds. We also provide a `Fin` valued version of
`Array.findIdx?`. Together, these quite ergonomically improve the array
indexing safety at a number of places in the compiler/elaborator.
This PR improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.
Example output for `#print Monad`:
```
class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
Monad.toApplicative : Applicative m
Monad.toBind : Bind m
fields:
Functor.map : {α β : Type u} → (α → β) → m α → m β
Functor.mapConst : {α β : Type u} → α → m β → m α
Pure.pure : {α : Type u} → α → m α
Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight
```
Suggested by Floris van Doorn [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637).
This PR adds the option `pp.parens` (default: false) that causes the
pretty printer to eagerly insert parentheses, which can be useful for
teaching and for understanding the structure of expressions. For
example, it causes `p → q → r` to pretty print as `p → (q → r)`.
Any notations with precedence greater than or equal to `maxPrec` do not
receive such discretionary parentheses, since this precedence level is
considered to be infinity.
This option was a feature in the Lean 3 community edition.
This PR improves the term info for coercions marked with
`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to
definition" on the function name work. Hovering over such a coerced
function will show the coercee rather than the coercion expression. The
coercion expression can still be seen by hovering over the whitespace in
the function application.
Example:
```lean
example : 0 = (0 : Nat) := by
exact Eq.refl (0 : Int)
/-
error: type mismatch
Eq.refl 0
has type
(0 : Int) = 0 : Prop
but is expected to have type
(0 : Nat) = 0 : Prop
-/
```
An important part of the interface of a function is the parameter names,
for making used of named arguments. This PR makes the parameter names
print in a reliable way. The parameters of the type now appear as
hygienic names if they cannot be used as named arguments.
Modifies the heuristic for how parameters are chosen to appear before or
after the colon. The rule is now that parameters start appearing after
the colon at the first non-dependent non-instance-implicit parameter
that has a name unusable as a named argument. This is a refinement of
#2846.
Fixes the issue where consecutive hygienic names pretty print without a
space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝
: Nat)`.
Breaking change: `Lean.PrettyPrinter.Formatter.pushToken` now takes an
additional boolean `ident` argument, which should be `true` for
identifiers. Used to insert discretionary space between consecutive
identifiers.
Closes#5810
Gives more control over pretty printing metavariables.
- When `pp.mvars.levels` is false, then universe level metavariables
pretty print as `_` rather than `?u.22`
- When `pp.mvars.anonymous` is false, then anonymous metavariables
pretty print as `?_` rather than `?m.22`. Named metavariables still
pretty print with their names. When this is false, it also sets
`pp.mvars.levels` to false, since every level metavariable is anonymous.
- When `pp.mvars` is false, then all metavariables pretty print as `?_`
or `_`.
Modifies TryThis to use `pp.mvars.anonymous` rather than doing a
post-delaboration modification. This incidentally improves TryThis since
it now prints universe level metavariables as `_` rather than `?u.22`.
Where before we had
```lean
#check fun x : Nat => ?a
-- fun x ↦ ?m.7 x : (x : Nat) → ?m.6 x
```
Now by default we have
```lean
#check fun x : Nat => ?a
-- fun x => ?a : (x : Nat) → ?m.6 x
```
In particular, delayed assignment metavariables such as `?m.7` pretty
print using the name of the metavariable they are delayed assigned to,
suppressing the bound variables used in the delayed assignment (hence
`?a` rather than `?a x`). Hovering over `?a` shows `?m.7 x`.
The benefit is that users can see the user-provided name in local
contexts. A justification for this pretty printing choice is that `?m.7
x` is supposed to stand for `?a`, and furthermore it is just as opaque
to assignment in defeq as `?a` is (however, when synthetic opaque
metavariables are made assignable, delayed assignments can be a little
less assignable than true synthetic opaque metavariables).
The original pretty printing behavior can be recovered using `set_option
pp.mvars.delayed true`.
This PR also extends the documentation for holes and synthetic holes,
with some technical details about what delayed assignments are. This
likely should be moved to the reference manual, but for now it is
included in this docstring.
(This PR is a simplified version of #3494, which has a round-trippable
notation for delayed assignments. The pretty printing in this PR is
unlikely to round trip, but it is better than the current situation,
which is that delayed assignment metavariables never round trip, and
plus it does not require introducing a new notation.)
The app unexpanders for `Name.mkStr1` through `Name.mkStr8` weren't
respecting the escaping rules for names. For example, ``#check `«a.b»``
would show `` `a.b``.
This PR folds the unexpanders into the name literal delaborator, where
escaping is already handled.
The formatter was using `tk ++ " "` to separate tokens from tokens they
would merge with, but `" "` is not whitespace that could merge. This
affected large binder lists, which wouldn't pretty print with any line
breaks. Now they can be flowed across multiple lines.
Closes#5424
Previously the formatter was using the builtin token table rather that
the one in the current environment. This could lead to round-tripping
failures for user-defined notations.
For an illustrative example, given the following notation
```lean
infixl:65 "+'" => Int.add
notation:65 a:65 "+'-" b:66 => Int.add a (id b)
```
then `5 +' -1` would parse as `Int.add 5 (-1)` and incorrectly pretty
print as `5+'-1`, which in turn would parse as `Int.add 5 (id 1)`. Now
it pretty prints as `5+' -1`.
For structure projections, the pretty printer assumed that the
expression was type correct. Now it checks that the object being
projected is of the correct type. Such terms appear in type mismatch
errors.
Also, fixes and improves `#print` for structures. The types of
projections now use MessageData (so are now hoverable), and the type of
`self` is now the correct type.
Closes#4670
Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves
the identifier when expanding the macro, saving needing to use the fully
qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`,
throws an error if the identifier cannot be resolved.
Closes#4899
Before, the delaborator was conservative about omitting optional
arguments, only omitting the very last one. Now it can omit arbitrarily
long sequences of optional arguments from the end.
For simplicity of implementation, every optional argument is delaborated
and then potentially discarded. It could save state and lazily
delaborate, but we're running under the hypothesis that most optional
arguments are for very simple values (like `true`, `false`, or a numeric
literal), so it is unlikely that efficiency gains, if any, are worth it.
In particular, in the future structure constructors will have optional
arguments, but `unexpandStructureInstance` assumes none of the optional
fields are omitted.
Closes#4812
For every parenthesized expression `(foo)`, the InfoView produces an
interactive component both for `(foo)` itself and its subexpression
`foo` because the corresponding `TaggedText` in the language server is
duplicated as well. Both of these subexpressions have the same
subexpression position and so they are identical w.r.t. interactive
features.
Removing this duplication would help reduce the size of the DOM of the
InfoView and ensure that the UI for InfoView features is consistent for
`(foo)` and `foo` (e.g. hovers would always highlight `(foo)`, not
either `(foo)` or `foo` depending on whether the mouse cursor is on the
bracket or not). It would also help resolve a bug where selecting a
subexpression will yield selection highlighting both for `(foo)` and
`foo`, as we use the subexpression position to identify which terms to
highlight.
This PR adjusts the parenthesizer to move the corresponding info instead
of duplicating it.
I noticed that a change to `Lean.PrettyPrinter.Delaborator.Builtins`
rebuilt more modules than I expected, so I moved a definition and
reduced some dependcies.
More reduction would be possible to move const-delaboration out of the
big `Lean.PrettyPrinter`, and import from `Lean.PrettyPrinter`
selectively.
Matchers usually have implicit arguments, and even if they don't the
notation hides the name of the matcher function.
Now when hovering over `match` expressions you can see the actual
underlying matcher expression.
In #3911, a refactor to share `MessageData` code between `ppConst` and
the signature pretty printer unintentionally caused the signature pretty
printer to use the `pp.tagAppFns` option. This causes, for example, `+`
in `a + b` to independently have its own hover information due to the
fact that `notation` app unexpanders use the head function's syntax as
the `ref` when constructing the notation syntax. This behavior of
`pp.tagAppFns` is intentional, and it is used by docgen, but it should
not be activated for signatures.
This affects `#check` and was reported by Kevin Buzzard [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/degraded.20hover.20experience.20on.20.23check/near/449380674).
This PR also makes sure the initial `ref` when applying app unexpanders
is `.missing`, rather than whatever random value might be present in the
`CoreM` context.
Now syntax nodes have their formatters run even if the parsers they wrap
are all arity zero. This fixes an issue where if `ppSpace` appears in a
`macro`/`elab` then it does not format with a space due to the fact that
macro argument processing wraps this as `group(ppSpace)`, and `ppSpace`
has arity zero.
Implementation note: the fix is to make the `visitArgs` formatter
combinator always visit the last child, even if it does not exist (in
which case the visited node will be `Syntax.missing`). To compensate,
parser combinators like many and optional need to be sure to keep track
of whether there any children. Only optional's needed to be modified.
Closes#4561
Before, `pp.instantiateMVars` generally had no effect because most call
sites for the pretty printer instantiated metavariables first, but now
this functionality is entrusted upon the `pp.instantiateMVars` option.
This also has an effect in hovers, where metavariables can be unfolded
one assignment at a time. However, the goal state still sees all
metavariables instantiated due to the fact that the algorithm relies on
expression equality post-instantiation (see
`Lean.Widget.goalToInteractive`).
Closes#4406
The `pp.maxSteps` option is a hard limit on the complexity of pretty
printer output, which is necessary to prevent the LSP from crashing when
there are accidental large terms. We're using the default value from the
corresponding Lean 3 option.
This PR also sets `pp.deepTerms` to `false` by default.
On
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Notation.20in.20namespace.20not.20showing.20in.20pp/near/437016468),
Peter Nelson reported that notations that could be pretty printed with
generalized field notation did not pretty print using the intended
notation.
This PR makes it so that app unexpanders are considered before
generalized field notation. The complexity before was that we wanted to
do parent projection collapse, and since we did the collapse before
pretty printing that argument, it meant it wasn't possible to do app
unexpanders when there was a field notation candidate. The new solution
is to collapse parent projections only when actually considering field
notation, which can be done because we can safely strip off projection
syntax in an expression-directed way.
In the following, hovering over `true` in the infoview was showing
`Nat.succ y`.
```lean
#check fun (x : Nat) =>
match h : x with
| 0 => false
| y + 1 => true
```
Now hovering over `true` shows `true`.
The issue was that SubExpr positions were not being tracked for
patterns, and the position for a pattern could coincide with the
position for a RHS, putting overwriting terminfo. Now the position given
to a pattern is correct and unique.
Refactors the `match` delaborator, makes it handle shadowing of `h :`
discriminant annotations correctly, and makes it use the standard
`withOverApp` combinator to handle overapplication.
* Setting `pp.mvars` to false causes metavariables to pretty print as
`?_`.
* Setting `pp.mvars.withType` to true causes metavariables to pretty
print with type ascriptions.
Motivation: when making tests, it is inconvenient using `#guard_msgs`
when there are metavariables, since the unique numbering is subject to
change.
This feature does not use `⋯` omissions since a metavariable is already
in a sense an omitted term. If repeated metavariables do not appear in
an expression, there is a chance that a term pretty printed with
`pp.mvars` set to false can still elaborate to the correct term, unlike
for other omissions.
(In the future we could consider an option that pretty prints uniquely
numbered metavariables as `?m✝`, `?m✝¹`, `?m✝²`, etc. to be able to tell
them apart, at least in the same pretty printed expression. It would
take care to make sure that these names are stable across different
hovers.)
Closes#3781
Modifies `withBindingBodyUnusedName` to annotate the syntax for the
variable with its corresponding fvar. Now, for example, you can hover
over the variables in `fun x y => ...` in the infoview to see their
types. This change affects notations such as `∃ n, n = 1`, where
hovering over `n` shows that `n : Nat`.
Also adds such annotations for the variables in `let` and `let_fun`.
Implementation note: the variables are annotated with fresh positions
using `nextExtraPos`.
Removes the unused and unnecessary
`Lean.PrettyPrinter.Delaborator.liftMetaM`.
Closes#1618, closes#2737
This avoids printing the entire docstring for `⋯` when hovering over it,
which is rather long, and instead it gives a brief reason for omission
and what option to set to pretty print the omitted term.
Given
```lean
structure A where
x : Nat
structure B extends A where
y : Nat
```
rather than pretty printing `{ x := 1, y := 2 : B }` as `{ toA := { x :=
1 }, y := 2 }`, it now pretty prints as `{ x := 1, y := 2 }`.
The option `pp.structureInstances.flatten` controls whether to flatten
structure instances like this.
Sets the default value to `pp.fieldNotation.generalized` to `true`.
Updates tests, and fixes some minor flaws in the implementation of the
generalized field notation pretty printer.
Now generalized field notation won't be used for any function that has a
`motive` argument. This is intended to prevent recursors from pretty
printing using it as (1) recursors are more like control flow structures
than actual functions and (2) generalized field notation tends to cause
elaboration problems for recursors.
Note: be sure functions that have an `@[app_unexpander]` use
`@[pp_nodot]` if applicable. For example, `List.toArray` needs
`@[pp_nodot]` to ensure the unexpander prints it using `#[...]`
notation.
