]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Parsing/Token.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic / Language / Symantic / Parsing / Token.hs
1 -- | Legacy code no longer used, for reminder only.
2 module Language.Symantic.Parsing.Token where
3
4 import Data.Semigroup (Semigroup(..))
5
6 import Language.Symantic.Grammar (Gram_Meta(..))
7
8 -- * Type 'Token'
9 type Token ss = TokenR ss ss
10
11 -- ** Type 'TokenR'
12 data TokenR (ss::[*]) (rs::[*]) (s:: *) where
13 TokenZ :: TokenT ss s -> TokenR ss (s ': rs) s
14 TokenS :: TokenR ss rs s -> TokenR ss (not_s ': rs) s
15 infixr 5 `TokenS`
16
17 -- ** Data family 'TokenT'
18 data family TokenT (ss::[*]) (s:: *) :: *
19
20 -- * Class 'Eq_Token'
21 type Eq_Token ss = TestEquality (Token ss)
22 instance
23 ( Eq (TokenT ss (Proxy s))
24 , TestEquality (TokenR ss (r ': rs))
25 ) => TestEquality (TokenR ss (Proxy s ': r ': rs)) where
26 ctxtEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
27 ctxtEquality (TokenS x) (TokenS y) | Just Refl <- ctxtEquality x y = Just Refl
28 ctxtEquality _ _ = Nothing
29 instance
30 Eq (TokenT ss (Proxy s)) =>
31 TestEquality (TokenR ss (Proxy s ': '[])) where
32 ctxtEquality (TokenZ x) (TokenZ y) | x == y = Just Refl
33 ctxtEquality _ _ = Nothing
34 instance TestEquality (TokenR ss rs) => Eq (TokenR ss rs s) where
35 x == y = isJust $ ctxtEquality x y
36
37 -- ** Type 'Show_Token'
38 type Show_Token ss = Show_TokenR ss ss
39
40 -- *** Type 'Show_TokenR'
41 class Show_TokenR (ss::[*]) (rs::[*]) where
42 show_TokenR :: TokenR ss rs x -> String
43 instance
44 ( Show (TokenT ss (Proxy s))
45 , Show_TokenR ss (r ': rs)
46 ) => Show_TokenR ss (Proxy s ': r ': rs) where
47 show_TokenR (TokenZ s) = show s
48 show_TokenR (TokenS rs) = show_TokenR rs
49 instance
50 Show (TokenT ss (Proxy s)) =>
51 Show_TokenR ss (Proxy s ': '[]) where
52 show_TokenR (TokenZ s) = show s
53 show_TokenR TokenS{} = error "Oops, the impossible happened..."
54 instance Show_TokenR ss rs => Show (TokenR ss rs s) where
55 show = show_TokenR
56
57 -- * Type 'Inj_Token'
58 -- | Convenient type synonym wrapping 'Inj_TokenP'
59 -- applied on the correct 'Index'.
60 type Inj_Token ss s
61 = Inj_TokenP (Index ss (Proxy s)) ss ss s
62
63 inj_Token
64 :: forall ss s. Inj_Token ss s
65 => TokenT ss (Proxy s)
66 -> Token ss (Proxy s)
67 inj_Token = inj_TokenP (Proxy @(Index ss (Proxy s)))
68
69 -- ** Class 'Inj_TokenP'
70 class Inj_TokenP p ss rs (s::ks) where
71 inj_TokenP :: Proxy p -> TokenT ss (Proxy s) -> TokenR ss rs (Proxy s)
72 instance Inj_TokenP Zero ss (Proxy s ': rs) s where
73 inj_TokenP _ = TokenZ
74 instance
75 Inj_TokenP p ss rs s =>
76 Inj_TokenP (Succ p) ss (not_t ': rs) s where
77 inj_TokenP _p = TokenS . inj_TokenP (Proxy @p)
78
79 -- ** Type 'Inj_Tokens'
80 type Inj_Tokens ss ts_to_inj
81 = Concat_Constraints (Inj_TokensR ss ts_to_inj)
82
83 -- *** Type family 'Inj_TokensR'
84 type family Inj_TokensR ss ts_to_inj where
85 Inj_TokensR ss '[] = '[]
86 Inj_TokensR ss (Proxy s ': rs) = Inj_Token ss s ': Inj_TokensR ss rs
87
88 -- * Class 'Proj_Token'
89 -- | Convenient type synonym wrapping 'Proj_TokenP'
90 -- applied on the correct 'Index'.
91 type Proj_Token ss s
92 = Proj_TokenP (Index ss (Proxy s)) ss ss s
93
94 proj_Token
95 :: forall ss s u.
96 Proj_Token ss s
97 => Token ss u
98 -> Maybe (Proxy s :~: u, TokenT ss u)
99 proj_Token = proj_TokenP (Proxy @(Index ss (Proxy s)))
100
101 -- ** Type 'Proj_TokenP'
102 class Proj_TokenP p ss rs s where
103 proj_TokenP
104 :: Proxy p -> TokenR ss rs u
105 -> Maybe (Proxy s :~: u, TokenT ss u)
106 instance Proj_TokenP Zero ss (Proxy s ': rs) s where
107 proj_TokenP _p (TokenZ tok) = Just (Refl, tok)
108 proj_TokenP _p TokenS{} = Nothing
109 instance Proj_TokenP p ss rs s => Proj_TokenP (Succ p) ss (not_t ': rs) s where
110 proj_TokenP _p TokenZ{} = Nothing
111 proj_TokenP _p (TokenS u) = proj_TokenP (Proxy @p) u
112
113 -- ** Type 'EToken'
114 -- | Existential 'Token'.
115 data EToken src (ss::[*])
116 = forall s. EToken src (Token ss (Proxy s))
117
118 instance Eq_Token ss => Eq (EToken src ss) where
119 EToken _sx x == EToken _sy y = isJust $ ctxtEquality x y
120 instance Show_Token ss => Show (EToken src ss) where
121 show (EToken _src x) = show x
122 type instance SourceOf (EToken src ss) = src
123 instance Source src => Sourceable (EToken src ss) where
124 sourceOf (EToken src _tok) = src
125 setSource (EToken _src tok) src = EToken src tok
126
127 inj_EToken
128 :: forall src ss s.
129 Inj_Token ss s
130 => src -> TokenT ss (Proxy s) -> EToken src ss
131 inj_EToken src = EToken src . inj_TokenP (Proxy @(Index ss (Proxy s)))
132
133 proj_EToken
134 :: forall src ss s.
135 Proj_Token ss s
136 => EToken src ss
137 -> Maybe (src, TokenT ss (Proxy s))
138 proj_EToken (EToken src (tok::TokenR ss ss (Proxy u))) =
139 case proj_Token tok of
140 Just (Refl :: Proxy s :~: Proxy u, to) -> Just (src, to)
141 Nothing -> Nothing