@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.
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.
for ordered_cancel_comm_monoid. The change to partial_order, with a derived lt relation, makes the lt axioms of ordered groups derivable with no additional assumptions.
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.
closes#1814
@kenmcmil: the error messages will now list aliased variables.
For example, in your file, the new error message is:
```
invalid type ascription, term has type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
but is expected to have type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
types contain aliased name(s): c'
remark: the tactic `dedup` can be used to rename aliases
state:
...
```
This is the equivalent of the `ginduction` tactic for cases, but rolled into the same syntax as `cases` itself. `cases h : term` is the syntax, and it will introduce a hypothesis `h : term = C a b...` demonstrating that the original term is equal to the current case.
I considered the possibility of calling `injection` on the generated equalities, but it's useless in the casaes when the equality carries some real information (such as `f x = C1 a`), and when the input term is a local constant, `injection` will do subst, which will undo the effect of the `cases`. If the input term is a constructor, then `injection` would do something interesting, but you would never want to call `cases` in this case because the constructor is already exposed.
