From 7b8bd97699be62daf957a6b24980cd5fb32f64a8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Nov 2013 19:06:25 -0800
Subject: [PATCH] feat(lua/expr): add method for extracting semantic attachment
 data

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/expr.cpp | 17 +++++++++++++++--
 tests/lua/num2.lua        | 10 ++++++++++
 2 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 tests/lua/num2.lua

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<expr_is_value>},
     {"is_metavar",      safe_function<expr_is_metavar>},
     {"fields",          safe_function<expr_fields>},
+    {"data",            safe_function<expr_fields>},
     {"args",            safe_function<expr_args>},
     {"num_args",        safe_function<expr_num_args>},
     {"arg",             safe_function<expr_arg>},
@@ -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"))
+