{-# 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 qualified Data.Map.Strict as MS
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.Core as C (Eval)
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

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

-- For the doctests:

-- $setup
-- >>> import qualified GHC.TypeLits as TL
-- >>> import           Fcf.Data.Nat

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


-- | 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]

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 (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__ >= 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 a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall {k} val (kind :: k). KnownVal val kind => Proxy kind -> val
fromType forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @sym 

#endif

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

-- List instances

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

instance (KnownVal typ x, KnownVal [typ] xs) => KnownVal [typ] (x ': xs) where
    fromType :: Proxy (x : xs) -> [typ]
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 typ k, KnownVal (T.Forest typ) trees) => KnownVal (T.Tree typ) ('FT.Node k trees)
  where
    fromType :: Proxy ('Node k trees) -> Tree typ
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))

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

-- 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))

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

-- Set

instance (Ord typ, KnownVal [typ] kind) => KnownVal (S.Set typ) ('FS.Set kind)
  where
    fromType :: Proxy ('Set kind) -> Set typ
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))
 
--------------------------------------------------------------------------------

-- 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))