feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/bit.lean

@@ -24,15 +24,20 @@ theorem cond_b1 {A : Type} (t e : A) : cond b1 t e = t
 definition bor (a b : bit)
 := bit_rec (bit_rec b0 b1 b) b1 a
 
-theorem bor_b1_left (a : bit) : bor b1 a = b1
+section
-:= refl (bor b1 a)
+  -- create section for setting temporary configuration option
+  set_option unifier.unfold_opaque true
 
-theorem bor_b1_right (a : bit) : bor a b1 = b1
+  theorem bor_b1_left (a : bit) : bor b1 a = b1
-:= bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a
+  := refl (bor b1 a)
 
-theorem bor_b0_left (a : bit) : bor b0 a = a
+  theorem bor_b1_right (a : bit) : bor a b1 = b1
-:= bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a
+  := bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a
 
-theorem bor_b0_right (a : bit) : bor a b0 = a
+  theorem bor_b0_left (a : bit) : bor b0 a = a
-:= bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a
+  := bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a
+
+  theorem bor_b0_right (a : bit) : bor a b0 = a
+  := bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a
+end
 end

src/frontends/lean/elaborator.cpp

@@ -196,7 +196,7 @@ public:
                bool check_unassigned):
         m_env(env), m_ios(ios),
         m_plugin([](constraint const &, name_generator const &) { return lazy_list<list<constraint>>(); }),
-        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional<module_idx>(0))),
+        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, true /* unfold opaque from the main module */)),
         m_pos_provider(pp) {
         m_check_unassigned = check_unassigned;
         m_use_local_instances = get_elaborator_local_instances(ios.get_options());
@@ -743,7 +743,7 @@ public:
         cs.append(m_constraints);
         m_constraints.clear();
         return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_plugin,
-                     true, get_unifier_max_steps(m_ios.get_options()));
+                     true, m_ios.get_options());
     }
 
     void collect_metavars(expr const & e, buffer<expr> & mvars) {

src/kernel/converter.cpp

@@ -484,4 +484,10 @@ std::unique_ptr<converter> mk_default_converter(environment const & env, optiona
                                                 bool memoize, name_set const & extra_opaque) {
     return std::unique_ptr<converter>(new default_converter(env, mod_idx, memoize, extra_opaque));
 }
+std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize, name_set const & extra_opaque) {
+    if (unfold_opaque_main)
+        return mk_default_converter(env, optional<module_idx>(0), memoize, extra_opaque);
+    else
+        return mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque);
+}
 }

src/kernel/converter.h

@@ -28,4 +28,6 @@ std::unique_ptr<converter> mk_default_converter(environment const & env,
                                                 optional<module_idx> mod_idx = optional<module_idx>(),
                                                 bool memoize = true,
                                                 name_set const & extra_opaque = name_set());
+std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main,
+                                                bool memoize = true, name_set const & extra_opaque = name_set());
 }

src/kernel/declaration.h

