lean2/tests/lua/unify1.lua

58 lines
2.5 KiB
Lua
Raw Normal View History

function test_unify_simple(lhs, rhs, expected)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(expected))
s = substitution()
r = unify_simple(s, lhs, rhs, justification())
if r == unify_status.Solved then
s:for_each_expr(function(n, v, j)
print(" " .. tostring(n) .. " := " .. tostring(v))
end)
s:for_each_level(function(n, v, j)
print(" " .. tostring(n) .. " := " .. tostring(v))
end)
end
if r ~= expected then print("r: " .. r) end
assert(r == expected)
end
local f = Const("f")
local a = Const("a")
local l1 = mk_local("l1", "x", Prop)
local l2 = mk_local("l2", "y", Prop)
local l3 = mk_local("l3", "z", Prop)
local m = mk_metavar("m", Prop)
test_unify_simple(m(l1, l2), f(f(a, l1), l1), unify_status.Solved)
test_unify_simple(m(l1, l2), m(l1, l2), unify_status.Solved)
test_unify_simple(m(l1, l2), m(l2, l2), unify_status.Unsupported)
test_unify_simple(m(l1, l2), f(f(l2, l1), l1), unify_status.Solved)
test_unify_simple(m(l1, a), f(f(a), l1), unify_status.Unsupported)
test_unify_simple(f(m, a), f(f(a), l1), unify_status.Unsupported)
test_unify_simple(m(l1, l2), f(f(m), l1), unify_status.Failed)
test_unify_simple(m(l1, l2), f(f(l3), l1), unify_status.Failed)
test_unify_simple(m, f(a), unify_status.Solved)
test_unify_simple(f(a), f(a), unify_status.Solved)
test_unify_simple(f(a), f(f(a)), unify_status.Failed)
test_unify_simple(f(f(a, l1), l1), m(l1, l2), unify_status.Solved)
test_unify_simple(m(l1, l1), f(f(l2, l1), l1), unify_status.Unsupported)
test_unify_simple(m(l1, l2, l1), f(f(l2, l1), l1), unify_status.Unsupported)
test_unify_simple(m(l1, l2), Fun(l3, f(f(a, l1), l3)), unify_status.Solved)
local zero = level()
local one = zero+1
local l = mk_param_univ("l")
local u = mk_global_univ("u")
local m = mk_meta_univ("m")
test_unify_simple(m+1, u+1, unify_status.Solved)
test_unify_simple(u+1, u+1, unify_status.Solved)
test_unify_simple(u+1, m+1, unify_status.Solved)
test_unify_simple(m, u+1, unify_status.Solved)
test_unify_simple(m, max_univ(u, l), unify_status.Solved)
test_unify_simple(max_univ(u, l), max_univ(u, l), unify_status.Solved)
test_unify_simple(m+1, m+1, unify_status.Solved)
test_unify_simple(l, l+1, unify_status.Failed)
test_unify_simple(m, m+1, unify_status.Failed)
test_unify_simple(m, max_univ(m, u), unify_status.Unsupported)
test_unify_simple(m, max_univ(m, u)+1, unify_status.Failed)
test_unify_simple(m+2, m+1, unify_status.Failed)
test_unify_simple(u+2, m+1, unify_status.Solved)