fix(kernel/level): bug in optional<level>() constructor

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

src/kernel/level.cpp

@@ -27,7 +27,7 @@ struct level_cell {
     MK_LEAN_RC()
     level_kind m_kind;
     unsigned   m_hash;
-    level_cell(level_kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {}
+    level_cell(level_kind k, unsigned h):m_rc(0), m_kind(k), m_hash(h) {}
 };
 
 struct level_composite : public level_cell {
@@ -216,7 +216,7 @@ level const & mk_level_one()  {
 }
 
 level::level():level(mk_level_zero()) {}
-level::level(level_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); }
+level::level(level_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
 level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
 level::level(level && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
 level::~level() { if (m_ptr) m_ptr->dec_ref(); }

src/library/kernel_bindings.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sstream.h"
 #include "util/script_state.h"
+#include "util/list_lua.h"
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
@@ -76,6 +77,14 @@ static int level_succ_of(lua_State * L) {
     else throw exception("arg #1 must be a level succ expression");
 }
 
+static int level_instantiate(lua_State * L) {
+    auto ps = table_to_list<name>(L, 2, to_name_ext);
+    auto ls = table_to_list<level>(L, 3, to_level);
+    if (length(ps) != length(ls))
+        throw exception("arg #2 and #3 size do not match");
+    return push_level(L, instantiate(to_level(L, 1), ps, ls));
+}
+
 static const struct luaL_Reg level_m[] = {
     {"__gc",            level_gc}, // never throws
     {"__tostring",      safe_function<level_tostring>},
@@ -98,6 +107,7 @@ static const struct luaL_Reg level_m[] = {
     {"lhs",             safe_function<level_lhs>},
     {"rhs",             safe_function<level_rhs>},
     {"succ_of",         safe_function<level_succ_of>},
+    {"instantiate",     safe_function<level_instantiate>},
     {0, 0}
 };
 

src/util/list_lua.h

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/list.h"
+
+namespace lean {
+/** \brief Convert a Lua table into a list<T> */
+template<typename T, typename Proc>
+list<T> table_to_list(lua_State * L, int idx, Proc const & to_value) {
+    if (lua_istable(L, idx)) {
+        int n = objlen(L, idx);
+        list<T> r;
+        for (int i = n; i >= 1; i--) {
+            lua_rawgeti(L, idx, i);
+            r = cons(to_value(L, -1), r);
+            lua_pop(L, 1);
+        }
+        return r;
+    } else {
+        throw exception("invalid argument, lua table expected");
+    }
+}
+}

tests/lua/level1.lua

@@ -26,3 +26,8 @@ assert(mk_level_one():kind() == level_kind.Succ)
 assert(not mk_level_one():has_meta())
 assert(not mk_level_succ(mk_param_univ("a")):has_meta())
 assert(mk_level_succ(mk_meta_univ("a")):has_meta())
+local l = mk_level_max(mk_param_univ("a"), mk_param_univ("b"))
+assert(l:instantiate({"a"}, {mk_level_one()}) == mk_level_max(mk_level_one(), mk_param_univ("b")))
+assert(l:instantiate({"a", "b"}, {mk_level_one(), mk_param_univ("c")}) == mk_level_max(mk_level_one(), mk_param_univ("c")))
+assert(not pcall(function() l:instantiate({"a", "b", "C"}, {mk_level_one(), mk_param_univ("c")}) end))
+