We don't need to use `opaque` for `thunk` and `task`. Their recursor and
projections can be implemented in constant time. We just need to create
a closure which uses the runtime thunk_get/task_get primitive.
@kha I was working in the new declaration type and using tasks there.
Since we don't have tasks yet in Lean, I decided to start refactoring
the `thunk` type. I defined it as:
```
-- TODO(Leo): mark as opaque, it is implemented by the new runtime
structure thunk (α : Type u) : Type u :=
(fn : unit → α)
def thunk.pure {α : Type u} (a : α) : thunk α :=
⟨λ _, a⟩
def thunk.get {α : Type u} (t : thunk α) : α :=
t.fn ()
```
The idea is to use the runtime primitives to implement them.
Then, I realized the support for `thunk`s in the elaborator are quite
hacky. Given `f x`, if `f`'s domain has type `thunk A`, we elaborate
`f x` as `f (fun _, x)` even if `x` has type `thunk A`.
This is quite bad, for example, suppose we have
```
def f (x : thunk A) := ...
```
Then, the following definition is type incorrect.
```
def g (x : thunk A) := f x
```
and we are forced to write
```
def g (x : thunk A) := f (x ())
```
The term `f (x ())` will be elaborated as `f (fun _, x ())` and an
unnecessary closure is created at runtime.
This mechanism inherited from Lean 3 is also incompatible with the
new thunk definition. Given `x : thunk A`, I want to write `x.get`
to retrieve the value instead of `x ()` as in Lean 3.
However, `x.get` expands into the nonsensical `(fun _, x).get`.
So, I decided to view the mapping `A` to `thunk A` as a "coercion".
I used double quotes, because it is a macro instead of a function.
If it were a coercion, then we would be using `thunk.pure` to coerce
values but this is not we want most of the time.
For example, given `f : thunk A -> B` and a term `t : A`, when we write
`f t`, we want it to be converted into `f (fun _, t)` instead of
`f (thunk.pure t)` which would eagerly compute `t`. The transformation
`t` into `fun _, t` is syntactic.
We cannot implement it using type classes. I implemented it as
a hard-coded extra case like the one from `Prop` to `bool`.
We can also add a coercion from `thunk A` to `A` to avoid the `.get`.
That being said, I had a few breakages in the code base since we only
use coercions when the given and expected type do not contain
metavariables.
We now define nat.le using (nat.ble : nat -> nat -> bool) function.
We will add builtin support for reducing `nat.ble` efficiently when the arguments are the to be added nat literals.
In Lean4, we will not generate non dependent recursors for inductive
predicates. The main goal is to make the shape of the automatically
generated recursors more uniform. The non uniform representation is
leftover from Lean2. In Lean2, we wanted to support different kernels
with different features. For example: we could create proof relevant
kernels, no impredicative universe, etc.
Recall that, in a kernel with an impredicative Prop and no proof
irrelevance, inductive predicates without dependent elimination are
weaker that inductive predicates with dependent elimination.
When proof irrelevance is enabled, we can generate the dependent
recursor from the non dependent one. Actually, the module drec.cpp
generates the dependent recursor.
Now, we only support one kind of kernel, and it doesn't make sense
anymore to generate non dependent recursors for inductive predicates.
This would only produce an unnecessary asymmetry on the inductive
datatype module.
Remark: we had to create non dependent recursors to help the elaborator.
This can be avoid if we improve the elaborator. I will do that in the
new elaborator implemented in Lean.
Remark: equation lemmas are broken for definitions that pattern match on
nested inductive datatypes. The problem is the super messy
`prove_eq_rec_invertible_aux` function. This function will not be needed
after I finish the new inductive datatype support in the kernel.
cc @kha
The `quot` type is now implemented in the kernel.
We will do the same thing for inductives.
We will not support normalizer extensions anymore in Lean4.
It doesn't make sense since we settled with 2 extensions: quotients and
inductives. Moreover, any new extension would require substantial
changes (e.g., code generator).
The normalizer_extension feature was useful when we were experimenting
with different kernel flavors.
Most efficient hash functions use uint32/uint64 and produce values
that do not fit in out small nat representation. Thus, GMP big numbers
would have to be created.
The idea is to match the precedence used in regular programming
languages, where `x = y || x = z` is parsed as `(x = y) || (x = z)`.
This commit also adds `!x` as notation for `bnot x`
With the current elaboration scheme, out_params and coercions do not mix well,
as evidenced by the following example by @digama:
```
variables {α : Type*} [group α]
def gpow : α → ℤ → α := sorry
instance group.has_pow : has_pow α ℤ := ⟨gpow⟩
example (a : α) : a ^ 0 = 1 := sorry -- failed to synth ⊢ has_pow α ℕ
example (a : α) : a ^ (0:ℕ) = 1 := sorry -- ok, coerces
example (a : α) : a ^ (0:ℤ) = 1 := sorry -- ok
```
The issue is that
* we first try to solve `has_pow ?α ?β`, which is postponed
* then infer `?α = nat` from `a`
* then at some point call `elaborator::synthesize()` and default `β` to `nat`
* then try to solve `has_pow nat nat`, which fails at `int =?= nat`
This command is not just a cosmetic feature.
We need it to defined `id_rhs` before the tactic framework is defined.
We want `id_rhs` to be used in all definitions generated by the equation
compiler. Right now, it is only used in definitions defined after the
tactic framework.
@kha: I decided to implement this change before I start the
type_context modifications. The change did not affect the corelib and
test suite much. The only annoying problem is that `out` cannot be
used to name locals anymore.
