{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Constant where

import Data.Text (Text)
import Data.Proxy
import Data.Type.Equality
import GHC.Exts (Constraint)
import qualified Data.Kind as Kind
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 class 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 'Const_from'
-- | Try to build a 'Const' from raw data.
class Const_from raw cs where
	const_from
	 :: raw -> (forall k c. Const cs (c::k) -> Maybe ret)
	 -> Maybe ret

instance Const_from raw '[] where
	const_from _c _k = Nothing

instance Const_from Text cs => Const_from Text (Proxy () ': cs) where
	const_from "()" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy Bounded ': cs) where
	const_from "Bounded" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy Enum ': cs) where
	const_from "Enum" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy Fractional ': cs) where
	const_from "Fractional" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy Real ': cs) where
	const_from "Real" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy String ': cs) where
	const_from "String" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS

-- * 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"

instance Show_Const cs => Show_Const (Proxy () ': cs) where
	show_const ConstZ{} = "()"
	show_const (ConstS c) = show_const c
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
instance Show_Const cs => Show_Const (Proxy String ': cs) where
	show_const ConstZ{} = "String"
	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 Bool
 , Proxy Char
 , Proxy Int
 , Proxy Integer
 , Proxy Integral
 , Proxy IO
 , Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy Maybe
 , Proxy String
 , 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 Num
 , Proxy Ord
 , Proxy Real
 , Proxy Traversable
 ]