From d103ff70fe017fdda3787988ab402819e7a79d68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Feb 2019 10:49:58 -0800 Subject: [PATCH] feat(library/compiler): avoid `cnstr_set_scalar` when possible --- src/library/compiler/emit_bytecode.cpp | 4 +-- src/library/compiler/emit_cpp.cpp | 7 ++++-- src/library/compiler/llnf.cpp | 34 +++++++++++++++++++++++--- src/library/compiler/llnf.h | 4 +-- 4 files changed, 39 insertions(+), 10 deletions(-) diff --git a/src/library/compiler/emit_bytecode.cpp b/src/library/compiler/emit_bytecode.cpp index 69b8201657..1ca3ef136b 100644 --- a/src/library/compiler/emit_bytecode.cpp +++ b/src/library/compiler/emit_bytecode.cpp @@ -194,8 +194,8 @@ class emit_bytecode_fn { buffer args; expr const & fn = get_app_args(e, args); lean_assert(is_llnf_reuse(fn)); - unsigned cidx, nusizes, ssz; - is_llnf_reuse(fn, cidx, nusizes, ssz); + unsigned cidx, nusizes, ssz; bool updt_cidx; + is_llnf_reuse(fn, cidx, nusizes, ssz, updt_cidx); if (ssz != 0 || nusizes != 0) throw_no_unboxed_support(); compile_args(args.size(), args.data(), bpz, m); emit(mk_reuse_instr(cidx, get_app_num_args(e) - 1)); diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 61fcbe05a0..687963f4dc 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -475,13 +475,16 @@ struct emit_fn_fn { void emit_reuse(expr const & x, expr const & fn, buffer const & args) { lean_assert(!args.empty()); unsigned cidx, num_usizes, num_bytes; - lean_verify(is_llnf_reuse(fn, cidx, num_usizes, num_bytes)); + bool updt_cidx; + lean_verify(is_llnf_reuse(fn, cidx, num_usizes, num_bytes, updt_cidx)); expr const & o = args[0]; m_out << "if (lean::is_scalar("; emit_fvar(o); m_out <<")) {\n"; m_out << " "; emit_alloc_cnstr(x, cidx, args.size()-1, num_usizes, num_bytes); m_out << "} else {\n"; m_out << " "; emit_lhs(x); emit_fvar(o); m_out << ";\n"; - m_out << " lean::cnstr_set_tag("; emit_fvar(o); m_out << ", " << cidx << ");\n"; + if (updt_cidx) { + m_out << " lean::cnstr_set_tag("; emit_fvar(o); m_out << ", " << cidx << ");\n"; + } m_out << "}\n"; emit_cnstr_sets(x, args.size()-1, args.data()+1); } diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 806bf9acd4..f8808df66f 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -70,6 +70,25 @@ static bool is_llnf_ternary_primitive(expr const & e, name const & prefix, unsig return true; } +static bool is_llnf_quaternary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2, unsigned & i3, unsigned & i4) { + if (!is_constant(e)) return false; + name const & n4 = const_name(e); + if (!is_internal_name(n4)) return false; + if (n4.is_atomic() || !n4.is_numeral()) return false; + i4 = n4.get_numeral().get_small_value(); + name const & n3 = n4.get_prefix(); + if (!is_internal_name(n3)) return false; + if (n3.is_atomic() || !n3.is_numeral()) return false; + i3 = n3.get_numeral().get_small_value(); + name const & n2 = n3.get_prefix(); + if (n2.is_atomic() || !n2.is_numeral()) return false; + i2 = n2.get_numeral().get_small_value(); + name const & n1 = n2.get_prefix(); + if (n1.is_atomic() || !n1.is_numeral() || n1.get_prefix() != prefix) return false; + i1 = n1.get_numeral().get_small_value(); + return true; +} + /* A constructor object contains a header, then a sequence of pointers to other Lean objects, a sequence of `usize` (i.e., `size_t`) scalar values, and a sequence of other scalar values. @@ -88,9 +107,16 @@ scalar fields. expr mk_llnf_cnstr(unsigned cidx, unsigned num_usizes, unsigned num_bytes) { return mk_constant(name(name(name(*g_cnstr, cidx), num_usizes), num_bytes)); } bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes) { return is_llnf_ternary_primitive(e, *g_cnstr, cidx, num_usizes, num_bytes); } -/* The `_reuse...` is similar to `_cnstr...`, but it takes an extra argument: a memory cell that may be reused. */ -expr mk_llnf_reuse(unsigned cidx, unsigned num_usizes, unsigned num_bytes) { return mk_constant(name(name(name(*g_reuse, cidx), num_usizes), num_bytes)); } -bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes) { return is_llnf_ternary_primitive(e, *g_reuse, cidx, num_usizes, num_bytes); } +/* The `_reuse....` is similar to `_cnstr...`, but it takes an extra argument: a memory cell that may be reused. */ +expr mk_llnf_reuse(unsigned cidx, unsigned num_usizes, unsigned num_bytes, bool updt_cidx) { + return mk_constant(name(name(name(name(*g_reuse, cidx), num_usizes), num_bytes), updt_cidx)); +} +bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes, bool & updt_cidx) { + unsigned aux; + bool r = is_llnf_quaternary_primitive(e, *g_reuse, cidx, num_usizes, num_bytes, aux); + updt_cidx = aux; + return r; +} expr mk_llnf_reset(unsigned n) { return mk_constant(name(*g_reset, n)); } bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_reset, n); } @@ -570,7 +596,7 @@ class to_llnf_fn { } j++; } - r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_num_usizes, k_info.m_scalar_sz), r), obj_args); + r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_num_usizes, k_info.m_scalar_sz, m_cinfo.m_cidx != k_info.m_cidx), r), obj_args); unsigned uidx = 0; unsigned offset = 0; j = nparams; diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h index 63f823ae57..ea3c21f72d 100644 --- a/src/library/compiler/llnf.h +++ b/src/library/compiler/llnf.h @@ -18,7 +18,7 @@ optional> mk_boxed_version(environment env, name co bool is_llnf_apply(expr const & e); bool is_llnf_closure(expr const & e); bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz); -bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz); +bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz, bool & updt_cidx); bool is_llnf_reset(expr const & e, unsigned & n); bool is_llnf_proj(expr const & e, unsigned & idx); bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset); @@ -33,7 +33,7 @@ bool is_llnf_dec(expr const & e); bool is_llnf_op(expr const & e); inline bool is_llnf_cnstr(expr const & e) { unsigned d1, d2, d3; return is_llnf_cnstr(e, d1, d2, d3); } -inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2, d3; return is_llnf_reuse(e, d1, d2, d3); } +inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2, d3; bool u; return is_llnf_reuse(e, d1, d2, d3, u); } inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); } inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); } inline bool is_llnf_sproj(expr const & e) { unsigned d1, d2, d3; return is_llnf_sproj(e, d1, d2, d3); }