index.idr

module Main

-- Type for unit tests
Test : Bool -> Type
Test = so

-- ok has type (Test b), whenever b evaluates to True
ok : Test True
ok = oh

-- Lists

-- defined in Idris as:
-- data List : (a:Type) -> Type where
--    Nil : List a
--    (::) : a -> List a -> List a

index : List a -> Nat -> Maybe a
index Nil n = Nothing
index (x :: xs) Z = Just x
index (x :: xs) (S n) = index xs n

-- Unit tests
test1 : Test (index [3,5,7,9] 2 == Just 7)
test1 = ok

test2 : Test (index [3,5,7,9] 5 == Nothing)
test2 = ok

-- Vectors: lists of a given length
data Vec : Type -> Nat -> Type where
  Nil : Vec a 0
  (::) : a -> Vec a n -> Vec a (1 + n)


-- first is safe: it cannot be applied to an empty vector
first : Vec a (1 + n) -> a
first (x :: xs) = x

test3 : Test (first [1,2,3] == 1)
test3 = ok

-- test4 : Test (first [] == 1) -- Won't compile!
-- test4 = ok

-- index' is a safe vector lookup
-- (lt is 'lesser than' on natural numbers)
index' : Vec a m -> (n:Nat) -> Test (lt n m) -> a
index' (x :: xs) Z     p = x
index' (x :: xs) (S n) p = index' xs n p

-- Unit tests
test5 : Test (index' [3, 5, 7, 9] 2 ok == 7)
test5 = ok

-- test6 : Test (index' [3, 5, 7, 9] 5 ok == 13) -- Won't compile (5 is not lt 4)
-- test6 = ok

-- What happens when the vector or the index is a dynamic value ?

-- to convert from Integer to Nat
fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n = if (n > 0) then S (fromIntegerNat (n - 1)) else Z

-- read a Nat from stdin                                                                
getIndex : IO Nat
getIndex = do
  print "Enter index:"
  n <- map cast getLine
  return (fromIntegerNat n)

-- ask for an index and try indexing into [1,2,3,4,5]
dynIndex : IO ()
dynIndex = do
  i <- getIndex
  case choose (lt i 5) of -- compulsory dynamic check
    Left prf => print (index' [1,2,3,4,5] i prf)
    Right _  => print "The index is out of bounds"
  -- print (index' [1,2,3,4,5] i ok) -- i is unknown, this won't compile !

main : IO ()
main = dynIndex