refactor(library): explicit initialization/finalization

src/library/init_module.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/string.h"
+#include "library/num.h"
 #include "library/resolve_macro.h"
 #include "library/annotation.h"
 #include "library/explicit.h"
@@ -21,14 +22,28 @@ Author: Leonardo de Moura
 #include "library/aliases.h"
 #include "library/coercion.h"
 #include "library/unifier_plugin.h"
+#include "library/io_state.h"
+#include "library/kernel_bindings.h"
+#include "library/match.h"
+#include "library/normalize.h"
+#include "library/sorry.h"
+#include "library/placeholder.h"
+#include "library/print.h"
 
 namespace lean {
 void initialize_library_module() {
+    initialize_print();
+    initialize_placeholder();
+    initialize_match();
+    initialize_normalize();
+    initialize_kernel_bindings();
+    initialize_io_state();
     initialize_unifier();
     initialize_kernel_serializer();
     initialize_let();
     initialize_typed_expr();
     initialize_choice();
+    initialize_num();
     initialize_string();
     initialize_resolve_macro();
     initialize_annotation();
@@ -41,9 +56,11 @@ void initialize_library_module() {
     initialize_aliases();
     initialize_coercion();
     initialize_unifier_plugin();
+    initialize_sorry();
 }
 
 void finalize_library_module() {
+    finalize_sorry();
     finalize_unifier_plugin();
     finalize_coercion();
     finalize_aliases();
@@ -56,10 +73,17 @@ void finalize_library_module() {
     finalize_annotation();
     finalize_resolve_macro();
     finalize_string();
+    finalize_num();
     finalize_choice();
     finalize_typed_expr();
     finalize_let();
     finalize_kernel_serializer();
     finalize_unifier();
+    finalize_io_state();
+    finalize_kernel_bindings();
+    finalize_normalize();
+    finalize_match();
+    finalize_placeholder();
+    finalize_print();
 }
 }

src/library/io_state.cpp

@@ -9,9 +9,18 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 
 namespace lean {
-static io_state g_dummy_ios(mk_print_formatter_factory());
+static io_state * g_dummy_ios = nullptr;
+
+void initialize_io_state() {
+    g_dummy_ios = new io_state(mk_print_formatter_factory());
+}
+
+void finalize_io_state() {
+    delete g_dummy_ios;
+}
+
 io_state const & get_dummy_ios() {
-    return g_dummy_ios;
+    return *g_dummy_ios;
 }
 
 io_state::io_state():io_state(mk_print_formatter_factory()) {}

src/library/io_state.h

@@ -45,4 +45,6 @@ public:
 };
 /** \brief Return a dummy io_state that is meant to be used in contexts that require an io_state, but it is not really used */
 io_state const & get_dummy_ios();
+void initialize_io_state();
+void finalize_io_state();
 }

src/library/kernel_bindings.cpp

@@ -877,7 +877,7 @@ static const struct luaL_Reg formatter_m[] = {
 };
 
 static char g_formatter_factory_key;
-static formatter_factory g_print_formatter_factory = mk_print_formatter_factory();
+static formatter_factory * g_print_formatter_factory = nullptr;
 
 optional<formatter_factory> get_global_formatter_factory_core(lua_State * L) {
     io_state * io = get_io_state_ptr(L);
@@ -902,7 +902,7 @@ formatter_factory get_global_formatter_factory(lua_State * L) {
     if (r)
         return *r;
     else
-        return g_print_formatter_factory;
+        return *g_print_formatter_factory;
 }
 
 void set_global_formatter_factory(lua_State * L, formatter_factory const & fmtf) {
@@ -1223,7 +1223,7 @@ static int io_state_get_options(lua_State * L) { return push_options(L, to_io_st
 static int io_state_get_formatter_factory(lua_State * L) { return push_formatter_factory(L, to_io_state(L, 1).get_formatter_factory()); }
 static int io_state_set_options(lua_State * L) { to_io_state(L, 1).set_options(to_options(L, 2)); return 0; }
 
-static mutex g_print_mutex;
+static mutex * g_print_mutex = nullptr;
 
 static void print(io_state * ios, bool reg, char const * msg) {
     if (ios) {
@@ -1238,7 +1238,7 @@ static void print(io_state * ios, bool reg, char const * msg) {
 
 /** \brief Thread safe version of print function */
 static int print(lua_State * L, int start, bool reg) {
-    lock_guard<mutex> lock(g_print_mutex);
+    lock_guard<mutex> lock(*g_print_mutex);
     io_state * ios = get_io_state_ptr(L);
     int n = lua_gettop(L);
     int i;
@@ -1864,15 +1864,15 @@ static int type_checker_infer(lua_State * L) { return push_ecs(L, to_type_checke
 static int type_checker_is_def_eq(lua_State * L) { return push_bcs(L, to_type_checker_ref(L, 1)->is_def_eq(to_expr(L, 2), to_expr(L, 3))); }
 static int type_checker_is_prop(lua_State * L) { return push_bcs(L, to_type_checker_ref(L, 1)->is_prop(to_expr(L, 2))); }
 
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
 
 static int mk_type_checker_with_hints(lua_State * L) {
     environment const & env = to_environment(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 1) {
-        return push_type_checker_ref(L, mk_type_checker(env, name_generator(g_tmp_prefix), false));
+        return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), false));
     } else if (nargs == 2 && lua_isboolean(L, 2)) {
-        return push_type_checker_ref(L, mk_type_checker(env, name_generator(g_tmp_prefix), lua_toboolean(L, 2)));
+        return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), lua_toboolean(L, 2)));
     } else if (nargs == 2) {
         return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2), false));
     } else {
@@ -2030,4 +2030,15 @@ void open_kernel_module(lua_State * L) {
     open_type_checker(L);
     open_inductive(L);
 }
+
+void initialize_kernel_bindings() {
+    g_print_formatter_factory = new formatter_factory(mk_print_formatter_factory());
+    g_print_mutex             = new mutex();
+    g_tmp_prefix              = new name(name::mk_internal_unique_name());
+}
+void finalize_kernel_bindings() {
+    delete g_tmp_prefix;
+    delete g_print_mutex;
+    delete g_print_formatter_factory;
+}
 }

src/library/kernel_bindings.h

@@ -92,4 +92,7 @@ io_state * get_io_state_ptr(lua_State * L);
 io_state get_io_state(lua_State * L);
 io_state to_io_state_ext(lua_State * L, int idx);
 void open_io_state(lua_State * L);
+
+void initialize_kernel_bindings();
+void finalize_kernel_bindings();
 }

src/library/match.cpp

@@ -14,17 +14,25 @@ Author: Leonardo de Moura
 #include "library/match.h"
 
 namespace lean {
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
+
+void initialize_match() {
+    g_tmp_prefix = new name(name::mk_internal_unique_name());
+}
+
+void finalize_match() {
+    delete g_tmp_prefix;
+}
 
 level mk_idx_meta_univ(unsigned i) {
-    return mk_meta_univ(name(g_tmp_prefix, i));
+    return mk_meta_univ(name(*g_tmp_prefix, i));
 }
 
 bool is_idx_meta_univ(level const & l) {
     if (!is_meta(l))
         return false;
     name const & n = meta_id(l);
-    return !n.is_atomic() && n.is_numeral() && n.get_prefix() == g_tmp_prefix;
+    return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
 }
 
 unsigned to_meta_idx(level const & l) {
@@ -341,7 +349,7 @@ bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buff
     if (prefix)
         return match_fn(esubst, lsubst, name_generator(*prefix), name_subst, plugin).match(p, t);
     else
-        return match_fn(esubst, lsubst, name_generator(g_tmp_prefix), name_subst, plugin).match(p, t);
+        return match_fn(esubst, lsubst, name_generator(*g_tmp_prefix), name_subst, plugin).match(p, t);
 }
 
 match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc) {

src/library/match.h

@@ -78,4 +78,6 @@ match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc);
 bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buffer<optional<level>> & lsubst,
            name const * prefix = nullptr, name_map<name> * name_subst = nullptr, match_plugin const * plugin = nullptr);
 void open_match(lua_State * L);
+void initialize_match();
+void finalize_match();
 }

