feat: add support for EIO

src/library/compiler/extern_attribute.cpp

@@ -38,6 +38,9 @@ static optional<unsigned> get_given_arity(environment const & env, name const &
     return optional<unsigned>(); // ignore big nums
 }
 
+bool is_io(expr const & type) {
+    return is_app_of(type, get_io_name()) || is_app_of(type, get_eio_name());
+}
 
 /*
   Similar to lean::get_arity, but adds `1` if resultant type is of the form `IO a`.
@@ -55,7 +58,7 @@ static unsigned get_arity_for_extern(expr type) {
         type = binding_body(type);
         r++;
     }
-    if (is_app_of(type, get_io_name())) {
+    if (is_io(type)) {
         r++;
     }
     return r;
@@ -92,7 +95,7 @@ bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bo
                 borrowed_args.resize(*given_arity, false);
                 return true;
             }
-        } else if (is_app_of(type, get_io_name())) {
+        } else if (is_io(type)) {
             /* See: `get_arity_for_extern`. We have special code for guessing
                the arity for external IO primitives. */
             borrowed_args.push_back(false);
@@ -134,7 +137,7 @@ optional<expr> get_extern_constant_ll_type(environment const & env, name const &
             } else {
                 ll_type = mk_runtime_type(st, lctx, type);
             }
-        } else if (is_app_of(type, get_io_name())) {
+        } else if (is_io(type)) {
             /* Add "world".
                See: `get_arity_for_extern`. We have special code for guessing
                the arity for external IO primitives. */

src/library/constants.cpp

@@ -108,6 +108,7 @@ name const * g_int_nat_abs = nullptr;
 name const * g_int_dec_lt = nullptr;
 name const * g_int_of_nat = nullptr;
 name const * g_inline = nullptr;
+name const * g_eio = nullptr;
 name const * g_io = nullptr;
 name const * g_ite = nullptr;
 name const * g_lc_proof = nullptr;
@@ -300,6 +301,7 @@ void initialize_constants() {
     g_int_dec_lt = new name{"Int", "decLt"};
     g_int_of_nat = new name{"Int", "ofNat"};
     g_inline = new name{"inline"};
+    g_eio = new name{"EIO"};
     g_io = new name{"IO"};
     g_ite = new name{"ite"};
     g_lc_proof = new name{"lcProof"};
@@ -493,6 +495,7 @@ void finalize_constants() {
     delete g_int_dec_lt;
     delete g_int_of_nat;
     delete g_inline;
+    delete g_eio;
     delete g_io;
     delete g_ite;
     delete g_lc_proof;
@@ -685,6 +688,7 @@ name const & get_int_nat_abs_name() { return *g_int_nat_abs; }
 name const & get_int_dec_lt_name() { return *g_int_dec_lt; }
 name const & get_int_of_nat_name() { return *g_int_of_nat; }
 name const & get_inline_name() { return *g_inline; }
+name const & get_eio_name() { return *g_eio; }
 name const & get_io_name() { return *g_io; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_lc_proof_name() { return *g_lc_proof; }

src/library/constants.h

@@ -110,6 +110,7 @@ name const & get_int_nat_abs_name();
 name const & get_int_dec_lt_name();
 name const & get_int_of_nat_name();
 name const & get_inline_name();
+name const & get_eio_name();
 name const & get_io_name();
 name const & get_ite_name();
 name const & get_lc_proof_name();

src/library/constants.txt

@@ -103,6 +103,7 @@ Int.natAbs
 Int.decLt
 Int.ofNat
 inline
+EIO
 IO
 ite
 lcProof