From fe6ab51c12f8da964ca1981e5234f6b60c1b2917 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Jun 2014 17:15:09 -0700 Subject: [PATCH] feat(kernel/inductive): add APIs for retrieving information about declared inductive datatypes, intro rules, and elimination rules The new API is important for implementing environment transformation procedures, and export Lean environment to different systems (e.g., Coq). Signed-off-by: Leonardo de Moura --- src/kernel/inductive/inductive.cpp | 63 ++++++++++++++++++++++++++---- src/kernel/inductive/inductive.h | 21 ++++++++++ 2 files changed, 76 insertions(+), 8 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index d2d1406e04..13ad57c4d7 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -98,13 +98,14 @@ static name g_tmp_prefix = name::mk_internal_unique_name(); /** \brief Environment extension used to store the computational rules associated with inductive datatype declarations. */ struct inductive_env_ext : public environment_extension { struct elim_info { + name m_inductive_name; // name of the inductive datatype associated with eliminator level_param_names m_level_names; // level parameter names used in computational rule unsigned m_num_params; // number of global parameters A unsigned m_num_ACe; // sum of number of global parameters A, type formers C, and minor preimises e. unsigned m_num_indices; // number of inductive datatype indices elim_info() {} - elim_info(level_param_names const & ls, unsigned num_ps, unsigned num_ACe, unsigned num_indices): - m_level_names(ls), m_num_params(num_ps), m_num_ACe(num_ACe), m_num_indices(num_indices) {} + elim_info(name const & id_name, level_param_names const & ls, unsigned num_ps, unsigned num_ACe, unsigned num_indices): + m_inductive_name(id_name), m_level_names(ls), m_num_params(num_ps), m_num_ACe(num_ACe), m_num_indices(num_indices) {} }; struct comp_rule { @@ -119,19 +120,33 @@ struct inductive_env_ext : public environment_extension { m_comp_rhs_body = binding_body(m_comp_rhs_body); } }; + // mapping from introduction rule name to computation rule data - rb_map m_elim_info; - rb_map m_comp_rules; + rb_map m_elim_info; + rb_map m_comp_rules; + // mapping from intro rule to datatype + rb_map m_intro_info; + rb_map m_inductive_info; inductive_env_ext() {} - void add_elim(name const & n, level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_indices) { - m_elim_info.insert(n, elim_info(ls, num_ps, num_ace, num_indices)); + void add_elim(name const & n, name const & id_name, level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_indices) { + m_elim_info.insert(n, elim_info(id_name, ls, num_ps, num_ace, num_indices)); } void add_comp_rhs(name const & n, name const & e, unsigned num_bu, expr const & rhs) { m_comp_rules.insert(n, comp_rule(e, num_bu, rhs)); } + + void add_intro_info(name const & ir_name, name const & id_name) { + m_intro_info.insert(ir_name, id_name); + } + + void add_inductive_info(level_param_names const & ps, unsigned num_params, list const & ds) { + inductive_decls decls(ps, num_params, ds); + for (auto const & d : ds) + m_inductive_info.insert(inductive_decl_name(d), decls); + } }; /** \brief Auxiliary object for registering the environment extension */ @@ -268,6 +283,9 @@ struct add_inductive_fn { for (auto d : m_decls) { m_env = m_env.add(check(m_env, mk_var_decl(inductive_decl_name(d), m_level_names, inductive_decl_type(d)))); } + inductive_env_ext ext(get_extension(m_env)); + ext.add_inductive_info(m_level_names, m_num_params, m_decls); + m_env = update(m_env, ext); updt_type_checker(); } @@ -406,10 +424,14 @@ struct add_inductive_fn { /** \brief Add all introduction rules (aka constructors) to environment. */ void declare_intro_rules() { + inductive_env_ext ext(get_extension(m_env)); for (auto d : m_decls) { - for (auto ir : inductive_decl_intros(d)) + for (auto ir : inductive_decl_intros(d)) { m_env = m_env.add(check(m_env, mk_var_decl(intro_rule_name(ir), m_level_names, intro_rule_type(ir)))); + ext.add_intro_info(intro_rule_name(ir), inductive_decl_name(d)); + } } + m_env = update(m_env, ext); updt_type_checker(); } @@ -656,7 +678,8 @@ struct add_inductive_fn { levels ls = get_elim_level_params(); inductive_env_ext ext(get_extension(m_env)); for (auto d : m_decls) { - ext.add_elim(get_elim_name(d), get_elim_level_param_names(), m_num_params, m_num_params + C.size() + e.size(), get_num_indices(d_idx)); + ext.add_elim(get_elim_name(d), inductive_decl_name(d), get_elim_level_param_names(), m_num_params, + m_num_params + C.size() + e.size(), get_num_indices(d_idx)); for (auto ir : inductive_decl_intros(d)) { buffer b; buffer u; @@ -775,5 +798,29 @@ optional inductive_normalizer_extension::operator()(expr const & e, extens r = instantiate_params(r, it1->m_level_names, const_levels(elim_fn)); return some_expr(r); } + +optional is_inductive_decl(environment const & env, name const & n) { + inductive_env_ext const & ext = get_extension(env); + if (auto it = ext.m_inductive_info.find(n)) + return optional(*it); + else + return optional(); +} + +optional is_intro_rule(environment const & env, name const & n) { + inductive_env_ext const & ext = get_extension(env); + if (auto it = ext.m_intro_info.find(n)) + return optional(*it); + else + return optional(); +} + +optional is_elim_rule(environment const & env, name const & n) { + inductive_env_ext const & ext = get_extension(env); + if (auto it = ext.m_elim_info.find(n)) + return optional(it->m_inductive_name); + else + return optional(); +} } } diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index dab2e60a8f..0721362363 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -40,5 +40,26 @@ environment add_inductive(environment env, level_param_names const & level_params, unsigned num_params, list const & decls); + +typedef std::tuple> inductive_decls; + +/** + \brief If \c n is the name of an inductive declaration in the environment \c env, then return the + list of all inductive decls that were simultaneously defined with \c n. + Return none otherwise +*/ +optional is_inductive_decl(environment const & env, name const & n); + +/** + \brief If \c n is the name of an introduction rule in \c env, then return the name of the inductive datatype D + s.t. \c n is an introduction rule of D. Otherwise, return none. +*/ +optional is_intro_rule(environment const & env, name const & n); + +/** + \brief If \c n is the name of an elimination rule in \c env, then return the name of the inductive datatype D + s.t. \c n is an elimination rule of D. Otherwise, return none. +*/ +optional is_elim_rule(environment const & env, name const & n); } }