max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/vm/vm_string): missing VM builtin for string_imp projections

Browse source
This commit is contained in:
Leonardo de Moura 2017-10-20 14:22:21 -07:00
parent ffb2464f1f
commit 47a8c2baef
3 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/vm/vm_string.cpp
View file

@ -120,6 +120,10 @@ unsigned string_imp_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
return 0;
}
vm_obj string_imp_data(vm_obj const & s) {
return string_to_list(s);
}
vm_obj string_fold(vm_obj const &, vm_obj const & a, vm_obj const & f, vm_obj const & s) {
vm_string const & vs = to_vm_string(s);
vm_obj r = a;
@ -407,6 +411,7 @@ vm_obj string_iterator_imp_snd(vm_obj const & o) {
void initialize_vm_string() {
DECLARE_VM_BUILTIN(name({"string_imp", "mk"}), string_imp_mk);
DECLARE_VM_BUILTIN(name({"string_imp", "data"}), string_imp_data);
DECLARE_VM_CASES_BUILTIN(name({"string_imp", "cases_on"}), string_imp_cases_on);
DECLARE_VM_BUILTIN(name({"string", "length"}), string_length);
@ -430,10 +435,10 @@ void initialize_vm_string() {
DECLARE_VM_BUILTIN(name({"string", "iterator", "next_to_string"}), string_iterator_next_to_string);
DECLARE_VM_BUILTIN(name({"string", "iterator", "prev_to_string"}), string_iterator_prev_to_string);
DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "mk"}), string_iterator_imp_mk);
DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "mk"}), string_iterator_imp_mk);
DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "fst"}), string_iterator_imp_fst);
DECLARE_VM_BUILTIN(name({"string", "iterator_imp", "snd"}), string_iterator_imp_snd);
DECLARE_VM_CASES_BUILTIN(name({"string", "iterator_imp", "cases_on"}), string_iterator_imp_cases_on);
DECLARE_VM_CASES_BUILTIN(name({"string", "iterator_imp", "cases_on"}), string_iterator_imp_cases_on);
}
void finalize_vm_string() {

1
tests/lean/string_imp2.lean
View file

@ -15,3 +15,4 @@ s ++ " " ++ s
#eval "αβγ".mk_iterator.next.1
#eval "αβγ".mk_iterator.next.next.1
#eval "αβγ".mk_iterator.next.2
#eval "αβ".1

1
tests/lean/string_imp2.lean.expected.out
View file

@ -12,3 +12,4 @@
['α']
['β', 'α']
['β', 'γ']
['α', 'β']