module Main

import Data.List

-- As an example of a generic function, slicesIndex takes
-- a list of any comparable type and an element of that
-- type and returns the index of the first occurrence of
-- v in s, or -1 if not present.
slicesIndex : Eq a => List a -> a -> Int
slicesIndex s v = case elemIndex v s of
                    Nothing -> -1
                    Just i  -> i

-- As an example of a generic type, List is already
-- a built-in generic type in Idris. We'll define a
-- custom LinkedList type to demonstrate.
data LinkedList : Type -> Type where
  Nil  : LinkedList a
  (::) : a -> LinkedList a -> LinkedList a

-- We can define functions on generic types just like we
-- do on regular types.
push : a -> LinkedList a -> LinkedList a
push x xs = x :: xs

-- allElements returns all the LinkedList elements as a list.
allElements : LinkedList a -> List a
allElements Nil = []
allElements (x :: xs) = x :: allElements xs

main : IO ()
main = do
  let s = ["foo", "bar", "zoo"]

  -- When invoking generic functions, we can often rely
  -- on type inference. Note that we don't have to
  -- specify the type when calling slicesIndex - the
  -- compiler infers it automatically.
  putStrLn $ "index of zoo: " ++ show (slicesIndex s "zoo")

  -- We could also specify the type explicitly if needed.
  let _ = slicesIndex {a = String} s "zoo"

  let lst = push 10 $ push 13 $ push 23 Nil
  putStrLn $ "list: " ++ show (allElements lst)

-- To run this program, save it as Generics.idr and use:
-- $ idris Generics.idr -o generics
-- $ ./generics
--
-- Output:
-- index of zoo: 2
-- list: [23, 13, 10]