From 1f53c4fd33abf0d03c3cedb3bc667e2538865bad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Jun 2019 15:30:58 -0700 Subject: [PATCH] feat(library/init/lean/eqncompiler): register `[matchPattern]` attribute using new attribute manager --- library/init/lean/default.lean | 1 + library/init/lean/eqncompiler/default.lean | 7 + .../init/lean/eqncompiler/matchpattern.lean | 23 +++ src/library/init_module.cpp | 3 - src/library/pattern_attribute.cpp | 24 +-- src/library/pattern_attribute.h | 3 - src/stage0/CMakeLists.txt | 2 +- src/stage0/init/lean/default.cpp | 5 +- src/stage0/init/lean/eqncompiler/default.cpp | 26 +++ .../init/lean/eqncompiler/matchpattern.cpp | 152 ++++++++++++++++++ 10 files changed, 217 insertions(+), 29 deletions(-) create mode 100644 library/init/lean/eqncompiler/default.lean create mode 100644 library/init/lean/eqncompiler/matchpattern.lean create mode 100644 src/stage0/init/lean/eqncompiler/default.cpp create mode 100644 src/stage0/init/lean/eqncompiler/matchpattern.cpp diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean index d37932b27e..9c53f817f0 100644 --- a/library/init/lean/default.lean +++ b/library/init/lean/default.lean @@ -14,3 +14,4 @@ import init.lean.evalconst import init.lean.parser import init.lean.reducibilityattrs import init.lean.elaborator +import init.lean.eqncompiler diff --git a/library/init/lean/eqncompiler/default.lean b/library/init/lean/eqncompiler/default.lean new file mode 100644 index 0000000000..82d44e9f46 --- /dev/null +++ b/library/init/lean/eqncompiler/default.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.lean.eqncompiler.matchpattern diff --git a/library/init/lean/eqncompiler/matchpattern.lean b/library/init/lean/eqncompiler/matchpattern.lean new file mode 100644 index 0000000000..8f815b8fed --- /dev/null +++ b/library/init/lean/eqncompiler/matchpattern.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.lean.attributes + +namespace Lean +namespace EqnCompiler + +def mkMatchPatternAttr : IO TagAttribute := +registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)" + +@[init mkMatchPatternAttr] +constant matchPatternAttr : TagAttribute := default _ + +@[export lean.has_match_pattern_attribute_core] +def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool := +matchPatternAttr.hasTag env n + +end EqnCompiler +end Lean diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index a8a39a9c94..bfff0312b1 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -32,7 +32,6 @@ Author: Leonardo de Moura #include "library/attribute_manager.h" #include "library/app_builder.h" #include "library/fun_info.h" -#include "library/pattern_attribute.h" #include "library/check.h" #include "library/parray.h" #include "library/profiling.h" @@ -91,7 +90,6 @@ void initialize_library_module() { initialize_fun_info(); initialize_abstract_context_cache(); initialize_type_context(); - initialize_pattern_attribute(); initialize_check(); initialize_parray(); initialize_time_task(); @@ -101,7 +99,6 @@ void finalize_library_module() { finalize_time_task(); finalize_parray(); finalize_check(); - finalize_pattern_attribute(); finalize_type_context(); finalize_abstract_context_cache(); finalize_fun_info(); diff --git a/src/library/pattern_attribute.cpp b/src/library/pattern_attribute.cpp index 98acf04549..424cae43b9 100644 --- a/src/library/pattern_attribute.cpp +++ b/src/library/pattern_attribute.cpp @@ -4,30 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/attribute_manager.h" +#include "kernel/environment.h" namespace lean { -static name * g_pattern_attr = nullptr; - -static basic_attribute const & get_pattern_attribute() { - return static_cast(get_system_attribute(*g_pattern_attr)); -} +uint8 has_match_pattern_attribute_core(object*, object*); bool has_pattern_attribute(environment const & env, name const & d) { - return has_attribute(env, *g_pattern_attr, d); -} - -environment set_pattern_attribute(environment const & env, name const & n) { - return get_pattern_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, true); -} - -void initialize_pattern_attribute() { - g_pattern_attr = new name({"matchPattern"}); - register_system_attribute(basic_attribute(*g_pattern_attr, "mark that a definition can be used in a pattern" - "(remark: the dependent pattern matching compiler will unfold the definition)")); -} - -void finalize_pattern_attribute() { - delete g_pattern_attr; + return has_match_pattern_attribute_core(env.to_obj_arg(), d.to_obj_arg()); } } diff --git a/src/library/pattern_attribute.h b/src/library/pattern_attribute.h index 85e4c7196b..c9c88bc6d7 100644 --- a/src/library/pattern_attribute.h +++ b/src/library/pattern_attribute.h @@ -8,7 +8,4 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { bool has_pattern_attribute(environment const & env, name const & d); -environment set_pattern_attribute(environment const & env, name const & d); -void initialize_pattern_attribute(); -void finalize_pattern_attribute(); } diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt index 8db2e7cdb8..950366612b 100644 --- a/src/stage0/CMakeLists.txt +++ b/src/stage0/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specializeattrs.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) +add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specializeattrs.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) diff --git a/src/stage0/init/lean/default.cpp b/src/stage0/init/lean/default.cpp index cd7cb7b247..8e1ab009be 100644 --- a/src/stage0/init/lean/default.cpp +++ b/src/stage0/init/lean/default.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.default -// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default +// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default init.lean.eqncompiler.default #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -24,6 +24,7 @@ obj* initialize_init_lean_evalconst(obj*); obj* initialize_init_lean_parser_default(obj*); obj* initialize_init_lean_reducibilityattrs(obj*); obj* initialize_init_lean_elaborator_default(obj*); +obj* initialize_init_lean_eqncompiler_default(obj*); static bool _G_initialized = false; obj* initialize_init_lean_default(obj* w) { if (_G_initialized) return w; @@ -49,5 +50,7 @@ w = initialize_init_lean_reducibilityattrs(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_elaborator_default(w); if (io_result_is_error(w)) return w; +w = initialize_init_lean_eqncompiler_default(w); +if (io_result_is_error(w)) return w; return w; } diff --git a/src/stage0/init/lean/eqncompiler/default.cpp b/src/stage0/init/lean/eqncompiler/default.cpp new file mode 100644 index 0000000000..3fa96d8178 --- /dev/null +++ b/src/stage0/init/lean/eqncompiler/default.cpp @@ -0,0 +1,26 @@ +// Lean compiler output +// Module: init.lean.eqncompiler.default +// Imports: init.lean.eqncompiler.matchpattern +#include "runtime/object.h" +#include "runtime/apply.h" +typedef lean::object obj; typedef lean::usize usize; +typedef lean::uint8 uint8; typedef lean::uint16 uint16; +typedef lean::uint32 uint32; typedef lean::uint64 uint64; +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +obj* initialize_init_lean_eqncompiler_matchpattern(obj*); +static bool _G_initialized = false; +obj* initialize_init_lean_eqncompiler_default(obj* w) { +if (_G_initialized) return w; +_G_initialized = true; +if (io_result_is_error(w)) return w; +w = initialize_init_lean_eqncompiler_matchpattern(w); +if (io_result_is_error(w)) return w; +return w; +} diff --git a/src/stage0/init/lean/eqncompiler/matchpattern.cpp b/src/stage0/init/lean/eqncompiler/matchpattern.cpp new file mode 100644 index 0000000000..6c97643853 --- /dev/null +++ b/src/stage0/init/lean/eqncompiler/matchpattern.cpp @@ -0,0 +1,152 @@ +// Lean compiler output +// Module: init.lean.eqncompiler.matchpattern +// Imports: init.lean.attributes +#include "runtime/object.h" +#include "runtime/apply.h" +typedef lean::object obj; typedef lean::usize usize; +typedef lean::uint8 uint8; typedef lean::uint16 uint16; +typedef lean::uint32 uint32; typedef lean::uint64 uint64; +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +namespace lean { +uint8 has_match_pattern_attribute_core(obj*, obj*); +} +obj* l_Lean_AttributeImpl_inhabited___lambda__4___boxed(obj*, obj*, obj*); +obj* l_Lean_EqnCompiler_matchPatternAttr; +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3; +obj* l_Lean_AttributeImpl_inhabited___lambda__3___boxed(obj*, obj*, obj*, obj*); +obj* l_Lean_EqnCompiler_mkMatchPatternAttr(obj*); +obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__1___boxed(obj*); +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1; +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(obj*, obj*); +obj* l_Array_mkEmpty(obj*, obj*); +obj* l_Lean_registerTagAttribute(obj*, obj*, obj*, obj*); +obj* l_Lean_AttributeImpl_inhabited___lambda__5(obj*, obj*); +obj* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(obj*, obj*); +obj* l_Lean_AttributeImpl_inhabited___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); +extern "C" obj* lean_name_mk_string(obj*, obj*); +obj* l_ExceptT_Monad___rarg___lambda__8___boxed(obj*, obj*); +uint8 l_Lean_TagAttribute_hasTag(obj*, obj*, obj*); +obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__2___boxed(obj*); +obj* l_Lean_AttributeImpl_inhabited___lambda__2___boxed(obj*, obj*, obj*, obj*); +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1; +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(obj*, obj*); +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2; +obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1() { +_start: +{ +obj* x_1; obj* x_2; +x_1 = lean::box(0); +x_2 = lean::alloc_cnstr(1, 1, 0); +lean::cnstr_set(x_2, 0, x_1); +return x_2; +} +} +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; +x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1; +return x_3; +} +} +obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1() { +_start: +{ +obj* x_1; obj* x_2; obj* x_3; +x_1 = lean::box(0); +x_2 = lean::mk_string("matchPattern"); +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2() { +_start: +{ +obj* x_1; +x_1 = lean::mk_string("mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"); +return x_1; +} +} +obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3() { +_start: +{ +obj* x_1; +x_1 = lean::alloc_closure(reinterpret_cast(l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed), 2, 0); +return x_1; +} +} +obj* l_Lean_EqnCompiler_mkMatchPatternAttr(obj* x_1) { +_start: +{ +obj* x_2; obj* x_3; obj* x_4; obj* x_5; +x_2 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1; +x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2; +x_4 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3; +x_5 = l_Lean_registerTagAttribute(x_2, x_3, x_4, x_1); +return x_5; +} +} +obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; +x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(x_1, x_2); +lean::dec(x_2); +lean::dec(x_1); +return x_3; +} +} +namespace lean { +uint8 has_match_pattern_attribute_core(obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; uint8 x_4; +x_3 = l_Lean_EqnCompiler_matchPatternAttr; +x_4 = l_Lean_TagAttribute_hasTag(x_3, x_1, x_2); +lean::dec(x_2); +lean::dec(x_1); +return x_4; +} +} +} +obj* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = lean::has_match_pattern_attribute_core(x_1, x_2); +x_4 = lean::box(x_3); +return x_4; +} +} +obj* initialize_init_lean_attributes(obj*); +static bool _G_initialized = false; +obj* initialize_init_lean_eqncompiler_matchpattern(obj* w) { +if (_G_initialized) return w; +_G_initialized = true; +if (io_result_is_error(w)) return w; +w = initialize_init_lean_attributes(w); +if (io_result_is_error(w)) return w; +l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1(); +lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1); +l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1(); +lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1); +l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2(); +lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2); +l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3(); +lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3); +REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "mkMatchPatternAttr"), 1, l_Lean_EqnCompiler_mkMatchPatternAttr); +w = l_Lean_EqnCompiler_mkMatchPatternAttr(w); +if (io_result_is_error(w)) return w; +l_Lean_EqnCompiler_matchPatternAttr = io_result_get_value(w); +lean::mark_persistent(l_Lean_EqnCompiler_matchPatternAttr); +lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "matchPatternAttr"), l_Lean_EqnCompiler_matchPatternAttr); +REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "hasMatchPatternAttribute"), 2, l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed); +return w; +}