From d3756fd915c124eb343fdb762b9ea635d618ba2e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Jan 2019 12:50:11 -0800
Subject: [PATCH] feat(library/compiler): add `_void` type for LLNF format

---
 src/library/compiler/llnf.cpp |  3 +--
 src/library/compiler/util.cpp | 11 +++++++++++
 src/library/compiler/util.h   |  3 +++
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 3e33e0a895..13a8add619 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -1414,8 +1414,7 @@ class explicit_rc_fn {
     }
 
     expr mk_void_type() {
-        /* TODO(Leo): add void type? */
-        return mk_enf_neutral();
+        return mk_llnf_void_type();
     }
 
     name next_name() {
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 9deb75c4a5..6f456638f9 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -336,6 +336,7 @@ unsigned get_lcnf_size(environment const & env, expr e) {
 static expr * g_neutral_expr     = nullptr;
 static expr * g_unreachable_expr = nullptr;
 static expr * g_object_type      = nullptr;
+static expr * g_void_type        = nullptr;
 
 expr mk_enf_unreachable() {
     return *g_unreachable_expr;
@@ -349,6 +350,10 @@ expr mk_enf_object_type() {
     return *g_object_type;
 }
 
+expr mk_llnf_void_type() {
+    return *g_void_type;
+}
+
 expr mk_enf_neutral_type() {
     return *g_neutral_expr;
 }
@@ -365,6 +370,10 @@ bool is_enf_object_type(expr const & e) {
     return e == *g_object_type;
 }
 
+bool is_llnf_void_type(expr const & e) {
+    return e == *g_void_type;
+}
+
 bool is_runtime_builtin_type(name const & n) {
     /* TODO(Leo): use an attribute? */
     return
@@ -468,6 +477,7 @@ void initialize_compiler_util() {
     g_neutral_expr     = new expr(mk_constant("_neutral"));
     g_unreachable_expr = new expr(mk_constant("_unreachable"));
     g_object_type      = new expr(mk_constant("_obj"));
+    g_void_type        = new expr(mk_constant("_void"));
     g_usize            = new expr(mk_constant(get_usize_name()));
     g_uint8            = new expr(mk_constant(get_uint8_name()));
     g_uint16           = new expr(mk_constant(get_uint16_name()));
@@ -511,6 +521,7 @@ void finalize_compiler_util() {
     delete g_neutral_expr;
     delete g_unreachable_expr;
     delete g_object_type;
+    delete g_void_type;
     delete g_usize;
     delete g_uint8;
     delete g_uint16;
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index b16ca77cff..0dddb6eb16 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -125,10 +125,13 @@ expr mk_enf_neutral();
 expr mk_enf_unreachable();
 expr mk_enf_object_type();
 expr mk_enf_neutral_type();
+/* "Void" type used in LLNF. Remark: the ENF types neutral and object are also used in LLNF. */
+expr mk_llnf_void_type();
 
 bool is_enf_neutral(expr const & e);
 bool is_enf_unreachable(expr const & e);
 bool is_enf_object_type(expr const & e);
+bool is_llnf_void_type(expr const & e);
 
 expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e);