lean2/tests/lua/unify1.lua
Leonardo de Moura 8e53643b61 feat(library/fo_unify): first order unification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:21:21 -08:00

30 lines
1.1 KiB
Lua

local f, g, a, b, c, x = Consts("f, g, a, b, c, x")
local m1 = mk_metavar("m1")
local m2 = mk_metavar("m2")
local m3 = mk_metavar("m3")
local s = fo_unify(f(m1, g(m2, c)), f(g(m2, a), g(m3, m3)))
assert(s)
assert(#s == 3)
assert(s:find(m2) == c)
assert(s:apply(f(m1, g(m2, c))) == s:apply(f(g(m2, a), g(m3, m3))))
assert(not fo_unify(f(a), g(m2)))
function must_unify(t1, t2)
local s = fo_unify(t1, t2)
assert(s)
print(t1, t2, s:apply(t1))
assert(s:apply(t1) == s:apply(t2))
end
Bool = Const("Bool")
must_unify(Eq(a, m1), Eq(m2, m2))
must_unify(Type(), m1)
must_unify(fun(x, Bool, x), fun(x, Bool, m1))
must_unify(Pi(x, Bool, x), Pi(x, Bool, m1))
must_unify(Var(0), m1)
must_unify(f(m1, m2, m3), f(m1, m1, m2))
must_unify(mk_let("x", f(b), Var(0)), mk_let("y", f(m1), Var(0)))
assert(not fo_unify(mk_let("x", Bool, f(b), Var(0)), mk_let("y", f(m1), Var(0))))
assert(not fo_unify(mk_let("x", f(b), Var(0)), mk_let("y", Bool, f(m1), Var(0))))
must_unify(mk_let("x", Bool, f(b), Var(0)), mk_let("y", Bool, f(m1), Var(0)))
assert(not fo_unify(mk_let("x", Bool, f(b), Var(0)), fun(x, Bool, x)))
must_unify(iVal(10), m1)
must_unify(iVal(10), iVal(10))