]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Parsing/Token.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic / Language / Symantic / Parsing / Token.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 module Language.Symantic.Parsing.Token where
6
7 import Data.Proxy (Proxy(..))
8 import Data.String (String)
9 import Data.Type.Equality
10 import Language.Symantic.Helper.Data.Type.List
11 import Language.Symantic.Helper.Data.Type.Peano
12
13 -- * Type 'Token'
14 type Token meta ts = TokenR meta ts ts
15
16 -- ** Type 'TokenR'
17 data TokenR meta (ts::[*]) (rs::[*]) (t:: *) where
18 TokenZ :: meta -> TokenT meta ts t
19 -> TokenR meta ts (t ': rs) t
20 TokenS :: TokenR meta ts rs t -> TokenR meta ts (not_t ': rs) t
21 infixr 5 `TokenS`
22
23 -- ** Data family 'TokenT'
24 data family TokenT meta (ts::[*]) (t:: *) :: *
25
26 -- ** Type 'Eq_Token'
27 type Eq_Token meta ts = Eq_TokenR meta ts ts
28
29 -- *** Type 'Eq_TokenR'
30 instance Eq_TokenR meta ts rs => Eq (TokenR meta ts rs t) where
31 (==) = eq_TokenR
32 class Eq_TokenR meta (ts::[*]) (rs::[*]) where
33 eq_TokenR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Bool
34 instance
35 ( Eq meta
36 , Eq (TokenT meta ts t)
37 , Eq_TokenR meta ts (r ': rs)
38 ) => Eq_TokenR meta ts (t ': r ': rs) where
39 eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
40 eq_TokenR (TokenS x) (TokenS y) = eq_TokenR x y
41 eq_TokenR _ _ = False
42 instance
43 ( Eq meta
44 , Eq (TokenT meta ts t)
45 ) => Eq_TokenR meta ts (t ': '[]) where
46 eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
47 eq_TokenR _ _ = False
48
49 -- ** Type 'TestEquality_Token'
50 type TestEquality_Token meta ts = TestEquality_TokenR meta ts ts
51
52 -- *** Type 'TestEquality_TokenR'
53 instance TestEquality_TokenR meta ts rs => TestEquality (TokenR meta ts rs) where
54 testEquality = testEqualityR
55 class TestEquality_TokenR meta (ts::[*]) (rs::[*]) where
56 testEqualityR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Maybe (x :~: y)
57 instance
58 ( Eq meta
59 , Eq (TokenT meta ts t)
60 , TestEquality_TokenR meta ts (r ': rs)
61 ) => TestEquality_TokenR meta ts (t ': r ': rs) where
62 testEqualityR (TokenZ mx x) (TokenZ my y)
63 | mx == my && x == y
64 = Just Refl
65 testEqualityR (TokenS x) (TokenS y) = testEqualityR x y
66 testEqualityR _ _ = Nothing
67 instance
68 ( Eq meta
69 , Eq (TokenT meta ts t)
70 ) => TestEquality_TokenR meta ts (t ': '[]) where
71 testEqualityR (TokenZ mx x) (TokenZ my y)
72 | mx == my && x == y
73 = Just Refl
74 testEqualityR _ _ = Nothing
75
76 -- ** Type 'Show_Token'
77 type Show_Token meta ts = Show_TokenR meta ts ts
78
79 -- *** Type 'Show_TokenR'
80 instance Show_TokenR meta ts rs => Show (TokenR meta ts rs t) where
81 show = show_TokenR
82 class Show_TokenR meta (ts::[*]) (rs::[*]) where
83 show_TokenR :: TokenR meta ts rs x -> String
84 instance
85 ( Show meta
86 , Show (TokenT meta ts t)
87 , Show_TokenR meta ts (r ': rs)
88 ) => Show_TokenR meta ts (t ': r ': rs) where
89 show_TokenR (TokenZ m t) = show (m, t)
90 show_TokenR (TokenS rs) = show_TokenR rs
91 instance
92 ( Show meta
93 , Show (TokenT meta ts t)
94 ) => Show_TokenR meta ts (t ': '[]) where
95 show_TokenR (TokenZ m t) = show (m, t)
96 show_TokenR TokenS{} = error "Oops, the impossible happened..."
97
98 -- ** Type 'EToken'
99 -- | Existential 'Token'.
100 data EToken meta (ts::[*]) = forall t. EToken (Token meta ts t)
101
102 instance Eq_Token meta ts => Eq (EToken meta ts) where
103 EToken x == EToken y = eq_TokenR x y
104 instance Show_Token meta ts => Show (EToken meta ts) where
105 show (EToken x) = show x
106
107 -- * Type 'Inj_Token'
108 -- | Convenient type synonym wrapping 'Inj_TokenP'
109 -- applied on the correct 'Index'.
110 type Inj_Token meta ts t = Inj_TokenP (Index ts (Proxy t)) meta ts ts t
111
112 inj_token
113 :: forall meta ts t.
114 Inj_Token meta ts t
115 => meta
116 -> TokenT meta ts (Proxy t)
117 -> Token meta ts (Proxy t)
118 inj_token = inj_tokenP (Proxy @(Index ts (Proxy t)))
119
120 inj_EToken
121 :: forall meta ts t.
122 Inj_Token meta ts t
123 => meta
124 -> TokenT meta ts (Proxy t)
125 -> EToken meta ts
126 inj_EToken meta = EToken . inj_tokenP (Proxy @(Index ts (Proxy t))) meta
127
128 -- ** Class 'Inj_TokenP'
129 class Inj_TokenP p meta ts rs (t::kt) where
130 inj_tokenP :: Proxy p -> meta
131 -> TokenT meta ts (Proxy t)
132 -> TokenR meta ts rs (Proxy t)
133 instance Inj_TokenP Zero meta ts (Proxy t ': rs) t where
134 inj_tokenP _ = TokenZ
135 instance
136 Inj_TokenP p meta ts rs t =>
137 Inj_TokenP (Succ p) meta ts (not_t ': rs) t where
138 inj_tokenP _p meta = TokenS . inj_tokenP (Proxy @p) meta
139
140 -- ** Type 'Inj_Tokens'
141 type Inj_Tokens meta ts ts_to_inj
142 = Concat_Constraints (Inj_TokensR meta ts ts_to_inj)
143
144 -- *** Type family 'Inj_TokensR'
145 type family Inj_TokensR meta ts ts_to_inj where
146 Inj_TokensR meta ts '[] = '[]
147 Inj_TokensR meta ts (Proxy t ': rs) = Inj_Token meta ts t ': Inj_TokensR meta ts rs
148
149 -- * Class 'Proj_Token'
150 -- | Convenient type synonym wrapping 'Proj_TokenP'
151 -- applied on the correct 'Index'.
152 type Proj_Token ts t = Proj_TokenP (Index ts (Proxy t)) ts ts t
153
154 proj_token :: forall meta ts t u.
155 Proj_Token ts t
156 => Token meta ts u
157 -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
158 proj_token = proj_tokenP (Proxy @(Index ts (Proxy t)))
159
160 proj_EToken :: forall meta ts t.
161 Proj_Token ts t
162 => EToken meta ts
163 -> Maybe (TokenT meta ts (Proxy t))
164 proj_EToken (EToken (tok::TokenR meta ts ts u)) =
165 case proj_token tok of
166 Just (Refl :: Proxy t :~: u, _meta, tokD) -> Just tokD
167 Nothing -> Nothing
168
169 -- ** Type 'Proj_TokenP'
170 class Proj_TokenP p ts rs t where
171 proj_tokenP
172 :: Proxy p -> TokenR meta ts rs u
173 -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
174 instance Proj_TokenP Zero ts (Proxy t ': rs) t where
175 proj_tokenP _p (TokenZ meta tok) = Just (Refl, meta, tok)
176 proj_tokenP _p TokenS{} = Nothing
177 instance Proj_TokenP p ts rs t => Proj_TokenP (Succ p) ts (not_t ': rs) t where
178 proj_tokenP _p TokenZ{} = Nothing
179 proj_tokenP _p (TokenS u) = proj_tokenP (Proxy @p) u
180
181 -- * Type 'At'
182 -- | Attach a location.
183 data At meta ts a
184 = At (Maybe (EToken meta ts)) a
185 deriving instance (Eq_Token meta ts, Eq a) => Eq (At meta ts a)
186 deriving instance (Show_Token meta ts, Show a) => Show (At meta ts a)
187 instance Functor (At meta ts) where
188 fmap f (At at a) = At at (f a)
189 unAt :: At meta ts a -> a
190 unAt (At _ a) = a
191
192 -- * Class 'Meta_of'
193 class Meta_of tok where
194 type Meta_Of tok
195 meta_of :: tok -> Meta_Of tok
196 instance Meta_of (TokenR meta ts rs t) where
197 type Meta_Of (TokenR meta ts rs t) = meta
198 meta_of (TokenZ m _) = m
199 meta_of (TokenS t) = meta_of t
200 instance Meta_of (EToken meta ts) where
201 type Meta_Of (EToken meta ts) = meta
202 meta_of (EToken t) = meta_of t