{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Language.Symantic.Typing.Constant where

import qualified Data.Kind as Kind
import qualified Data.Map.Strict as Map
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import Data.NonNull (NonNull)
import Data.Proxy
import Data.Text (Text)
import Data.Type.Equality
import GHC.Exts (Constraint)
import qualified System.IO as IO

import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Lib.Data.Type.Peano
import Language.Symantic.Typing.Kind

-- * Type 'Const'
-- | A /type constant/,
-- indexed at the Haskell type and term level amongst a list of them.
-- When used, @c@ is actually wrapped within a 'Proxy'
-- to be able to handle constants of different 'Kind's.
data Const (cs::[Kind.Type]) (c::k) where
	ConstZ :: SKind k -> Const (Proxy c ': cs) (c::k)
	ConstS :: Const cs c -> Const (not_c ': cs) c
infixr 5 `ConstS`

eq_kind_const :: Const cs (x::kx) -> Const cs (y::ky) -> Maybe (kx:~:ky)
eq_kind_const x y = eq_skind (kind_of_const x) (kind_of_const y)

instance TestEquality (Const cs) where
	testEquality ConstZ{} ConstZ{}     = Just Refl
	testEquality (ConstS x) (ConstS y) = testEquality x y
	testEquality _ _                   = Nothing

kind_of_const :: Const cs (h::k) -> SKind k
kind_of_const (ConstZ ki) = ki
kind_of_const (ConstS c)  = kind_of_const c

-- * Type 'Inj_Const'
-- | Convenient type synonym wrapping 'Inj_ConstP'
-- applied on the correct 'Index'.
type Inj_Const cs c = Inj_ConstP (Index cs (Proxy c)) cs c

-- | Inject a given /type constant/ @c@ into a list of them,
-- by returning a proof that 'Proxy'@ c@ is in @cs@.
inj_const :: forall cs c. Inj_Const cs c => Const cs c
inj_const = inj_constP (Proxy::Proxy (Index cs (Proxy c)))

-- ** Class 'Inj_ConstP'
class Inj_ConstP p cs c where
	inj_constP :: Proxy p -> Const cs c
{- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933
         which makes it fail to calculate the right kind,
         it seems to wrongly reuse the kind of the first use (sic)…
instance IKind k => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
	inj_constP _ = ConstZ kind
-}
instance
 ( IKindP (Ty_of_Type k)
 , Type_of_Ty (Ty_of_Type k) ~ k
 ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
	inj_constP _ = ConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
	inj_constP _p = ConstS (inj_constP (Proxy::Proxy p))

-- * Class 'Proj_Const'
-- | Convenient type synonym wrapping 'Proj_ConstP'
-- applied on the correct 'Index'.
type Proj_Const cs c = Proj_ConstP (Index cs (Proxy c)) cs c

-- | Project a 'Const' onto a Haskell type level /type constant/ @c@,
-- returning a proof that the 'Const' indexes @c@ iif. it's the case.
proj_const :: forall cs k (c::k) (u::k).
 Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
proj_const = proj_constP (Proxy::Proxy (Index cs (Proxy c)))

(=?) :: forall cs c u. Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
(=?) = proj_constP (Proxy::Proxy (Index cs (Proxy c)))

-- ** Type 'Proj_ConstP'
class Proj_ConstP p cs c where
	proj_constP :: Proxy p -> Const cs u -> Proxy c -> Maybe (c :~: u)
instance Proj_ConstP Zero (Proxy c ': cs) c where
	proj_constP _p ConstZ{} _c = Just Refl
	proj_constP _p ConstS{} _c = Nothing
instance Proj_ConstP p cs c => Proj_ConstP (Succ p) (not_c ': cs) c where
	proj_constP _p ConstZ{} _c  = Nothing
	proj_constP _p (ConstS u) c = proj_constP (Proxy::Proxy p) u c

-- ** Type 'Proj_Consts'
type Proj_Consts cs cs_to_proj
 = Concat_Constraints (Proj_ConstsR cs cs_to_proj)

-- *** Type family 'Proj_ConstsR'
type family Proj_ConstsR cs cs_to_proj :: [Constraint] where
 Proj_ConstsR cs '[] = '[]
 Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs

-- * Class 'Show_Const'
class Show_Const cs where
	show_const :: Const cs c -> String

-- deriving instance Show (Const cs c)
instance Show_Const cs => Show (Const cs c) where
	show = show_const
instance Show_Const '[] where
	show_const = error "Show_Const unreachable pattern"

-- TODO: move each of these to a dedicated module.
instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
	show_const ConstZ{} = "Bounded"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
	show_const ConstZ{} = "Enum"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
	show_const ConstZ{} = "Fractional"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Real ': cs) where
	show_const ConstZ{} = "Real"
	show_const (ConstS c) = show_const c

-- * Type 'Constants'
-- | Usual 'Const's.
type Constants = Terms ++ Constraints

-- ** Type 'Terms'
-- | Usual 'Const's of /terms constructors/.
type Terms =
 [ Proxy ()
 , Proxy (,)
 , Proxy (->)
 , Proxy []
 , Proxy Bool
 , Proxy Char
 , Proxy Either
 , Proxy Int
 , Proxy Integer
 , Proxy Integral
 , Proxy IO
 , Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy Map.Map
 , Proxy Maybe
 , Proxy NonNull
 , Proxy Text
 ]

-- ** Type 'Constraints'
-- | Usual 'Const's of /type constraint constructors/.
type Constraints =
 [ Proxy Applicative
 , Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 , Proxy Seqs.IsSequence
 , Proxy Seqs.SemiSequence
 , Proxy Show
 , Proxy Traversable
 ]