85092412c7
@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 |
||
|---|---|---|
| .. | ||
| cases_tactic.cpp | ||
| cases_tactic.h | ||
| clear_tactic.cpp | ||
| clear_tactic.h | ||
| CMakeLists.txt | ||
| elaborator_exception.cpp | ||
| elaborator_exception.h | ||
| hsubstitution.cpp | ||
| hsubstitution.h | ||
| induction_tactic.cpp | ||
| induction_tactic.h | ||
| init_module.cpp | ||
| init_module.h | ||
| intro_tactic.cpp | ||
| intro_tactic.h | ||
| kabstract.cpp | ||
| kabstract.h | ||
| occurrences.cpp | ||
| occurrences.h | ||
| revert_tactic.cpp | ||
| revert_tactic.h | ||
| subst_tactic.cpp | ||
| subst_tactic.h | ||
| tactic_evaluator.cpp | ||
| tactic_evaluator.h | ||
| tactic_state.cpp | ||
| tactic_state.h | ||