From 6916a8cecaf95b6704c4434c8abcc84ee353d441 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Mar 2017 18:51:47 -0800 Subject: [PATCH] fix(library/compiler/inliner): inliner was unfolding constants aggressively when trying to reduce projections @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 ``` --- src/library/compiler/inliner.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 752f6bac00..8e8b34a41d 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -110,6 +110,12 @@ class inline_simple_definitions_fn : public compiler_step_visitor { return e; } + optional 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); } }