Serge D. Mechveliani mechvel at botik.ru
Tue Oct 2 12:07:07 CEST 2012

```People,
I have a beginner question on  IO  in the  Standard Libarary lib-0.6
(for Agda-2.3.0.1, MAlonzo).

The below small program intends to
(1) read a string  str  (like "1011")  from the file "inp.txt",
(2) convert  str  to  b : Bin,
(3) show b  to  bStr : String  and print  bStr  to the screen.

I know how to arrange (2) and (3).
But I need to find how to arrange the following operations related to
(1).

a) What to write in the below program instead of the `do' sequence
construct?
I recall that in  Haskell,  it is somewhat like
do
let (a, _) = readS coStr :: ...   -- reading from String
putStr (show a)

b) coStr <- readFile "inp.txt"     -- (what to write instead of `<-')
produces  coStr : Costring = Colist Char.
And it is difficult to find out  what is Colist.
But I hope that converting by  toList coStr  produces a reasonable
character list  chars : List Character.
Right?

c) About reading a natural. Having a string like  "103" : String,
what is the simplest way to convert it to  Nat  (unary natural) ?
For I observe that for  n : Nat,  the compiler converts  `n = 103'
to the needed number.

Thank you in advance for explanation,

------
Sergei

---------------------------------------------------------------
open import IO.Primitive
...
open import Prelude using ( toCostring )  -- by F. Kettelhoit

-- readFile : String Б├▓ IO Costring
main : IO Unit
main = do                               -- help needed with `do'
coStr : Colist Char
coStr <- readFile "inp.txt"    -- ? help needed

chars : List Char
chars = String.toList coStr    -- ? help needed
str : String
str = fromList chars

digs : List Bit
digs = stringToBits str        -- I can find this
b : Bin                        --
b = fromBits digs              --
bStr = showBin b               --

putStrLn (toCostring bStr)
-----------------------------------------------------------------

```