{-# LANGUAGE CPP                    #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# OPTIONS_GHC -Wall                       #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

{-|
Module      : Fcf.Data.Reflect
Description : List helpers / utils
Copyright   : (c) gspia 2023-
License     : BSD
Maintainer  : gspia

= Fcf.Data.Reflect

Helpers to get results from type-level computations into the fromType-level.

-}

--------------------------------------------------------------------------------

module Fcf.Data.Reflect where

import qualified GHC.TypeLits as TL
import           GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol)
import           Data.String (fromString, IsString)
import           Data.Proxy
import           Data.Typeable (Typeable, typeRep)
import           Data.Kind (Type)
import qualified Data.Map as DM
import qualified Data.IntMap.Strict as IMS
import qualified Data.Set as S
-- #if __GLASGOW_HASKELL__ >= 902
-- #endif
import qualified Data.Tree as T

import qualified Fcf.Data.MapC as MC
import qualified Fcf.Data.NatMap as NM
import qualified Fcf.Data.Set as FS
#if __GLASGOW_HASKELL__ >= 902
import qualified Fcf.Data.NewText as FTxt
#endif
import qualified Fcf.Data.Tree as FT

--------------------------------------------------------------------------------

-- | Reflect a list of Nats
--
-- Note that you may also use the KnownVal methods given below.
--
-- This method is taken from
-- https://hackage.haskell.org/package/numhask-array-0.10.1/docs/src/NumHask.Array.Shape.html#natVals
--
-- === __Example__
--
-- > :{
-- afun :: forall n. (n ~ '[1,2,3,4]) => [Int]
-- afun = natVals @n Proxy
-- :}
--
-- > afun
-- [1,2,3,4]
class KnownNats (ns :: [Nat]) where
  natVals :: Proxy ns -> [Int]

{-# DEPRECATED KnownNats "Replaced with KnownVal" #-}

instance KnownNats '[] where
  natVals :: Proxy '[] -> [Int]
natVals Proxy '[]
_ = []

instance (TL.KnownNat n, KnownNats ns) => KnownNats (n : ns) where
  natVals :: Proxy (n : ns) -> [Int]
natVals Proxy (n : ns)
_ = forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
TL.natVal (forall {k} (t :: k). Proxy t
Proxy @n)) forall a. a -> [a] -> [a]
: forall (ns :: [Nat]). KnownNats ns => Proxy ns -> [Int]
natVals (forall {k} (t :: k). Proxy t
Proxy @ns)


--------------------------------------------------------------------------------

class KnownVal val kind where
    fromType :: Proxy kind -> val

instance (KnownNat n, Num a) => KnownVal a (n :: Nat) where
    fromType :: Proxy n -> a
fromType Proxy n
_ = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
TL.natVal (forall {k} (t :: k). Proxy t
Proxy @n)

instance KnownVal Bool 'True where fromType :: Proxy 'True -> Bool
fromType Proxy 'True
_ = Bool
True
instance KnownVal Bool 'False where fromType :: Proxy 'False -> Bool
fromType Proxy 'False
_ = Bool
False
instance KnownVal () '() where fromType :: Proxy '() -> ()
fromType Proxy '()
_ = ()

instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol) where
    fromType :: Proxy s -> str
fromType Proxy s
_ = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
TL.symbolVal (forall {k} (t :: k). Proxy t
Proxy @s)

#if __GLASGOW_HASKELL__ >= 920
instance (TL.KnownChar c) => KnownVal Char c where
    fromType _ = TL.charVal (Proxy @c)
#endif

instance (IsString str, Typeable typ) => KnownVal str (typ :: Type) where
    fromType :: Proxy typ -> str
fromType = forall a. IsString a => String -> a
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep

#if __GLASGOW_HASKELL__ >= 902

-- | Text instance.
--
-- === __Example__
--
-- > import qualified Data.Text as Txt
-- > :{
-- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text
-- afun = fromType (Proxy @r)
-- :}
--
-- > afun
-- "hmm"
instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)
  where
    fromType :: Proxy ('Text sym) -> str
fromType Proxy ('Text sym)
_ = forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @str (forall {k} (t :: k). Proxy t
Proxy @sym) 

#endif

--------------------------------------------------------------------------------

-- List instances

instance KnownVal [a] '[] where
    fromType :: Proxy '[] -> [a]
fromType Proxy '[]
_ = []

instance (KnownVal val x, KnownVal [val] xs) => KnownVal [val] (x ': xs) where
    fromType :: Proxy (x : xs) -> [val]
fromType Proxy (x : xs)
_ = forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @x) forall a. a -> [a] -> [a]
: forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @xs)

--------------------------------------------------------------------------------

-- Trees
--
instance (KnownVal val k, KnownVal (T.Forest val) trees) => KnownVal (T.Tree val) ('FT.Node k trees)
  where
    fromType :: Proxy ('Node k trees) -> Tree val
fromType Proxy ('Node k trees)
_ = forall a. a -> [Tree a] -> Tree a
T.Node (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @k)) (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @trees))

--------------------------------------------------------------------------------

-- NatMaps / IntMaps
--
instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) ('NM.NatMap pairs)
  where
    fromType :: Proxy ('NatMap pairs) -> IntMap val
fromType Proxy ('NatMap pairs)
_ = forall a. [(Int, a)] -> IntMap a
IMS.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @pairs))

instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) (pairs :: [(Nat, val')])
  where
    fromType :: Proxy pairs -> IntMap val
fromType Proxy pairs
_ = forall a. [(Int, a)] -> IntMap a
IMS.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @pairs))

--------------------------------------------------------------------------------

-- Maps

instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) ('MC.MapC pairs)
  where
    fromType :: Proxy ('MapC pairs) -> Map key val
fromType Proxy ('MapC pairs)
_ = forall k a. Ord k => [(k, a)] -> Map k a
DM.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @pairs))

instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) (pairs :: [(key',val')])
  where
    fromType :: Proxy pairs -> Map key val
fromType Proxy pairs
_ = forall k a. Ord k => [(k, a)] -> Map k a
DM.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @pairs))

