Now, the elaborator only uses the quasi-pattern unifier approximation
for inferring the implicit motive in recursor-like applications.
This change was motivated by counterintuitive behavior associated with
this approximation. For example, before this commit
```
variables {δ σ : Type}
def ex1 : state_t δ (state_t σ id) σ :=
monad_lift (get : state_t σ id σ) -- doesn't work
def ex2 : state_t δ (state_t σ id) σ :=
do s ← monad_lift (get : state_t σ id σ), -- works
return s
```
The first one doesn't work because when we elaborate
`@monad_lift ?m ?n ?c ?α (get : state_t σ id σ) : ?n ?α`
with expected type `state_t δ (state_t σ id) σ`
It first produces the following unification problem by processing
matching the inferred type with the expected one.
```
?n ?α =?= state_t δ (state_t σ id) σ
==> (approximate using first-order unification)
?n := state_t δ (state_t σ id)
?α := σ
```
Then we try to solve
```
?m ?α =?= state_t σ id σ
==> instantiate metavars
?m σ =?= state_t σ id σ
==> (approximate since it is a quasi-pattern unification constraint)
?m := λ σ, state_t σ id σ
```
Remark: the constraint is not a Milner pattern because `σ` is in
the local context of `?m`. By assuming it is a Milner pattern,
we are ignoring the other possible solutions:
```
?m := λ σ', state_t σ id σ
?m := λ σ', state_t σ' id σ
?m := λ σ', state_t σ id σ'
```
We need the quasi-pattern approximation for elaborating recursors.
So, this commit enable this kind of approximation only when
elaborating recursors and executing induction-like tactics.
If we had used first-order unification, then we would have produced
the right answer: `?m := state_t σ id`
Haskell would solve this example since it always uses
first-order unification during elaboration.
The second one works because when we elaborate
`monad_lift (get : state_t σ id σ)`, the expected type is `state_t δ (state_t σ id) ?α`.
So, `?m ?α =?= state_t σ id σ` will not considered to be a quasi-pattern
since `?α` is not yet assigned to a local constant.
We are not fully confident this commit produces a better user
experience. We know that
- Full higher-order unification (used in Lean2) produces a combinatoric
explosion, and generates a lot of non-termination in complex type class
hierarchies (monad library, has_coe, etc). The problem is that
higher-order unification manages to create new solutions that we
cannot find using first-order unification.
- Lean3 is more reliable than Lean2 for elaborating monadic code because
it does not use higher-order unification.
- For elaborating recursor-like applications, we need at least the
quasi-patterns. We need it when trying to infer the implicit
motive. First-order unification works poorly in this case. Note that
the lack of higher-order unification in Lean3 forces us to provide the
motive explicitly for terms that Lean2 can elaborate.
- We need quasi-patterns for solving unification constraints in the
induction-like tactics. Similar to the previous item. We use it to infer
the motive. (edited) I will try to disable the quasi-pattern
approximation when elaborating regular applications. At least, we will
behave like Haskell for this kind of application.
Next steps:
- Implement more validators (e.g., blockid validator, type checker).
- Implement C++ code generator (in Lean). We can use it for testing the new
lean_obj module implemented in C++.
- Implement interpreter (in C++) for sanity checking.
- Implement LLVM IR generator (in Lean). It just outputs a text file using LLVM
syntax. After, we are confident we are generating valid LLVM IR, we
can try to link LLVM with Lean.
Remark: the non monadic versions are called list.all and list.any.
We did not use `list.mall` and `list.many` since `mall` and `many` are
existing words.
Before this commit, the unifier would try to solve the unification consraint
?m =?= fun x_1 ... x_n, ?m x_1 ... x_n
by assigning
?m := fun x_1 ... x_n, ?m x_1 ... x_n
which fails the occurs check.
This commit skips the assignment by using eta-reduction.
The new lean_obj objects will be defined at util.
Reason: we will define `name`, `options`, `format`, ... on top of lean_obj.
lean_obj depends on mpz.
Remark: lean_obj will replace vm_obj.
numeric_traits is dead code. It was used to implement a simplex that was
parametric on the number type. This code has been moved to Z3.
So, we don't need it anymore.
It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.
memory_pool object introduces memory contention and unnecessary
complexity. Moreover, it actually reduces performance when we compile
Lean using JEMALLOC.
Here are the numbers for corelib
jemalloc with memory_pool: 13.83 secs
jemalloc without memory_pool: 13.60 secs
We use small_object_allocator to allocate vm_obj's.
However small_object_allocator is not thread safe. So, we need to copy
vm_obj's between threads. Moreover, in our experiments, we observed that
JEMALLOC is actually faster than the small_object_allocator.
Here are numbers for the reduced corelib.
small_object_allocator: 15.62 secs
gcc 4.9 allocator: 16.19 secs
jemalloc: 13.83 secs
This abstraction was added when we started Lean.
We wanted to focus on nonlinear arithmetic and support dReal.
The zpz module was going to be used to implement polynomial
factorization procedures similar to the ones in Z3 and computer algebra
systems.
This is not a goal for the Lean project anymore.
These two abstractions were added when we planned to have an efficient
Simplex module, written in C++, in Lean. We have moved this module to
Z3. So, we don't need these abstractions anymore.
Binary rationals were added when we started the Lean project.
We wanted to use them to implement an algebraic number module similar to the
one we implemented in Z3.
If one day we implement algebraic numbers in Lean, we will do it in Lean
instead of C++.
