Skip to content

Commit

Permalink
Refactor IO (#66)
Browse files Browse the repository at this point in the history
  • Loading branch information
jonaprieto authored May 23, 2023
1 parent f07b4f9 commit d40b0b9
Show file tree
Hide file tree
Showing 6 changed files with 55 additions and 38 deletions.
43 changes: 5 additions & 38 deletions Stdlib/System/IO.juvix
Original file line number Diff line number Diff line change
@@ -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;
9 changes: 9 additions & 0 deletions Stdlib/System/IO/Base.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module Stdlib.System.IO.Base;

builtin IO
axiom IO : Type;

syntax infixl 1 >>;
builtin IO-sequence
axiom >> : IO → IO → IO;

11 changes: 11 additions & 0 deletions Stdlib/System/IO/Bool.juvix
Original file line number Diff line number Diff line change
@@ -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";
6 changes: 6 additions & 0 deletions Stdlib/System/IO/Int.juvix
Original file line number Diff line number Diff line change
@@ -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;
11 changes: 11 additions & 0 deletions Stdlib/System/IO/Nat.juvix
Original file line number Diff line number Diff line change
@@ -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";
13 changes: 13 additions & 0 deletions Stdlib/System/IO/String.juvix
Original file line number Diff line number Diff line change
@@ -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";

0 comments on commit d40b0b9

Please sign in to comment.