test(lua/metavar_env): add missing tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/bindings/lua/metavar_env.cpp

@@ -133,6 +133,10 @@ static int menv_copy(lua_State * L) {
     return push_metavar_env(L, metavar_env(to_metavar_env(L, 1)));
 }
 
+static int instantiate_metavars(lua_State * L) {
+    return push_expr(L, instantiate_metavars(to_expr(L, 1), to_metavar_env(L, 2)));
+}
+
 static const struct luaL_Reg metavar_env_m[] = {
     {"__gc",              metavar_env_gc}, // never throws
     {"mk_metavar",        safe_function<menv_mk_metavar>},
@@ -144,7 +148,7 @@ static const struct luaL_Reg metavar_env_m[] = {
     {"assign",            safe_function<menv_assign>},
     {"get_subst",         safe_function<menv_get_subst>},
     {"get_justification", safe_function<menv_get_justification>},
-    {"get_subt_jst",      safe_function<menv_get_subst_jst>},
+    {"get_subst_jst",     safe_function<menv_get_subst_jst>},
     {"for_each_subst",    safe_function<menv_for_each_subst>},
     {"copy",              safe_function<menv_copy>},
     {0, 0}
@@ -158,5 +162,6 @@ void open_metavar_env(lua_State * L) {
 
     SET_GLOBAL_FUN(mk_metavar_env,   "metavar_env");
     SET_GLOBAL_FUN(metavar_env_pred, "is_metavar_env");
+    SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
 }
 }

tests/lua/menv1.lua

@@ -0,0 +1,54 @@
+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)))