michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): add universe constraint unifier test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-23 14:19:02 -07:00
parent a0e4dccdac
commit 7df397fe63
2 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/unifier.cpp
View file

@ -915,7 +915,6 @@ struct unifier_fn {
return true;
}
/** \brief Process the next constraint in the constraint queue m_cnstrs */
bool process_next() {
lean_assert(!m_cnstrs.empty());

27
tests/lua/unify6.lua Normal file
View file

@ -0,0 +1,27 @@
local env = environment()
local m1 = mk_meta_univ("m1")
local m2 = mk_meta_univ("m2")
local m3 = mk_meta_univ("m3")
local l1 = mk_param_univ("l1")
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):normalize()))
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_level_eq_cnstr(m1, max_univ(m2, max_univ(m2, l1, 1))),
mk_level_eq_cnstr(m2, level()+1),
mk_level_eq_cnstr(m3+1, m2+1)
}
display_solutions(m1, unify(env, cs, o))