tdd.idr

import Data.Vect

total isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

fourInts : Vect 4 Nat
fourInts = [1,2,3,4]

sixInts : Vect 6 Nat
sixInts = 5::6::7::8::9::10::[]


total words_len : Vect len String -> Vect len Nat
words_len [] = []
words_len (x :: xs) = length x :: words_len xs

insert : Ord elem =>  (x : elem) -> (xs_sorded : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

total ins_sort : Ord elem =>  Vect len elem -> Vect len elem
ins_sort [] = []
ins_sort (x :: xs) = let xs_sorded = ins_sort xs in
                        insert x xs_sorded

data PowerSource = Pedal | Petrol

data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol


total refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 40
refuel (Bus fuel) = Bus 60
refuel Bicycle impossible

total finToNat2 : Fin n -> Nat
finToNat2 FZ = Z
finToNat2 (FS x) = S (finToNat2 x)

partial vectTake : (i:Fin (S n)) -> Vect n x -> Vect (finToNat i) x
vectTake FZ _ = []
vectTake (FS y) (z :: xs) = z :: vectTake y xs

total tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} x xs = case integerToFin x n of
                      Nothing => Nothing
                      Just idx => Just(index idx xs)

total sumEntries: Num a=> (pos:Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                            Nothing => Nothing
                            Just pos => Just(index pos xs + index pos ys)