@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
`proj_sname` is not just for enabling better pretty printing. It is
necessary in the compiler when type information is lost, and we can't
infer the type of a `proj`-term argument (field `proj_expr`).
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
((fun (x : t), b) v)
We also use a macro (let-macro) to mark this pattern.
Thus, the pretty-printer knows how to display it correctly.
2- Transparent 'let'-expressions are eagerly expanded by the parser.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Before this commit, we "stored" macro arguments using applications.
This representation had some issues. Suppose we use [m a] to denote a macro
application. In the old representation, ([m a] b) and [m a b] would have
the same representation. Another problem is that some procedures (e.g., type inference)
would not have a clean implementation.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The main motivation is that we will be able to move equalities between universes.
For example, suppose we have
A : (Type i)
B : (Type i)
H : @eq (Type j) A B
where j > i
We didn't find any trick for deducing (@eq (Type i) A B) from H.
Before this commit, heterogeneous equality as a constant with type
heq : {A B : (Type U)} : A -> B -> Bool
So, from H, we would only be able to deduce
(@heq (Type j) (Type j) A B)
Not being able to move the equality back to a smaller universe is
problematic in several cases. I list some instances in the end of the commit message.
With this commit, Heterogeneous equality is a special kind of expression.
It is not a constant anymore. From H, we can deduce
H1 : A == B
That is, we are essentially "erasing" the universes when we move to heterogeneous equality.
Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is
(to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B)
So, it remains to explain why we need this feature.
For example, suppose we want to state the Pi extensionality axiom.
axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} :
A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)
This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous
equality as a constant. The conclusion
(∀ x, B x) == (∀ x, B' x)
is syntax sugar for
(@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x))
Even if A, A', B, B' live in a much smaller universe.
As I described above, it doesn't seem to be a way to move this equality back to a smaller universe.
So, if we wanted to keep the heterogeneous equality as a constant, it seems we would
have to support axiom schemas. That is, hpiext would be parametrized by the universes where
A, A', B and B'. Another possibility would be to have universe polymorphism like Agda.
None of the solutions seem attractive.
So, we decided to have heterogeneous equality as a special kind of expression.
And use the trick above to move equalities back to the right universe.
BTW, the parser is not creating the new heterogeneous equalities yet.
Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous
equality as a constant.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
It is not incorrect to use size, but it can easily overflow due to sharing.
The following script demonstrates the problem:
local f = Const("f")
local a = Const("a")
function mk_shared(d)
if d == 0 then
return a
else
local c = mk_shared(d-1)
return f(c, c)
end
end
print(mk_shared(33):size())
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.
TODO: do the same for kernel objects, sexprs, etc.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
