{-# Language
    DataKinds
  , MultiParamTypeClasses
  , TypeInType
  , ConstraintKinds
  , FunctionalDependencies
  , FlexibleInstances
  , TypeApplications
  , RankNTypes
  , ScopedTypeVariables
  #-}
module Data.IndexedListLiterals (
    IndexedListLiterals(..)
  , ILL
  , module Data.Tuple.Only
  , ZeroTuple(..)
  , len
  , fromList
  , fromListP
  ) where

import GHC.TypeLits
import Data.Kind
import Data.Tuple.Only
import Data.Proxy
import GHC.Stack
import Control.Monad

-- | An alias for IndexedListLiterals
type ILL = IndexedListLiterals

-- | the fromList variants take a list and convert it into a tuple
--   it's sort of the inverse of toList
--
--   >> fromListP (len @3) [1,2,3]
--   >  Just (1,2,3)
--
--   >> fromListP (len @3) ["word","up"]
--   >  Nothing
--
--   >> fromListP (len @1) ['z']
--   >  Just (Only 'z') @
fromListP :: forall input (length :: Nat) output len.
             (KnownNat length, ILL input length output)
          => len length -> [output] -> Maybe input
fromListP :: len length -> [output] -> Maybe input
fromListP len length
_length = [output] -> Maybe input
forall input (length :: Nat) output.
(KnownNat length, ILL input length output) =>
[output] -> Maybe input
fromList

len :: Proxy a
len :: Proxy a
len = Proxy a
forall k (t :: k). Proxy t
Proxy

-- | >> fromList [1,2,3] :: Maybe (Int, Int, Int)
--   >  Just (1,2,3)
--
--   >> fromList ["word","up"] :: Maybe (String, String, String)
--   >  Nothing
-- 
--   >> fromList ['z'] :: Maybe (Only Char)
--   >  Just (Only 'z')
fromList :: forall input (length :: Nat) output.
            (KnownNat length, ILL input length output)
         => [output] -> Maybe input
fromList :: [output] -> Maybe input
fromList [output]
xs
  | [output] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [output]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i = input -> Maybe input
forall a. a -> Maybe a
Just (input -> Maybe input) -> input -> Maybe input
forall a b. (a -> b) -> a -> b
$ [output] -> input
forall input (length :: Nat) output.
IndexedListLiterals input length output =>
[output] -> input
fromList' [output]
xs
  | Bool
otherwise      = Maybe input
forall a. Maybe a
Nothing
  where i :: Int
i = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy length -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy length
forall k (t :: k). Proxy t
len @length)

-- | A type class which allows you to write tuples which can be transformed to and from a list
--   the length of the list is also provided as a Nat
class IndexedListLiterals (input :: Type) (length :: Nat) (output :: Type) | output length -> input, input -> output length where
  -- | >> toList (Only 1)
  --   >  [1]
  --
  --   >> toList (1,2,3)
  --   >  [1,2,3]
  --
  --   >> toList ZeroTuple
  --   >  []
  toList    :: input -> [output]
  -- | a partial fromList with bad error messages
  fromList' :: [output] -> input

instance IndexedListLiterals (ZeroTuple a) 0 a where
  toList :: ZeroTuple a -> [a]
toList ZeroTuple a
ZeroTuple = []
  fromList' :: [a] -> ZeroTuple a
fromList' [] = ZeroTuple a
forall k (a :: k). ZeroTuple a
ZeroTuple

instance IndexedListLiterals (Only a) 1 a where
  toList :: Only a -> [a]
toList (Only a
a) = [a
a]
  fromList' :: [a] -> Only a
fromList' [a
a] = a -> Only a
forall a. a -> Only a
Only a
a

-- | Intuitively the zero tuple is () or Void but this breaks the Functional Dependency
--   "input -> output length" stopping reliable inference, so this constructor is used to preserve type information
data ZeroTuple a = ZeroTuple

-- all code generated below comes from this function
generate :: Int -- ^ up to N
         -> String
