From 9b9041fa2ed60573595d0d23bbddca65afcb87e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 May 2014 10:56:26 -0700 Subject: [PATCH] feat(kernel/environment): add method for adding declarations that were not type checked (if trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 9 +++++++++ src/kernel/environment.h | 24 ++++++++++++++++++++---- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index c55110c03..f2f3b8be5 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -75,6 +75,15 @@ declaration environment::get(name const & n) const { throw_kernel_exception(env, "invalid declaration, it was checked/certified in an incompatible environment"); } +environment environment::add(declaration const & d) const { + if (trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL) + throw_kernel_exception(*this, "environment trust level does not allow users to add declarations that were not type checked"); + name const & n = d.get_name(); + if (find(n)) + throw_already_declared(*this, n); + return environment(m_header, m_id, insert(m_declarations, n, d), m_global_levels, m_extensions); +} + environment environment::add(certified_declaration const & d) const { if (!m_id.is_descendant(d.get_id())) throw_incompatible_environment(*this); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 11bd09bdb..c41e4ae9c 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -17,6 +17,12 @@ Author: Leonardo de Moura #include "kernel/constraint.h" #include "kernel/declaration.h" +#ifndef LEAN_BELIEVER_TRUST_LEVEL +// If an environment E is created with a trust level > LEAN_BELIEVER_TRUST_LEVEL, then +// we can add declarations to E without type checking them. +#define LEAN_BELIEVER_TRUST_LEVEL 1024 +#endif + namespace lean { class type_checker; class environment; @@ -40,11 +46,11 @@ public: */ class environment_header { /* In the following field, 0 means untrusted mode (i.e., check everything), - >= 1 means do not check imported modules, and do not check macros - with level less than the value of this field. + higher level allow us to trust the implementation of macros, and even + allow us to add declarations without type checking them (e.g., m_trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) */ - unsigned m_trust_lvl; //!the given one. - bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Bool/Type (aka Type(0)) + unsigned m_trust_lvl; + bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Bool/Type (aka Type.{0}) bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool. list m_cls_proof_irrel; //!< list of proof irrelevant classes, if we want Id types to be proof irrelevant, we the name 'Id' in this list. @@ -163,6 +169,16 @@ public: */ environment add(certified_declaration const & d) const; + /** + \brief Adds a declaration that was not type checked. This method throws an excetion if + trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL. + It is mainly when importing pre-compiled .olean files, and trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL. + + \remark If trust_lvl() == 0, then this method will always throw an exception. No matter what is + the value of LEAN_BELIEVER_TRUST_LEVEL used to compile Lean. + */ + environment add(declaration const & d) const; + /** \brief Replace the axiom with name t.get_declaration().get_name() with the theorem t.get_declaration(). This method throws an exception if: