81 lines
3.4 KiB
Lua
81 lines
3.4 KiB
Lua
|
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))))))))
|