12f79aa · Idris-dev · git.iko.soy

382

383 vadd : Vect n Int -> Vect n Int -> Vect n Int

384 vadd [] [] = []

385− vadd (x :: idris xs) (y :: ys) = x + y :: vadd xs ys

385+ vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys

386

387Using , we can set up a program so that it reads input from a user,

388checks that the input is valid (i.e both vectors contain integers, and

410

411This returns a dependent pair of a length, and a vector of that

412length, because we cannot know in advance how many integers the user

413−is going to input. One way to implement this function, using ``-1`` to

414−indicate the end of input, is shown in Listing [readvec]. This uses a

413+is going to input. We can use ``-1`` to indicate the end of input:

414+

415+.. code-block:: idris

416+

417+ read_vec : Eff (p ** Vect p Int) [STDIO]

418+ read_vec = do putStr "Number (-1 when done): "

419+ case the (Maybe Int) $ run (parseNumber (trim !getStr)) of

420+ Nothing => do putStrLn "Input error"

421+ read_vec

422+ Just v => if (v /= -1)

423+ then do (_ ** xs) <- read_vec

424+ pure (_ ** v :: xs)

425+ else pure (_ ** [])

426+ where

427+ parseNumber : String -> Eff Int [EXCEPTION String]

428+ parseNumber str

429+ = if all (\x => isDigit x || x == '-') (unpack str)

430+ then pure (cast str)

431+ else raise "Not a number"

432+

415−variation on ``parseNumber`` which does not require a number to be

433+This uses a variation on ``parseNumber`` which does not require a

416−within range.

434+number to be within range.

417

435

418Finally, we write a program which reads two vectors and prints the

436Finally, we write a program which reads two vectors and prints the

419result of pairwise addition of them, throwing an exception if the

437result of pairwise addition of them, throwing an exception if the

434does require that the lengths are checked and any discrepancy is dealt

452does require that the lengths are checked and any discrepancy is dealt

435with gracefully.

453with gracefully.

436

454

437−.. code-block:: idris

438−

439− read_vec : Eff (p ** Vect p Int) [STDIO]

440− read_vec = do putStr "Number (-1 when done): "

441− case run (parseNumber (trim !getStr)) of

442− Nothing => do putStrLn "Input error"

443− read_vec

444− Just v => if (v /= -1)

445− then do (_ ** xs) <- read_vec

446− pure (_ ** v :: xs)

447− else pure (_ ** [])

448− where

449− parseNumber : String -> Eff Int [EXCEPTION String]

450− parseNumber str

451− = if all (\x => isDigit x || x == '-') (unpack str)

452− then pure (cast str)

453− else raise "Not a number"

454

455

455Example: An Expression Calculator

456Example: An Expression Calculator

456=================================

457=================================