src/library/normalize.cpp

@@ -10,7 +10,15 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 
 namespace lean {
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
+
+void initialize_normalize() {
+    g_tmp_prefix = new name(name::mk_internal_unique_name());
+}
+
+void finalize_normalize() {
+    delete g_tmp_prefix;
+}
 
 class normalize_fn {
     type_checker   m_tc;
@@ -46,7 +54,7 @@ class normalize_fn {
     }
 
 public:
-    normalize_fn(environment const & env):m_tc(env), m_ngen(g_tmp_prefix) {}
+    normalize_fn(environment const & env):m_tc(env), m_ngen(*g_tmp_prefix) {}
     expr operator()(expr const & e) { return normalize(e); }
 };
 

src/library/normalize.h

@@ -10,4 +10,6 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Return the \c e normal form with respect to the environment \c env. */
 expr normalize(environment const & env, expr const & e);
+void initialize_normalize();
+void finalize_normalize();
 }

src/library/num.cpp

@@ -8,23 +8,43 @@ Author: Leonardo de Moura
 #include "library/num.h"
 
 namespace lean {
-static expr g_num(Const("num"));
+static expr * g_num     = nullptr;
-static expr g_pos_num(Const("pos_num"));
+static expr * g_pos_num = nullptr;
-static expr g_zero(Const({"num", "zero"}));
+static expr * g_zero    = nullptr;
-static expr g_pos(Const({"num", "pos"}));
+static expr * g_pos     = nullptr;
-static expr g_one(Const({"pos_num", "one"}));
+static expr * g_one     = nullptr;
-static expr g_bit0(Const({"pos_num", "bit0"}));
+static expr * g_bit0    = nullptr;
-static expr g_bit1(Const({"pos_num", "bit1"}));
+static expr * g_bit1    = nullptr;
+
+void initialize_num() {
+    g_num = new expr(Const("num"));
+    g_pos_num = new expr(Const("pos_num"));
+    g_zero = new expr(Const({"num", "zero"}));
+    g_pos = new expr(Const({"num", "pos"}));
+    g_one = new expr(Const({"pos_num", "one"}));
+    g_bit0 = new expr(Const({"pos_num", "bit0"}));
+    g_bit1 = new expr(Const({"pos_num", "bit1"}));
+}
+
+void finalize_num() {
+    delete g_num;
+    delete g_pos_num;
+    delete g_zero;
+    delete g_pos;
+    delete g_one;
+    delete g_bit0;
+    delete g_bit1;
+}
 
 bool has_num_decls(environment const & env) {
     try {
         type_checker tc(env);
         return
-            tc.infer(g_zero).first == g_num &&
+            tc.infer(*g_zero).first == *g_num &&
-            tc.infer(g_pos).first  == mk_arrow(g_pos_num, g_num) &&
+            tc.infer(*g_pos).first  == mk_arrow(*g_pos_num, *g_num) &&
-            tc.infer(g_one).first  == g_pos_num &&
+            tc.infer(*g_one).first  == *g_pos_num &&
-            tc.infer(g_bit0).first == mk_arrow(g_pos_num, g_pos_num) &&
+            tc.infer(*g_bit0).first == mk_arrow(*g_pos_num, *g_pos_num) &&
-            tc.infer(g_bit1).first == mk_arrow(g_pos_num, g_pos_num);
+            tc.infer(*g_bit1).first == mk_arrow(*g_pos_num, *g_pos_num);
     } catch (...) {
         return false;
     }
@@ -33,32 +53,32 @@ bool has_num_decls(environment const & env) {
 expr from_pos_num(mpz const & n) {
     lean_assert(n > 0);
     if (n == 1)
-        return g_one;
+        return *g_one;
     if (n % mpz(2) == 1)
-        return mk_app(g_bit1, from_pos_num(n / 2));
+        return mk_app(*g_bit1, from_pos_num(n / 2));
     else
-        return mk_app(g_bit0, from_pos_num(n / 2));
+        return mk_app(*g_bit0, from_pos_num(n / 2));
 }
 
 expr from_num(mpz const & n) {
     expr r;
     lean_assert(n >= 0);
     if (n == 0)
-        r = g_zero;
+        r = *g_zero;
     else
-        r = mk_app(g_pos, from_pos_num(n));
+        r = mk_app(*g_pos, from_pos_num(n));
     lean_assert(*to_num(r) == n);
     return r;
 }
 
 optional<mpz> to_pos_num(expr const & e) {
-    if (e == g_one) {
+    if (e == *g_one) {
         return some(mpz(1));
     } else if (is_app(e)) {
-        if (app_fn(e) == g_bit0) {
+        if (app_fn(e) == *g_bit0) {
             if (auto r = to_pos_num(app_arg(e)))
                 return some(2*(*r));
-        } else if (app_fn(e) == g_bit1) {
+        } else if (app_fn(e) == *g_bit1) {
             if (auto r = to_pos_num(app_arg(e)))
                 return some(2*(*r) + 1);
         }
@@ -67,9 +87,9 @@ optional<mpz> to_pos_num(expr const & e) {
 }
 
 optional<mpz> to_num(expr const & e) {
-    if (e == g_zero)
+    if (e == *g_zero)
         return some(mpz(0));
-    else if (is_app(e) && app_fn(e) == g_pos)
+    else if (is_app(e) && app_fn(e) == *g_pos)
         return to_pos_num(app_arg(e));
     else
         return optional<mpz>();

src/library/num.h

@@ -36,4 +36,7 @@ expr from_num(mpz const & n);
    \see from_num
 */
 optional<mpz> to_num(expr const & e);
+
+void initialize_num();
+void finalize_num();
 }

src/library/placeholder.cpp

@@ -10,10 +10,24 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 
 namespace lean {
-static name g_implicit_placeholder_name = name(name::mk_internal_unique_name(), "_");
+static name * g_implicit_placeholder_name = nullptr;
-static name const & g_placeholder_name  = g_implicit_placeholder_name;
+static name * g_placeholder_name          = nullptr;
-static name g_strict_placeholder_name   = name(name::mk_internal_unique_name(), "_");
+static name * g_strict_placeholder_name   = nullptr;
-static name g_explicit_placeholder_name = name(name::mk_internal_unique_name(), "_");
+static name * g_explicit_placeholder_name = nullptr;
+
+void initialize_placeholder() {
+    g_implicit_placeholder_name = new name(name::mk_internal_unique_name(), "_");
+    g_placeholder_name          = g_implicit_placeholder_name;
+    g_strict_placeholder_name   = new name(name::mk_internal_unique_name(), "_");
+    g_explicit_placeholder_name = new name(name::mk_internal_unique_name(), "_");
+}
+
+void finalize_placeholder() {
+    delete g_implicit_placeholder_name;
+    delete g_strict_placeholder_name;
+    delete g_explicit_placeholder_name;
+}
+
 MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0)
 static unsigned next_placeholder_id() {
     unsigned & c = get_placeholder_id();
@@ -21,12 +35,12 @@ static unsigned next_placeholder_id() {
     c++;
     return r;
 }
-level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, next_placeholder_id())); }
+level mk_level_placeholder() { return mk_global_univ(name(*g_placeholder_name, next_placeholder_id())); }
 static name const & to_prefix(expr_placeholder_kind k) {
     switch (k) {
-    case expr_placeholder_kind::Implicit:       return g_implicit_placeholder_name;
+    case expr_placeholder_kind::Implicit:       return *g_implicit_placeholder_name;
-    case expr_placeholder_kind::StrictImplicit: return g_strict_placeholder_name;
+    case expr_placeholder_kind::StrictImplicit: return *g_strict_placeholder_name;
-    case expr_placeholder_kind::Explicit:       return g_explicit_placeholder_name;
+    case expr_placeholder_kind::Explicit:       return *g_explicit_placeholder_name;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -41,13 +55,13 @@ static bool is_placeholder(name const & n) {
     if (n.is_atomic())
         return false;
     name const & p = n.get_prefix();
-    return p == g_implicit_placeholder_name || p == g_strict_placeholder_name || p == g_explicit_placeholder_name;
+    return p == *g_implicit_placeholder_name || p == *g_strict_placeholder_name || p == *g_explicit_placeholder_name;
 }
 static bool is_strict_placeholder(name const & n) {
-    return !n.is_atomic() && n.get_prefix() == g_strict_placeholder_name;
+    return !n.is_atomic() && n.get_prefix() == *g_strict_placeholder_name;
 }
 static bool is_explicit_placeholder(name const & n) {
-    return !n.is_atomic() && n.get_prefix() == g_explicit_placeholder_name;
+    return !n.is_atomic() && n.get_prefix() == *g_explicit_placeholder_name;
 }
 bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); }
 bool is_placeholder(expr const & e) {

src/library/placeholder.h

@@ -43,4 +43,6 @@ optional<expr> placeholder_type(expr const & e);
 bool has_placeholder(expr const & e);
 
 void open_placeholder(lua_State * L);
+void initialize_placeholder();
+void finalize_placeholder();
 }

src/library/print.cpp

@@ -40,22 +40,33 @@ bool is_internal_name(name n) {
     return n.is_numeral();
 }
 
-static name g_x("x");
+static name * g_x        = nullptr;
+static name * g_internal = nullptr;
+
+void initialize_print() {
+    g_internal = new name("M");
+    g_x        = new name("x");
+}
+
+void finalize_print() {
+    delete g_x;
+    delete g_internal;
+}
+
 pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
     lean_assert(is_binding(b));
     name n = binding_name(b);
     if (is_internal_name(n))
-        n = g_x;
+        n = *g_x;
     n = pick_unused_name(binding_body(b), n);
     expr c = mk_local(n, preserve_type ? binding_domain(b) : expr(), binding_info(b));
     return mk_pair(instantiate(binding_body(b), c), c);
 }
 
-static name g_internal("M");
 name fix_internal_name(name const & a) {
     if (a.is_atomic()) {
         if (a.is_numeral())
-            return g_internal;
+            return *g_internal;
         else
             return a;
     } else {

src/library/print.h

@@ -28,4 +28,7 @@ formatter_factory mk_print_formatter_factory();
 
 /** \brief Use simple formatter as the default print function */
 void init_default_print_fn();
+
+void initialize_print();
+void finalize_print();
 }

src/library/sorry.cpp

@@ -9,25 +9,37 @@ Author: Leonardo de Moura
 #include "library/module.h"
 
 namespace lean {
-static name g_sorry_name("sorry");
+static name * g_sorry_name = nullptr;
-static name  g_l("l");
+static name * g_l          = nullptr;
-static expr  g_sorry_type(mk_pi("A", mk_sort(mk_param_univ(g_l)), mk_var(0), binder_info(true)));
+static expr * g_sorry_type = nullptr;
+
+void initialize_sorry() {
+    g_sorry_name = new name("sorry");
+    g_l          = new name("l");
+    g_sorry_type = new expr(mk_pi("A", mk_sort(mk_param_univ(*g_l)), mk_var(0), binder_info(true)));
+}
+
+void finalize_sorry() {
+    delete g_sorry_type;
+    delete g_l;
+    delete g_sorry_name;
+}
 
 bool has_sorry(environment const & env) {
-    auto decl = env.find(g_sorry_name);
+    auto decl = env.find(*g_sorry_name);
-    return decl && decl->get_type() == g_sorry_type;
+    return decl && decl->get_type() == *g_sorry_type;
 }
 
 environment declare_sorry(environment const & env) {
-    if (auto decl = env.find(g_sorry_name)) {
+    if (auto decl = env.find(*g_sorry_name)) {
-        if (decl->get_type() != g_sorry_type)
+        if (decl->get_type() != *g_sorry_type)
             throw exception("failed to declare 'sorry', environment already has an object named 'sorry'");
         return env;
     } else {
-        return module::add(env, check(env, mk_var_decl(g_sorry_name, list<name>(g_l), g_sorry_type)));
+        return module::add(env, check(env, mk_var_decl(*g_sorry_name, list<name>(*g_l), *g_sorry_type)));
     }
 }
 
-expr mk_sorry() { return mk_constant(g_sorry_name); }
+expr mk_sorry() { return mk_constant(*g_sorry_name); }
-name const & get_sorry_name() { return g_sorry_name; }
+name const & get_sorry_name() { return *g_sorry_name; }
 }

src/library/sorry.h

@@ -18,4 +18,6 @@ environment declare_sorry(environment const & env);
 /** \brief Return the constant \c sorry */
 expr mk_sorry();
 name const & get_sorry_name();
+void initialize_sorry();
+void finalize_sorry();
 }

src/library/unifier.cpp

@@ -47,24 +47,6 @@ static name * g_unifier_max_steps         = nullptr;
 static name * g_unifier_computation       = nullptr;
 static name * g_unifier_expensive_classes = nullptr;
 
-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);
 }
@@ -264,7 +246,7 @@ unify_status unify_simple(substitution & s, constraint const & c) {
         return unify_status::Unsupported;
 }
 
-static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
+static constraint * g_dont_care_cnstr = nullptr;
 static unsigned g_group_size = 1u << 28;
 constexpr unsigned g_num_groups = 8;
 static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size};
@@ -1027,7 +1009,7 @@ struct unifier_fn {
     bool process_constraint_cidx(unsigned cidx) {
         if (in_conflict())
             return false;
-        cnstr c(g_dont_care_cnstr, cidx);
+        cnstr c(*g_dont_care_cnstr, cidx);
         if (auto it = m_cnstrs.find(c)) {
             constraint c2 = it->first;
             m_cnstrs.erase(c);
@@ -2196,7 +2178,7 @@ static unifier_plugin to_unifier_plugin(lua_State * L, int idx) {
 }
 #endif
 
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
 
 static int unify(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -2237,4 +2219,27 @@ void open_unifier(lua_State * L) {
     SET_ENUM("Unsupported",  unify_status::Unsupported);
     lua_setglobal(L, "unify_status");
 }
+
+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");
+
+    g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification(), false));
+    g_tmp_prefix      = new name(name::mk_internal_unique_name());
+}
+
+void finalize_unifier() {
+    delete g_tmp_prefix;
+    delete g_dont_care_cnstr;
+    delete g_unifier_max_steps;
+    delete g_unifier_computation;
+    delete g_unifier_expensive_classes;
+}
 }