3e1fd06903
After this commit, a value of type 'expr' cannot be a reference to nullptr. This commit also fixes several bugs due to the use of 'null' expressions. TODO: do the same for kernel objects, sexprs, etc. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
47 lines
1.4 KiB
Lua
47 lines
1.4 KiB
Lua
function print_leaves(e, ctx)
|
|
if (not e) 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())
|