import Data.Vect
import Data.List

-- Unlike arrays, lists in Idris are typed only by the
-- elements they contain (not the number of elements).
-- An empty list is represented as [].
main : IO ()
main = do
    let s : List String = []
    putStrLn $ "uninit: " ++ show s ++ " " ++ show (s == []) ++ " " ++ show (length s == 0)

    -- To create an empty list with non-zero length, we can use replicate.
    -- Here we make a list of Strings of length 3 (initially empty strings).
    let s = replicate 3 ""
    putStrLn $ "emp: " ++ show s ++ " len: " ++ show (length s)

    -- We can set and get just like with arrays.
    let s = ["a", "b", "c"]
    putStrLn $ "set: " ++ show s
    putStrLn $ "get: " ++ show (index 2 s)

    -- length returns the length of the list as expected.
    putStrLn $ "len: " ++ show (length s)

    -- In addition to these basic operations, lists support
    -- several more that make them richer than arrays.
    -- One is the (++) operator for concatenation.
    let s = s ++ ["d"]
    let s = s ++ ["e", "f"]
    putStrLn $ "apd: " ++ show s

    -- Lists can also be copied. Here we create a new list c
    -- that is a copy of s.
    let c = s
    putStrLn $ "cpy: " ++ show c

    -- Lists support a "slice" operator with the syntax
    -- take and drop. For example, this gets a slice
    -- of the elements s[2], s[3], and s[4].
    let l = take 3 $ drop 2 s
    putStrLn $ "sl1: " ++ show l

    -- This slices up to (but excluding) s[5].
    let l = take 5 s
    putStrLn $ "sl2: " ++ show l

    -- And this slices up from (and including) s[2].
    let l = drop 2 s
    putStrLn $ "sl3: " ++ show l

    -- We can declare and initialize a variable for list
    -- in a single line as well.
    let t = ["g", "h", "i"]
    putStrLn $ "dcl: " ++ show t

    -- Idris has built-in equality checking for lists.
    let t2 = ["g", "h", "i"]
    if t == t2
        then putStrLn "t == t2"
        else putStrLn "t != t2"

    -- Lists can be composed into multi-dimensional data
    -- structures. The length of the inner lists can
    -- vary, unlike with multi-dimensional vectors.
    let twoD = [[0], [1,2], [2,3,4]]
    putStrLn $ "2d: " ++ show twoD