From c883c638d64f6c8cf55d8632f4305ccf6a16e949 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 May 2014 16:50:43 -0700
Subject: [PATCH] feat(library/kernel_bindings): expose expression tags in the
 Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/kernel_bindings.cpp |  8 ++++++++
 tests/lua/tag1.lua              | 17 +++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 tests/lua/tag1.lua

diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index ebb616f038..dcd273a7b8 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -481,6 +481,12 @@ static int macro_def(lua_State * L) { return push_macro_definition(L, macro_def(
 static int macro_num_args(lua_State * L) { return push_integer(L, macro_num_args(to_macro_app(L, 1))); }
 static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), luaL_checkinteger(L, 2))); }
 
+static int expr_set_tag(lua_State * L) { to_expr(L, 1).set_tag(luaL_checkinteger(L, 2)); return 0; }
+static int expr_tag(lua_State * L) {
+    auto t = to_expr(L, 1).get_tag();
+    return (t == nulltag) ? push_nil(L) : push_integer(L, t);
+}
+
 static const struct luaL_Reg expr_m[] = {
     {"__gc",             expr_gc}, // never throws
     {"__tostring",       safe_function<expr_tostring>},
@@ -527,6 +533,8 @@ static const struct luaL_Reg expr_m[] = {
     {"is_eqp",           safe_function<expr_is_eqp>},
     {"is_lt",            safe_function<expr_is_lt>},
     {"hash",             safe_function<expr_hash>},
+    {"tag",              safe_function<expr_tag>},
+    {"set_tag",          safe_function<expr_set_tag>},
     {0, 0}
 };
 
diff --git a/tests/lua/tag1.lua b/tests/lua/tag1.lua
new file mode 100644
index 0000000000..ac1035375f
--- /dev/null
+++ b/tests/lua/tag1.lua
@@ -0,0 +1,17 @@
+local f  = Const("f")
+local x  = Const("x")
+local a  = Const("a")
+local t1 = f(x, a, Var(1))
+local t2 = Fun(x, Bool, t1)
+assert(not t2:tag())
+assert(not t2:binder_body():tag())
+t2:set_tag(2)
+t2:binder_body():set_tag(1)
+assert(t2:tag() == 2)
+assert(t2:binder_body():tag() == 1)
+print(t2)
+local new_t2 = t2:instantiate(Const("b"))
+assert(new_t2:tag() == 2)
+assert(new_t2:binder_body():tag() == 1)
+assert(not (t2 == new_t2))
+