refactor(library/type_inference): move (non-temporary) class.* options to type_inference module

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<expr> 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;
 }
 

src/library/type_inference.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <algorithm>
 #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;
 }
 }

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.