lean2/tests/lua/unify5.lua
Leonardo de Moura 60c60c6cf5 feat(library/kernel_bindings): add mk_choice_cnstr to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 13:39:21 -07:00

37 lines
1.3 KiB
Lua

local env = environment()
env = add_decl(env, mk_var_decl("N", Type))
local N = Const("N")
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_var_decl("b", N))
local f = Const("f")
local a = Const("a")
local b = Const("b")
local m1 = mk_metavar("m1", N)
local m2 = mk_metavar("m2", N)
local m3 = mk_metavar("m3", N)
local m4 = mk_metavar("m4", N)
local o = options({"unifier", "use_exceptions"}, false)
function display_solutions(m, ss)
local n = 0
for s in ss do
print("solution: " .. tostring(s:instantiate(m)))
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)
n = n + 1
end
end
cs = { mk_eq_cnstr(m1, f(m2, f(m3, m4))),
mk_choice_cnstr(m2, function(e, s, ngen) return {{a, justification(), {}}, {f(a, a), justification(), {}}} end),
mk_choice_cnstr(m3, function(e, s, ngen) return {{b, justification(), {}}, {f(b, b), justification(), {}}} end),
mk_choice_cnstr(m4, function(e, s, ngen) return {a, b} end)
}
display_solutions(m1, unify(env, cs, o))