From 358074ae3df65fced807cbc131ef109fbe18121c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Sep 2014 09:16:03 -0700 Subject: [PATCH] refactor(kernel/record): remove kernel extension for records, we will implement it outside of the kernel on top of the inductive datatypes --- src/CMakeLists.txt | 2 - src/frontends/lean/structure_cmd.cpp | 5 +-- src/kernel/record/CMakeLists.txt | 2 - src/kernel/record/record.cpp | 66 ---------------------------- src/kernel/record/record.h | 57 ------------------------ src/library/standard_kernel.cpp | 7 +-- 6 files changed, 3 insertions(+), 136 deletions(-) delete mode 100644 src/kernel/record/CMakeLists.txt delete mode 100644 src/kernel/record/record.cpp delete mode 100644 src/kernel/record/record.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ddae504de..7c3ce4ccb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -250,8 +250,6 @@ add_subdirectory(kernel) set(LEAN_LIBS ${LEAN_LIBS} kernel) add_subdirectory(kernel/inductive) set(LEAN_LIBS ${LEAN_LIBS} inductive) -add_subdirectory(kernel/record) -set(LEAN_LIBS ${LEAN_LIBS} record) add_subdirectory(library) set(LEAN_LIBS ${LEAN_LIBS} library) add_subdirectory(library/tactic) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index abd6a7cb0..5dedfd776 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/replace_fn.h" -#include "kernel/record/record.h" #include "library/scoped_ext.h" #include "library/placeholder.h" #include "library/locals.h" @@ -280,9 +279,7 @@ struct structure_cmd_fn { level r_lvl = mk_result_level(m_env, r_lvls); m_type = update_result_sort(m_type, r_lvl); } - m_env = record::add_record(m_p.env(), to_list(m_level_names.begin(), m_level_names.end()), m_name, m_type, - m_mk, intro_type); - // TODO(Leo): create aliases, declare notation, create to_parent methods. + // TODO(Leo): create record, aliases, declare notation, create to_parent methods. return m_env; } }; diff --git a/src/kernel/record/CMakeLists.txt b/src/kernel/record/CMakeLists.txt deleted file mode 100644 index c64a45e47..000000000 --- a/src/kernel/record/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_library(record record.cpp) -target_link_libraries(record ${LEAN_LIBS}) diff --git a/src/kernel/record/record.cpp b/src/kernel/record/record.cpp deleted file mode 100644 index 4343929da..000000000 --- a/src/kernel/record/record.cpp +++ /dev/null @@ -1,66 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "kernel/type_checker.h" -#include "kernel/record/record.h" - -namespace lean { namespace record { -static name g_tmp_prefix = name::mk_internal_unique_name(); - -/** \brief Environment extension used to store record information */ -struct record_env_ext : public environment_extension { - struct record_info { - list m_fields; - }; - - // mapping from introduction rule name to computation rule data - rb_map m_record_info; - record_env_ext() {} -}; - -/** \brief Helper functional object for processing record declarations. */ -struct add_record_fn { - typedef std::unique_ptr type_checker_ptr; - environment m_env; - name_generator m_ngen; - type_checker_ptr m_tc; - level_param_names const & m_level_params; - name const & m_record_name; - expr const & m_record_type; - name const & m_intro_name; - expr const & m_intro_type; - add_record_fn(environment const & env, level_param_names const & level_params, name const & rec_name, expr const & rec_type, - name const & intro_name, expr const & intro_type): - m_env(env), m_ngen(g_tmp_prefix), m_tc(new type_checker(m_env)), - m_level_params(level_params), m_record_name(rec_name), m_record_type(rec_type), - m_intro_name(intro_name), m_intro_type(intro_type) {} - - environment operator()() { - // TODO(Leo): - std::cout << m_record_name << " : " << m_record_type << "\n"; - std::cout << " >> " << m_intro_name << " : " << m_intro_type << "\n"; - return m_env; - } -}; - -environment add_record(environment const & env, level_param_names const & level_params, name const & rec_name, expr const & rec_type, - name const & intro_name, expr const & intro_type) { - return add_record_fn(env, level_params, rec_name, rec_type, intro_name, intro_type)(); -} - -optional> record_normalizer_extension::operator()(expr const &, extension_context &) const { - return none_ecs(); -} - -bool record_normalizer_extension::may_reduce_later(expr const &, extension_context &) const { - return false; -} - -bool record_normalizer_extension::supports(name const &) const { - return false; -} -}} diff --git a/src/kernel/record/record.h b/src/kernel/record/record.h deleted file mode 100644 index 46e4d6c72..000000000 --- a/src/kernel/record/record.h +++ /dev/null @@ -1,57 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "util/list.h" -#include "util/optional.h" -#include "kernel/environment.h" - -namespace lean { namespace record { -typedef pair field; -inline name const & field_name(field const & f) { return f.first; } -inline expr const & field_type(field const & f) { return f.second; } - -/** \brief Declare a record type. */ -environment add_record(environment const & env, - level_param_names const & level_params, - name const & rec_name, - expr const & rec_type, - name const & intro_name, - expr const & intro_type); - -/** \brief Normalizer extension for applying record computational rules. */ -class record_normalizer_extension : public normalizer_extension { -public: - virtual optional> operator()(expr const & e, extension_context & ctx) const; - virtual bool may_reduce_later(expr const & e, extension_context & ctx) const; - virtual bool supports(name const & feature) const; -}; - -/** \brief If \c n is the name of a record in the environment \c env, then return the - list of all fields. Return none otherwise -*/ -optional> is_record(environment const & env, name const & n); - -/** \brief If \c n is the name of a record's field in \c env, then return the name of the record type - associated with it. -*/ -optional is_field(environment const & env, name const & n); - -/** \brief If \c n is the name of an introduction rule for a record in \c env, then return the name of the record type - associated with it. -*/ -optional is_intro_rule(environment const & env, name const & n); - -/** \brief If \c n is the name of an elimination rule for a record in \c env, then return the name of the record type - associated with it. -*/ -optional is_elim_rule(environment const & env, name const & n); - -/** \brief Given the eliminator \c n, this function return the position of major premise */ -optional get_elim_major_idx(environment const & env, name const & n); -}} diff --git a/src/library/standard_kernel.cpp b/src/library/standard_kernel.cpp index da4d1fdae..ad80b25fb 100644 --- a/src/library/standard_kernel.cpp +++ b/src/library/standard_kernel.cpp @@ -5,12 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/inductive/inductive.h" -#include "kernel/record/record.h" #include "library/inductive_unifier_plugin.h" namespace lean { using inductive::inductive_normalizer_extension; -using record::record_normalizer_extension; /** \brief Create standard Lean environment */ environment mk_environment(unsigned trust_lvl) { @@ -18,9 +16,8 @@ environment mk_environment(unsigned trust_lvl) { true /* Type.{0} is proof irrelevant */, true /* Eta */, true /* Type.{0} is impredicative */, - /* builtin support for inductive and record datatypes */ - compose(std::unique_ptr(new inductive_normalizer_extension()), - std::unique_ptr(new record_normalizer_extension()))); + /* builtin support for inductive */ + std::unique_ptr(new inductive_normalizer_extension())); return set_unifier_plugin(env, mk_inductive_unifier_plugin()); } }