This PR adds support for correctly handling computations on fields in
`casesOn` for inductive predicates that support large elimination. In
any such predicate, the only relevant fields allowed are those that are
also used as an index, in which case we can find the supplied index and
use that term instead.
This PR changes `internalizeCode` to replace all substitutions with
non-param-bound fvars in `Expr`s (which are all types) with `lcAny`,
preserving the invariant that there are no such dependencies. The
violation of this invariant across files caused test failures in a
pending PR, but it is difficult to write a direct test for it. In the
future, we should probably change the LCNF checker to detect this.
This change also speeds up some compilation-heavy benchmarks much more
than I would've expected, which is a pleasant surprise. This indicates
we might get more speedups from reducing the amount of type information
we preserve in LCNF.
This PR addresses a missing check in the module system where private
names that remain in the public environment map for technical reasons
(e.g. inductive constructors generated by the kernel and relied on by
the code generator) accidentally were accessible in the public scope.
This PR removes an error which implicitly assumes that the sort of type
dependency between erased types present in the test being added can not
occur. It would be difficult to refine the error using only the
information present in LCNF types, and it is of very little ongoing
value (I don't recall it ever finding an actual problem), so it makes
more sense to delete it.
Fixes#9692.
This PR changes the LCNF `elimDeadBranches` pass so that it considers
all non-`Nat` literal types to be `⊤`. It turns out that fixing this to
correctly handle all of these types with the current abstract value
representation is surprisingly nontrivial, and it's better to just land
the fix first.
The `isUnderBinder` check is intended to avoid inlining repeated
computations into specializations, but this doesn’t apply to local
function decls whose bodies are already delayed.
This PR consolidates common attribute-related error messages into
reusable functions and updates the wording and formatting of relevant
error messages.
This extends the specialization behavior of functions taking instance
implicits to ordinary implicit arguments that are of instance type. The
choice between the two is often made for subtle inference-related
reasons. It also affects visibility of these functions, because the
module system makes template-like decls visible to the compiler in other
modules.
This PR makes the second instance of the `inferVisibility` pass run
after the `saveMono` pass. As the comment above the first instance of
the pass indicates, this needs to be after `saveMono` in order to see
all decls with their updated bodies.
(Almost) only typos in constant names and doc-strings were considered;
grammar was not considered. Also, along others,
`mkDefinitionValInferrringUnsafe` has been fixed :-)
This PR removes uses of `Lean.RBMap` in Lean itself.
Furthermore some massaging of the import graph is done in order to avoid
having `Std.Data.TreeMap.AdditionalOperations` (which is quite
expensive) be the critical path for a large chunk of Lean. In particular
we can build `Lean.Meta.Simp` and `Lean.Meta.Grind` without it thanks to
these changes.
We did previously not conduct this change as `Std.TreeMap` was not
outperforming `Lean.RBMap` yet, however this has changed with the new
code generator.
This PR adds support for compilation of `casesOn` for subsingletons. We
rely on the elaborator's type checking to restrict this to inductives in
`Prop` that can actually eliminate into `Type n`. This does not yet
cover other recursors of these types (or of inductives not in `Prop` for
that matter).
This PR changes the implementation of `trace.Compiler.result` to use the
decls as they are provided rather than looking them up in the LCNF mono
environment extension, which was seemingly done to save the trouble of
re-normalizing fvar IDs before printing the decl. This means that the
`._closed` decls created by the `extractClosed` pass will now be
included in the output, which was definitely confusing before if you
didn't know what was happening.
This currently relies on the encoding pun of Nat.zero as the first
tagged constructor of Nat. Since Nat.succ is lowered to addition, it
makes sense to also lower Nat.zero to a zero literal. This might also
expose more optimization opportunities in the future.
This PR adds support for `.mdata` in LCNF mono types (and then drops it
at the IR type level instead). This better matches the behavior of
extern decls in the C++ code of the old compiler, which is still being
used to create extern decls at the moment and will soon be replaced.
This is covered by existing tests.
