]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Variable.hs
Sync with ghc-8.2.2 and megaparsec-6.3.0.
[haskell/symantic.git] / 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 -}