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