@@ -22,10 +22,10 @@ namespace lean {
     to be transparent for any other opaque definition in module m1.
 */
 typedef unsigned module_idx;
+/** \brief The main module is the module being currently compiled. We always assigned it the index 0. */
+constexpr unsigned g_main_module_idx = 0;
 
-/**
+/** \brief Environment definitions, theorems, axioms and variable declarations. */
-   \brief Environment definitions, theorems, axioms and variable declarations.
-*/
 class declaration {
     struct cell;
     cell * m_ptr;

src/library/module.cpp

@@ -232,6 +232,7 @@ struct import_modules_fn {
         r->m_fname        = fname;
         r->m_counter      = imports.size();
         r->m_module_idx   = m_import_counter+1; // importate modules have idx > 0, we reserve idx 0 for new module
+        lean_assert(r->m_module_idx != g_main_module_idx);
         m_import_counter++;
         std::swap(r->m_obj_code, code);
         m_module_info.insert(mname, r);

src/library/unifier.cpp

@@ -24,14 +24,10 @@ Author: Leonardo de Moura
 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");
-static name g_unifier_use_exceptions {"unifier", "use_exceptions"};
+static name g_unifier_unfold_opaque{"unifier", "unfold_opaque"};
-RegisterBoolOption(g_unifier_use_exceptions, true, "(unifier) throw an exception when there are no more solutions");
+RegisterBoolOption(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE, "(unifier) unfold opaque definitions from the current module");
-unsigned get_unifier_max_steps(options const & opts) {
+unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); }
-    return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+bool get_unifier_unfold_opaque(options const & opts) { return opts.get_bool(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); }
-}
-bool get_unifier_use_exceptions(options const & opts) {
-    return opts.get_bool(g_unifier_use_exceptions, true);
-}
 
 // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where
 // l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args.
@@ -333,9 +329,9 @@ struct unifier_fn {
 
     unifier_fn(environment const & env, unsigned num_cs, constraint const * cs,
                name_generator const & ngen, substitution const & s, unifier_plugin const & p,
-               bool use_exception, unsigned max_steps):
+               bool use_exception, unsigned max_steps, bool unfold_opaque):
         m_env(env), m_ngen(ngen), m_subst(s), m_plugin(p),
-        m_tc(env, m_ngen.mk_child(), mk_default_converter(env, optional<module_idx>(0))),
+        m_tc(env, m_ngen.mk_child(), mk_default_converter(env, unfold_opaque)),
         m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
         m_next_assumption_idx = 0;
         m_next_cidx = 0;
@@ -1277,17 +1273,17 @@ lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) {
 }
 
 lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p, bool use_exception, unsigned max_steps) {
+                              unifier_plugin const & p, bool use_exception, unsigned max_steps, bool unfold_opaque) {
-    return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, substitution(), p, use_exception, max_steps));
+    return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, substitution(), p, use_exception, max_steps, unfold_opaque));
 }
 
 lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p, options const & o) {
+                              unifier_plugin const & p, bool use_exception, options const & o) {
-    return unify(env, num_cs, cs, ngen, p, get_unifier_use_exceptions(o), get_unifier_max_steps(o));
+    return unify(env, num_cs, cs, ngen, p, use_exception, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              unifier_plugin const & p, unsigned max_steps) {
+                              unifier_plugin const & p, unsigned max_steps, bool unfold_opaque) {
     name_generator new_ngen(ngen);
     type_checker tc(env, new_ngen.mk_child());
     expr _lhs = s.instantiate(lhs);
@@ -1301,13 +1297,13 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
     if (cs.empty()) {
         return lazy_list<substitution>(s);
     } else {
-        return unify(std::make_shared<unifier_fn>(env, cs.size(), cs.data(), ngen, s, p, false, max_steps));
+        return unify(std::make_shared<unifier_fn>(env, cs.size(), cs.data(), ngen, s, p, false, max_steps, unfold_opaque));
     }
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
                               substitution const & s, unifier_plugin const & p, options const & o) {
-    return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o));
+    return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
 }
 
 static int unify_simple(lua_State * L) {
@@ -1368,6 +1364,7 @@ static void to_constraint_buffer(lua_State * L, int idx, buffer<constraint> & cs
     lua_pop(L, 1);
 }
 
+#if 0
 static constraints to_constraints(lua_State * L, int idx) {
     buffer<constraint> cs;
     to_constraint_buffer(L, idx, cs);
@@ -1421,6 +1418,7 @@ static unifier_plugin to_unifier_plugin(lua_State * L, int idx) {
             return r;
         });
 }
+#endif
 
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
@@ -1429,17 +1427,19 @@ static int unify(lua_State * L) {
     lazy_list<substitution> r;
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
-        if (nargs == 6 && is_substitution(L, 5))
+        if (nargs == 6)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(), to_options(L, 6));
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(),
+                      to_options(L, 6));
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_unifier_plugin(L, 6), to_options(L, 7));
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(),
+                      options());
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
-        if (nargs == 4 && is_options(L, 4))
+        if (nargs == 4)
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), to_options(L, 4));
+            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, to_options(L, 4));
         else
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5));
+            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, options());
     }
     return push_substitution_seq_it(L, r);
 }

src/library/unifier.h

@@ -19,9 +19,13 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 10000
 #endif
 
