import("util.lua")
local menv = metavar_env()
assert(is_metavar_env(menv))
local m1   = menv:mk_metavar()
local m2   = menv:mk_metavar()
print(m1, m2)
assert(m1 ~= m2)
assert(m1:is_metavar())
assert(m2:is_metavar())
assert(not menv:is_assigned(m1))
assert(not menv:is_assigned(m2))
local ctx  = context():extend("x", Const("Int"))
local m3   = menv:mk_metavar(ctx)
local m4   = menv:mk_metavar(ctx, Const("Int"))
assert(not menv:is_assigned(m3))
assert(not menv:is_assigned(m4))
local ts1  = menv:get_timestamp()
local m5   = menv:mk_metavar()
local ts2  = menv:get_timestamp()
assert(ts2 > ts1)
print(menv:get_context(m3))
assert(menv:get_context(m3):size() == 1)
assert(menv:get_context(m1):size() == 0)
assert(menv:get_context{"M", 3}:size() == 1)
assert(not menv:has_type(m3))
assert(menv:has_type(m4))
assert(menv:has_type(m4:fields()))
assert(menv:get_type(m4) == Const("Int"))
assert(menv:get_type(m4:fields()) == Const("Int"))
local f, a, b = Consts("f, a, b")
menv:assign(m1, f(a, b))
assert(menv:is_assigned(m1))
assert(menv:is_assigned(m1:fields()))
local menv2 = menv:copy()
local as    = mk_assumption_justification(1)
menv:assign(m2, f(a, a), as)
assert(menv:is_assigned(m2))
assert(menv:is_assigned(m2:fields()))
assert(not menv2:is_assigned(m2))
assert(not menv2:is_assigned(m2:fields()))
assert(menv:get_justification(m1):is_null())
assert(menv:get_justification(m1:fields()):is_null())
assert(not menv:get_justification(m2):is_null())
local s1, jst1 = menv:get_subst_jst(m1)
assert(s1 == f(a, b))
assert(jst1:is_null())
local s2, jst2 = menv:get_subst_jst(m2)
assert(s2 == f(a, a))
assert(jst2:depends_on(as))
assert(menv:get_subst(m1) == f(a, b))
assert(menv:get_subst(m2:fields()) == f(a, a))
local counter = 0
menv:for_each_subst(function (m, s) print(m, s); counter = counter + 1 end)
assert(counter == 2)
assert(instantiate_metavars(f(m1, m2), menv) == f(f(a, b), f(a, a)))