generate :: Int -> String
generate Int
n = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ ([String] -> [String]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (String
""String -> [String] -> [String]
forall a. a -> [a] -> [a]
:) ([[String]] -> [[String]]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ Int -> [[String]] -> [[String]]
forall a. Int -> [a] -> [a]
take Int
n ([[String]] -> [[String]]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ [[String]] -> [[String]]
forall a. [a] -> [a]
dropOneTuple [[String]]
res where
  values :: [String]
values = (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((:) Char
'a' (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [Int
1 :: Int ..]
  types :: [String]
types  = String
"a" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
types
  withCommas :: [String] -> [String]
withCommas = (String -> String -> String) -> [String] -> [String]
forall a. (a -> a -> a) -> [a] -> [a]
scanl1 (\String
a String
b -> String
aString -> String -> String
forall a. [a] -> [a] -> [a]
++String
","String -> String -> String
forall a. [a] -> [a] -> [a]
++String
b)
  className :: String
className = String
"IndexedListLiterals"
  template :: String -> String -> a -> [String]
template String
tys String
vals a
length =
      [String
"instance " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
className String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tys String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
length String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
head [String]
types String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" where"
    ,String
"  toList    (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
vals String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") = [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
vals String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
    ,String
"  fromList' [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
vals String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] = (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
vals String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    ]
  res :: [[String]]
res = (String -> String -> Int -> [String])
-> [String] -> [String] -> [Int] -> [[String]]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 String -> String -> Int -> [String]
forall a. Show a => String -> String -> a -> [String]
template ([String] -> [String]
withCommas [String]
types) ([String] -> [String]
withCommas [String]
values) [Int
1 :: Int ..]
  dropOneTuple :: [a] -> [a]
dropOneTuple = [a] -> [a]
forall a. [a] -> [a]
tail

instance IndexedListLiterals (a,a) 2 a where
  toList :: (a, a) -> [a]
toList    (a
a1,a
a2) = [a
a1,a
a2]
  fromList' :: [a] -> (a, a)
fromList' [a
a1,a
a2] = (a
a1,a
a2)

instance IndexedListLiterals (a,a,a) 3 a where
  toList :: (a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3) = [a
a1,a
a2,a
a3]
  fromList' :: [a] -> (a, a, a)
fromList' [a
a1,a
a2,a
a3] = (a
a1,a
a2,a
a3)

instance IndexedListLiterals (a,a,a,a) 4 a where
  toList :: (a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4) = [a
a1,a
a2,a
a3,a
a4]
  fromList' :: [a] -> (a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4] = (a
a1,a
a2,a
a3,a
a4)

instance IndexedListLiterals (a,a,a,a,a) 5 a where
  toList :: (a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5) = [a
a1,a
a2,a
a3,a
a4,a
a5]
  fromList' :: [a] -> (a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5] = (a
a1,a
a2,a
a3,a
a4,a
a5)

instance IndexedListLiterals (a,a,a,a,a,a) 6 a where
  toList :: (a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6]
  fromList' :: [a] -> (a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6)

instance IndexedListLiterals (a,a,a,a,a,a,a) 7 a where
  toList :: (a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7]
  fromList' :: [a] -> (a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7)

instance IndexedListLiterals (a,a,a,a,a,a,a,a) 8 a where
  toList :: (a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a) 9 a where
  toList :: (a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a) 10 a where
  toList :: (a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a) 11 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a) 12 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a) 13 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a) 14 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 15 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 16 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 17 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 18 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 19 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19)

instance IndexedListLiterals (a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a) 20 a where
  toList :: (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) -> [a]
toList    (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19,a
a20) = [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19,a
a20]
  fromList' :: [a] -> (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
fromList' [a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19,a
a20] = (a
a1,a
a2,a
a3,a
a4,a
a5,a
a6,a
a7,a
a8,a
a9,a
a10,a
a11,a
a12,a
a13,a
a14,a
a15,a
a16,a
a17,a
a18,a
a19,a
a20)