@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: ensure the correct type `IRType` is inferred for definitions
such as
```
def f (n : UInt32) : UInt32 :=
if n == 0 then panic! "foo"
else n+1
```
Motivation: auxiliary recursors such as `brecOn` do not depend on
user-facing projection definitions anymore.
Thus, we can simplify `whnfCore` at `TypeUtil`.
@kha @dselsam: I added this notation because I am tired of writing
`[elem1, elem2, ...].toArray`. BTW, the new notation is based on the
one available in SML.
@kha @dselsam:
The main motivation for this change are functions such as `panic`.
I marked `panic` with the attribute `@[effectful]`.
Here is the summary of the changes. If `f` is marked as `@[effectful]`
1- Compiler will not perform common subexpression elimination on terms of the form `f ...`.
2- Compiler will not extract closed terms of the form `f ...`.
3- Compiler will throw an error if `f` is partially applied.
