The `no_confusion` construction is only generated for inductive
datatypes supported in the kernel.
Before this commit, given `h : T`, `cases h` could leak the internal encoding
used by the inductive compiler WHEN a nested and/or mutual inductive
datatype is used to index the inductive datatype `T`.
The new test exposes the problem.
The solution implemented in this commit uses inj_arrow lemmas
generated by the inductive compiler. We only use the lemmas
if the target is a proposition. If it is not, we sign an error.
The reason for this limitation is documented in the source code.
cc @jroesch @dselsam
Jared: the information leakage has been fixed. So, students will not be
confused by the internal encoding used in the inductive compiler.
I added the example I posted on slack as a new test.
Note that, the workaround I used has been removed.
`{s with ...}` is now `{..., ..s}`, which more clearly expresses that the
result type is not necessarily equal to the type of `s` (in absence of an
expected type and a structure name, we still default to the type of `s`).
Multiple fallback sources can be given: `{..., ..s, ..t}` will fall back to
searching a field in `s`, then in `t`. The last component can also be `..`,
which will replace any missing fields with a placeholder.
The old notation will be removed in the future.
Now, `cmp` is just a fixed helper function.
In the future, we will be able to use (more efficient) specialized
versions during code generation by defining simp rules.
This should match the meaning of "$?" in bash:
"3.7.5 Exit Status
The exit status of an executed command is the value returned by the waitpid system call or equivalent function. Exit statuses fall between 0 and 255."
Fixes#1868
The new test exposes the problem. Before this commit, the common
subexpressions at
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
match f v with
| tt := tst l + tst l - tst l -- <<< HERE
| ff := tst r
end
```
were not converted into a let-exprs.
We use the auxiliary procedure pull_nested_rec_fn to pull recursive
application in nested match expressions. This is needed because the
nested match expression is compiled before we process the recursive
procedure that contains it. This transformation may produce
performance problems if the recursive application does not depend on
the data being matched. Here is an example from the new test:
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
match f v with
| tt := tst l
| ff := tst r
end
```
pull_nested_rec_fn will convert it into
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) := tst._match_1 (f v) (tst l) (tst r)
```
Since our interpreter uses eager evaluation, both `(tst l)` and `(tst r)`
are executed. This commit fixes this issue by expanding `tst._match_1`
during code generation.
@kha I added the `d_array` type that we discussed today.
However, the VM implemantion is still using persistent arrays.
If we remove the persistent array support, then code using
hash_map will only be efficient if the hash_map is used linearly.
This is not the case in the reader module because we are planning
to support backtracking.
On the other hand, it is awkward we currently don't have a vanilla
array implementation in the VM. I suspect this will be a problem in
the future.
So, I see the following possibilities:
1- We implement a map data-structure using red-black trees in Lean.
We use this new data-structure to implement all maps in the new reader and
macro expander.
2- We implement a very simple map as a list of pairs.
Then, we replace it in the VM with an efficient implementation.
The VM implementation may use our internal red-black trees.
We may also use a persistent hash table implemented in C++,
but it would be awkward to ask the user to provide a hash function in the reference
implementation (i.e., the one using list of pairs), but not use it
anywhere :)
In contrast, if we use the red-black tree implementation we
would have to ask the user to provide a total order.
It is overkill for the list of pair reference implementation because
we just need an equality test, but, at least, the comparison function
will be used in the implementation.
3- Add types `d_parray` (dependent persistent array) and
`parray` (persistent array). In Lean, they would just wrap the
`d_array` and `array` types. In the VM, `d_array` and `array` would
be implemented using vanilla arrays and `d_parray` and `parray` would
be implemented using persistent arrays. Then, we could have
`d_hash_map`, `hash_map`, `d_phash_map` and `phash_map`. Argh, so many
versions :(
We would use `phash_map` to implement our reader and macro expander.
4- Add a `(persistent : bool := ff)` parameter to `d_array` and
`array` types. The disadvantage of this approach is that it has
a performance impact. The VM implementation would have to check
the `persisent` flag at runtime. The value of this flag is known
at compilation time, but we currently don't have a mechanism
for specializing native builtin C++ implementations for VM functions.
The equation compiler uses different strategies for processing
recursive equations. Some of them may produce unclear runtime cost
model. For example, the following fibonacci functions was running in
linear time instead of exponential time because the equation compiler
used the brec_on recursor.
def fib : nat → nat
| 0 := 1
| 1 := 1
| (n+2) := fib (n+1) + fib n
@dselsam and @jroesch have reported examples were the equation compiler
produces a negative performance impact. The new test (`eval` function)
captures the problem reported by @jroesch. In this example, the runtime
should not depend on the "amount of fuel".
This commit addresses this issue.
Motivations:
- Clear execution cost semantics for recursive functions.
- Auxiliary meta definition may assist recursive definition unfolding in the type_context object.
Next step: use meta auxiliary definition at code generation.
closes#1175
The types `string_imp` and `string.iterator_imp` were supposed to be
marked private, but we cannot do it because we need to provide
`string_imp.mk`, `string_imp.cases_on`, `string.iterator_imp.mk` and
`string.iterator_imp.cases_on` in the VM since we use a different
internal representation. Note that marking them as private does not
work since users can still access `string_imp.cases_on` using
meta-programming.
So, we need better support for private declarations.
Missing feature, char literals do not support non ASCII values.
That is, in the current implementation, we cannot write 'α'.
This will be implemented in the future.
The VM native implementation does not behave correctly for huge
strings (i.e., strings with more than 4G characters).
The problem is that the current implementation relies on
```
size_t force_to_size_t(vm_obj const & o, size_t def)
```
We may also have overflow problems in the string.iterator implementation
code. This is not a big deal right now, since I doubt we will try
to process string with more than 2^32 characters.
@Kha the `core_lib` and tests seem to be working correctly, but
we need more tests.
