symantic/Language/Symantic/Typing/Variable.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE PolyKinds #-}
   5 {-# LANGUAGE TypeInType #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 module Language.Symantic.Typing.Variable where
   8
   9 import Data.Proxy (Proxy(..))
  10 import Data.String (IsString(..))
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(..), (:~~:)(..))
  13 import qualified Data.Kind as K
  14
  15 import Language.Symantic.Grammar
  16 import Language.Symantic.Typing.List
  17 import Language.Symantic.Typing.Kind
  18
  19 -- * Type 'Var'
  20 -- | A /type variable/, indexed amongst a type-level list.
  21 -- @v@ is wrapped within a 'Proxy' to have a kind-heterogeneous list.
  22 data Var src (vs::[K.Type]) (v::kv) where
  23         VarZ :: Kind src kv
  24              -> Len     (Proxy (v::kv) ': vs)
  25              -> Var src (Proxy (v::kv) ': vs) (v::kv)
  26         VarS :: Var src vs v
  27              -> Var src (not_v ': vs) v
  28 infixr 5 `VarS`
  29 type instance SourceOf (Var src vs t) = src
  30 instance Show (Var src tys v) where
  31         showsPrec p v = showsPrec p (indexVar v)
  32 instance SourceInj (EVar src vs) src => KindOf (Var src vs) where
  33         kindOf v = kindOfVar v `withSource` EVar v
  34 instance LenVars (Var src vs v) where
  35         lenVars (VarZ _k l) = l
  36         lenVars (VarS v)    = LenS (lenVars v)
  37 instance AllocVars (Var src) where
  38         allocVarsL LenZ v       = v
  39         allocVarsL (LenS len) v = VarS $ allocVarsL len v
  40
  41         allocVarsR len (VarZ k l) = VarZ k (addLen l len)
  42         allocVarsR len (VarS v)   = VarS $ allocVarsR len v
  43
  44 varZ ::
  45  forall src vs kv (v::kv).
  46  Source src =>
  47  LenInj vs =>
  48  KindInj kv =>
  49  Var src (Proxy v ': vs) v
  50 varZ = VarZ kindInj lenInj
  51
  52 -- | Return the 'Kind' of given 'Var'.
  53 kindOfVar :: Var src vs (v::kv) -> Kind src kv
  54 kindOfVar (VarZ k _l) = k
  55 kindOfVar (VarS v)    = kindOfVar v
  56
  57 -- ** Comparison
  58 eqVar :: Var xs vs x -> Var ys vs y -> Maybe (x:~:y)
  59 eqVar VarZ{} VarZ{}     = Just Refl
  60 eqVar (VarS x) (VarS y) = eqVar x y
  61 eqVar _ _               = Nothing
  62
  63 eqVarKi :: Var xs vs x -> Var ys vs y -> Maybe ((x::kx) :~~: (y::ky))
  64 eqVarKi VarZ{} VarZ{}     = Just HRefl
  65 eqVarKi (VarS x) (VarS y) = eqVarKi x y
  66 eqVarKi _ _               = Nothing
  67
  68 ordVarKi :: Var xs vs x -> Var ys vs y -> Ordering
  69 ordVarKi VarZ{}    VarZ{}  = EQ
  70 ordVarKi VarZ{}    VarS{}  = LT
  71 ordVarKi VarS{}    VarZ{}  = GT
  72 ordVarKi (VarS x) (VarS y) = ordVarKi x y
  73
  74 -- * Type 'EVar'
  75 -- | Existential 'Var'.
  76 data EVar src vs = forall v. EVar (Var src vs v)
  77
  78 -- ** Type 'IndexVar'
  79 -- | Index of a 'Var'.
  80 type IndexVar = Int
  81 indexVar :: Var src vs v -> Int
  82 indexVar VarZ{} = 0
  83 indexVar (VarS v) = 1 + indexVar v
  84
  85 -- * Class 'LenVars'
  86 -- | Return the 'Len' of the 'Var' context.
  87 class LenVars a where
  88         lenVars :: a -> Len (VarsOf a)
  89
  90 -- * Class 'AllocVars'
  91 -- | Allocate 'Var's in a 'Var' context,
  92 -- either to the left or to the right.
  93 class AllocVars (a::[K.Type] -> k -> K.Type) where
  94         allocVarsL :: Len len -> a vs x -> a (len ++ vs) x
  95         allocVarsR :: Len len -> a vs x -> a (vs ++ len) x
  96
  97 appendVars ::
  98  AllocVars a =>
  99  AllocVars b =>
 100  LenVars (a vs_x x) =>
 101  LenVars (b vs_y y) =>
 102  VarsOf (a vs_x x) ~ vs_x =>
 103  VarsOf (b vs_y y) ~ vs_y =>
 104  a vs_x (x::kx) ->
 105  b vs_y (y::ky) ->
 106  ( a (vs_x ++ vs_y) x
 107  , b (vs_x ++ vs_y) y )
 108 appendVars x y =
 109         ( allocVarsR (lenVars y) x
 110         , allocVarsL (lenVars x) y
 111         )
 112
 113 -- * Type 'NameVar'
 114 newtype NameVar = NameVar Text
 115  deriving (Eq, Ord, Show)
 116 instance IsString NameVar where
 117         fromString = NameVar . fromString
 118
 119 -- * Class 'VarOccursIn'
 120 -- | Test whether a given 'Var' occurs within something.
 121 class VarOccursIn a where
 122         varOccursIn :: Var src (VarsOf a) v -> a -> Bool
 123
 124 -- * Type family 'VarsOf'
 125 -- | Return the 'Var' context of something.
 126 type family   VarsOf a :: [K.Type]
 127 type instance VarsOf (Var src vs v) = vs
 128 type instance VarsOf (UsedVars src vs vs') = vs'
 129
 130 -- * Type 'Vars'
 131 -- | Growable list of 'Var's.
 132 data Vars src vs where
 133  VarsZ :: Vars src '[]
 134  VarsS :: NameVar ->
 135           Kind src kv ->
 136           Vars src vs ->
 137           Vars src (Proxy (v::kv) ': vs)
 138 type instance VarsOf (Vars src vs) = vs
 139 instance LenVars (Vars src vs) where
 140         lenVars VarsZ = LenZ
 141         lenVars (VarsS _n _kv vs) = LenS $ lenVars vs
 142
 143 lookupVars ::
 144  NameVar ->
 145  Vars src vs ->
 146  Maybe (EVar src vs)
 147 lookupVars _n VarsZ = Nothing
 148 lookupVars n (VarsS n' kv vs) =
 149         if n == n'
 150         then Just $ EVar $ VarZ kv (LenS $ lenVars vs)
 151         else (\(EVar v) -> EVar $ VarS v) <$> lookupVars n vs
 152
 153 insertVars ::
 154  NameVar ->
 155  Kind src k ->
 156  Vars src vs ->
 157  (forall vs'. Vars src vs' -> ret) -> ret
 158 insertVars n kv vs k =
 159         case lookupVars n vs of
 160          Just{} -> k vs -- TODO: check kind?
 161          Nothing -> k $ VarsS n kv vs
 162
 163 -- ** Type 'EVars'
 164 -- | Existential 'Vars'.
 165 data EVars src = forall vs. EVars (Vars src vs)
 166
 167 -- * Type 'UsedVars'
 168 -- | List of 'Var's, used to change the context of a 'Var'
 169 -- when removing unused 'Var's.
 170 data UsedVars src vs vs' where
 171  UsedVarsZ :: UsedVars src vs '[]
 172  UsedVarsS :: Var src vs (v::k) ->
 173               UsedVars src vs vs' ->
 174               UsedVars src vs (Proxy v ': vs')
 175 instance LenVars (UsedVars src vs vs') where
 176         lenVars UsedVarsZ         = LenZ
 177         lenVars (UsedVarsS _v vs) = LenS $ lenVars vs
 178
 179 lookupUsedVars ::
 180  Var src vs v ->
 181  UsedVars src vs vs' ->
 182  Maybe (Var src vs' v)
 183 lookupUsedVars _v UsedVarsZ = Nothing
 184 lookupUsedVars v (UsedVarsS v' vs) =
 185         case v `eqVarKi` v' of
 186          Just HRefl -> Just $ VarZ (kindOfVar v) (LenS $ lenVars vs)
 187          Nothing -> VarS <$> lookupUsedVars v vs
 188
 189 insertUsedVars ::
 190  Var src vs v ->
 191  UsedVars src vs vs' ->
 192  Maybe (UsedVars src vs (Proxy v ': vs'))
 193 insertUsedVars v vs =
 194         case lookupUsedVars v vs of
 195          Just{} -> Nothing
 196          Nothing -> Just $ UsedVarsS v vs
 197
 198 -- ** Class 'UsedVarsOf'
 199 class UsedVarsOf a where
 200         usedVarsOf ::
 201          UsedVars (SourceOf a) (VarsOf a) vs -> a ->
 202          (forall vs'. UsedVars (SourceOf a) (VarsOf a) vs' -> ret) -> ret
 203
 204 -- * Type 'UnProxy'
 205 type family UnProxy (x::K.Type) :: k where
 206         UnProxy (Proxy x) = x
 207
 208 {-
 209 -- ** Type family 'V'
 210 type family V (vs::[K.Type]) (i::Nat) :: k where
 211         V (v ': vs) 'Z  = UnProxy v
 212         V (not_v ': vs) ('S i) = V vs i
 213
 214 -- ** Type family 'KV'
 215 type family KV (vs::[K.Type]) (i::Nat) :: K.Type where
 216         KV (Proxy v ': vs) 'Z     = K v
 217         KV (not_v   ': vs) ('S i) = KV vs i
 218 -}