@Kha We currently have a few macros that create binder names
such as `x`. These macros rely on the hygienic framework. This part is
great. Before this commit we were simply erasing the macro
scopes when creating the actual binders at `Expr.lean`.
The result produced expressions that were hard to debug.
For example, consider the following scenario
1- Macro creates a few binder names using ``x <- `(x)``
2- We create a lambda expression `t` with these binder names.
3- Then, we use `lambdaTelescope t fun xs body => ...`
Now, if we trace `xs` and `body`, we get `#[x, x, ... x]` and
we can't distinguish the different `x`s in `body`.
So, it is really hard to debug anything using the traces.
This commit adds `Name.simpMacroScopes` for simplying "macro scoped"
names. Example: given `x._@.Init.Data.List.Basic._hyg.2.5`, it
produces `x.2.5`. I exported this function, and used it in the old
pretty printer.
I have considered modifying `lambdaTelescope` to make sure it creates
unused names. I think this option is bad because it introduces
overhead, and in a few places we want to preserve the binder names.
I have also considered replacing the `let x := x.eraseMacroScopes` at
`Expr.lean` with `let x := x.simpMacroScopes`. I think this option is
bad since we are destroying scoping information and will not be able
to distiguish which variables have macro scopes when processing
tactics.
Anyway, the solution in this commit is good for this week, but we
should discuss a more permanent solution next week.
@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
- Lean strings (like std::string) may contain null characters. The
codebase was ignoring this issue.
- We now have a wrapper `string_ref` for wrapping Lean string objects in
C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
Remark: I also found a few places where the code relies on the
following property which is not true
Forall s : std::string, std::string(s.c_str()) == s
- `name` object wrapper was assuming that all numerals were small
`nat` values. This is true in most cases, but the system would
crash when processing if it is a big number.
- The commit tries to make sure runtime/util/kernel are correct.
Modules that will be deleted contain many `TODO` comments
indicating they may crash and/or produce incorrect results
when strings contain null characters and numerals are big.
cc @kha
@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.
After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.
I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
