git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/effects/ReadInt.idr
22 lines 740 B history raw
1module ReadInt
3import Effects
4import Effect.State
5import Effect.StdIO
7readInt : { [STATE (Vect n Int), STDIO] ==>
8 {ok} if ok then [STATE (Vect (S n) Int), STDIO]
9 else [STATE (Vect n Int), STDIO] } Eff Bool
10readInt = do let x = trim !getStr
11 case all isDigit (unpack x) of
12 False => pure False
13 True => do updateM (\xs => cast x ::xs)
14 pure True
16readN : (n : Nat) ->
17 { [STATE (Vect m Int), STDIO] ==>
18 [STATE (Vect (n + m) Int), STDIO] } Eff ()
19readN Z = pure ()
20readN {m} (S k) = case !readInt of
21 True => rewrite plusSuccRightSucc k m in readN k
22 False => readN (S k)