--------------------------------------------------------------------------------

-- Set

instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) ('FS.Set kind)
  where
    fromType :: Proxy ('Set kind) -> Set val
fromType Proxy ('Set kind)
_ = forall a. Ord a => [a] -> Set a
S.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @kind))

instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) (kind :: [kind'])
  where
    fromType :: Proxy kind -> Set val
fromType Proxy kind
_ = forall a. Ord a => [a] -> Set a
S.fromList (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @kind))
 
--------------------------------------------------------------------------------

-- Either

instance (KnownVal a1 a) => KnownVal (Either a1 b1) ('Left a) where
    fromType :: Proxy ('Left a) -> Either a1 b1
fromType Proxy ('Left a)
_ = forall a b. a -> Either a b
Left (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a))

instance (KnownVal b1 b) => KnownVal (Either a1 b1) ('Right b) where
    fromType :: Proxy ('Right b) -> Either a1 b1
fromType Proxy ('Right b)
_ = forall a b. b -> Either a b
Right (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @b1 (forall {k} (t :: k). Proxy t
Proxy @b))

--------------------------------------------------------------------------------

-- Maybe

instance (KnownVal a1 a) => KnownVal (Maybe a1) ('Just a) where
    fromType :: Proxy ('Just a) -> Maybe a1
fromType Proxy ('Just a)
_ = forall a. a -> Maybe a
Just (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a))

instance KnownVal (Maybe a1) 'Nothing where
    fromType :: Proxy 'Nothing -> Maybe a1
fromType Proxy 'Nothing
_ = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- Tuples

instance (KnownVal a1 a, KnownVal b1 b) => KnownVal (a1,b1) '(a,b) where
    fromType :: Proxy '(a, b) -> (a1, b1)
fromType Proxy '(a, b)
_ = (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @b1 (forall {k} (t :: k). Proxy t
Proxy @b))

instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c) => KnownVal (a1,b1,c1) '(a,b,c) where
    fromType :: Proxy '(a, b, c) -> (a1, b1, c1)
fromType Proxy '(a, b, c)
_ = (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @b1 (forall {k} (t :: k). Proxy t
Proxy @b), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @c1 (forall {k} (t :: k). Proxy t
Proxy @c))

instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d) => KnownVal (a1,b1,c1,d1) '(a,b,c,d) where
    fromType :: Proxy '(a, b, c, d) -> (a1, b1, c1, d1)
fromType Proxy '(a, b, c, d)
_ = (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @b1 (forall {k} (t :: k). Proxy t
Proxy @b), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @c1 (forall {k} (t :: k). Proxy t
Proxy @c), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @d1 (forall {k} (t :: k). Proxy t
Proxy @d))

instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d, KnownVal e1 e) => KnownVal (a1,b1,c1,d1,e1) '(a,b,c,d,e) where
    fromType :: Proxy '(a, b, c, d, e) -> (a1, b1, c1, d1, e1)
fromType Proxy '(a, b, c, d, e)
_ = (forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @a1 (forall {k} (t :: k). Proxy t
Proxy @a), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @b1 (forall {k} (t :: k). Proxy t
Proxy @b), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @c1 (forall {k} (t :: k). Proxy t
Proxy @c), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @d1 (forall {k} (t :: k). Proxy t
Proxy @d), forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @e1 (forall {k} (t :: k). Proxy t
Proxy @e))

--------------------------------------------------------------------------------

-- ErrorMessage from GHC.TypeLits

instance (IsString str, KnownSymbol sym) => KnownVal str ('TL.Text sym) where
  fromType :: Proxy ('Text sym) -> str
fromType Proxy ('Text sym)
_ = forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType @str (forall {k} (t :: k). Proxy t
Proxy @sym)

instance (IsString str, Typeable typ) => KnownVal str ('TL.ShowType typ) where
  fromType :: Proxy ('ShowType typ) -> str
fromType Proxy ('ShowType typ)
_ = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @typ)

instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:<>: err2) where
  fromType :: Proxy (err1 ':<>: err2) -> str
fromType Proxy (err1 ':<>: err2)
_ = forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @err1) forall a. Semigroup a => a -> a -> a
<> forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @err2)

instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:$$: err2) where
  fromType :: Proxy (err1 ':$$: err2) -> str
fromType Proxy (err1 ':$$: err2)
_ = forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @err1) forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString String
"\n" forall a. Semigroup a => a -> a -> a
<> forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType (forall {k} (t :: k). Proxy t
Proxy @err2)