60 lines
2.3 KiB
Lua
60 lines
2.3 KiB
Lua
local env = environment()
|
|
local N = Const("N")
|
|
local p = Const("p")
|
|
local q = Const("q")
|
|
local a = Const("a")
|
|
local b = Const("b")
|
|
local f = Const("f")
|
|
local H1 = Const("H1")
|
|
local H2 = Const("H2")
|
|
local And = Const("and")
|
|
local and_intro = Const("and_intro")
|
|
local A = Local("A", Prop)
|
|
local B = Local("B", Prop)
|
|
local C = Local("C", Prop)
|
|
env = add_decl(env, mk_var_decl("N", Type))
|
|
env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Prop)))
|
|
env = add_decl(env, mk_var_decl("q", mk_arrow(N, Prop)))
|
|
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N)))
|
|
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("and", mk_arrow(Prop, Prop, Prop)))
|
|
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, C, 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("Ax2", q(a)))
|
|
env = add_decl(env, mk_axiom("Ax3", q(b)))
|
|
local Ax1 = Const("Ax1")
|
|
local Ax2 = Const("Ax2")
|
|
local Ax3 = Const("Ax3")
|
|
local foo_intro = Const("foo_intro")
|
|
local foo_intro2 = Const("foo_intro2")
|
|
local ng = name_generator("foo")
|
|
local tc = type_checker(env, ng)
|
|
local m1 = mk_metavar("m1", Prop)
|
|
print("before is_def_eq")
|
|
assert(not tc:next_cnstr())
|
|
local tc = type_checker(env, ng)
|
|
assert(tc:is_def_eq(foo_intro(m1, q(a), q(a), Ax1), foo_intro(q(a), q(a), q(a), Ax2)))
|
|
local c = tc:next_cnstr()
|
|
assert(c)
|
|
assert(not tc:next_cnstr())
|
|
assert(c:lhs() == m1)
|
|
assert(c:rhs() == q(a))
|
|
local tc = type_checker(env, ng)
|
|
assert(not tc:next_cnstr())
|
|
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(not tc:next_cnstr())
|
|
local tc = type_checker(env, ng)
|
|
print("before failure")
|
|
assert(not pcall(function() print(tc:check(and_intro(m1, q(a), Ax1, Ax3))) end))
|
|
assert(not tc:next_cnstr())
|
|
print("before success")
|
|
print(tc:check(and_intro(m1, q(a), Ax1, Ax2)))
|
|
assert(tc:next_cnstr())
|
|
assert(not tc:next_cnstr())
|