Motivation: consider the following example
```
let m := if b then m1 else m2,
state.bind m (fun p, BIG p.1 p.2)
```
we first eta-expand the term, put in LCNF and inline state.bind
```
fun s,
let m := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
then, we apply `*-of-cases` at `m := ...` and its continuation, but we
need a joint point since the continuation is big. Then, we get
```
fun s,
let j_1 := fun x_1,
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
(fun h, let y := m1 in j_1 y)
(fun h, let y := m2 in j_1 y)
```
This code is not good if `m1` and `m2` are functions. At runtime, we
need to create a closure and pass it to the join point.
If we apply `app-of-cases` before other floating `cases` variants we
avoid this problem.
Here is the sequence of transformations if we apply `app-of-cases`
eagerly. We get
```
fun s,
let m := decidable.cases_on b (fun h, m1) (fun h, m2) in
let x_1 := m s in
prod.cases_on x_1 (fun a s', BIG a s')
```
as before. Then, we apply `app-of-cases` at `m s`, and get
```
fun s,
let x_1 := decidable.cases_on b (fun h, m1 s) (fun h, m2 s) in
prod.cases_on x_1 (fun a s', BIG a s')
```
Then, we apply `cases-of-cases`, but we again create a join point.
```
fun s,
let j_1 := fun x_1, prod.cases_on x_1 (fun a s', BIG a s') in
decidable.cases_on b
(fun h, let y := m1 s in j_1 y)
(fun h, let y := m2 s in j_1 y)
```
However, this time we are passing a value to `j_1` instead of a closure.
`app-of-cases` has two benefits:
1- It never creates new join points since applications are always small in LCNF
2- It may reduce a `cases` that returns a closure into a `cases` that
returns a value.
Motivation: explicit control flow graph
TODO: disabled `split_entries` for now.
I believe the new feature exposed a bug at `move_to_entries`.
I will fix this new issue in another commit.
This transformation is useful for caching the construction of closures
at runtime. For example, consider the following piece of code
```
λ α a,
@tree.cases_on a visit._main._lambda_1
(λ a_a a_a_1 a_a_2,
let _x_1 := visit._main ◾ a_a,
_x_2 := visit._main._lambda_5 a_a_1 a_a_2
in bind._main ◾◾◾◾ _x_1 _x_2)
```
where `visit._main._lambda_1` is of the form
```
visit._main._lambda_1 :=
λ _x, ...
```
At runtime, we will create a closure object for `visit._main._lambda_1`
since it has arity 1, but no arguments have been provided.
This commit implements a new transformation that creates an auxiliary
declaration with arity 0.
```
visit._main._closed_1 :=
visit._main._lambda_1
```
Its value is cached by the runtime. That is, the closure is created only
once.
@kha This optimizations reduces the number of closures by another 200k
at `parser1.lean`. We are now under 2million :)
We must make sure we do not accidentally change the arity of a join
point. The arity is the number of nested lambda expressions.
For example, suppose we have
```
let jp := fun (x : unit), t
```
where `jp` is a join point of arity 1, i.e., `t` is not a lambda.
All "jumps" will be of the form: `jp ()`.
Now, suppose we simplify `t` and it becomes a lambda `fun (y : nat), y`.
We should to represent `jp` as
```
let jp := fun (x : unit) (y : nat), y
```
Because we would be changing `jp`'s arity.
We have the same problem with `cases_on` applications in LCNF.
So, we fix the problem using the same approach: an auxiliary
`let`-declaration. The simplified join point above is encoded as
```
let jp := fun (x : unit),
let _z := fun (y : nat), y
in _z
```
cc @kha This is the bug that I mentioned on slack :)
The compiler applies transformations `t ==> s` where `t` and `s` are
only provably equal, but not definitionally equal. Moreover, in
dependent type theory `C[t]` may be type correct, but `C[s]` is not
when `t` is provably equal to `s`, but not definitionally equal.
Consider the following example:
```
fun n : nat,
let v : nat := 0+n in
let b : bv (0+n) := bv.mk v in
b
```
If we replace the first `0+n` with `n`, we produce the type incorrect
term
```
fun n : nat,
let v : nat := n in
let b : bv (0+n) := bv.mk v in
b
```
This is incorrect because `b : bv (0+n)` and `bv.mk v : bv n`, and
`0+n` is not definitionally equal to `n`.
We considered two approaches to address this problem:
1- A relaxed type checker (see deleted file `ctype_checker.cpp`).
This approach does not solve the problem, see example in the end
of the commit.
2- Introduce `lc_cast`-applications to "fix" type problems. However,
it seems it is too expensive to detect all places that require a
`lc_ast` application. We did that in a few places, but there is major
omission: when we simplify `x : t := v` to `x : t := w` (like in the
example above), we did not find an efficient way to repair all
affected places. We have implemented the function `replace_fvar_with`,
but we would have to execute after each `x : t := v` ==> `x : t := w`
where `v` is not definitionally equal to `w`. We considered grouping
many `replace_fvar_with` together, but it would still be very
expensive. Basically, for any occurrence of `x` we would have to check
whether the resulting type changed or not. Another issue is that the
restrictions considered at `replace_fvar_with` seem to restrictive:
for example `x` cannot occur in lambda/let-decl types. This happens
very frequently in code that uses types such as `decidable p`.
Remark: note that the Lean3 simplifier does not have support for
simplyfing let-decls for this reason. It offers only two options:
expand the `let`, or skip it.
So, this commit gives up the idea of ensuring that each compiler step
produces a type correct Lean term. That is, we preserve type
information, but we do not guarantee the terms are type correct after
we apply compiler transformations.
Here are examples that demonstrate the `ctype_checker` approach does
not work.
```
def C : bool → Type → Type
| tt α := nat × α
| ff α := string × α
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β :=
let f : Π (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), nat × β
:= λ (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β),
let x₁ : C b β := @eq.ndrec Type α (λ z : Type, C b z) x β h₂ in
@eq.ndrec bool b (λ z : bool, C z β) x₁ tt h₁
in f tt rfl α β x h₂
```
Now, suppose we want to put in LCNF. Then, we have to decide whether
each `eq.ndrec` will become a cast or not. Now, suppose we use the
compiler type checker `is_def_eq`.
Then, the first `eq.ndrec` application is `@eq.ndrec Type α (λ z :
Type, C b z) x β h₂`, and we have that `x : C b α` and the expected
type is `C b β`, both types are stuck since they reduce to
`bool.cases_on b (string × α) (nat × α)` and `bool.cases_on b (string
× β) (nat × β)` respectively. Thus, they are considered definitionally
equal, and we do not introduce a cast.
The second `eq.ndrec` application is
`@eq.ndrec bool b (λ z : bool, C z β) x₁ tt h₁`, and we have
`x₁ : C b β` and the expected type is `nat × β`, again they are definitionally equal since `C b β`.
Thus, in LCNF, the example above would be:
```
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β :=
let f : Π (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), nat × β
:= λ (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), x
in f tt rfl α β x h₂
```
The compiler type checker (`ctype_checker`) would say this is a type correct term.
Now, suppose we reduce `f tt rfl α β x h₂` using `csimp`, this term
would reduce to `x`.
Then, `f` is eliminated since it is not used anymore and we have the new simplified term
```
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β := x
```
`ctype_checker` will report it to be type incorrect. Since, `x : nat × α`
and the result type is `nat × β`, and both are not stuck.
This example shows that by applying simple reduction rules (zeta/beta
in the example above) we can transform a type correct term into a type
incorrect one.
The type `any` is also problematic. Consider the following example.
```
def ex (x : nat) : real :=
let f : any -> real := fun z, z in
f x
```
It is type correct. If we apply `csimp`, we will get.
```
def ex (x : nat) : real := x
```
which is type incorrect. Again, reduction may transform a type correct term into a type incorrect one.
Note that, I am not using anything fancy here. We are just treating
`any` as definitionally equal to any type.
