[Agda] read-output Nat example

[Sergei Meshveliani]

People,

The below program reads  n : Nat  from file and outputs the value of 
n * n.

Can it be written somewhat simpler/shorter?


--------------------------------------------------------------------
open import Foreign.Haskell
open import IO.Primitive
open import Data.String using (String; Costring; toCostring)
import Data.BoundedVec.Inefficient as BVec
import Data.Colist as Colist

open import Function        using (_∘_)
open import Data.List       using (List)
open import Data.Char       using (Char)
open import Data.Nat as Nat using (ℕ; _*_)
import Data.Nat.Show as NatShow

open import Int.Nat0 using (readNat)

main : IO Unit
main = (readFile "data.txt") >>= putStrLn ∘ toCostring ∘ g
       where
       g : Costring -> String          -- Costring = Colist Char 
       g coStr = NatShow.show (n * n)
                 where
                 numLength = 6

                 chars : List Char
                 chars = BVec.toList (Colist.take numLength coStr)

                 n : ℕ
                 n = readNat chars
----------------------------------------------------------------------


1. readNat  converts a list of decimal digits into  ℕ
            by the method of  d0 + 10*(d1 + 10*(d2 + ... + 10*dn)).

Has Standard library something to replace this?

2. Setting  numLength, 
   using BoundedVec, String - Costring, Colist ...
   looks rather messy.

Can the whole be somewhat simplified?

Thanks,

------
Sergei