From c759fc93f73b4452c4540c1f3562fdb1fedda949 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Nov 2013 20:59:28 -0800
Subject: [PATCH] test(lua): object Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/object.cpp        | 27 +++++++++------
 tests/lean/lua11.lean              | 54 ++++++++++++++++++++++++++++++
 tests/lean/lua11.lean.expected.out |  5 +++
 3 files changed, 75 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/lua11.lean
 create mode 100644 tests/lean/lua11.lean.expected.out

diff --git a/src/bindings/lua/object.cpp b/src/bindings/lua/object.cpp
index b9ab57fdc..986397e53 100644
--- a/src/bindings/lua/object.cpp
+++ b/src/bindings/lua/object.cpp
@@ -63,9 +63,10 @@ static int object_has_name(lua_State * L) {
 }
 
 static int object_get_name(lua_State * L) {
-    if (!to_nonnull_object(L, 1).has_name())
+    object const & o = to_nonnull_object(L, 1);
+    if (!o.has_name())
         throw exception("kernel object does not have a name");
-    return push_name(L, to_nonnull_object(L, 1).get_name());
+    return push_name(L, o.get_name());
 }
 
 static int object_has_type(lua_State * L) {
@@ -74,9 +75,10 @@ static int object_has_type(lua_State * L) {
 }
 
 static int object_get_type(lua_State * L) {
-    if (!to_nonnull_object(L, 1).has_type())
+    object const & o = to_nonnull_object(L, 1);
+    if (!o.has_type())
         throw exception("kernel object does not have a type");
-    return push_expr(L, to_nonnull_object(L, 1).get_type());
+    return push_expr(L, o.get_type());
 }
 
 static int object_has_cnstr_level(lua_State * L) {
@@ -85,21 +87,24 @@ static int object_has_cnstr_level(lua_State * L) {
 }
 
 static int object_get_cnstr_level(lua_State * L) {
-    if (!to_nonnull_object(L, 1).has_cnstr_level())
+    object const & o = to_nonnull_object(L, 1);
+    if (!o.has_cnstr_level())
         throw exception("kernel object does not have a constraint level");
-    return push_level(L, to_nonnull_object(L, 1).get_cnstr_level());
+    return push_level(L, o.get_cnstr_level());
 }
 
 static int object_get_value(lua_State * L) {
-    if (!to_nonnull_object(L, 1).is_definition())
-        throw exception("kernel object is not a definition/theorem");
-    return push_expr(L, to_nonnull_object(L, 1).get_value());
+    object const & o = to_nonnull_object(L, 1);
+    if (!o.is_definition() && !o.is_builtin())
+        throw exception("kernel object is not a definition/theorem/builtin");
+    return push_expr(L, o.get_value());
 }
 
 static int object_get_weight(lua_State * L) {
-    if (!to_nonnull_object(L, 1).is_definition())
+    object const & o = to_nonnull_object(L, 1);
+    if (!o.is_definition())
         throw exception("kernel object is not a definition");
-    lua_pushinteger(L, to_nonnull_object(L, 1).get_weight());
+    lua_pushinteger(L, o.get_weight());
     return 1;
 }
 
diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean
new file mode 100644
index 000000000..aef940208
--- /dev/null
+++ b/tests/lean/lua11.lean
@@ -0,0 +1,54 @@
+(**
+
+ local env = get_environment()
+ local o1  = env:find_object(name("Int", "add"))
+ local o2  = env:find_object("xyz31213")
+ print(o1:get_value())
+ assert(is_kernel_object(o1))
+ assert(is_kernel_object(o2))
+ assert(not o1:is_null())
+ assert(o2:is_null())
+ assert(o1:is_builtin())
+ assert(o1:keyword() == "Builtin")
+ assert(o1:get_name() == name("Int", "add"))
+ assert(not pcall(function() o2:get_name() end))
+ assert(not pcall(function() o2:keyword() end))
+
+ local found1 = false
+ local found2 = false
+ local bs = nil
+ for obj in env:objects() do
+    if not obj:has_name() then
+       found1 = true
+    end
+    if obj:is_builtin_set() then
+       if not found2 then
+          found2 = true
+          bs = obj
+       end
+    end
+ end
+ assert(found1)
+ assert(found2)
+ print(bs)
+ assert(not bs:in_builtin_set(Const("a")))
+ assert(not pcall(function() M:in_builtin_set(Const("a")) end))
+
+ local M   = env:find_object("M")
+ assert(not M:has_type())
+ assert(not pcall(function() M:get_type() end))
+ assert(M:has_cnstr_level())
+ print(M:get_cnstr_level())
+ assert(not pcall(function() o1:get_cnstr_level() end))
+ assert(not pcall(function() M:get_value() end))
+ env:add_var("x", Const("Int"))
+ env:add_definition("val", Const("Int"), Const("x"))
+ assert(env:find_object("val"):get_value() == Const("x"))
+ assert(env:find_object("val"):get_weight() == 1)
+ assert(not pcall(function() M:get_weight() end))
+ assert(env:find_object("Congr"):is_opaque())
+ assert(env:find_object("Congr"):is_theorem())
+ assert(env:find_object("Refl"):is_axiom())
+ assert(env:find_object(name("Int", "sub")):is_definition())
+ assert(env:find_object("x"):is_var_decl())
+**)
diff --git a/tests/lean/lua11.lean.expected.out b/tests/lean/lua11.lean.expected.out
new file mode 100644
index 000000000..8252f0cec
--- /dev/null
+++ b/tests/lean/lua11.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+Int::add
+BuiltinSet Nat::numeral
+512