{-# OPTIONS --cubical-compatible --guardedness #-}
module IO.Infinite where
open import Codata.Musical.Costring
open import Agda.Builtin.String
open import Data.Unit.Polymorphic.Base
import Data.Unit.Base as Unit0
open import IO.Base
import IO.Primitive as Prim
import IO.Primitive.Infinite as Prim
open import Level
private
variable
a : Level
getContents : IO Costring
getContents = lift Prim.getContents
private
lift′ : Prim.IO Unit0.⊤ → IO {a} ⊤
lift′ io = lift (io Prim.>>= λ _ → Prim.return _)
writeFile : String → Costring → IO {a} ⊤
writeFile f s = lift′ (Prim.writeFile f s)
appendFile : String → Costring → IO {a} ⊤
appendFile f s = lift′ (Prim.appendFile f s)
putStr : Costring → IO {a} ⊤
putStr s = lift′ (Prim.putStr s)
putStrLn : Costring → IO {a} ⊤
putStrLn s = lift′ (Prim.putStrLn s)