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

fix(tests/lua/tc_bug1): update test to reflect recent changes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 16:50:30 -07:00
parent 4bc1f3cf81
commit d027c90bd0
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lua/tc_bug1.lua
View file

@ -11,6 +11,7 @@ local And = Const("and")
local and_intro = Const("and_intro") local and_intro = Const("and_intro")
local A = Local("A", Bool) local A = Local("A", Bool)
local B = Local("B", Bool) local B = Local("B", Bool)
local C = Local("C", Bool)
env = add_decl(env, mk_var_decl("N", Type)) env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Bool))) env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Bool)))
env = add_decl(env, mk_var_decl("q", mk_arrow(N, Bool))) env = add_decl(env, mk_var_decl("q", mk_arrow(N, Bool)))
@ -19,8 +20,8 @@ env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_var_decl("b", N)) env = add_decl(env, mk_var_decl("b", N))
env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool))) env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool)))
env = add_decl(env, mk_var_decl("and_intro", Pi({A, B}, mk_arrow(A, B, And(A, B))))) env = add_decl(env, mk_var_decl("and_intro", Pi({A, B}, mk_arrow(A, B, And(A, B)))))
env = add_decl(env, mk_var_decl("foo_intro", Pi({A, B}, mk_arrow(B, B)))) env = add_decl(env, mk_var_decl("foo_intro", Pi({A, B, C}, mk_arrow(B, B))))
env = add_decl(env, mk_var_decl("foo_intro2", Pi({A, B}, mk_arrow(B, B)))) env = add_decl(env, mk_var_decl("foo_intro2", Pi({A, B, C}, mk_arrow(B, B))))
env = add_decl(env, mk_axiom("Ax1", q(a))) env = add_decl(env, mk_axiom("Ax1", q(a)))
env = add_decl(env, mk_axiom("Ax2", q(a))) env = add_decl(env, mk_axiom("Ax2", q(a)))
env = add_decl(env, mk_axiom("Ax3", q(b))) env = add_decl(env, mk_axiom("Ax3", q(b)))
@ -38,13 +39,18 @@ assert(not tc:is_def_eq(and_intro(m1, q(a)), and_intro(q(a), q(b))))
assert(#cs == 0) assert(#cs == 0)
local cs = {} local cs = {}
local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
assert(tc:is_def_eq(foo_intro(m1, q(a), Ax1), foo_intro(q(a), q(a), Ax2))) assert(tc:is_def_eq(foo_intro(m1, q(a), q(a), Ax1), foo_intro(q(a), q(a), q(a), Ax2)))
assert(#cs == 1) -- constraint is used, but there is an alternative that does not use it assert(#cs == 1) -- constraint is used, but there is an alternative that does not use it
assert(cs[1]:lhs() == m1) assert(cs[1]:lhs() == m1)
assert(cs[1]:rhs() == q(a)) assert(cs[1]:rhs() == q(a))
cs = {} cs = {}
local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)
assert(tc:is_def_eq(foo_intro(m1, q(a), Ax1), foo_intro2(q(a), q(a), Ax2))) assert(#cs == 0)
print(tostring(foo_intro) .. " : " .. tostring(tc:check(foo_intro)))
print(tostring(foo_intro2) .. " : " .. tostring(tc:check(foo_intro2)))
assert(tc:is_def_eq(foo_intro, foo_intro2))
print("before is_def_eq2")
assert(tc:is_def_eq(foo_intro(m1, q(a), q(b), Ax1), foo_intro2(q(a), q(a), q(a), Ax2)))
assert(#cs == 0) -- constraint should be ignored since we have shown definitional equality using proof irrelevance assert(#cs == 0) -- constraint should be ignored since we have shown definitional equality using proof irrelevance
cs = {} cs = {}
local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end) local tc = type_checker(env, ng, function (c) print(c); cs[#cs+1] = c end)