+#ifndef LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE
+#define LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE false
+#endif
+
 namespace lean {
 unsigned get_unifier_max_steps(options const & opts);
-bool get_unifier_use_exceptions(options const & opts);
+bool get_unifier_unfold_opaque(options const & opts);
 
 bool is_simple_meta(expr const & e);
 
@@ -46,10 +50,13 @@ typedef std::function<lazy_list<constraints>(constraint const &, name_generator
 unifier_plugin get_noop_unifier_plugin();
 
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+                              unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true,
-lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unifier_plugin const & p, options const & o);
+                              unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s = substitution(),
+lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p = get_noop_unifier_plugin(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+                              unifier_plugin const & p, bool use_exception, options const & o);
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              substitution const & s = substitution(), unifier_plugin const & p = get_noop_unifier_plugin(),
+                              unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
                               unifier_plugin const & p, options const & o);
 

tests/lean/run/tactic23.lean

@@ -32,5 +32,9 @@ theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
 definition is_zero (n : nat)
 := nat_rec true (λ n r, false) n
 
-theorem T2 : ∃ a, (is_zero a) = true
+section
-:= by apply exists_intro; apply refl
+  set_option unifier.unfold_opaque true
+
+  theorem T2 : ∃ a, (is_zero a) = true
+  := by apply exists_intro; apply refl
+end

tests/lua/unify3.lua

@@ -13,35 +13,4 @@ local real_group = Const("real_group")
 local nat_group  = Const("nat_group")
 local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))
 local cs  = { mk_eq_cnstr(carrier(m), real) }
-local o   = options({"unifier", "use_exceptions"}, false)
+assert(not unify(env, cs, name_generator())())
-print(o)
-assert(not unify(env, cs, name_generator(), o)())
-
-function hint(c, ngen)
-   local lhs = c:lhs()
-   local rhs = c:rhs()
-   local j   = c:justification()
-   if lhs:is_app() and lhs:fn() == carrier and lhs:arg():is_meta() then
-      return
-         {{ mk_eq_cnstr(lhs:arg(), nat_group, j) }, -- first possible solution
-          { mk_eq_cnstr(lhs:arg(), real_group, j) }}
-   else
-      return nil
-   end
-end
-
-function display_solutions(ss)
-   local n = 0
-   for s in ss do
-      print("solution: ")
-      s:for_each_expr(function(n, v, j)
-                         print("  " .. tostring(n) .. " := " .. tostring(v))
-      end)
-      s:for_each_level(function(n, v, j)
-                          print("  " .. tostring(n) .. " := " .. tostring(v))
-      end)
-      n = n + 1
-   end
-end
-
-display_solutions(unify(env, cs, name_generator(), hint, o))

tests/lua/unify5.lua

@@ -12,8 +12,6 @@ local m2 = mk_metavar("m2", N)
 local m3 = mk_metavar("m3", N)
 local m4 = mk_metavar("m4", N)
 
-local o   = options({"unifier", "use_exceptions"}, false)
-
 function display_solutions(m, ss)
    local n = 0
    for s in ss do
@@ -34,4 +32,4 @@ cs = { mk_eq_cnstr(m1, f(m2, f(m3, m4))),
        mk_choice_cnstr(m4, function(m, e, s, ngen) return {a, b} end)
      }
 
-display_solutions(m1, unify(env, cs, name_generator(), o))
+display_solutions(m1, unify(env, cs, name_generator()))

tests/lua/unify6.lua

@@ -3,7 +3,6 @@ local m1  = mk_meta_univ("m1")
 local m2  = mk_meta_univ("m2")
 local m3  = mk_meta_univ("m3")
 local l1  = mk_param_univ("l1")
-local o   = options({"unifier", "use_exceptions"}, false)
 
 function display_solutions(m, ss)
    local n = 0
@@ -24,4 +23,4 @@ cs = { mk_level_eq_cnstr(m1, max_univ(m2, max_univ(m2, l1, 1))),
        mk_level_eq_cnstr(m3+1, m2+1)
      }
 
-display_solutions(m1, unify(env, cs, name_generator(), o))
+display_solutions(m1, unify(env, cs, name_generator()))

tests/lua/unify7.lua

@@ -10,8 +10,7 @@ print(env:infer_type(t))
 local m   = mk_metavar("m", mk_arrow(N, N, Type))
 local cs  = { mk_eq_cnstr(m(a, a), t) }
 
-local o   = options({"unifier", "use_exceptions"}, false)
+ss = unify(env, cs, name_generator())
-ss = unify(env, cs, name_generator(), o)
 local n = 0
 for s in ss do
    print("solution: " .. tostring(s:instantiate(m)))