test(lua/expr): add missing tests

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

src/bindings/lua/expr.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/buffer.h"
 #include "util/sexpr/options.h"
+#include "util/sstream.h"
 #include "kernel/expr.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
@@ -251,7 +252,11 @@ static int expr_num_args(lua_State * L) {
 }
 
 static int expr_arg(lua_State * L) {
-    return push_expr(L, arg(to_app(L, 1), luaL_checkinteger(L, 2)));
+    expr & e = to_app(L, 1);
+    int i    = luaL_checkinteger(L, 2);
+    if (i >= static_cast<int>(num_args(e)) || i < 0)
+        throw exception(sstream() << "invalid application argument #" << i << ", application has " << num_args(e) << " arguments");
+    return push_expr(L, arg(e, i));
 }
 
 static int expr_fields(lua_State * L) {

tests/lua/expr8.lua

@@ -0,0 +1,44 @@
+local f, g, a, b, c, d = Consts("f, g, a, b, c, d")
+local N, M = Consts("N, M")
+local x = Var(0)
+local y = Var(1)
+assert(f(a):closed())
+local F = f(g(x, a), f(b, f(x, c)))
+assert(F:has_free_vars())
+assert(F:has_free_var(0))
+assert(not F:has_free_var(1))
+assert(F:has_free_var(0, 2))
+assert(not F:has_free_var(1, 3))
+local c = 0
+F:for_each(function() c = c + 1; return false end)
+assert(c == 1)
+assert(x:is_var())
+assert(not x:is_app())
+assert(F:is_app())
+assert(Let(a, b, f(a)):is_let())
+assert(fun(a, N, f(a)):is_lambda())
+assert(Pi(a, N, f(a)):is_pi())
+assert(Pi(a, N, f(a)):is_abstraction())
+assert(fun(a, N, f(a)):is_abstraction())
+assert(mk_metavar("M"):is_metavar())
+assert(mk_real_value(mpq(10)):is_value())
+assert(not F:has_metavar())
+assert(f(mk_metavar("M")):has_metavar())
+assert(Eq(a, b):is_eq())
+assert(F:num_args() == 3)
+assert(F:arg(0) == f)
+assert(F:arg(1) == g(x, a))
+assert(not pcall(function() F:arg(3) end))
+assert(not pcall(function() F:arg(-3) end))
+local l1 = level(level("N"), 10)
+print(l1)
+assert(Type(l1):fields() == l1)
+assert(a:fields() == name("a"))
+assert(y:fields() == 1)
+assert(mk_metavar("M"):fields() == name("M"))
+assert(a:occurs(F))
+assert(F:hash() == F:hash())
+assert(a:hash() ~= F:hash())
+assert(mk_nat_value(mpz(10)):is_value())
+assert(not pcall(function() Var(0):num_args() end))
+assert(not pcall(function() print(fun(N, a)) end))