module Main

import Data.Vect

main : IO ()
main = do
    -- Here we create a vector `a` that will hold exactly 5 Ints.
    -- By default, a vector is initialized with zeros.
    let a : Vect 5 Int = replicate 5 0
    putStrLn $ "emp: " ++ show (toList a)

    -- We can set a value at an index using the `updateAt` function,
    -- and get a value with index access.
    let a' = updateAt 4 (const 100) a
    putStrLn $ "set: " ++ show (toList a')
    putStrLn $ "get: " ++ show (index 4 a')

    -- The `length` function returns the length of a vector.
    putStrLn $ "len: " ++ show (length a')

    -- Use this syntax to declare and initialize a vector in one line.
    let b : Vect 5 Int = [1, 2, 3, 4, 5]
    putStrLn $ "dcl: " ++ show (toList b)

    -- In Idris, we can't have the compiler count the number of elements for us,
    -- we need to specify the length explicitly.

    -- Idris doesn't have a direct equivalent to Go's slice notation with `:`
    -- for initializing arrays with zeroed elements in between.
    -- We can achieve a similar effect using `replicate` and `++`:
    let c : Vect 5 Int = [100] ++ replicate 3 0 ++ [500]
    putStrLn $ "idx: " ++ show (toList c)

    -- Vector types in Idris are already multi-dimensional.
    -- Here's an example of a 2D vector:
    let twoD : Vect 2 (Vect 3 Int) = [[0, 1, 2], [1, 2, 3]]
    putStrLn $ "2d: " ++ show (map toList (toList twoD))

    -- You can create and initialize multi-dimensional vectors at once too.
    let twoD' : Vect 2 (Vect 3 Int) = [[1, 2, 3], [1, 2, 3]]
    putStrLn $ "2d: " ++ show (map toList (toList twoD'))