Add postulated IO bindings

lib/Haskell/Law/Applicative.agda

@@ -2,5 +2,6 @@ module Haskell.Law.Applicative where
 
 open import Haskell.Law.Applicative.Def    public
 open import Haskell.Law.Applicative.Either public
+open import Haskell.Law.Applicative.IO     public
 open import Haskell.Law.Applicative.List   public
 open import Haskell.Law.Applicative.Maybe  public

lib/Haskell/Law/Applicative/IO.agda

@@ -0,0 +1,12 @@
+module Haskell.Law.Applicative.IO where
+
+open import Haskell.Prim
+open import Haskell.Prim.IO
+
+open import Haskell.Prim.Applicative
+
+open import Haskell.Law.Applicative.Def
+
+open import Haskell.Law.Functor.IO
+
+instance postulate iLawfulApplicativeIO : IsLawfulApplicative IO

lib/Haskell/Law/Functor.agda

@@ -2,5 +2,6 @@ module Haskell.Law.Functor where
 
 open import Haskell.Law.Functor.Def    public
 open import Haskell.Law.Functor.Either public
+open import Haskell.Law.Functor.IO     public
 open import Haskell.Law.Functor.List   public
 open import Haskell.Law.Functor.Maybe  public

lib/Haskell/Law/Functor/IO.agda

@@ -0,0 +1,10 @@
+module Haskell.Law.Functor.IO where
+
+open import Haskell.Prim
+open import Haskell.Prim.IO
+
+open import Haskell.Prim.Functor
+
+open import Haskell.Law.Functor.Def
+
+instance postulate isLawFulFunctorIO : IsLawfulFunctor IO

lib/Haskell/Law/Monad.agda

@@ -2,5 +2,6 @@ module Haskell.Law.Monad where
 
 open import Haskell.Law.Monad.Def    public
 open import Haskell.Law.Monad.Either public
+open import Haskell.Law.Monad.IO     public
 open import Haskell.Law.Monad.List   public
 open import Haskell.Law.Monad.Maybe  public

lib/Haskell/Law/Monad/IO.agda

@@ -0,0 +1,12 @@
+module Haskell.Law.Monad.IO where
+
+open import Haskell.Prim
+open import Haskell.Prim.IO
+
+open import Haskell.Prim.Monad
+
+open import Haskell.Law.Monad.Def
+
+open import Haskell.Law.Applicative.IO
+
+instance postulate iLawfulMonadIO : IsLawfulMonad IO

lib/Haskell/Prelude.agda

@@ -26,6 +26,7 @@ open import Haskell.Prim.Foldable    public
 open import Haskell.Prim.Functor     public
 open import Haskell.Prim.Int         public
 open import Haskell.Prim.Integer     public
+open import Haskell.Prim.IO          public
 open import Haskell.Prim.List        public
 open import Haskell.Prim.Maybe       public
 open import Haskell.Prim.Monad       public

lib/Haskell/Prim/Applicative.agda

@@ -4,6 +4,7 @@ open import Haskell.Prim
 open import Haskell.Prim.Either
 open import Haskell.Prim.Foldable
 open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Monoid
@@ -85,3 +86,5 @@ instance
     .pure x → mempty ; mempty ; mempty ; x ; tt
     ._<*>_ (a ; b ; c ; f ; tt) (a₁ ; b₁ ; c₁ ; x ; tt) →
       a <> a₁ ; b <> b₁ ; c <> c₁ ; f x ; tt
+
+instance postulate iApplicativeIO : Applicative IO

lib/Haskell/Prim/Functor.agda

@@ -3,6 +3,7 @@ module Haskell.Prim.Functor where
 
 open import Haskell.Prim
 open import Haskell.Prim.Either
+open import Haskell.Prim.IO
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Tuple
@@ -77,3 +78,5 @@ instance
 
   iFunctorTuple₄ : Functor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
   iFunctorTuple₄ = fmap= λ f (x ; y ; z ; w ; tt) → x ; y ; z ; f w ; tt
+
+instance postulate iFunctiorIO : Functor IO

lib/Haskell/Prim/IO.agda

@@ -0,0 +1,27 @@
+module Haskell.Prim.IO where
+
+open import Haskell.Prim
+open import Haskell.Prim.Show
+open import Haskell.Prim.String
+
+postulate IO : ∀{a} → Set a → Set a
+
+FilePath = String
+
+postulate
+  -- Input functions
+  interact       : (String → String) → IO ⊤
+  getContents    : IO String
+  getLine        : IO String
+  getChar        : IO Char
+
+  -- Output functions
+  print          : ⦃ Show a ⦄ → a → IO ⊤
+  putChar        : Char → IO ⊤
+  putStr         : String → IO ⊤
+  putStrLn       : String → IO ⊤
+
+  -- Files
+  readFile       : FilePath → IO String
+  writeFile      : FilePath → String → IO ⊤
+  appendFile     : FilePath → String → IO ⊤

lib/Haskell/Prim/Monad.agda

@@ -6,6 +6,7 @@ open import Haskell.Prim.Applicative
 open import Haskell.Prim.Either
 open import Haskell.Prim.Foldable
 open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Monoid
@@ -97,6 +98,8 @@ instance
     case k x of λ where
       (a₁ ; b₁ ; c₁ ; y ; tt) → a <> a₁ ; b <> b₁ ; c <> c₁ ; y ; tt
 
+instance postulate iMonadIO : Monad IO
+
 record MonadFail (m : Set → Set) : Set₁ where
   field
     fail : String → m a

test/AllTests.agda

@@ -55,6 +55,8 @@ import TypeOperators
 import ErasedTypeArguments
 import TypeOperatorExport
 import TypeOperatorImport
+import IOFile
+import IOInput
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -110,4 +112,6 @@ import TypeOperators
 import ErasedTypeArguments
 import TypeOperatorExport
 import TypeOperatorImport
+import IOFile
+import IOInput
 #-}

test/IOFile.agda

@@ -0,0 +1,13 @@
+module IOFile where
+
+open import Haskell.Prelude
+
+main : IO ⊤
+main = do file ← readFile "IOFile.agda"
+          writeFile "IOFile2.agda" file
+          appendFile "IOFile2.agda" "-- Written by appendFile"
+          file2 ← readFile "IOFile2.agda"
+          print file2
+          return tt
+
+{-# COMPILE AGDA2HS main #-}

test/IOInput.agda

@@ -0,0 +1,11 @@
+module IOInput where
+
+open import Haskell.Prelude
+
+main : IO ⊤
+main = do putStrLn "Write something "
+          x ← getLine
+          putStr $ "You wrote: " ++ x
+          return tt
+
+{-# COMPILE AGDA2HS main #-}

test/golden/AllTests.hs

@@ -53,4 +53,6 @@ import TypeOperators
 import ErasedTypeArguments
 import TypeOperatorExport
 import TypeOperatorImport
+import IOFile
+import IOInput
 

test/golden/IOFile.hs

@@ -0,0 +1,11 @@
+module IOFile where
+
+main :: IO ()
+main
+  = do file <- readFile "IOFile.agda"
+       writeFile "IOFile2.agda" file
+       appendFile "IOFile2.agda" "-- Written by appendFile"
+       file2 <- readFile "IOFile2.agda"
+       print file2
+       return ()
+

test/golden/IOInput.hs

@@ -0,0 +1,9 @@
+module IOInput where
+
+main :: IO ()
+main
+  = do putStrLn "Write something "
+       x <- getLine
+       putStr $ "You wrote: " ++ x
+       return ()
+