]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Parsing/Token.hs
Renaming textI_app* to textI*.
[haskell/symantic.git] / 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.Lib.Data.Type.List
11 import Language.Symantic.Lib.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::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::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::Proxy p) meta
139
140 -- * Class 'Proj_Token'
141 -- | Convenient type synonym wrapping 'Proj_TokenP'
142 -- applied on the correct 'Index'.
143 type Proj_Token ts t = Proj_TokenP (Index ts (Proxy t)) ts ts t
144
145 proj_token :: forall meta ts t u.
146 Proj_Token ts t
147 => Token meta ts u
148 -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
149 proj_token = proj_tokenP (Proxy::Proxy (Index ts (Proxy t)))
150
151 proj_etoken :: forall meta ts t.
152 Proj_Token ts t
153 => EToken meta ts
154 -> Maybe (TokenT meta ts (Proxy t))
155 proj_etoken (EToken (tok::TokenR meta ts ts u)) =
156 case proj_token tok of
157 Just (Refl :: Proxy t :~: u, _meta, tokD) -> Just tokD
158 Nothing -> Nothing
159
160 -- ** Type 'Proj_TokenP'
161 class Proj_TokenP p ts rs t where
162 proj_tokenP
163 :: Proxy p -> TokenR meta ts rs u
164 -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
165 instance Proj_TokenP Zero ts (Proxy t ': rs) t where
166 proj_tokenP _p (TokenZ meta tok) = Just (Refl, meta, tok)
167 proj_tokenP _p TokenS{} = Nothing
168 instance Proj_TokenP p ts rs t => Proj_TokenP (Succ p) ts (not_t ': rs) t where
169 proj_tokenP _p TokenZ{} = Nothing
170 proj_tokenP _p (TokenS u) = proj_tokenP (Proxy::Proxy p) u
171
172 -- * Type 'At'
173 -- | Attach a location.
174 data At meta ts a
175 = At (Maybe (EToken meta ts)) a
176 deriving instance (Eq_Token meta ts, Eq a) => Eq (At meta ts a)
177 deriving instance (Show_Token meta ts, Show a) => Show (At meta ts a)
178 instance Functor (At meta ts) where
179 fmap f (At at a) = At at (f a)
180 unAt :: At meta ts a -> a
181 unAt (At _ a) = a
182
183 -- * Class 'Meta_of'
184 class Meta_of tok where
185 type Meta_Of tok
186 meta_of :: tok -> Meta_Of tok
187 instance Meta_of (TokenR meta ts rs t) where
188 type Meta_Of (TokenR meta ts rs t) = meta
189 meta_of (TokenZ m _) = m
190 meta_of (TokenS t) = meta_of t
191 instance Meta_of (EToken meta ts) where
192 type Meta_Of (EToken meta ts) = meta
193 meta_of (EToken t) = meta_of t