git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/effects/vadd.idr
41 lines 1.4 kB history raw
1module Main
3import Effects
4import Effect.Exception
5import Effect.StdIO
7parseNumber : String -> { [EXCEPTION String] } Eff Int
8parseNumber str
9 = if all (\x => isDigit x || x == '-') (unpack str)
10 then pure (cast str)
11 else raise "Not a number"
13vadd : Vect n Int -> Vect n Int -> Vect n Int
14vadd [] [] = []
15vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
17vadd_check : Vect n Int -> Vect m Int ->
18 { [EXCEPTION String] } Eff (Vect m Int)
19vadd_check {n} {m} xs ys with (decEq n m)
20 vadd_check {n} {m=n} xs ys | (Yes Refl) = pure (vadd xs ys)
21 vadd_check {n} {m} xs ys | (No _) = raise "Length mismatch"
23read_vec : { [STDIO] } Eff (p ** Vect p Int)
24read_vec = do putStr "Number (-1 when done): "
25 case run {m=Maybe} (parseNumber (trim !getStr)) of
26 Nothing => do putStrLn "Input error"
27 read_vec
28 Just v => if (v /= -1)
29 then do (_ ** xs) <- read_vec
30 pure (_ ** v :: xs)
31 else pure (_ ** [])
33do_vadd : { [STDIO, EXCEPTION String] } Eff ()
34do_vadd = do putStrLn "Vector 1"
35 (_ ** xs) <- read_vec
36 putStrLn "Vector 2"
37 (_ ** ys) <- read_vec
38 putStrLn (show !(vadd_check xs ys))
40main : IO ()
41main = run do_vadd