Variable.hs

{-# 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

-- | /Heterogeneous propositional equality/:
-- like (:~:) but prove also that the kinds are equal.
data (:~~:) (a::ka) (b::kb) where
	HRefl :: a :~~: a

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