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

feat(frontends/lean/elaborator): add [elab_as_eliminator] attribute

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-10 21:58:30 -07:00
parent 214e91d1ae
commit f53ff9a3b6
2 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/datatypes.lean
View file

@ -354,6 +354,7 @@ namespace eq
variables {A : Type}
variables {a b c a': A}
attribute [elab_as_eliminator]
theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
eq.rec H₂ H₁

14
src/frontends/lean/elaborator.cpp
View file

@ -47,6 +47,7 @@ MK_THREAD_LOCAL_GET(type_context_cache_manager, get_tcm, true /* use binder info
static name * g_level_prefix = nullptr;
static name * g_elab_with_expected_type = nullptr;
static name * g_elab_as_eliminator = nullptr;
#define trace_elab(CODE) lean_trace("elaborator", scope_trace_env _scope(m_env, m_ctx); CODE)
#define trace_elab_detail(CODE) lean_trace("elaborator_detail", scope_trace_env _scope(m_env, m_ctx); CODE)
@ -56,6 +57,10 @@ bool elab_with_expected_type(environment const & env, name const & d) {
return has_attribute(env, *g_elab_with_expected_type, d);
}
bool elab_as_eliminator(environment const & env, name const & d) {
return has_attribute(env, *g_elab_as_eliminator, d);
}
elaborator::elaborator(environment const & env, options const & opts, metavar_context const & mctx,
local_context const & lctx):
m_env(env), m_opts(opts),
@ -206,9 +211,7 @@ bool elaborator::is_elim_elab_candidate(name const & fn) {
return true;
if (is_user_defined_recursor(m_env, fn))
return true;
// TODO(Leo): add attribute for adding extra-cases,
// and remove hard coded case
if (fn == get_eq_subst_name())
if (elab_as_eliminator(m_env, fn))
return true;
return false;
}
@ -2232,6 +2235,7 @@ expr nested_elaborate(environment & env, options const & opts, metavar_context &
void initialize_elaborator() {
g_elab_with_expected_type = new name("elab_with_expected_type");
g_elab_as_eliminator = new name("elab_as_eliminator");
g_level_prefix = new name("_elab_u");
register_trace_class("elaborator");
register_trace_class("elaborator_detail");
@ -2239,10 +2243,14 @@ void initialize_elaborator() {
register_system_attribute(basic_attribute(*g_elab_with_expected_type,
"instructs elaborator that the arguments of the function application (f ...) "
"should be elaborated using information about the expected type"));
register_system_attribute(basic_attribute(*g_elab_as_eliminator,
"instructs elaborator that the arguments of the function application (f ...) "
"should be elaborated as f were an eliminator"));
}
void finalize_elaborator() {
delete g_level_prefix;
delete g_elab_with_expected_type;
delete g_elab_as_eliminator;
}
}