git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/tutorial006/tutorial006c.idr
20 lines 744 B history raw
1import Effects
2import Effect.Exception
3import Effect.StdIO
4import Data.Vect
6read_vec : Eff (p ** Vect p Int) [STDIO]
7read_vec = do putStr "Number (-1 when done): "
8 case run (parseNumber (trim !getStr)) of
9 Nothing => do putStrLn "Input error"
10 read_vec
11 Just v => if (v /= -1)
12 then do (_ ** xs) <- read_vec
13 pure (_ ** v :: xs)
14 else pure (_ ** [])
15 where
16 parseNumber : String -> Eff Int [EXCEPTION String]
17 parseNumber str
18 = if all (\x => isDigit x || x == '-') (unpack str)
19 then pure (cast str)
20 else raise "Not a number"