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

fix(library/compiler/simp_inductive): array^.data should not be treated as a regular projection

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-09 19:11:51 -08:00
parent 6916a8ceca
commit b0a33259ee
3 changed files with 38 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/library/compiler/simp_inductive.cpp
View file

@ -203,12 +203,16 @@ class simp_inductive_fn : public compiler_step_visitor {
}
}
expr visit_default(name const & fn, buffer<expr> const & args) {
buffer<expr> new_args;
for (expr const & arg : args)
new_args.push_back(visit(arg));
return mk_app(mk_constant(fn), new_args);
}
expr visit_constructor(name const & fn, buffer<expr> const & args) {
if (is_vm_builtin_function(fn)) {
buffer<expr> new_args;
for (expr const & arg : args)
new_args.push_back(visit(arg));
return mk_app(mk_constant(fn), new_args);
return visit_default(fn, args);
} else {
/* The following invariant should hold since erase_irrelevant rejected code
where it doesn't hold. */
@ -235,30 +239,34 @@ class simp_inductive_fn : public compiler_step_visitor {
}
expr visit_projection(name const & fn, buffer<expr> const & args) {
projection_info const & info = *get_projection_info(env(), fn);
expr major = visit(args[info.m_nparams]);
buffer<bool> rel_fields;
name I_name = *inductive::is_intro_rule(env(), info.m_constructor);
get_constructor_info(info.m_constructor, rel_fields);
lean_assert(info.m_i < rel_fields.size());
lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
/* Adjust projection index by ignoring irrelevant fields */
unsigned j = 0;
for (unsigned i = 0; i < info.m_i; i++) {
if (rel_fields[i])
j++;
}
expr r;
if (has_trivial_structure(I_name, rel_fields)) {
lean_assert(j == 0);
r = major;
if (is_vm_builtin_function(fn)) {
return visit_default(fn, args);
} else {
r = mk_app(mk_proj(j), major);
projection_info const & info = *get_projection_info(env(), fn);
expr major = visit(args[info.m_nparams]);
buffer<bool> rel_fields;
name I_name = *inductive::is_intro_rule(env(), info.m_constructor);
get_constructor_info(info.m_constructor, rel_fields);
lean_assert(info.m_i < rel_fields.size());
lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
/* Adjust projection index by ignoring irrelevant fields */
unsigned j = 0;
for (unsigned i = 0; i < info.m_i; i++) {
if (rel_fields[i])
j++;
}
expr r;
if (has_trivial_structure(I_name, rel_fields)) {
lean_assert(j == 0);
r = major;
} else {
r = mk_app(mk_proj(j), major);
}
/* Add additional arguments */
for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
r = mk_app(r, visit(args[i]));
return r;
}
/* Add additional arguments */
for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
r = mk_app(r, visit(args[i]));
return r;
}
virtual expr visit_app(expr const & e) override {

1
src/library/vm/vm_array.cpp
View file

@ -168,6 +168,7 @@ unsigned array_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
void initialize_vm_array() {
DECLARE_VM_BUILTIN(name({"array", "mk"}), array_mk);
DECLARE_VM_BUILTIN(name({"mk_array"}), mk_array);
DECLARE_VM_BUILTIN(name({"array", "data"}), array_read);
DECLARE_VM_BUILTIN(name({"array", "read"}), array_read);
DECLARE_VM_BUILTIN(name({"array", "write"}), array_write);
DECLARE_VM_BUILTIN(name({"array", "push_back"}), array_push_back);

4
tests/lean/run/array1.lean
View file

@ -23,4 +23,6 @@ a^.foldl 0 (+)
#eval array_sum (mk_array 10 1)
#eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩
#eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩ + 20
#eval (mk_array 10 1)^.data 2
#eval (mk_array 10 3)^.data 2