@kha @dselsam: I added a small repro for the bug reported by Daniel on
Zulip. The current fix is not polished at all since we will replace
the equation compiler with one implemented in Lean. The bug is once
again on the code that handle nested `match`-expressions containing
recursive calls. We had problems in this module before, and the
current compilation strategy using auxiliary `*._match_<id>` functions
is also very inconvenient for users. They are often puzzled when they
see these auxiliary functions appearing in proof goals after unfolding
and/or simplification. They usually don't know what to do with these
auxiliary definitions, and have no idea how they were defined and what
they correspond to if the function has several nested
`match`-expression. Right now, the best option is to use `#print
<fun-name>._match_<id>` which is far from ideal.
@kha: @dselsam and I discussed an alternative approach where we do not
create the auxiliary definitions, annotate the generated `cases_on`
applications with meta-data indicating they correspond to a nested
match, and modify the pretty printer to display these annotated
`cases_on` applications using the `match` syntax. With these
modifications, the behavior will be similar to the one in Coq where
complex `match`-expressions are reduced to atomic ones. The only
difference is that we represent these "atomic" `match`-expressions
using `cases_on` applications.
This commit uses a simpler version of this approach where we do not
create auxiliary `*._match_<id>` functions, and more importantly do
not use the dreadful `pull_nested_rec_fn` code.
@kha This is another instance of a problem we discussed last summer.
I guess there are many more instances like this one that we are not handling.
Recall that we want to preserve types at `csimp` because we eventually
want to allow users to use equational theorems as rewriting rules during
compilation.
However, some of the transformations that `csimp` perform do not
preserve typeability in CIC.
Moreover, some of the optimizations require type inference.
I see the possible long term solutions:
1- Erase types and proofs as soon as possible. The main drawback here is
that we would have to develop an approach for translating Lean theorems
into valid rewriting rules for lambda pure. For example, the following
theorem should not be used as a rewriting rule after we erase types.
```
forall (xs : List Unit) (f : Unit -> Unit), List.map f xs = List.map id xs
```
BTW, I don't want to abandon the idea of using lemmas as rewriting rules in
the compiler.
2- Go over `csimp` and other compiler steps and make sure they work
properly even when `type_checker::infer_type` fails.
The array read and write operations are now called:
- "Comfortable" version (with runtime bound checks):
`Array.get` and `Array.set` like OCaml.
It is also consistent with `Ref.get` and `Ref.put`,
and `get` and `set` for `MonadState`.
- `Fin` version (without runtime bound checks):
`Array.index` and `Array.update` like in F*.
- `USize` version (without runtime bound checks and unboxing):
`Array.idx` and `Array.updt`.
cc @kha
@kha I have disabled this check. It was implemented 2 years ago by
Daniel, and I don't want to fix it. It seems you have already fixed a
bug there. AFAICT, this check is just for improving error messages.
I believe we may not even need it since the kernel now supports nested
inductive types. AFAIR, Daniel implemented this check here because the
inductive compiler was introducing a lot of auxiliary declarations
that were making the kernel error messages unreadable.
