Both `alternative` and `monad` implement `applicative`. However,
their default implementations for `seq_right` and `seq_left` are
different. The `alternative` implementation uses the inefficient default
version for `seq_right` available at `applicative`:
```
(seq_right := λ α β a b, const α id <$> a <*> b)
```
instead of the more efficient
```
(seq_right := λ α β x y, x >>= λ _, y)
```
defined at `monad` using the `bind` operator.
This commit makes sure the `applicative` instances for `reader_t`,
`state_t`, `option` and `parsec_t` use the efficient version.
I found the problem when inspecting the generated code for:
```
def symbol (s : string) : parsec' unit :=
(str s *> whitespace) <?> ("'" ++ s ++ "'")
```
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
@kha, `eqn_compiler.lemmas` is false by default.
I will keep them disabled until I remove the inductive compiler.
I'm building the new inductive datatype module (to replace the inductive
compiler), and the lemmas will fail to be proved in the next commits
until the transition is complete.
Motivation: in 64-bit machines, we can store boxed uint32 values as a
tagged pointer. In 32-bit machines, we need to allocated an object (like
Haskell) to store the uint32 value. So, the generated bytecode is quite
different in each platform.
This change also allow us to simplify the IR. Example: we don't need the
type `sizet` anymore.
Impact: To be able to bootstrap in both platforms,
we will have to store two versions of the generated code: 32 and 64
versions. In principle, we only need to store the 64-bit version,
and use cross-compilation to build the 32-bit version.
Without these annotations, Lean will timeout when trying to synthesize
the type class instance `decidable_eq uint32`. The type class resolution
problem will produce the unification problem:
```
decidable (@eq uint32 a b) =?= decidable (@eq usize ?x ?y)
```
which Lean tries to solve by assigning `?x := a`.
During the assignment, the types of `?x` and `a` are unified with "full
force". Thus, we get the constraint
```
usize_sz =?= uint32_sz
```
which will take forever to be solved when peforming the computation in
unary arithmetic.
Remark: this commit also makes sure that `type_context` will not unfold
irreducible definitions when trying to unify/match the types.
The new test `type_class_performance1.lean` exposes the problem fixed
by this commit.
