{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Main where

import Control.Monad
import Data.Promotion.Prelude hiding (Nat)
import Data.Singletons
import Data.Singletons.Prelude.Ord
import Data.Singletons.TH
import Prelude hiding (length)

singletons [d|
  data Nat = Zero | Succ Nat deriving (Eq, Ord)
           |]

sNatToInt :: SNat n -> Int
sNatToInt SZero = 0
sNatToInt (SSucc n) = 1 +  sNatToInt n

intToNat :: Int -> Nat
intToNat 0 = Zero
intToNat n | n > 0 = Succ (intToNat (n-1))
           | otherwise = error "Has to be > 0"

data Vector ::  Nat -> * -> * where
    Nil :: Vector 'Zero a
    Cons :: a -> Vector n a -> Vector ('Succ n) a

parseInt :: String -> Maybe Int
parseInt str = case reads str of
                ((i,_):_) -> Just i
                _ -> Nothing


data Fin :: Nat -> * where
    FZero :: Fin n
    FSucc :: Fin n -> Fin ('Succ n)

intToFin :: forall n . Int -> SNat n -> Maybe (Fin n)
intToFin 0 _ = Just FZero
intToFin n _ | n < 0 = Nothing
intToFin _ SZero = Nothing
intToFin n (SSucc m) = case intToFin (n-1) m of
                        Nothing -> Nothing
                        Just f -> Just $ FSucc f


indexVector :: Fin n -> Vector ('Succ n) a -> a
indexVector FZero (Cons a _) = a
indexVector (FSucc m)  (Cons _ vs) = indexVector m vs

enumVector :: SNat n -> Vector n Int
enumVector SZero = Nil
enumVector (SSucc n) = Cons (sNatToInt n) (enumVector n)

-- -- Actual program of interest:

main :: IO ()
main = do
  putStrLn "How big should the vector be?"
  sizeString <- getLine
  case parseInt sizeString of
    Nothing ->
      putStrLn "Couldn't parse an integer."
    Just int ->
        case toSing (intToNat int) of
         SomeSing length' -> do
          let length = SSucc length'
          let myVector = enumVector length
          forever
           (do putStrLn "Enter an index to look at: "
               indexString <- getLine
               case parseInt indexString of
                 Nothing -> putStrLn "Couldn't parse an integer."
                 Just mbIdx ->
                   case intToFin mbIdx length' of
                    Nothing -> putStrLn "Couldn't convert to number within bounds."
                    Just idx ->
                       do putStrLn "The value is:"
                          print (indexVector idx myVector))