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

import Data.Proxy
import Data.Type.Equality
import GHC.Prim (Constraint)

import Language.Symantic.Lib.Data.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::[*]) (c:: *) where
	ConstZ :: SKind (Kind_of_UnProxy c) -> Const (c ': cs) c
	ConstS :: Const cs c -> Const (not_c ': cs) c
infixr 5 `ConstS`

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 -> SKind (Kind_of_UnProxy h)
kind_of_const (ConstZ ki) = ki
kind_of_const (ConstS c)  = kind_of_const c

-- ** Type 'Const_of'
-- | Convenient type synonym.
type Const_of cs c = Const cs (Proxy c)

-- ** Type 'ConstP'
-- | Return the position of a 'Const' within a list of them.
-- This is useful to work around @OverlappingInstances@
-- in 'Inj_ConstP' and 'Proj_ConstP'.
type family ConstP cs c where
	ConstP (c  ': cs) c = Zero
	ConstP (nc ': cs) c = Succ (ConstP cs c)

-- ** Type 'Inj_Const'
-- | Convenient type synonym wrapping 'Inj_ConstP'
-- applied on the correct 'ConstP'.
type Inj_Const cs c = Inj_ConstP (ConstP cs (Proxy c)) cs (Proxy 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 (Proxy c)
inj_const = inj_constP (Proxy::Proxy (ConstP cs (Proxy c)))

-- ** Class 'Inj_ConstP'
class Inj_ConstP p cs c where
	inj_constP :: Proxy p -> Const cs c
instance IKind (Kind_of_UnProxy c) => Inj_ConstP Zero (c ': cs) c where
	inj_constP _ = ConstZ kind
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 'ConstP'.
--
-- NOTE: using a /class synonym/ instead of a /type synonym/
-- allows to use it partially applied, which is useful in 'Map_Consts'.
class    Proj_ConstP (ConstP cs c) cs c => Proj_Const cs c
instance Proj_ConstP (ConstP cs c) cs c => Proj_Const cs c
-- type Proj_Const cs c = Proj_ConstP (ConstP cs 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 c u. Proj_Const cs c => Const cs u -> c -> Maybe (c :~: u)
proj_const = proj_constP (Proxy::Proxy (ConstP cs c))

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

-- *** Type 'Proj_ConstP'
class Proj_ConstP p cs c where
	proj_constP :: Proxy p -> Const cs u -> c -> Maybe (c :~: u)
instance Proj_ConstP Zero (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 rs cs = Concat_Constraints (Map_Consts (Proj_Const rs) cs)

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

-- ** Type 'Terms'
-- | Usual 'Const's of /terms constructors/.
type Terms =
 [ Proxy []
 , Proxy (->)
 , Proxy Bool
 , Proxy Int
 , Proxy Integral
 , Proxy IO
 , Proxy Maybe
 ]

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

-- * Class 'Const_from'
-- | Try to build a 'Const' from raw data.
class Const_from raw cs where
	const_from
	 :: raw -> (forall c. Const cs c -> Maybe ret)
	 -> Maybe ret

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

instance Const_from String cs => Const_from String (Proxy [] ': cs) where
	const_from "[]" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy (->) ': cs) where
	const_from "(->)" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Applicative ': cs) where
	const_from "Applicative" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Bool ': cs) where
	const_from "Bool" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Bounded ': cs) where
	const_from "Bounded" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Char ': cs) where
	const_from "Char" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Eq ': cs) where
	const_from "Eq" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Enum ': cs) where
	const_from "Enum" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Foldable ': cs) where
	const_from "Foldable" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Fractional ': cs) where
	const_from "Fractional" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Functor ': cs) where
	const_from "Functor" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Int ': cs) where
	const_from "Int" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Integer ': cs) where
	const_from "Integer" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Integral ': cs) where
	const_from "Integral" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy IO ': cs) where
	const_from "IO" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Maybe ': cs) where
	const_from "Maybe" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Monad ': cs) where
	const_from "Monad" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Monoid ': cs) where
	const_from "Monoid" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Num ': cs) where
	const_from "Num" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Ord ': cs) where
	const_from "Ord" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Real ': cs) where
	const_from "Real" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from String cs => Const_from String (Proxy Traversable ': cs) where
	const_from "Traversable" 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

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 (->) ': cs) where
	show_const ConstZ{} = "(->)"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
	show_const ConstZ{} = "Applicative"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
	show_const ConstZ{} = "Bool"
	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 Char ': cs) where
	show_const ConstZ{} = "Char"
	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 Eq ': cs) where
	show_const ConstZ{} = "Eq"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
	show_const ConstZ{} = "Foldable"
	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 Functor ': cs) where
	show_const ConstZ{} = "Functor"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Int ': cs) where
	show_const ConstZ{} = "Int"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
	show_const ConstZ{} = "Integer"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
	show_const ConstZ{} = "Integral"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy IO ': cs) where
	show_const ConstZ{} = "IO"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
	show_const ConstZ{} = "Maybe"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
	show_const ConstZ{} = "Monad"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
	show_const ConstZ{} = "Monoid"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Num ': cs) where
	show_const ConstZ{} = "Num"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
	show_const ConstZ{} = "Ord"
	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 Traversable ': cs) where
	show_const ConstZ{} = "Traversable"
	show_const (ConstS c) = show_const c

-- * Type family @(++)@
type family (++) xs ys where
	'[] ++ ys = ys
	(x ': xs) ++ ys = x ': xs ++ ys
infixr 5 ++

-- * Type family 'Concat_Constraints'
type family Concat_Constraints (cs::[Constraint]) :: Constraint where
	Concat_Constraints '[] = ()
	Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)

-- * Type family 'Map_Consts'
type family Map_Consts (f:: * -> k) (cs::[*]) :: [k] where
	Map_Consts f '[] = '[]
	Map_Consts f (c ': cs) = f c ': Map_Consts f cs