From 9fdf2a3f55edddb9eaadb9b796393ad9da0766e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 03:43:45 -0800 Subject: [PATCH] feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules "Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip type checking when importing these files. TODO: add a check-sum. Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 32 +++++++++++++++++++++++++------- src/kernel/environment.h | 9 ++++++++- src/shell/lean.cpp | 12 ++++++++++-- 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 24efb1e0b..fe346455f 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "util/realpath.h" #include "util/sstream.h" #include "util/lean_path.h" +#include "util/flet.h" #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" #include "kernel/kernel_exception.h" @@ -355,10 +356,12 @@ void environment_cell::check_no_cached_type(expr const & e) { v is not convertible to \c t. */ void environment_cell::check_type(name const & n, expr const & t, expr const & v) { - m_type_checker->check_type(t); - expr v_t = m_type_checker->check(v); - if (!m_type_checker->is_convertible(v_t, t)) - throw def_type_mismatch_exception(env(), n, t, v, v_t); + if (m_type_check) { + m_type_checker->check_type(t); + expr v_t = m_type_checker->check(v); + if (!m_type_checker->is_convertible(v_t, t)) + throw def_type_mismatch_exception(env(), n, t, v, v_t); + } } /** \brief Throw exception if it is not a valid new definition */ @@ -407,7 +410,11 @@ void environment_cell::add_definition(name const & n, expr const & t, expr const void environment_cell::add_definition(name const & n, expr const & v, bool opaque) { check_no_cached_type(v); check_name(n); - expr v_t = m_type_checker->check(v); + expr v_t; + if (m_type_check) + v_t = m_type_checker->check(v); + else + v_t = m_type_checker->infer_type(v); unsigned w = get_max_weight(v) + 1; register_named_object(mk_definition(n, v_t, v, w)); if (opaque) @@ -434,7 +441,8 @@ void environment_cell::set_opaque(name const & n, bool opaque) { void environment_cell::add_axiom(name const & n, expr const & t) { check_no_cached_type(t); check_name(n); - m_type_checker->check_type(t); + if (m_type_check) + m_type_checker->check_type(t); register_named_object(mk_axiom(n, t)); } @@ -442,7 +450,8 @@ void environment_cell::add_axiom(name const & n, expr const & t) { void environment_cell::add_var(name const & n, expr const & t) { check_no_cached_type(t); check_name(n); - m_type_checker->check_type(t); + if (m_type_check) + m_type_checker->check_type(t); register_named_object(mk_var_decl(n, t)); } @@ -534,6 +543,10 @@ void environment_cell::import_builtin(char const * id, std::function fn) } } +void environment_cell::set_trusted_imported(bool flag) { + m_trust_imported = flag; +} + static char const * g_olean_header = "oleanfile"; static char const * g_olean_end_file = "EndFile"; void environment_cell::export_objects(std::string const & fname) { @@ -598,6 +611,7 @@ bool environment_cell::load_core(std::string const & fname, io_state const & ios } bool environment_cell::import(std::string const & fname, io_state const & ios) { + flet set(m_type_check, !m_trust_imported); return load_core(realpath(find_file(fname, {".olean"}).c_str()), ios, optional(fname)); } @@ -607,12 +621,16 @@ void environment_cell::load(std::string const & fname, io_state const & ios) { environment_cell::environment_cell(): m_num_children(0) { + m_trust_imported = false; + m_type_check = true; init_uvars(); } environment_cell::environment_cell(std::shared_ptr const & parent): m_num_children(0), m_parent(parent) { + m_trust_imported = false; + m_type_check = true; parent->inc_children(); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 73c4faf32..aa6af8251 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -43,7 +43,8 @@ class environment_cell { object_dictionary m_object_dictionary; std::unique_ptr m_type_checker; std::set m_imported_modules; // set of imported files and builtin modules - + bool m_trust_imported; // if true, then imported modules are not type checked. + bool m_type_check; // auxiliary flag used to implement m_trust_imported. std::vector> m_extensions; friend class environment_extension; @@ -324,6 +325,12 @@ public: void load(std::string const & fname, io_state const & ios); + /** + \brief When trusted_imported flag is true, the environment will + not type check imported modules. + */ + void set_trusted_imported(bool flag); + /** \brief Execute function \c fn. Any object created by \c fn is not exported by the environment. diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 75819f52d..e8c507d9c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -65,6 +65,7 @@ static void display_help(std::ostream & out) { std::cout << " --luahook=num -c how often the Lua interpreter checks the interrupted flag,\n"; std::cout << " it is useful for interrupting non-terminating user scripts,\n"; std::cout << " 0 means 'do not check'.\n"; + std::cout << " --trust -t trust imported modules\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -95,6 +96,7 @@ static struct option g_long_options[] = { {"luahook", required_argument, 0, 'c'}, {"githash", no_argument, 0, 'g'}, {"output", required_argument, 0, 'o'}, + {"trust", no_argument, 0, 't'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -105,12 +107,13 @@ int main(int argc, char ** argv) { try { lean::save_stack_info(); lean::register_modules(); - bool kernel_only = false; + bool kernel_only = false; bool export_objects = false; + bool trust_imported = false; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { - int c = getopt_long(argc, argv, "klupgvhc:012s:012o:", g_long_options, NULL); + int c = getopt_long(argc, argv, "tklupgvhc:012s:012o:", g_long_options, NULL); if (c == -1) break; // end of command line switch (c) { @@ -148,6 +151,9 @@ int main(int argc, char ** argv) { output = optarg; export_objects = true; break; + case 't': + trust_imported = true; + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -164,6 +170,7 @@ int main(int argc, char ** argv) { std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; #endif environment env; + env->set_trusted_imported(trust_imported); io_state ios; init_frontend(env, ios, kernel_only); script_state S; @@ -179,6 +186,7 @@ int main(int argc, char ** argv) { } } else { environment env; + env->set_trusted_imported(trust_imported); io_state ios; init_frontend(env, ios, kernel_only); script_state S;