[Agda] Agda IO - accessing command-line arguments

[Andreas Abel]

Hi Stephan,

On 18.07.12 6:31 PM, stvienna wiener wrote:
> Hello,
>
> Today I was experimenting with Agda and IO. However, I can’t find any
> up-to-date information on how to access command-line arguments in Agda.
> How can I use “getArgs” (or similar) using the IO module from the
> std-library?

I'd expect it works analogously to the bindings in IO.Primitive in the 
standard library.  It seems all you need is to postulate getArgs and 
then give the {-# COMPILED #-} pragma.  Did you try this already?
[I have not tested it, though, so I might be wrong...]

> Also, is there standard and also efficient way to convert/parse a String
> to a natural number (e.g., “20” -> 20)?

Frederik has it in the Agda Prelude:

   https://github.com/fkettelhoit/agda-prelude/blob/master/Prelude.agda

I copy the code here:

charToℕ : Char → Maybe ℕ
charToℕ '0' = just 0
charToℕ '1' = just 1
charToℕ '2' = just 2
charToℕ '3' = just 3
charToℕ '4' = just 4
charToℕ '5' = just 5
charToℕ '6' = just 6
charToℕ '7' = just 7
charToℕ '8' = just 8
charToℕ '9' = just 9
charToℕ _   = nothing

stringToℕ' : List Char → (acc : ℕ) → Maybe ℕ
stringToℕ' []       acc = just acc
stringToℕ' (x ∷ xs) acc = charToℕ x >>= λ n → stringToℕ' xs $ 10 * acc + n

stringToℕ : String → Maybe ℕ
stringToℕ s = stringToℕ' (toList s) 0


There is also Data.Digit, but it does not seem to go all the way from 
String to Nat.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/