```
module Revise.IO where```

# Characters

```
open import Data.Char using (Char)```

The `Char` type:

``Char : Set    -- abstract``

Agda has character literals:

```
char_a : Char
char_a = 'a'```

Some operations on characters:

``````toNat : Char → ℕ   -- unicode code

_==_ : Char → Char → Bool

_≟_ : Decidable {A = Char} _≡_   -- see later``````

# Strings

```
open import Data.String using (String; Costring; toCostring; _++_)```

The `String` and `Costring` types:

``````String : Set     -- abstract

Costring : Set
Costring = Colist Char``````

Agda has string literals:

```
string_hello : String
string_hello = "hello"```

Some operations:

``````_++_ : String → String → String

toList : String → List Char

toCostring : String → Costring

toVec : (s : String) → Vec Char (length (toList s))

fromList : List Char → String``````

# Exercise

```
open import Data.List using (List; _∷_; [])

unlines : List String → String
unlines []       = ""
unlines (x ∷ xs) = x ++ "\n" ++ unlines xs```

# Equality on strings

``````_==_ : String → String → Bool

_≟_ : Decidable {A = String} _≡_``````

# The `IO` type

```
open import IO.Primitive```

`IO A` denotes a computation which may do I/O operations and at the end delivers a value of type `A`.

For example, `IO ℕ` is a computation which delivers a natural number.

``IO : Set → Set``

# The unit type

```
open import Foreign.Haskell using (Unit; unit)```

`Unit` is isomorphic to `⊤`:

``````data Unit : Set where
unit : Unit``````

# IO primitives

``````getContents : IO Costring
putStr      : Costring → IO Unit
putStrLn    : Costring → IO Unit

readFile    : String → IO Costring
writeFile   : String → Costring → IO Unit
appendFile  : String → Costring → IO Unit``````

# The `main` function

```
main : IO Unit
main = putStrLn (toCostring "Hello World!")```

# Compilation

Compilation of the `main` function: C-`c` C-`x` C-`c`
(or from the Emacs Agda menu)

If you get the error `Could not find module IO.FFI`, try to do

``````\$ cd <path-to-standard-library>
\$ cd ffi
\$ cabal install``````

# IO connectives: `return`

`return x` do no I/O operations just returns `x`

``return : {A : Set} → A → IO A``

This program does nothing:

```
main′ : IO Unit
main′ = return unit```

# IO connectives: `_>>=_`

The computation `m >>= f` first runs the computation `m` which delivers a return value `a`, then runs the computation `f a` and returns its return value.

``_>>=_  : {A B : Set} → IO A → (A → IO B) → IO B``

With `return`, `_>>=_` and the privitives we can construct lots of computations already!

This is how to add a new primitive if not present.

```
postulate
getLine : IO Costring

{-# COMPILED getLine getLine #-}```

The second argument of the `COMPILED` pragma should be a valid Haskell expression.

# Examples

```
main″ = getLine >>= putStrLn

open import Data.Colist renaming (_++_ to _+++_)

main‴ =
getLine >>= λ x →
putStrLn (toCostring "Hello " +++ x)```

# Exercise

Write a program which gets a line, and echoes it if the line is not empty.

# Infinite computations

```
open import Data.List renaming (_++_ to _++L_)
open import Coinduction

f : List Char → List Char → Costring → Costring
f acc [] [] = []
f acc [] ('\n' ∷ xs) = '\n' ∷ ♯ ( f [] (reverse acc ++L '\n' ∷ []) (♭ xs))
f acc [] (x ∷ xs) = x ∷ ♯ f (x ∷ acc) [] (♭ xs)
f acc (x ∷ xs) zs = x ∷ ♯ f acc xs zs

trans : Costring → Costring
trans = f [] []

main⁗ = getContents >>= λ x → putStr (trans x)```