fix(library/constants): more Io -> IO

script/gen_constants_cpp.py

@@ -20,8 +20,8 @@ def error(msg):
     exit(1)
 
 def to_c_const(s):
-    # insert '_' instead of '.' and between lower case and upper case
-    s = re.sub(r"\.|(?<=[a-z0-9])(?=[A-Z])", '_', s)
+    # insert '_' instead of '.', between lower case and upper case, and after 'IO'
+    s = re.sub(r"\.|(?<=[a-z0-9])(?=[A-Z])|(?<=IO)(?=[A-Z][a-z])", '_', s)
     return s.lower()
 
 def main(argv=None):

src/library/compiler/compiler.cpp

@@ -123,7 +123,7 @@ bool is_uint32_or_unit(expr const & type) {
         is_constant(type, get_punit_name());
 }
 
-/* Return true iff type is `list string -> io uint32` or `io uint32` */
+/* Return true iff type is `List String -> IO UInt32` or `IO UInt32` */
 bool is_main_fn_type(expr const & type) {
     if (is_arrow(type)) {
         expr d = binding_domain(type);
@@ -158,7 +158,7 @@ environment compile(environment const & env, options const & opts, names cs) {
 
     for (name const & c : cs) {
         if (is_main_fn(env, c) && !is_main_fn_type(env.get(c).get_type())) {
-            throw exception("invalid `main` function, it must have type `list string -> io uint32`");
+            throw exception("invalid `main` function, it must have type `List String -> IO UInt32`");
         }
     }
 

src/library/constants.cpp

@@ -418,14 +418,14 @@ void initialize_constants() {
     g_interactive_param_desc = new name{"interactive", "paramDesc"};
     g_interactive_parse = new name{"interactive", "parse"};
     g_io_core = new name{"ioCore"};
-    g_monad_io_impl = new name{"monadIoImpl"};
-    g_monad_io_terminal_impl = new name{"monadIoTerminalImpl"};
-    g_monad_io_file_system_impl = new name{"monadIoFileSystemImpl"};
-    g_monad_io_environment_impl = new name{"monadIoEnvironmentImpl"};
-    g_monad_io_process_impl = new name{"monadIoProcessImpl"};
-    g_monad_io_random_impl = new name{"monadIoRandomImpl"};
+    g_monad_io_impl = new name{"monadIOImpl"};
+    g_monad_io_terminal_impl = new name{"monadIOTerminalImpl"};
+    g_monad_io_file_system_impl = new name{"monadIOFileSystemImpl"};
+    g_monad_io_environment_impl = new name{"monadIOEnvironmentImpl"};
+    g_monad_io_process_impl = new name{"monadIOProcessImpl"};
+    g_monad_io_random_impl = new name{"monadIORandomImpl"};
     g_inline = new name{"inline"};
-    g_io = new name{"Io"};
+    g_io = new name{"IO"};
     g_ite = new name{"ite"};
     g_lc_proof = new name{"lcProof"};
     g_lc_unreachable = new name{"lcUnreachable"};

src/library/constants.txt

@@ -128,15 +128,14 @@ Int.ofNat
 Int.negSuccOfNat
 interactive.paramDesc
 interactive.parse
-ioCore
-monadIoImpl
-monadIoTerminalImpl
-monadIoFileSystemImpl
-monadIoEnvironmentImpl
-monadIoProcessImpl
-monadIoRandomImpl
+monadIOImpl
+monadIOTerminalImpl
+monadIOFileSystemImpl
+monadIOEnvironmentImpl
+monadIOProcessImpl
+monadIORandomImpl
 inline
-Io
+IO
 ite
 lcProof
 lcUnreachable