From 7b6d55543373f1a8d6e3b870ec6d51b3a2512fca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 May 2014 20:11:50 -0700 Subject: [PATCH] refactor(kernel): remove level constraints from definitions Signed-off-by: Leonardo de Moura --- src/kernel/definition.cpp | 45 ++++++++++++++++---------------- src/kernel/definition.h | 23 ++++++++-------- src/kernel/type_checker.cpp | 10 ------- src/library/kernel_bindings.cpp | 29 +++++++++----------- src/tests/kernel/environment.cpp | 22 ++++++++-------- tests/lua/def1.lua | 25 ++++-------------- 6 files changed, 63 insertions(+), 91 deletions(-) diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp index 3b4e3ff94..1d321b1f1 100644 --- a/src/kernel/definition.cpp +++ b/src/kernel/definition.cpp @@ -16,7 +16,6 @@ struct definition::cell { MK_LEAN_RC(); name m_name; param_names m_params; - level_cnstrs m_cnstrs; expr m_type; bool m_theorem; optional m_value; // if none, then definition is actually a postulate @@ -33,12 +32,12 @@ struct definition::cell { bool m_use_conv_opt; void dealloc() { delete this; } - cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_axiom): - m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_axiom), + cell(name const & n, param_names const & params, expr const & t, bool is_axiom): + m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {} - cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_thm, expr const & v, + cell(name const & n, param_names const & params, expr const & t, bool is_thm, expr const & v, bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt): - m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_thm), + m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm), m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {} void write(serializer & s) const { @@ -52,7 +51,7 @@ struct definition::cell { } if (m_theorem) k |= 8; - s << k << m_name << m_params << m_cnstrs << m_type; + s << k << m_name << m_params << m_type; if (m_value) { s << *m_value; if (!m_theorem) @@ -61,7 +60,7 @@ struct definition::cell { } }; -definition g_dummy = mk_axiom(name(), param_names(), level_cnstrs(), expr()); +definition g_dummy = mk_axiom(name(), param_names(), expr()); definition::definition():definition(g_dummy) {} definition::definition(cell * ptr):m_ptr(ptr) {} @@ -79,7 +78,6 @@ bool definition::is_theorem() const { return is_definition() && m_ptr->m_theo name definition::get_name() const { return m_ptr->m_name; } param_names const & definition::get_params() const { return m_ptr->m_params; } -level_cnstrs const & definition::get_level_cnstrs() const { return m_ptr->m_cnstrs; } expr definition::get_type() const { return m_ptr->m_type; } bool definition::is_opaque() const { return m_ptr->m_opaque; } @@ -90,10 +88,12 @@ bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; } void definition::write(serializer & s) const { m_ptr->write(s); } -definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) { - return definition(new definition::cell(n, params, cs, t, false, v, opaque, weight, mod_idx, use_conv_opt)); +definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v, + bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) { + return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt)); } -definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt) { +definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v, + bool opaque, module_idx mod_idx, bool use_conv_opt) { unsigned w = 0; for_each(v, [&](expr const & e, unsigned) { if (is_constant(e)) { @@ -103,16 +103,16 @@ definition mk_definition(environment const & env, name const & n, param_names co } return true; }); - return mk_definition(n, params, cs, t, v, opaque, w+1, mod_idx, use_conv_opt); + return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt); } -definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v) { - return definition(new definition::cell(n, params, cs, t, true, v, true, 0, 0, false)); +definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v) { + return definition(new definition::cell(n, params, t, true, v, true, 0, 0, false)); } -definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) { - return definition(new definition::cell(n, params, cs, t, true)); +definition mk_axiom(name const & n, param_names const & params, expr const & t) { + return definition(new definition::cell(n, params, t, true)); } -definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) { - return definition(new definition::cell(n, params, cs, t, false)); +definition mk_var_decl(name const & n, param_names const & params, expr const & t) { + return definition(new definition::cell(n, params, t, false)); } definition read_definition(deserializer & d, unsigned module_idx) { @@ -121,23 +121,22 @@ definition read_definition(deserializer & d, unsigned module_idx) { bool is_theorem = (k & 8) != 0; name n = read_name(d); param_names ps = read_params(d); - level_cnstrs cs = read_level_cnstrs(d); expr t = read_expr(d); if (has_value) { expr v = read_expr(d); if (is_theorem) { - return mk_theorem(n, ps, cs, t, v); + return mk_theorem(n, ps, t, v); } else { unsigned w = d.read_unsigned(); bool is_opaque = (k & 2) != 0; bool use_conv_opt = (k & 4) != 0; - return mk_definition(n, ps, cs, t, v, is_opaque, w, module_idx, use_conv_opt); + return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt); } } else { if (is_theorem) - return mk_axiom(n, ps, cs, t); + return mk_axiom(n, ps, t); else - return mk_var_decl(n, ps, cs, t); + return mk_var_decl(n, ps, t); } } } diff --git a/src/kernel/definition.h b/src/kernel/definition.h index a52dd106c..8446458d8 100644 --- a/src/kernel/definition.h +++ b/src/kernel/definition.h @@ -59,7 +59,6 @@ public: name get_name() const; param_names const & get_params() const; - level_cnstrs const & get_level_cnstrs() const; expr get_type() const; expr get_value() const; @@ -68,13 +67,13 @@ public: module_idx get_module_idx() const; bool use_conv_opt() const; - friend definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, + friend definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt); - friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, + friend definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt); - friend definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); - friend definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); - friend definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); + friend definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v); + friend definition mk_axiom(name const & n, param_names const & params, expr const & t); + friend definition mk_var_decl(name const & n, param_names const & params, expr const & t); void write(serializer & s) const; }; @@ -83,9 +82,11 @@ inline optional none_definition() { return optional(); } inline optional some_definition(definition const & o) { return optional(o); } inline optional some_definition(definition && o) { return optional(std::forward(o)); } -definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true); -definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true); -definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); -definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); -definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); +definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v, + bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true); +definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v, + bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true); +definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v); +definition mk_axiom(name const & n, param_names const & params, expr const & t); +definition mk_var_decl(name const & n, param_names const & params, expr const & t); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 183a413e2..4a6d3fcd5 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -341,16 +341,6 @@ struct type_checker::imp { definition d = m_env.get(const_name(e)); auto const & ps = d.get_params(); auto const & ls = const_level_params(e); - auto const & cs = d.get_level_cnstrs(); - if (!infer_only && !is_nil(cs)) { - // add level constraints associated with the definition - for (auto const & c : cs) { - level lhs = lean::instantiate(c.first, ps, ls); - level rhs = lean::instantiate(c.second, ps, ls); - if (!is_trivial(lhs, rhs)) - add_cnstr(mk_level_cnstr(lhs, rhs, mk_lvl_cnstr_jst(e, lhs, rhs))); - } - } r = instantiate_params(d.get_type(), ps, ls); break; } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index a23ef8a00..fe83e0e2b 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -621,7 +621,6 @@ DEFINITION_PRED(is_opaque) DEFINITION_PRED(use_conv_opt) static int definition_get_name(lua_State * L) { return push_name(L, to_definition(L, 1).get_name()); } static int definition_get_params(lua_State * L) { return push_list_name(L, to_definition(L, 1).get_params()); } -static int definition_get_level_cnstrs(lua_State * L) { return push_list_pair_level(L, to_definition(L, 1).get_level_cnstrs()); } static int definition_get_type(lua_State * L) { return push_expr(L, to_definition(L, 1).get_type()); } static int definition_get_value(lua_State * L) { if (to_definition(L, 1).is_definition()) @@ -633,23 +632,23 @@ static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_ static int mk_var_decl(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 2) - return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2))); + return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), to_expr(L, 2))); else - return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4))); + return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3))); } static int mk_axiom(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 2) - return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2))); + return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), to_expr(L, 2))); else - return push_definition(L, mk_axiom(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4))); + return push_definition(L, mk_axiom(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3))); } static int mk_theorem(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 3) - return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), to_expr(L, 3))); + return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), to_expr(L, 2), to_expr(L, 3))); else - return push_definition(L, mk_theorem(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4), to_expr(L, 5))); + return push_definition(L, mk_theorem(to_name_ext(L, 1), to_list_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4))); } static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) { opaque = get_bool_named_param(L, idx, "opaque", opaque); @@ -663,23 +662,22 @@ static int mk_definition(lua_State * L) { if (is_environment(L, 1)) { if (nargs <= 5) { get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt); - return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), level_cnstrs(), + return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt)); } else { - get_definition_args(L, 7, opaque, weight, mod_idx, use_conv_opt); + get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt); return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_list_name_ext(L, 3), - to_list_pair_level_ext(L, 4), to_expr(L, 5), to_expr(L, 6), - opaque, mod_idx, use_conv_opt)); + to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt)); } } else { if (nargs <= 4) { get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt); - return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), + return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), to_expr(L, 2), to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt)); } else { - get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt); - return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), - to_expr(L, 4), to_expr(L, 5), opaque, weight, mod_idx, use_conv_opt)); + get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt); + return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), + to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt)); } } } @@ -694,7 +692,6 @@ static const struct luaL_Reg definition_m[] = { {"use_conv_opt", safe_function}, {"name", safe_function}, {"univ_params", safe_function}, - {"univ_cnstrs", safe_function}, {"type", safe_function}, {"value", safe_function}, {"weight", safe_function}, diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 32e399203..7de58915e 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -20,43 +20,43 @@ static environment add_def(environment const & env, definition const & d) { static void tst1() { environment env1; - auto env2 = add_def(env1, mk_definition("Bool", param_names(), level_cnstrs(), mk_Type(), mk_Bool())); + auto env2 = add_def(env1, mk_definition("Bool", param_names(), mk_Type(), mk_Bool())); lean_assert(!env1.find("Bool")); lean_assert(env2.find("Bool")); lean_assert(env2.find("Bool")->get_value() == mk_Bool()); try { - auto env3 = add_def(env2, mk_definition("Bool", param_names(), level_cnstrs(), mk_Type(), mk_Bool())); + auto env3 = add_def(env2, mk_definition("Bool", param_names(), mk_Type(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; } try { - auto env4 = add_def(env2, mk_definition("BuggyBool", param_names(), level_cnstrs(), mk_Bool(), mk_Bool())); + auto env4 = add_def(env2, mk_definition("BuggyBool", param_names(), mk_Bool(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; } try { - auto env5 = add_def(env2, mk_definition("Type1", param_names(), level_cnstrs(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type())); + auto env5 = add_def(env2, mk_definition("Type1", param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; } try { - auto env6 = add_def(env2, mk_definition("Type1", param_names(), level_cnstrs(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l"))))); + auto env6 = add_def(env2, mk_definition("Type1", param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l"))))); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; } try { - auto env7 = add_def(env2, mk_definition("foo", param_names(), level_cnstrs(), mk_Type() >> mk_Type(), mk_Bool())); + auto env7 = add_def(env2, mk_definition("foo", param_names(), mk_Type() >> mk_Type(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; } expr A = Const("A"); expr x = Const("x"); - auto env3 = add_def(env2, mk_definition("id", param_names(), level_cnstrs(), + auto env3 = add_def(env2, mk_definition("id", param_names(), Pi(A, mk_Type(), A >> A), Fun({{A, mk_Type()}, {x, A}}, x))); expr c = mk_local("c", Bool); @@ -73,16 +73,16 @@ static void tst1() { static void tst2() { environment env; name base("base"); - env = add_def(env, mk_var_decl(name(base, 0u), param_names(), level_cnstrs(), Bool >> (Bool >> Bool))); + env = add_def(env, mk_var_decl(name(base, 0u), param_names(), Bool >> (Bool >> Bool))); expr x = Const("x"); expr y = Const("y"); for (unsigned i = 1; i <= 100; i++) { expr prev = Const(name(base, i-1)); - env = add_def(env, mk_definition(env, name(base, i), param_names(), level_cnstrs(), Bool >> (Bool >> Bool), + env = add_def(env, mk_definition(env, name(base, i), param_names(), Bool >> (Bool >> Bool), Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x))))); } expr A = Const("A"); - env = add_def(env, mk_definition("id", param_names(), level_cnstrs(), + env = add_def(env, mk_definition("id", param_names(), Pi(A, mk_Type(), A >> A), Fun({{A, mk_Type()}, {x, A}}, x))); type_checker checker(env, name_generator("tmp")); @@ -129,7 +129,7 @@ static void tst3() { expr A = Const("A"); expr x = Const("x"); expr id = Const("id"); - env = add_def(env, mk_definition("id", param_names(), level_cnstrs(), + env = add_def(env, mk_definition("id", param_names(), Pi(A, mk_Type(), A >> A), Fun({{A, mk_Type()}, {x, A}}, x))); expr mk = Const("mk"); diff --git a/tests/lua/def1.lua b/tests/lua/def1.lua index 4ecd23ca8..25d215b55 100644 --- a/tests/lua/def1.lua +++ b/tests/lua/def1.lua @@ -1,7 +1,7 @@ local b = mk_var_decl("bit", Type) local l1 = mk_param_univ("l1") local l2 = mk_param_univ("l2") -local p = mk_var_decl("tst", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2))) +local p = mk_var_decl("tst", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2))) assert(p:is_var_decl()) assert(not p:is_axiom()) assert(p:name() == name("tst")) @@ -10,16 +10,11 @@ assert(p:type() == mk_arrow(mk_sort(l1), mk_sort(l2))) assert(#(p:univ_params()) == 2) assert(p:univ_params():head() == name("l1")) assert(p:univ_params():tail():head() == name("l2")) -assert(#(p:univ_cnstrs()) == 2) -assert(p:univ_cnstrs():head():first() == l1) -assert(p:univ_cnstrs():head():second() == l2) -assert(p:univ_cnstrs():tail():head():first() == l2) -assert(p:univ_cnstrs():tail():head():second() == l1) -local ax = mk_axiom("ax", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2))) +local ax = mk_axiom("ax", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2))) assert(ax:is_var_decl()) assert(ax:is_axiom()) assert(ax:name() == name("ax")) -local th = mk_theorem("t1", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0))) +local th = mk_theorem("t1", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0))) assert(th:is_theorem()) assert(th:is_definition()) assert(th:value() == mk_lambda("x", mk_sort(l1), Var(0))) @@ -53,30 +48,20 @@ assert(not d5:opaque()) assert(d5:weight() == 1) assert(d5:module_idx() == 3) assert(d5:use_conv_opt()) -local d6 = mk_definition("d6", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, A, B, {opaque=true, weight=5}) +local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5}) assert(d6:type() == A) assert(d6:value() == B) assert(#(d6:univ_params()) == 2) assert(d6:univ_params():head() == name("l1")) assert(d6:univ_params():tail():head() == name("l2")) -assert(#(d6:univ_cnstrs()) == 2) -assert(d6:univ_cnstrs():head():first() == l1) -assert(d6:univ_cnstrs():head():second() == l2) -assert(d6:univ_cnstrs():tail():head():first() == l2) -assert(d6:univ_cnstrs():tail():head():second() == l1) assert(d6:opaque()) assert(d6:weight() == 5) -local d7 = mk_definition(env, "d7", {"l1", "l2"}, {{l1, l2}, {l2, l1}}, A, B, {opaque=true, weight=5}) +local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {opaque=true, weight=5}) assert(d7:type() == A) assert(d7:value() == B) assert(d7:weight() == 1) assert(#(d7:univ_params()) == 2) assert(d7:univ_params():head() == name("l1")) assert(d7:univ_params():tail():head() == name("l2")) -assert(#(d7:univ_cnstrs()) == 2) -assert(d7:univ_cnstrs():head():first() == l1) -assert(d7:univ_cnstrs():head():second() == l2) -assert(d7:univ_cnstrs():tail():head():first() == l2) -assert(d7:univ_cnstrs():tail():head():second() == l1) assert(d7:opaque()) print("done")