test(lua): expr LUA API test

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

src/bindings/lua/context.cpp

@@ -107,7 +107,7 @@ static int mk_context(lua_State * L) {
     } else if (nargs == 3) {
         return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_nonnull_expr(L, 3)));
     } else {
-        return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)));
+        return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_nonnull_expr(L, 4)));
     }
 }
 

src/bindings/lua/expr.cpp

@@ -114,6 +114,10 @@ static int expr_mk_pi(lua_State * L) {
     return push_expr(L, mk_pi(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
 }
 
+static int expr_mk_arrow(lua_State * L) {
+    return push_expr(L, mk_arrow(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2)));
+}
+
 static int expr_mk_let(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 3)
@@ -322,6 +326,7 @@ void open_expr(lua_State * L) {
     SET_GLOBAL_FUN(expr_mk_eq,       "Eq");
     SET_GLOBAL_FUN(expr_mk_lambda,        "mk_lambda");
     SET_GLOBAL_FUN(expr_mk_pi,       "mk_pi");
+    SET_GLOBAL_FUN(expr_mk_arrow,    "mk_arrow");
     SET_GLOBAL_FUN(expr_mk_let,      "mk_let");
     SET_GLOBAL_FUN(expr_fun,         "fun");
     SET_GLOBAL_FUN(expr_fun,         "Fun");

tests/lua/expr6.lua

@@ -0,0 +1,51 @@
+
+function print_leaves(e, ctx)
+   if e:is_null() then
+      return
+   end
+   local k = e:kind()
+   if k == expr_kind.Var then
+      local i = e:fields()
+      local e = ctx:lookup(i)
+      print("var idx: " .. i .. ", name: " .. tostring(e:get_name()))
+   elseif k == expr_kind.Const then
+      local n = e:fields()
+      print("constant name: " .. n)
+   elseif k == expr_kind.App then
+      local num, args = e:fields()
+      print("application num args: " .. num)
+      for a in args do
+         print_leaves(a, ctx)
+      end
+   elseif k == expr_kind.Lambda or k == expr_kind.Pi then
+      local name, domain, body = e:fields()
+      print("abstraction var name: " .. tostring(name))
+      print_leaves(domain, ctx)
+      print_leaves(body, ctx:extend(name, domain))
+   elseif k == expr_kind.Eq then
+      local lhs, rhs = e:fields()
+      print_leaves(lhs, ctx)
+      print_leaves(rhs, ctx)
+   elseif k == expr_kind.Let then
+      local name, ty, val, body = e:fields()
+      print("let var name: " .. tostring(name))
+      print_leaves(ty, ctx)
+      print_leaves(val, ctx)
+      print_leaves(body, ctx:extend(name, ty, val))
+   else
+      print(e)
+   end
+end
+
+local f, g, h, a, b, c = Consts("f, g, h, a, b, c")
+local N, M    = Consts("N, M")
+local x, y, z = Consts("x, y, z")
+assert(is_expr(f))
+
+local F = fun(h, mk_arrow(N, N),
+              Let(x, h(a), Eq(f(x), h(x))))
+print(F)
+print_leaves(F, context())
+
+
+