From 5a48a2cebe7e375a8d5d78ca98dc9de281e0c3c0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Nov 2015 11:41:24 -0800 Subject: [PATCH] feat(library/app_builder): add mk_sorry method --- src/library/app_builder.cpp | 4 ++++ src/library/app_builder.h | 3 +++ src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/module.cpp | 1 + src/library/sorry.cpp | 13 +++++-------- src/library/sorry.h | 1 - 8 files changed, 19 insertions(+), 9 deletions(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index bcf4e7b53..b7a49263e 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -527,6 +527,10 @@ optional app_builder::mk_eq_drec(expr const & C, expr const & H1, expr con return m_ptr->mk_eq_drec(C, H1, H2); } +optional app_builder::mk_sorry(expr const & type) { + return mk_app(get_sorry_name(), type); +} + void app_builder::set_local_instances(list const & insts) { m_ptr->m_ctx->set_local_instances(insts); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 9e4922785..ac724e374 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -106,6 +106,9 @@ public: because eq.rec is a dependent eliminator in HoTT. */ optional mk_eq_drec(expr const & C, expr const & H1, expr const & H2); + /** \brief Create (@sorry type) */ + optional mk_sorry(expr const & type); + /** \brief Set the local instances. This method is relevant when we want to expose local class instances to the app_builder. diff --git a/src/library/constants.cpp b/src/library/constants.cpp index bdc6151e7..8aa7caed0 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -88,6 +88,7 @@ name const * g_rat_divide = nullptr; name const * g_rat_of_num = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; +name const * g_sorry = nullptr; name const * g_string = nullptr; name const * g_string_empty = nullptr; name const * g_string_str = nullptr; @@ -245,6 +246,7 @@ void initialize_constants() { g_rat_of_num = new name{"rat", "of_num"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; + g_sorry = new name{"sorry"}; g_string = new name{"string"}; g_string_empty = new name{"string", "empty"}; g_string_str = new name{"string", "str"}; @@ -403,6 +405,7 @@ void finalize_constants() { delete g_rat_of_num; delete g_sigma; delete g_sigma_mk; + delete g_sorry; delete g_string; delete g_string_empty; delete g_string_str; @@ -560,6 +563,7 @@ name const & get_rat_divide_name() { return *g_rat_divide; } name const & get_rat_of_num_name() { return *g_rat_of_num; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } +name const & get_sorry_name() { return *g_sorry; } name const & get_string_name() { return *g_string; } name const & get_string_empty_name() { return *g_string_empty; } name const & get_string_str_name() { return *g_string_str; } diff --git a/src/library/constants.h b/src/library/constants.h index 8aee4c4b5..bbbee7933 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -90,6 +90,7 @@ name const & get_rat_divide_name(); name const & get_rat_of_num_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); +name const & get_sorry_name(); name const & get_string_name(); name const & get_string_empty_name(); name const & get_string_str_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 1861c2d42..76cefda92 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -83,6 +83,7 @@ rat.divide rat.of_num sigma sigma.mk +sorry string string.empty string.str diff --git a/src/library/module.cpp b/src/library/module.cpp index 57f82f437..12dea2f38 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -25,6 +25,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/noncomputable.h" #include "library/sorry.h" +#include "library/constants.h" #include "library/kernel_serializer.h" #include "library/unfold_macros.h" #include "library/decl_stats.h" diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp index 269039601..34f211ffa 100644 --- a/src/library/sorry.cpp +++ b/src/library/sorry.cpp @@ -7,14 +7,13 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/environment.h" #include "library/module.h" +#include "library/constants.h" namespace lean { -static name * g_sorry_name = nullptr; static name * g_l = nullptr; static expr * g_sorry_type = nullptr; void initialize_sorry() { - g_sorry_name = new name("sorry"); g_l = new name("l"); g_sorry_type = new expr(mk_pi("A", mk_sort(mk_param_univ(*g_l)), mk_var(0), binder_info(true))); } @@ -22,25 +21,23 @@ void initialize_sorry() { void finalize_sorry() { delete g_sorry_type; delete g_l; - delete g_sorry_name; } bool has_sorry(environment const & env) { - auto decl = env.find(*g_sorry_name); + auto decl = env.find(get_sorry_name()); return decl && decl->get_type() == *g_sorry_type; } environment declare_sorry(environment const & env) { - if (auto decl = env.find(*g_sorry_name)) { + if (auto decl = env.find(get_sorry_name())) { if (decl->get_type() != *g_sorry_type) throw exception("failed to declare 'sorry', environment already has an object named 'sorry'"); return env; } else { - return module::add(env, check(env, mk_constant_assumption(*g_sorry_name, list(*g_l), *g_sorry_type))); + return module::add(env, check(env, mk_constant_assumption(get_sorry_name(), list(*g_l), *g_sorry_type))); } } -expr mk_sorry() { return mk_constant(*g_sorry_name); } -name const & get_sorry_name() { return *g_sorry_name; } +expr mk_sorry() { return mk_constant(get_sorry_name()); } bool is_sorry(expr const & e) { return is_constant(e) && const_name(e) == get_sorry_name(); } } diff --git a/src/library/sorry.h b/src/library/sorry.h index a3df99ab5..2fe904f06 100644 --- a/src/library/sorry.h +++ b/src/library/sorry.h @@ -17,7 +17,6 @@ environment declare_sorry(environment const & env); /** \brief Return the constant \c sorry */ expr mk_sorry(); -name const & get_sorry_name(); /** \brief Return true iff \c e is a sorry expression */ bool is_sorry(expr const & e); void initialize_sorry();