[Agda] readFile and output

[Serge D. Mechveliani]

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  
     str <- readFile "inp.txt"
     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 Foreign.Haskell
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)
-----------------------------------------------------------------