2014-07-22 16:43:18 +00:00
|
|
|
local m = mk_metavar("m", Prop)
|
2014-05-01 22:30:30 +00:00
|
|
|
local s = substitution()
|
|
|
|
|
assert(not s:is_assigned(m))
|
|
|
|
|
assert(not s:is_expr_assigned("m"))
|
|
|
|
|
assert(not s:is_level_assigned("m"))
|
|
|
|
|
local f = Const("f")
|
|
|
|
|
local g = Const("g")
|
|
|
|
|
local a = Const("a")
|
|
|
|
|
local t = f(f(a))
|
|
|
|
|
s = s:assign(m, t)
|
|
|
|
|
assert(s:is_assigned(m))
|
|
|
|
|
assert(s:is_expr_assigned("m"))
|
|
|
|
|
assert(not s:is_level_assigned("m"))
|
|
|
|
|
assert(s:instantiate(g(m)) == g(t))
|
|
|
|
|
s = s:assign("m", a)
|
|
|
|
|
assert(s:instantiate(g(m)) == g(a))
|
|
|
|
|
local l = mk_level_one()
|
|
|
|
|
local u = mk_meta_univ("u")
|
|
|
|
|
s = s:assign(u, l)
|
|
|
|
|
assert(s:is_assigned(u))
|
|
|
|
|
assert(s:is_level_assigned("u"))
|
|
|
|
|
assert(not s:is_expr_assigned("u"))
|
|
|
|
|
assert(s:get_expr("m") == a)
|
2014-07-22 16:43:18 +00:00
|
|
|
local m2 = mk_metavar("m2", Prop)
|
2014-05-01 22:30:30 +00:00
|
|
|
s = s:assign(m2, f(m))
|
|
|
|
|
print(s:get_expr("m2"))
|
|
|
|
|
assert(s:occurs(m, f(m2)))
|
|
|
|
|
assert(s:occurs_expr("m", f(m2)))
|
|
|
|
|
print(s:get_level("u"))
|
|
|
|
|
print(s:instantiate(mk_sort(u)))
|
|
|
|
|
assert(s:instantiate(mk_sort(u)) == mk_sort(l))
|
|
|
|
|
assert(s:get_assignment(m) == a)
|
|
|
|
|
assert(s:get_assignment(u) == l)
|
|
|
|
|
assert(s:get_expr_assignment("m") == a)
|
|
|
|
|
assert(s:get_level_assignment("u") == l)
|
