Refactor IO

Stdlib/System/IO.juvix

@@ -1,40 +1,7 @@
 module Stdlib.System.IO;
 
-import Stdlib.Data.Nat open;
-import Stdlib.Data.String open;
-import Stdlib.Data.Bool open;
-import Stdlib.Data.Int open using {Int};
-
-builtin IO
-axiom IO : Type;
-
-syntax infixl 1 >>;
-builtin IO-sequence
-axiom >> : IO → IO → IO;
-
-builtin nat-print
-axiom printNat : Nat → IO;
-
-builtin string-print
-axiom printString : String → IO;
-
-builtin bool-print
-axiom printBool : Bool → IO;
-
-builtin int-print
-axiom printInt : Int → IO;
-
-builtin IO-readline
-axiom readLn : (String → IO) → IO;
-
-printNatLn : Nat → IO;
-printNatLn n := printNat n >> printString "\n";
-
-printStringLn : String → IO;
-printStringLn s := printString s >> printString "\n";
-
-printBoolLn : Bool → IO;
-printBoolLn b := printBool b >> printString "\n";
-
-printIntLn : Int → IO;
-printIntLn i := printInt i >> printString "\n";
+import Stdlib.System.IO.Base open public;
+import Stdlib.System.IO.Bool open public;
+import Stdlib.System.IO.Nat open public;
+import Stdlib.System.IO.Int open public;
+import Stdlib.System.IO.String open public;

Stdlib/System/IO/Base.juvix

@@ -0,0 +1,9 @@
+module Stdlib.System.IO.Base;
+
+builtin IO
+axiom IO : Type;
+
+syntax infixl 1 >>;
+builtin IO-sequence
+axiom >> : IO → IO → IO;
+

Stdlib/System/IO/Bool.juvix

@@ -0,0 +1,11 @@
+module Stdlib.System.IO.Bool;
+
+import Stdlib.System.IO.Base open;
+import Stdlib.Data.Bool open;
+import Stdlib.System.IO.String open;
+
+builtin bool-print
+axiom printBool : Bool → IO;
+
+printBoolLn : Bool → IO;
+printBoolLn b := printBool b >> printString "\n";

Stdlib/System/IO/Int.juvix

@@ -0,0 +1,6 @@
+module Stdlib.System.IO.Int;
+
+import Stdlib.System.IO.Base open;
+import Stdlib.Data.Int open using {Int};
+
+axiom printInt : Int → IO;

Stdlib/System/IO/Nat.juvix

@@ -0,0 +1,11 @@
+module Stdlib.System.IO.Nat;
+
+import Stdlib.System.IO.Base open;
+import Stdlib.Data.Nat open;
+import Stdlib.System.IO.String open;
+
+builtin nat-print
+axiom printNat : Nat → IO;
+
+printNatLn : Nat → IO;
+printNatLn n := printNat n >> printString "\n";

Stdlib/System/IO/String.juvix

@@ -0,0 +1,13 @@
+module Stdlib.System.IO.String;
+
+import Stdlib.System.IO.Base open;
+import Stdlib.Data.String open;
+
+builtin string-print
+axiom printString : String → IO;
+
+builtin IO-readline
+axiom readLn : (String → IO) → IO;
+
+printStringLn : String → IO;
+printStringLn s := printString s >> printString "\n";