lean2/tests/lua/expr6.lua
Leonardo de Moura 1bf6051866 test(lua): expr LUA API test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 15:29:31 -08:00

51 lines
1.4 KiB
Lua

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())