For example, in the new test `qsort64.lean`, the new optimization
prevents the repeated execution of `box UInt64.inhabited`.
On my machine
```
./run.sh qsort64.lean 2000000
```
Goes from 1.22s to 0.355s
If `persistent == true`, then object is known to be persistent at
compilation time. `emitc` omits `inc/dec` operations to
persistent objects. The interpreter does not to avoid memory leaks.
@kha It is unclear why the C++ compilers were accepting our generated
files without `lean::`. I found the issue by accident while working on
the new C backend.
We are going to use a simpler approach to help users writing hygienic
macros. Suppose we have a syntax quotation such as
```
`(let x := %%a;
ite x x %%b)
```
We will parse this quotation, and during elaboration, we must create
code (i.e., an `Expr`) such that given `a` and `b`, it constructs
a (new) syntax object, and we want to guarantee that there is no accidental name capture.
So, given the syntax object `S` representing the quotation above, we
first pre-resolve the identifiers in `S`. In this step, we annotate the
identifier `ite` with the global declaration `_root_.ite`.
Then, we create a fresh identifier for each identifier, but we would
preserve the pre-resolved information.
Assume the monadic action `mkFresh <id>` creates a fresh identifier with
prefix `<id>`, and `mkFreshWithPreresolved <id> <pre-list>` creates a
fresh identifier with prefix <id> and pre-resolved list `<pre-list>`.
Then, the quotation above would be transformed into:
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
`(let %%x := %%a;
%%ite %%x %%x %%b)
```
Here, the new quotation is just syntax sugar for a sequence of `Syntax`
constructor applications. Now, whenever we want to create a syntax
object using the quotation above, we guarantee there is no accidental
name capture because we are creating a fresh identifier for all
identifiers in the quotation. Global references are preserved using the
field preresolved that we already have.
It is straightforward to implement the transformation above using a
mapping. Note that if we use the same mapping to elaborate two different
quotations, we are essentially saying they share the same scope.
For example, suppose we have
```
let c := `(ite x x %%b);
`(let x := %%a; %%c)
```
If we use the same mapping, we produce
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
let c := `(%%ite %%x %%x %%b);
`(let %%x := %%a; %%c)
```
If we create a new mapping when compiling each quotation, we get
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
let c := `(%%ite %%x %%x %%b);
let x1 := mkFresh `x;
`(let %%x1 := %%a; %%c)
```
which is probably not what the user wants.
We can provide a simple notation for users specifying which behavior
they want. The default may be super simple. Example: we have a new mapping (aka scope) per declaration.
The approach above is simple and efficient. It is also great for
users that want to create syntax objects during the elaboration phase
and want to avoid name capture.
In Lean 4, we will support the more general
`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`
