From 52eb7872880c0e872f2f957c8afe6c18c13b53bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Oct 2015 17:05:23 -0700 Subject: [PATCH] refactor(library/type_inference): move (non-temporary) class.* options to type_inference module --- src/library/class_instance_resolution.cpp | 43 ------------------- src/library/type_inference.cpp | 50 ++++++++++++++++++++--- src/library/type_inference.h | 4 ++ 3 files changed, 48 insertions(+), 49 deletions(-) diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 27f1e2139..8140b0d6c 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -29,40 +29,13 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/metavar_closure.h" -#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES -#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false -#endif - -#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH -#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 -#endif - -#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES -#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true -#endif - namespace lean { [[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } [[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); } -static name * g_class_trace_instances = nullptr; -static name * g_class_instance_max_depth = nullptr; -static name * g_class_trans_instances = nullptr; static name * g_class_force_new = nullptr; static name * g_prefix = nullptr; -bool get_class_trace_instances(options const & o) { - return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES); -} - -unsigned get_class_instance_max_depth(options const & o) { - return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); -} - -bool get_class_trans_instances(options const & o) { - return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES); -} - bool get_class_force_new(options const & o) { return o.get_bool(*g_class_force_new, false); } @@ -237,30 +210,14 @@ optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, void initialize_class_instance_resolution() { g_prefix = new name(name::mk_internal_unique_name()); - g_class_trace_instances = new name{"class", "trace_instances"}; - g_class_instance_max_depth = new name{"class", "instance_max_depth"}; - g_class_trans_instances = new name{"class", "trans_instances"}; g_class_force_new = new name{"class", "force_new"}; - register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES, - "(class) display messages showing the class-instances resolution execution trace"); - - register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, - "(class) max allowed depth in class-instance resolution"); - - register_bool_option(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES, - "(class) use automatically derived instances from the transitive closure of " - "the structure instance graph"); - register_bool_option(*g_class_force_new, false, "(class) force new type class resolution procedure to be used even in HoTT mode (THIS IS TEMPORARY OPTION)"); } void finalize_class_instance_resolution() { delete g_prefix; - delete g_class_trace_instances; - delete g_class_instance_max_depth; - delete g_class_trans_instances; delete g_class_force_new; } diff --git a/src/library/type_inference.cpp b/src/library/type_inference.cpp index 862962fa2..9a45dccb8 100644 --- a/src/library/type_inference.cpp +++ b/src/library/type_inference.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include "util/interrupt.h" +#include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" @@ -19,8 +20,35 @@ Author: Leonardo de Moura #include "library/generic_exception.h" #include "library/class.h" +#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES +#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false +#endif + +#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH +#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 +#endif + +#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES +#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true +#endif + namespace lean { -static name * g_prefix = nullptr; +static name * g_prefix = nullptr; +static name * g_class_trace_instances = nullptr; +static name * g_class_instance_max_depth = nullptr; +static name * g_class_trans_instances = nullptr; + +bool get_class_trace_instances(options const & o) { + return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES); +} + +unsigned get_class_instance_max_depth(options const & o) { + return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); +} + +bool get_class_trans_instances(options const & o) { + return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES); +} struct type_inference::ext_ctx : public extension_context { type_inference & m_owner; @@ -50,11 +78,6 @@ struct type_inference::ext_ctx : public extension_context { } }; -// TODO(Leo): move this methods to this module -bool get_class_trace_instances(options const & o); -unsigned get_class_instance_max_depth(options const & o); -bool get_class_trans_instances(options const & o); - type_inference::type_inference(environment const & env, io_state const & ios, bool multiple_instances): m_env(env), m_ios(ios), @@ -1727,9 +1750,24 @@ bool default_type_inference::ignore_universe_def_eq(level const & l1, level cons void initialize_type_inference() { g_prefix = new name(name::mk_internal_unique_name()); + g_class_trace_instances = new name{"class", "trace_instances"}; + g_class_instance_max_depth = new name{"class", "instance_max_depth"}; + g_class_trans_instances = new name{"class", "trans_instances"}; + register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES, + "(class) display messages showing the class-instances resolution execution trace"); + + register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, + "(class) max allowed depth in class-instance resolution"); + + register_bool_option(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES, + "(class) use automatically derived instances from the transitive closure of " + "the structure instance graph"); } void finalize_type_inference() { delete g_prefix; + delete g_class_trace_instances; + delete g_class_instance_max_depth; + delete g_class_trans_instances; } } diff --git a/src/library/type_inference.h b/src/library/type_inference.h index 9d6f02ce6..2eec7c70e 100644 --- a/src/library/type_inference.h +++ b/src/library/type_inference.h @@ -13,6 +13,10 @@ Author: Leonardo de Moura #include "library/projection.h" namespace lean { +bool get_class_trace_instances(options const & o); +unsigned get_class_instance_max_depth(options const & o); +bool get_class_trans_instances(options const & o); + /** \brief Light-weight type inference, normalization and definitional equality. It is simpler and more efficient version of the kernel type checker. It does not generate unification constraints.