From 93a61748e99a5ea058f4fec8fa2d741ab0b5fe3e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Apr 2014 16:57:19 -0700
Subject: [PATCH] fix(kernel/level): bug in optional<level>() constructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/kernel/level.cpp | 4 ++--
src/library/kernel_bindings.cpp | 10 ++++++++++
src/util/list_lua.h | 27 +++++++++++++++++++++++++++
tests/lua/level1.lua | 5 +++++
4 files changed, 44 insertions(+), 2 deletions(-)
create mode 100644 src/util/list_lua.h
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index c04553de5..f915a4236 100644
--- a/src/kernel/level.cpp
+++ b/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(); }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 2375d010b..b9df2dbfc 100644
--- a/src/library/kernel_bindings.cpp
+++ b/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}
};
diff --git a/src/util/list_lua.h b/src/util/list_lua.h
new file mode 100644
index 000000000..001322fa1
--- /dev/null
+++ b/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");
+ }
+}
+}
diff --git a/tests/lua/level1.lua b/tests/lua/level1.lua
index 90e3a309a..103245a80 100644
--- a/tests/lua/level1.lua
+++ b/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))
+