@Kha @dselsam:
This hack was preventing us from making `Expr` a "real" Lean type.
This was bad for a few reasons:
- It was hard to extend/modify `Expr` in Lean since we would also have
to modify the C++ code that creates the `Expr` objects with the hidden
fields.
- `Expr.lam` and `Expr.forallE` were not following the Lean layout
standard where we sort fields by size. @Kha: recall we used that to
avoid a UB. The issue with `Expr.lam` and `Expr.forallE` is that they
have a "visible" field (`BinderInfo`), which is smaller than
hidden fields such as hash code.
- `Expr.fvar` had only one field at `Expr.lean,` but four behind the
scenes.
I added a new constructor `Local` that is only accessible from C++.
It is only used in legacy code we inherited from Lean2.
We will eventually delete it.
This refactoring was quite painful since many parts of the codebase
were mixing the new `Expr.fvar` with the old `Expr.local`.
I doubt I would be able to do it without the new staging framework
@Kha built.
BTW, some of the patches are horrible. I didn't care much since we
are going to deleted the super ugly files. That being said,
you should expect new weird bevaior due to `Expr.fvar` vs `Expr.local`.
Next step: use the new `ExprCachedData` to make all `Expr` hidden visibles
accessible from Lean.
checkpoint
Motivation: auxiliary recursors such as `brecOn` do not depend on
user-facing projection definitions anymore.
Thus, we can simplify `whnfCore` at `TypeUtil`.
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.
f a =?= f b
-----------
a =?= b
This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.
The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
in the Lean2 codebase when we were not caching failures and
the kernel type checker was also used during elaboration.
In Lean4, we will not generate non dependent recursors for inductive
predicates. The main goal is to make the shape of the automatically
generated recursors more uniform. The non uniform representation is
leftover from Lean2. In Lean2, we wanted to support different kernels
with different features. For example: we could create proof relevant
kernels, no impredicative universe, etc.
Recall that, in a kernel with an impredicative Prop and no proof
irrelevance, inductive predicates without dependent elimination are
weaker that inductive predicates with dependent elimination.
When proof irrelevance is enabled, we can generate the dependent
recursor from the non dependent one. Actually, the module drec.cpp
generates the dependent recursor.
Now, we only support one kind of kernel, and it doesn't make sense
anymore to generate non dependent recursors for inductive predicates.
This would only produce an unnecessary asymmetry on the inductive
datatype module.
Remark: we had to create non dependent recursors to help the elaborator.
This can be avoid if we improve the elaborator. I will do that in the
new elaborator implemented in Lean.
Remark: equation lemmas are broken for definitions that pattern match on
nested inductive datatypes. The problem is the super messy
`prove_eq_rec_invertible_aux` function. This function will not be needed
after I finish the new inductive datatype support in the kernel.
cc @kha
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
