{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Variable where

import Data.Proxy (Proxy(..))
import Data.String (IsString(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(..), (:~~:)(..))
import qualified Data.Kind as K

import Language.Symantic.Grammar
import Language.Symantic.Typing.List
import Language.Symantic.Typing.Kind

-- * Type 'Var'
-- | A /type variable/, indexed amongst a type-level list.
-- @v@ is wrapped within a 'Proxy' to have a kind-heterogeneous list.
data Var src (vs::[K.Type]) (v::kv) where
        VarZ :: Kind src kv
             -> Len     (Proxy (v::kv) ': vs)
             -> Var src (Proxy (v::kv) ': vs) (v::kv)
        VarS :: Var src vs v
             -> Var src (not_v ': vs) v
infixr 5 `VarS`
type instance SourceOf (Var src vs t) = src
instance Show (Var src tys v) where
        showsPrec p v = showsPrec p (indexVar v)
instance SourceInj (EVar src vs) src => KindOf (Var src vs) where
        kindOf v = kindOfVar v `withSource` EVar v
instance LenVars (Var src vs v) where
        lenVars (VarZ _k l) = l
        lenVars (VarS v)    = LenS (lenVars v)
instance AllocVars (Var src) where
        allocVarsL LenZ v       = v
        allocVarsL (LenS len) v = VarS $ allocVarsL len v

        allocVarsR len (VarZ k l) = VarZ k (addLen l len)
        allocVarsR len (VarS v)   = VarS $ allocVarsR len v

varZ ::
 forall src vs kv (v::kv).
 Source src =>
 LenInj vs =>
 KindInj kv =>
 Var src (Proxy v ': vs) v
varZ = VarZ kindInj lenInj

-- | Return the 'Kind' of given 'Var'.
kindOfVar :: Var src vs (v::kv) -> Kind src kv
kindOfVar (VarZ k _l) = k
kindOfVar (VarS v)    = kindOfVar v

-- ** Comparison
eqVar :: Var xs vs x -> Var ys vs y -> Maybe (x:~:y)
eqVar VarZ{} VarZ{}     = Just Refl
eqVar (VarS x) (VarS y) = eqVar x y
eqVar _ _               = Nothing

eqVarKi :: Var xs vs x -> Var ys vs y -> Maybe ((x::kx) :~~: (y::ky))
eqVarKi VarZ{} VarZ{}     = Just HRefl
eqVarKi (VarS x) (VarS y) = eqVarKi x y
eqVarKi _ _               = Nothing

ordVarKi :: Var xs vs x -> Var ys vs y -> Ordering
ordVarKi VarZ{}    VarZ{}  = EQ
ordVarKi VarZ{}    VarS{}  = LT
ordVarKi VarS{}    VarZ{}  = GT
ordVarKi (VarS x) (VarS y) = ordVarKi x y

-- * Type 'EVar'
-- | Existential 'Var'.
data EVar src vs = forall v. EVar (Var src vs v)

-- ** Type 'IndexVar'
-- | Index of a 'Var'.
type IndexVar = Int
indexVar :: Var src vs v -> Int
indexVar VarZ{} = 0
indexVar (VarS v) = 1 + indexVar v

-- * Class 'LenVars'
-- | Return the 'Len' of the 'Var' context.
class LenVars a where
        lenVars :: a -> Len (VarsOf a)

-- * Class 'AllocVars'
-- | Allocate 'Var's in a 'Var' context,
-- either to the left or to the right.
class AllocVars (a::[K.Type] -> k -> K.Type) where
        allocVarsL :: Len len -> a vs x -> a (len ++ vs) x
        allocVarsR :: Len len -> a vs x -> a (vs ++ len) x

appendVars ::
 AllocVars a =>
 AllocVars b =>
 LenVars (a vs_x x) =>
 LenVars (b vs_y y) =>
 VarsOf (a vs_x x) ~ vs_x =>
 VarsOf (b vs_y y) ~ vs_y =>
 a vs_x (x::kx) ->
 b vs_y (y::ky) ->
 ( a (vs_x ++ vs_y) x
 , b (vs_x ++ vs_y) y )
appendVars x y =
        ( allocVarsR (lenVars y) x
        , allocVarsL (lenVars x) y
        )

-- * Type 'NameVar'
newtype NameVar = NameVar Text
 deriving (Eq, Ord, Show)
instance IsString NameVar where
        fromString = NameVar . fromString

-- * Class 'VarOccursIn'
-- | Test whether a given 'Var' occurs within something.
class VarOccursIn a where
        varOccursIn :: Var src (VarsOf a) v -> a -> Bool

-- * Type family 'VarsOf'
-- | Return the 'Var' context of something.
type family   VarsOf a :: [K.Type]
type instance VarsOf (Var src vs v) = vs
type instance VarsOf (UsedVars src vs vs') = vs'

-- * Type 'Vars'
-- | Growable list of 'Var's.
data Vars src vs where
 VarsZ :: Vars src '[]
 VarsS :: NameVar ->
          Kind src kv ->
          Vars src vs ->
          Vars src (Proxy (v::kv) ': vs)
type instance VarsOf (Vars src vs) = vs
instance LenVars (Vars src vs) where
        lenVars VarsZ = LenZ
        lenVars (VarsS _n _kv vs) = LenS $ lenVars vs

lookupVars ::
 NameVar ->
 Vars src vs ->
 Maybe (EVar src vs)
lookupVars _n VarsZ = Nothing
lookupVars n (VarsS n' kv vs) =
        if n == n'
        then Just $ EVar $ VarZ kv (LenS $ lenVars vs)
        else (\(EVar v) -> EVar $ VarS v) <$> lookupVars n vs

insertVars ::
 NameVar ->
 Kind src k ->
 Vars src vs ->
 (forall vs'. Vars src vs' -> ret) -> ret
insertVars n kv vs k =
        case lookupVars n vs of
         Just{} -> k vs -- TODO: check kind?
         Nothing -> k $ VarsS n kv vs

-- ** Type 'EVars'
-- | Existential 'Vars'.
data EVars src = forall vs. EVars (Vars src vs)

-- * Type 'UsedVars'
-- | List of 'Var's, used to change the context of a 'Var'
-- when removing unused 'Var's.
data UsedVars src vs vs' where
 UsedVarsZ :: UsedVars src vs '[]
 UsedVarsS :: Var src vs (v::k) ->
              UsedVars src vs vs' ->
              UsedVars src vs (Proxy v ': vs')
instance LenVars (UsedVars src vs vs') where
        lenVars UsedVarsZ         = LenZ
        lenVars (UsedVarsS _v vs) = LenS $ lenVars vs

lookupUsedVars ::
 Var src vs v ->
 UsedVars src vs vs' ->
 Maybe (Var src vs' v)
lookupUsedVars _v UsedVarsZ = Nothing
lookupUsedVars v (UsedVarsS v' vs) =
        case v `eqVarKi` v' of
         Just HRefl -> Just $ VarZ (kindOfVar v) (LenS $ lenVars vs)
         Nothing -> VarS <$> lookupUsedVars v vs

insertUsedVars ::
 Var src vs v ->
 UsedVars src vs vs' ->
 Maybe (UsedVars src vs (Proxy v ': vs'))
insertUsedVars v vs =
        case lookupUsedVars v vs of
         Just{} -> Nothing
         Nothing -> Just $ UsedVarsS v vs

-- ** Class 'UsedVarsOf'
class UsedVarsOf a where
        usedVarsOf ::
         UsedVars (SourceOf a) (VarsOf a) vs -> a ->
         (forall vs'. UsedVars (SourceOf a) (VarsOf a) vs' -> ret) -> ret

-- * Type 'UnProxy'
type family UnProxy (x::K.Type) :: k where
        UnProxy (Proxy x) = x

{-
-- ** Type family 'V'
type family V (vs::[K.Type]) (i::Nat) :: k where
	V (v ': vs) 'Z  = UnProxy v
	V (not_v ': vs) ('S i) = V vs i

-- ** Type family 'KV'
type family KV (vs::[K.Type]) (i::Nat) :: K.Type where
	KV (Proxy v ': vs) 'Z     = K v
	KV (not_v   ': vs) ('S i) = KV vs i
-}