This PR translates `lean::mk_projections` into Lean, adding
`Lean.Meta.mkProjections`. It also puts `hasLooseBVarInExplicitDomain`
back in sync with the kernel version. Deletes
`src/library/constructions/projection.{h,cpp}`.
This PR splits the environment used by the kernel from that used by the
elaborator, providing the foundation for tracking of asynchronously
elaborated declarations, which will exist as a concept only in the
latter.
Minor changes:
* kernel diagnostics are moved from an environment extension to a direct
environment as they are the only extension used directly by the kernel
* `initQuot` is moved from an environment header field to a direct
environment as it is the only header field used by the kernel; this also
makes the remaining header immutable after import
closes#5333
This PR tries to address issue #5333.
My conjecture is that the binder annotations for `C.toB` and
`Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations
where the new command `set_synth_order` was used. Both classes, `C` and
`Algebra`, are parametric over instances, and in both cases, the issue
arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's
focus on the binder annotations for `C.toB`. They are as follows:
```
C.toB [inst : A 20000] [self : @C inst] : @B ...
```
As a projection, it seems odd that `inst` is an instance-implicit
argument instead of an implicit one, given that its value is fixed by
`self`. We observe the same issue in `Algebra.toSMul`:
```
Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A]
[self : @Algebra R A inst1 inst2] : SMul R A
```
The PR changes the binder annotations as follows:
```
C.toB {inst : A 20000} [self : @C inst] : @B ...
```
and
```
Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A}
[self : @Algebra R A inst1 inst2] : SMul R A
```
In both cases, the `set_synth_order` is used to force `self` to be
processed first.
In the MWE, there is no instance for `C ...`, and `C.toB` is quickly
discarded. I suspect a similar issue occurs when trying to use
`Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean
spends unnecessary time trying to synthesize `CommSemiring R` and
`Semiring A` instances. I believe the new binder annotations make sense,
as if there is a way to synthesize `Algebra R A ... ...`, it will tell
us how to retrieve the instance-implicit arguments.
TODO:
- Impact on Mathlib.
- Document changes.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
This ports the `.below` and `.brecOn` constructions to lean.
I kept them in the same file, as they were in the C code, because they
are
highly coupled and the constructions are very analogous.
For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all declarations found in Lean and Mathlib are
equivalent, up to
def canon (e : Expr) : CoreM Expr := do
Core.transform (← Core.betaReduce e) (pre := fun
| .const n ls => return .done (.const n (ls.map (·.normalize)))
| .sort l => return .done (.sort l.normalize)
| _ => return .continue)
It was not feasible to make them completely equal, because the kernel's
type inference code seem to optimize level expressions a bit less
aggressively, and beta-reduces less in inference.
The private helper functions about `PProd` can later move into their own
file, used by these constructions as well as the structural recursion
module.
this is the simplest of the constructions to be ported from C++ to Lean,
so I’ll PR this one first.
This begins to put each construction into its own file, as it was the
case with C++.
For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all `.recOn` declarations found in Lean and Mathlib are
identical (per `==`) to the ones produced by the C code.
this is a first step towards porting the code `constructions.cpp` to
Lean: It leaves the construction of the `Declaration` untouched, but
moves adding the declarations to the environment, and setting various
attributes, to the Lean world.
This allows the remaining logic (the construction of the `Declaration`)
to be implemented in Lean separately and easily compared to the C++
implementation, before we replace that too.
To that end, `Declaraion` gains an `BEq` instance.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: Arthur Adjedj <arthur.adjedj@ens-paris-saclay.fr>
sed -Ei 's/(g_\w+)\s*= new (name|expr|format|level|string_ref)\W.*;/\0\n mark_persistent(\1->raw());/' src/kernel/**/*.cpp src/util/**/*.cpp src/library/**/*.cpp
@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`.
