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

test(lua): add test for mutually recursive inductive type recursor/eliminator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-20 09:41:50 -07:00
parent 8a8c5a2b84
commit ddccca529a
1 changed files with 80 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

80
tests/lua/ind3.lua Normal file
View file

@ -0,0 +1,80 @@
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(env:normalize(env:type_check(t))))
end
local env = environment()
local nat = Const("nat")
local zero = Const("zero")
local succ = Const("succ")
env = add_inductive(env,
"nat", Type,
"zero", nat,
"succ", mk_arrow(nat, nat))
local a = Local("a", nat)
local b = Local("b", nat)
local n = Local("n", nat)
local r = Local("r", nat)
local nat_rec_nat = Const("nat_rec", {1})(Fun(a, nat))
local add = Fun({a, b}, nat_rec_nat(b, Fun({n, r}, succ(r)), a))
local tc = type_checker(env)
assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
succ(succ(succ(zero)))))
print(env:normalize(add(succ(succ(zero)), succ(succ(succ(zero))))))
local l = param_univ("l")
local U_l = mk_sort(l)
local U_l1 = mk_sort(max_univ(l, 1))
local tree_l = Const("tree", {l})
local tree_list_l = Const("tree_list", {l})
local A = Local("A", U_l)
local v = Local("v", A)
local children = Local("children", tree_list_l(A))
local head = Local("head", tree_l(A))
local tail = Local("tail", tree_list_l(A))
env = add_inductive(env, {l}, 1,
{"tree", Pi(A, U_l1),
"leaf", Pi(A, tree_l(A)),
"node", Pi({A, v, children}, tree_l(A))
},
{"tree_list", Pi(A, U_l1),
"nil", Pi(A, tree_list_l(A)),
"cons", Pi({A, head, tail}, tree_list_l(A))})
local tree_nat = Const("tree", {1})(nat)
local tree_list_nat = Const("tree_list", {1})(nat)
local t = Local("t", tree_nat)
local tl = Local("tl", tree_list_nat)
local tree_rec_nat = Const("tree_rec", {1, 1})(nat, Fun(t, nat), Fun(tl, nat))
local r1 = Local("r1", nat)
local r2 = Local("r2", nat)
local length_tree_nat = Fun(t, tree_rec_nat(zero,
Fun({a, tl, r}, succ(r)),
zero,
Fun({t, tl, r1, r2}, add(r1, r2)),
t))
display_type(env, length_tree_nat)
local leaf_nat = Const("leaf", {1})(nat)
local node_nat = Const("node", {1})(nat)
local nil_nat = Const("nil", {1})(nat)
local cons_nat = Const("cons", {1})(nat)
local one = succ(zero)
local two = succ(one)
local tree1 = node_nat(one, nil_nat)
local tree2 = node_nat(two, cons_nat(leaf_nat, cons_nat(leaf_nat, nil_nat)))
local tree3 = node_nat(one, cons_nat(tree1, cons_nat(tree2, nil_nat)))
local tree4 = node_nat(one, cons_nat(tree3, cons_nat(tree3, nil_nat)))
display_type(env, tree4)
print("norm(tree1): " .. tostring(env:normalize(length_tree_nat(tree1))))
print("norm(tree2): " .. tostring(env:normalize(length_tree_nat(tree2))))
print("norm(tree3): " .. tostring(env:normalize(length_tree_nat(tree3))))
print("norm(tree4): " .. tostring(env:normalize(length_tree_nat(tree4))))
assert(env:normalize(length_tree_nat(tree1)) == succ(zero))
assert(env:normalize(length_tree_nat(tree2)) == succ(zero))
assert(env:normalize(length_tree_nat(tree3)) == succ(succ(succ(zero))))
assert(env:normalize(length_tree_nat(tree4)) == succ(succ(succ(succ(succ(succ(succ(zero))))))))