]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Variable.hs
Add some Eq and Show instances.
[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 -- | /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 Inj_Source (EVar src vs) src => KindOf (Var src vs) where
38 kindOf v = kindOfVar v `source` 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 Inj_Len vs =>
53 Inj_Kind kv =>
54 Var src (Proxy v ': vs) v
55 varZ = VarZ inj_Kind inj_Len
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 -}