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

fix(library/compiler/inliner): inliner was unfolding constants aggressively when trying to reduce projections

Browse source 
@digama0 After this commit, your example will also produce a
non-destructive update.

```lean
structure test :=
(data1 : array nat 3)
(data2 : array nat 3)
(sz: nat)

def test.write (s : test) (i : fin 3) (v : nat) :=
{s with data1 := s^.data1^.write i v, data2 := s^.data2^.write i v}

set_option trace.array.update true
  (fin.of_nat 1) 10 in
  (a^.data1^.read (fin.of_nat 1), a^.data2^.read (fin.of_nat 2)) -- destructive write
```
This commit is contained in:
Leonardo de Moura 2017-03-09 18:51:47 -08:00
parent 9d3c0497cb
commit 6916a8ceca
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/inliner.cpp
View file

@ -110,6 +110,12 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
return e;
}
optional<expr> reduce_projection(expr const & e) {
/* When trying to reduce a projection, we should only unfold reducible constants. */
type_context::transparency_scope _(ctx(), transparency_mode::Reducible);
return ctx().reduce_projection(e);
}
virtual expr visit_app(expr const & e) override {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
@ -136,7 +142,7 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
}
if (arity <= nargs) {
if (auto r = ctx().reduce_projection(e)) {
if (auto r = reduce_projection(e)) {
return visit(*r);
}
}