From b1ee888aae352d7b4ab9ff8f0a3ae76a89c60079 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Sep 2014 10:27:48 -0700 Subject: [PATCH] refactor(*): start move to explicit initialization/finalization, explicitly initialize/finalize options Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 + src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 18 +++- src/frontends/lean/elaborator.h | 2 + src/frontends/lean/init_module.cpp | 22 ++++ src/frontends/lean/init_module.h | 12 +++ src/frontends/lean/parser.cpp | 29 ++++-- src/frontends/lean/parser.h | 3 + src/frontends/lean/pp_options.cpp | 133 +++++++++++++++---------- src/frontends/lean/pp_options.h | 3 + src/init/CMakeLists.txt | 3 + src/init/init.cpp | 34 +++++++ src/init/init.h | 18 ++++ src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 17 ++++ src/library/init_module.h | 12 +++ src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 17 ++++ src/library/tactic/init_module.h | 12 +++ src/library/tactic/proof_state.cpp | 19 +++- src/library/tactic/proof_state.h | 3 + src/library/unifier.cpp | 41 ++++++-- src/library/unifier.h | 3 + src/shell/lean.cpp | 2 + src/tests/util/format.cpp | 3 + src/tests/util/options.cpp | 9 +- src/tests/util/sexpr.cpp | 3 + src/util/sexpr/CMakeLists.txt | 4 +- src/util/sexpr/format.cpp | 42 +++++--- src/util/sexpr/format.h | 3 + src/util/sexpr/init_module.cpp | 23 +++++ src/util/sexpr/init_module.h | 12 +++ src/util/sexpr/option_declarations.cpp | 18 ++++ src/util/sexpr/option_declarations.h | 5 + src/util/sexpr/options.cpp | 30 +++--- src/util/sexpr/options.h | 3 + 36 files changed, 452 insertions(+), 114 deletions(-) create mode 100644 src/frontends/lean/init_module.cpp create mode 100644 src/frontends/lean/init_module.h create mode 100644 src/init/CMakeLists.txt create mode 100644 src/init/init.cpp create mode 100644 src/init/init.h create mode 100644 src/library/init_module.cpp create mode 100644 src/library/init_module.h create mode 100644 src/library/tactic/init_module.cpp create mode 100644 src/library/tactic/init_module.h create mode 100644 src/util/sexpr/init_module.cpp create mode 100644 src/util/sexpr/init_module.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3b93af89d..ddae504de 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -262,6 +262,8 @@ add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) add_subdirectory(frontends/lua) set(LEAN_LIBS ${LEAN_LIBS} leanlua) +add_subdirectory(init) +set(LEAN_LIBS ${LEAN_LIBS} init) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}") if(("${MULTI_THREAD}" MATCHES "ON") AND (NOT (("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") AND ("${BOOST}" MATCHES "ON")))) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 8747c56c3..efaa9f8e8 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,6 +7,6 @@ dependencies.cpp parser_bindings.cpp begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp -coercion_elaborator.cpp proof_qed_elaborator.cpp) +coercion_elaborator.cpp proof_qed_elaborator.cpp init_module.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b87307aae..7a98ce354 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/lazy_list_fn.h" #include "util/sstream.h" #include "util/name_map.h" +#include "util/sexpr/option_declarations.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" @@ -54,10 +55,21 @@ Author: Leonardo de Moura namespace lean { // ========================================== // elaborator configuration options -static name g_elaborator_local_instances{"elaborator", "local_instances"}; -RegisterBoolOption(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances"); +static name * g_elaborator_local_instances = nullptr; + +void initialize_elaborator() { + g_elaborator_local_instances = new name{"elaborator", "local_instances"}; + + register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, + "(lean elaborator) use local declarates as class instances"); +} + +void finalize_elaborator() { + delete g_elaborator_local_instances; +} + bool get_elaborator_local_instances(options const & opts) { - return opts.get_bool(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES); + return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES); } // ========================================== diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index f0b71480b..0e4de6c4e 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -36,4 +36,6 @@ std::tuple elaborate(elaborator_context & env, list elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v, bool is_opaque); +void initialize_elaborator(); +void finalize_elaborator(); } diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp new file mode 100644 index 000000000..570d0c59e --- /dev/null +++ b/src/frontends/lean/init_module.cpp @@ -0,0 +1,22 @@ +/* +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 "frontends/lean/elaborator.h" +#include "frontends/lean/pp_options.h" +#include "frontends/lean/parser.h" + +namespace lean { +void initialize_frontend_lean_module() { + initialize_elaborator(); + initialize_pp_options(); + initialize_parser(); +} +void finalize_frontend_lean_module() { + finalize_parser(); + finalize_pp_options(); + finalize_elaborator(); +} +} diff --git a/src/frontends/lean/init_module.h b/src/frontends/lean/init_module.h new file mode 100644 index 000000000..fa1714a7c --- /dev/null +++ b/src/frontends/lean/init_module.h @@ -0,0 +1,12 @@ +/* +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 + +namespace lean { +void initialize_frontend_lean_module(); +void finalize_frontend_lean_module(); +} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 2211ec1a3..6a3b08437 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/flet.h" #include "util/lean_path.h" +#include "util/sexpr/option_declarations.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" #include "kernel/abstract.h" @@ -51,14 +52,30 @@ Author: Leonardo de Moura namespace lean { // ========================================== // Parser configuration options -static name g_parser_show_errors {"parser", "show_errors"}; -static name g_parser_parallel_import {"parser", "parallel_import"}; +static name * g_parser_show_errors; +static name * g_parser_parallel_import; -RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel"); -RegisterBoolOption(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT, "(lean parser) import modules in parallel"); +void initialize_parser() { + g_parser_show_errors = new name{"parser", "show_errors"}; + g_parser_parallel_import = new name{"parser", "parallel_import"}; + register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, + "(lean parser) display error messages in the regular output channel"); + register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT, + "(lean parser) import modules in parallel"); +} -bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); } -bool get_parser_parallel_import(options const & opts) { return opts.get_bool(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT); } +void finalize_parser() { + delete g_parser_show_errors; + delete g_parser_parallel_import; +} + +bool get_parser_show_errors(options const & opts) { + return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); +} + +bool get_parser_parallel_import(options const & opts) { + return opts.get_bool(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT); +} // ========================================== parser::local_scope::local_scope(parser & p): diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 0318f8ff0..d8e399e62 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -355,4 +355,7 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c declaration_index * index = nullptr); bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr); + +void initialize_parser(); +void finalize_parser(); } diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 0fd1f6813..b76839ee5 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sexpr/option_declarations.h" #include "frontends/lean/pp_options.h" #ifndef LEAN_DEFAULT_PP_MAX_DEPTH @@ -47,61 +48,87 @@ Author: Leonardo de Moura #endif namespace lean { -static name g_pp_max_depth {"pp", "max_depth"}; -static name g_pp_max_steps {"pp", "max_steps"}; -static name g_pp_notation {"pp", "notation"}; -static name g_pp_implicit {"pp", "implicit"}; -static name g_pp_coercions {"pp", "coercions"}; -static name g_pp_universes {"pp", "universes"}; -static name g_pp_full_names {"pp", "full_names"}; -static name g_pp_private_names {"pp", "private_names"}; -static name g_pp_metavar_args {"pp", "metavar_args"}; -static name g_pp_beta {"pp", "beta"}; +static name * g_pp_max_depth = nullptr; +static name * g_pp_max_steps = nullptr; +static name * g_pp_notation = nullptr; +static name * g_pp_implicit = nullptr; +static name * g_pp_coercions = nullptr; +static name * g_pp_universes = nullptr; +static name * g_pp_full_names = nullptr; +static name * g_pp_private_names = nullptr; +static name * g_pp_metavar_args = nullptr; +static name * g_pp_beta = nullptr; +static list * g_distinguishing_pp_options = nullptr; -name const & get_pp_coercions_option_name() { return g_pp_coercions; } -name const & get_pp_full_names_option_name() { return g_pp_full_names; } +void initialize_pp_options() { + g_pp_max_depth = new name{"pp", "max_depth"}; + g_pp_max_steps = new name{"pp", "max_steps"}; + g_pp_notation = new name{"pp", "notation"}; + g_pp_implicit = new name{"pp", "implicit"}; + g_pp_coercions = new name{"pp", "coercions"}; + g_pp_universes = new name{"pp", "universes"}; + g_pp_full_names = new name{"pp", "full_names"}; + g_pp_private_names = new name{"pp", "private_names"}; + g_pp_metavar_args = new name{"pp", "metavar_args"}; + g_pp_beta = new name{"pp", "beta"}; + register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, + "(pretty printer) maximum expression depth, after that it will use ellipsis"); + register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, + "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"); + register_bool_option(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION, + "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); + register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, + "(pretty printer) display implicit parameters"); + register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS, + "(pretty printer) display coercionss"); + register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES, + "(pretty printer) display universes"); + register_bool_option(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES, + "(pretty printer) display fully qualified names"); + register_bool_option(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES, + "(pretty printer) display internal names assigned to private declarations"); + register_bool_option(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS, + "(pretty printer) display metavariable arguments"); + register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA, + "(pretty printer) apply beta-reduction when pretty printing"); -list const & get_distinguishing_pp_options() { - static options g_universes_true(g_pp_universes, true); - static options g_implicit_true(g_pp_implicit, true); - static options g_coercions_true(g_pp_coercions, true); - static options g_notation_false(g_pp_notation, false); - static options g_implicit_coercions = join(g_coercions_true, g_implicit_true); - static options g_implicit_notation = join(g_notation_false, g_implicit_true); - static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercions_true, g_notation_false)); - static list g_distinguishing_pp_options({g_implicit_true, g_coercions_true, g_implicit_coercions, g_implicit_notation, g_universes_true, g_all}); - return g_distinguishing_pp_options; + options universes_true(*g_pp_universes, true); + options implicit_true(*g_pp_implicit, true); + options coercions_true(*g_pp_coercions, true); + options notation_false(*g_pp_notation, false); + options implicit_coercions = join(coercions_true, implicit_true); + options implicit_notation = join(notation_false, implicit_true); + options all = join(join(universes_true, implicit_true), join(coercions_true, notation_false)); + g_distinguishing_pp_options = new list({implicit_true, coercions_true, implicit_coercions, + implicit_notation, universes_true, all}); } -RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, - "(pretty printer) maximum expression depth, after that it will use ellipsis"); -RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, - "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"); -RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, - "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); -RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, - "(pretty printer) display implicit parameters"); -RegisterBoolOption(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS, - "(pretty printer) display coercionss"); -RegisterBoolOption(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES, - "(pretty printer) display universes"); -RegisterBoolOption(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES, - "(pretty printer) display fully qualified names"); -RegisterBoolOption(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES, - "(pretty printer) display internal names assigned to private declarations"); -RegisterBoolOption(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS, - "(pretty printer) display metavariable arguments"); -RegisterBoolOption(g_pp_beta, LEAN_DEFAULT_PP_BETA, - "(pretty printer) apply beta-reduction when pretty printing"); - -unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } -unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } -bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } -bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } -bool get_pp_coercions(options const & opts) { return opts.get_bool(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); } -bool get_pp_universes(options const & opts) { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } -bool get_pp_full_names(options const & opts) { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); } -bool get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } -bool get_pp_metavar_args(options const & opts) { return opts.get_bool(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); } -bool get_pp_beta(options const & opts) { return opts.get_bool(g_pp_beta, LEAN_DEFAULT_PP_BETA); } +void finalize_pp_options() { + delete g_pp_max_depth; + delete g_pp_max_steps; + delete g_pp_notation; + delete g_pp_implicit; + delete g_pp_coercions; + delete g_pp_universes; + delete g_pp_full_names; + delete g_pp_private_names; + delete g_pp_metavar_args; + delete g_pp_beta; + delete g_distinguishing_pp_options; +} + +name const & get_pp_coercions_option_name() { return *g_pp_coercions; } +name const & get_pp_full_names_option_name() { return *g_pp_full_names; } + +unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } +unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } +bool get_pp_notation(options const & opts) { return opts.get_bool(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } +bool get_pp_implicit(options const & opts) { return opts.get_bool(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } +bool get_pp_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); } +bool get_pp_universes(options const & opts) { return opts.get_bool(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } +bool get_pp_full_names(options const & opts) { return opts.get_bool(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); } +bool get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } +bool get_pp_metavar_args(options const & opts) { return opts.get_bool(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); } +bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } +list const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; } } diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index 8bfe661d7..1c118ed84 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -21,4 +21,7 @@ bool get_pp_private_names(options const & opts); bool get_pp_metavar_args(options const & opts); bool get_pp_beta(options const & opts); list const & get_distinguishing_pp_options(); + +void initialize_pp_options(); +void finalize_pp_options(); } diff --git a/src/init/CMakeLists.txt b/src/init/CMakeLists.txt new file mode 100644 index 000000000..cfd1dd399 --- /dev/null +++ b/src/init/CMakeLists.txt @@ -0,0 +1,3 @@ +add_library(init init.cpp) + +target_link_libraries(init ${LEAN_LIBS}) diff --git a/src/init/init.cpp b/src/init/init.cpp new file mode 100644 index 000000000..023e30751 --- /dev/null +++ b/src/init/init.cpp @@ -0,0 +1,34 @@ +/* +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 "util/sexpr/init_module.h" +#include "library/init_module.h" +#include "library/tactic/init_module.h" +#include "frontends/lean/init_module.h" +#include "init/init.h" + +namespace lean { +void initialize() { + initialize_sexpr_module(); + initialize_library_module(); + initialize_tactic_module(); + initialize_frontend_lean_module(); +} +void finalize() { + finalize_frontend_lean_module(); + finalize_tactic_module(); + finalize_library_module(); + finalize_sexpr_module(); +} + +initializer::initializer() { + initialize(); +} + +initializer::~initializer() { + finalize(); +} +} diff --git a/src/init/init.h b/src/init/init.h new file mode 100644 index 000000000..6b4df266d --- /dev/null +++ b/src/init/init.h @@ -0,0 +1,18 @@ +/* +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 + +namespace lean { +void initialize(); +void finalize(); +/** \brief Helper object for initializing Lean */ +class initializer { +public: + initializer(); + ~initializer(); +}; +} diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 41c1681ce..fbb4205a0 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -9,6 +9,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp explicit.cpp num.cpp string.cpp head_map.cpp match.cpp definition_cache.cpp declaration_index.cpp print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp - protected.cpp metavar_closure.cpp reducible.cpp) + protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp new file mode 100644 index 000000000..42066ad8c --- /dev/null +++ b/src/library/init_module.cpp @@ -0,0 +1,17 @@ +/* +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 "library/unifier.h" + +namespace lean { +void initialize_library_module() { + initialize_unifier(); +} + +void finalize_library_module() { + finalize_unifier(); +} +} diff --git a/src/library/init_module.h b/src/library/init_module.h new file mode 100644 index 000000000..78e228b70 --- /dev/null +++ b/src/library/init_module.h @@ -0,0 +1,12 @@ +/* +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 + +namespace lean { +void initialize_library_module(); +void finalize_library_module(); +} diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 814dc03d2..c3a30ae23 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp -expr_to_tactic.cpp) +expr_to_tactic.cpp init_module.cpp) # simplify_tactic.cpp) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp new file mode 100644 index 000000000..b41b935f7 --- /dev/null +++ b/src/library/tactic/init_module.cpp @@ -0,0 +1,17 @@ +/* +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/tactic/proof_state.h" + +namespace lean { +void initialize_tactic_module() { + initialize_proof_state(); +} + +void finalize_tactic_module() { + finalize_proof_state(); +} +} diff --git a/src/library/tactic/init_module.h b/src/library/tactic/init_module.h new file mode 100644 index 000000000..4051777de --- /dev/null +++ b/src/library/tactic/init_module.h @@ -0,0 +1,12 @@ +/* +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 + +namespace lean { +void initialize_tactic_module(); +void finalize_tactic_module(); +} diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 08435238d..186feb576 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "util/interrupt.h" +#include "util/sexpr/option_declarations.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -23,9 +24,21 @@ Author: Leonardo de Moura #endif namespace lean { -static name g_proof_state_goal_names {"tactic", "goal_names"}; -RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state"); -bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } +static name * g_proof_state_goal_names = nullptr; + +void initialize_proof_state() { + g_proof_state_goal_names = new name{"tactic", "goal_names"}; + register_bool_option(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, + "(tactic) display goal names when pretty printing proof state"); +} + +void finalize_proof_state() { + delete g_proof_state_goal_names; +} + +bool get_proof_state_goal_names(options const & opts) { + return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); +} format proof_state::pp(formatter const & fmt) const { options const & opts = fmt.get_options(); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index b23ef934c..3ecad84e3 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -46,4 +46,7 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons UDATA_DEFS_CORE(goals) UDATA_DEFS(proof_state) void open_proof_state(lua_State * L); + +void initialize_proof_state(); +void finalize_proof_state(); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 2ec6d511b..32a385a38 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/lbool.h" #include "util/flet.h" +#include "util/sexpr/option_declarations.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" @@ -42,20 +43,38 @@ Author: Leonardo de Moura #endif namespace lean { -static name g_unifier_max_steps {"unifier", "max_steps"}; -RegisterUnsignedOption(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); -unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); } +static name * g_unifier_max_steps = nullptr; +static name * g_unifier_computation = nullptr; +static name * g_unifier_expensive_classes = nullptr; -static name g_unifier_computation {"unifier", "computation"}; -RegisterBoolOption(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION, - "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints"); -bool get_unifier_computation(options const & opts) { return opts.get_bool(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION); } +void initialize_unifier() { + g_unifier_max_steps = new name{"unifier", "max_steps"}; + g_unifier_computation = new name{"unifier", "computation"}; + g_unifier_expensive_classes = new name{"unifier", "expensive_classes"}; + + register_unsigned_option(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); + register_bool_option(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION, + "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints"); + register_bool_option(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES, + "(unifier) use \"full\" higher-order unification when solving class instances"); +} + +void finalize_unifier() { + delete g_unifier_max_steps; + delete g_unifier_computation; + delete g_unifier_expensive_classes; +} + +unsigned get_unifier_max_steps(options const & opts) { + return opts.get_unsigned(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); +} + +bool get_unifier_computation(options const & opts) { + return opts.get_bool(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION); +} -static name g_unifier_expensive_classes {"unifier", "expensive_classes"}; -RegisterBoolOption(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES, - "(unifier) use \"full\" higher-order unification when solving class instances"); bool get_unifier_expensive_classes(options const & opts) { - return opts.get_bool(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES); + return opts.get_bool(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES); } unifier_config::unifier_config(bool use_exceptions, bool discard): diff --git a/src/library/unifier.h b/src/library/unifier.h index ccdddbfe2..6c31c74b4 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -95,4 +95,7 @@ public: }; void open_unifier(lua_State * L); + +void initialize_unifier(); +void finalize_unifier(); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 059960bf6..fccd0b4bb 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -35,6 +35,7 @@ Author: Leonardo de Moura #include "frontends/lean/server.h" #include "frontends/lean/dependencies.h" #include "frontends/lua/register_modules.h" +#include "init/init.h" #include "version.h" #include "githash.h" // NOLINT @@ -197,6 +198,7 @@ int main(int argc, char ** argv) { lean::save_stack_info(); lean::init_default_print_fn(); lean::register_modules(); + lean::initializer init; bool export_objects = false; unsigned trust_lvl = 0; bool server = false; diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp index b57581d19..548bb4dd4 100644 --- a/src/tests/util/format.cpp +++ b/src/tests/util/format.cpp @@ -14,6 +14,7 @@ Author: Soonho Kong #include "util/sexpr/format.h" #include "util/sexpr/sexpr_fn.h" #include "util/sexpr/options.h" +#include "util/sexpr/init_module.h" using namespace lean; using std::cout; @@ -126,11 +127,13 @@ static void tst6() { int main() { save_stack_info(); + initialize_sexpr_module(); tst1(); tst2(); tst3(); tst4(); tst5(); tst6(); + finalize_sexpr_module(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp index b56f8e3b1..f6b0fd603 100644 --- a/src/tests/util/options.cpp +++ b/src/tests/util/options.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/sexpr/options.h" #include "util/sexpr/option_declarations.h" +#include "util/sexpr/init_module.h" using namespace lean; static void tst1() { @@ -128,8 +129,6 @@ static void tst4() { lean_assert(s.str() == "Bool Int Unsigned Int Double String S-Expression"); } -RegisterBoolOption("fakeopt", false, "fake option"); - static void tst5() { option_declarations const & decls = get_option_declarations(); auto it = decls.find("fakeopt"); @@ -156,11 +155,17 @@ static void tst6() { int main() { save_stack_info(); + initialize_sexpr_module(); + name fakeopt("fakeopt"); + register_bool_option(fakeopt, false, "fake option"); + tst1(); tst2(); tst3(); tst4(); tst5(); tst6(); + + finalize_sexpr_module(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp index 562b51f13..2c7608b40 100644 --- a/src/tests/util/sexpr.cpp +++ b/src/tests/util/sexpr.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/sexpr/sexpr_fn.h" #include "util/sexpr/format.h" #include "util/sexpr/options.h" +#include "util/sexpr/init_module.h" using namespace lean; static void tst1() { @@ -239,6 +240,7 @@ static void tst10() { int main() { save_stack_info(); + initialize_sexpr_module(); tst1(); tst2(); tst3(); @@ -249,5 +251,6 @@ int main() { tst8(); tst9(); tst10(); + finalize_sexpr_module(); return has_violations() ? 1 : 0; } diff --git a/src/util/sexpr/CMakeLists.txt b/src/util/sexpr/CMakeLists.txt index d99b33f16..a323bb190 100644 --- a/src/util/sexpr/CMakeLists.txt +++ b/src/util/sexpr/CMakeLists.txt @@ -1,2 +1,4 @@ -add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp option_declarations.cpp) +add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp + option_declarations.cpp init_module.cpp) + target_link_libraries(sexpr ${LEAN_LIBS}) diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 52a3967bf..895d890c6 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -18,6 +18,7 @@ #include "util/sexpr/format.h" #include "util/sexpr/sexpr_fn.h" #include "util/sexpr/options.h" +#include "util/sexpr/option_declarations.h" #ifndef LEAN_DEFAULT_PP_INDENTATION #define LEAN_DEFAULT_PP_INDENTATION 2 @@ -48,32 +49,41 @@ #endif namespace lean { -static name g_pp_indent{"pp", "indent"}; -static name g_pp_unicode{"pp", "unicode"}; -static name g_pp_colors{"pp", "colors"}; -static name g_pp_width{"pp", "width"}; +static name * g_pp_indent = nullptr; +static name * g_pp_unicode = nullptr; +static name * g_pp_colors = nullptr; +static name * g_pp_width = nullptr; -RegisterUnsignedOption(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation"); -RegisterBoolOption(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters"); -RegisterBoolOption(g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors"); -RegisterUnsignedOption(g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width"); +void initialize_format() { + g_pp_indent = new name{"pp", "indent"}; + g_pp_unicode = new name{"pp", "unicode"}; + g_pp_colors = new name{"pp", "colors"}; + g_pp_width = new name{"pp", "width"}; + register_unsigned_option(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation"); + register_bool_option(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters"); + register_bool_option(*g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors"); + register_unsigned_option(*g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width"); +} + +void finalize_format() { + delete g_pp_indent; + delete g_pp_unicode; + delete g_pp_colors; + delete g_pp_width; +} unsigned get_pp_indent(options const & o) { - return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION); + return o.get_unsigned(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION); } - bool get_pp_unicode(options const & o) { - return o.get_bool(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE); + return o.get_bool(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE); } - bool get_pp_colors(options const & o) { - return o.get_bool(g_pp_colors, LEAN_DEFAULT_PP_COLORS); + return o.get_bool(*g_pp_colors, LEAN_DEFAULT_PP_COLORS); } - unsigned get_pp_width(options const & o) { - return o.get_unsigned(g_pp_width, LEAN_DEFAULT_PP_WIDTH); + return o.get_unsigned(*g_pp_width, LEAN_DEFAULT_PP_WIDTH); } - format compose(format const & f1, format const & f2) { return format(format::sexpr_compose({f1.m_value, f2.m_value})); } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index e0d2d6366..7fcd0c1c0 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -323,4 +323,7 @@ bool format_pp_eq(format const & f1, format const & f2, options const & o); UDATA_DEFS(format) void open_format(lua_State * L); + +void initialize_format(); +void finalize_format(); } diff --git a/src/util/sexpr/init_module.cpp b/src/util/sexpr/init_module.cpp new file mode 100644 index 000000000..a10d7ba12 --- /dev/null +++ b/src/util/sexpr/init_module.cpp @@ -0,0 +1,23 @@ +/* +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 "util/sexpr/option_declarations.h" +#include "util/sexpr/options.h" +#include "util/sexpr/format.h" + +namespace lean { +void initialize_sexpr_module() { + initialize_option_declarations(); + initialize_options(); + initialize_format(); +} + +void finalize_sexpr_module() { + finalize_format(); + finalize_options(); + finalize_option_declarations(); +} +} diff --git a/src/util/sexpr/init_module.h b/src/util/sexpr/init_module.h new file mode 100644 index 000000000..185ff4ac2 --- /dev/null +++ b/src/util/sexpr/init_module.h @@ -0,0 +1,12 @@ +/* +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 + +namespace lean { +void initialize_sexpr_module(); +void finalize_sexpr_module(); +} diff --git a/src/util/sexpr/option_declarations.cpp b/src/util/sexpr/option_declarations.cpp index 489c92e48..b33a5fc7c 100644 --- a/src/util/sexpr/option_declarations.cpp +++ b/src/util/sexpr/option_declarations.cpp @@ -51,4 +51,22 @@ void option_declaration::display_value(std::ostream & out, options const & o) co if (!contains) out << get_default_value(); } + +static option_declarations * g_option_declarations = nullptr; + +void initialize_option_declarations() { + g_option_declarations = new option_declarations(); +} + +void finalize_option_declarations() { + delete g_option_declarations; +} + +option_declarations const & get_option_declarations() { + return *g_option_declarations; +} + +void register_option(name const & n, option_kind k, char const * default_value, char const * description) { + g_option_declarations->insert(mk_pair(n, option_declaration(n, k, default_value, description))); +} } diff --git a/src/util/sexpr/option_declarations.h b/src/util/sexpr/option_declarations.h index 4a5ecaa00..81fbaa255 100644 --- a/src/util/sexpr/option_declarations.h +++ b/src/util/sexpr/option_declarations.h @@ -32,5 +32,10 @@ public: }; typedef std::map option_declarations; +void initialize_option_declarations(); +void finalize_option_declarations(); option_declarations const & get_option_declarations(); +void register_option(name const & n, option_kind k, char const * default_value, char const * description); +#define register_bool_option(n, v, d) register_option(n, BoolOption, #v, d) +#define register_unsigned_option(n, v, d) register_option(n, UnsignedOption, #v, d) } diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index f537b8d27..48fcaa656 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -16,9 +16,20 @@ Author: Leonardo de Moura #endif namespace lean { -static name g_verbose("verbose"); -RegisterBoolOption(g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages"); -bool get_verbose(options const & opts) { return opts.get_bool(g_verbose, LEAN_DEFAULT_VERBOSE); } +static name * g_verbose = nullptr; + +void initialize_options() { + g_verbose = new name("verbose"); + register_bool_option(*g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages"); +} + +void finalize_options() { + delete g_verbose; +} + +bool get_verbose(options const & opts) { + return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE); +} std::ostream & operator<<(std::ostream & out, option_kind k) { switch (k) { @@ -32,19 +43,6 @@ std::ostream & operator<<(std::ostream & out, option_kind k) { return out; } -option_declarations & get_option_declarations_core() { - static option_declarations g_option_declarations; - return g_option_declarations; -} - -option_declarations const & get_option_declarations() { - return get_option_declarations_core(); -} - -mk_option_declaration::mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description) { - get_option_declarations_core().insert(mk_pair(n, option_declaration(n, k, default_value, description))); -} - bool options::empty() const { return is_nil(m_value); } diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index c8d970c8f..378726da9 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -114,4 +114,7 @@ options get_global_options(lua_State * L); */ void set_global_options(lua_State * L, options const & o); void open_options(lua_State * L); + +void initialize_options(); +void finalize_options(); }