diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index 25ace2892..dffe4faa8 100644 --- a/src/bindings/lua/expr.cpp +++ b/src/bindings/lua/expr.cpp @@ -265,7 +265,16 @@ static int expr_fields(lua_State * L) { case expr_kind::Var: lua_pushinteger(L, var_idx(e)); return 1; case expr_kind::Constant: return push_name(L, const_name(e)); case expr_kind::Type: return push_level(L, ty_level(e)); - case expr_kind::Value: return 0; + case expr_kind::Value: + if (is_nat_value(e)) { + return push_mpz(L, nat_value_numeral(e)); + } else if (is_int_value(e)) { + return push_mpz(L, int_value_numeral(e)); + } else if (is_real_value(e)) { + return push_mpq(L, real_value_numeral(e)); + } else { + return 0; + } case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2; case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2; case expr_kind::Lambda: @@ -389,6 +398,7 @@ static const struct luaL_Reg expr_m[] = { {"is_value", safe_function}, {"is_metavar", safe_function}, {"fields", safe_function}, + {"data", safe_function}, {"args", safe_function}, {"num_args", safe_function}, {"arg", safe_function}, @@ -408,7 +418,10 @@ static const struct luaL_Reg expr_m[] = { }; static int mk_nat_value(lua_State * L) { - return push_expr(L, mk_nat_value(to_mpz_ext(L, 1))); + mpz v = to_mpz_ext(L, 1); + if (v < 0) + throw exception("arg #1 must be non-negative"); + return push_expr(L, mk_nat_value(v)); } static int mk_int_value(lua_State * L) { diff --git a/tests/lua/num2.lua b/tests/lua/num2.lua new file mode 100644 index 000000000..0a54705c7 --- /dev/null +++ b/tests/lua/num2.lua @@ -0,0 +1,10 @@ +assert(nVal(10):data() == mpz(10)) +assert(not pcall(function() nVal(-10) end)) +assert(iVal(10):data() == mpz(10)) +assert(iVal(-10):data() == mpz(-10)) +assert(rVal(10):data() == mpq(10)) +assert(rVal(10):data() ~= mpz(10)) +assert(rVal("10/3"):data() == mpq(10)/3) +assert(rVal("-10/3"):data() == mpq(-10)/3) +assert(Const("a"):data() == name("a")) +