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.Semigroup (Semigroup(..))
   9 import Data.String (String)
  10 import Data.Type.Equality
  11
  12 import Language.Symantic.Grammar (Gram_Meta(..))
  13 import Language.Symantic.Helper.Data.Type.List
  14 import Language.Symantic.Helper.Data.Type.Peano
  15
  16 -- * Type 'Token'
  17 type Token src ts = TokenR src ts ts
  18
  19 -- ** Type 'TokenR'
  20 data TokenR src (ts::[*]) (rs::[*]) (t:: *) where
  21         TokenZ :: src -> TokenT src ts t -> TokenR src ts (t ': rs) t
  22         TokenS :: TokenR src ts rs t -> TokenR src ts (not_t ': rs) t
  23 infixr 5 `TokenS`
  24
  25 instance Source src => Sourced (TokenR src ts rs t) where
  26         type Source_of (TokenR src ts rs t) = src
  27         source_of (TokenZ src _) = src
  28         source_of (TokenS tok)   = source_of tok
  29         source_is (TokenZ _ tok) src = TokenZ src tok
  30         source_is (TokenS tok)   src = TokenS $ source_is tok src
  31
  32 -- ** Data family 'TokenT'
  33 data family TokenT src (ts::[*]) (t:: *) :: *
  34
  35 -- ** Type 'Eq_Token'
  36 type Eq_Token src ts = Eq_TokenR src ts ts
  37
  38 -- *** Type 'Eq_TokenR'
  39 instance (Eq src, Eq_TokenR src ts rs) => Eq (TokenR src ts rs t) where
  40         (==) = eq_TokenR (==)
  41 class Eq_TokenR src (ts::[*]) (rs::[*]) where
  42         eq_TokenR :: (src -> src -> Bool)
  43                   -> TokenR src ts rs x
  44                   -> TokenR src ts rs y -> Bool
  45 instance
  46  ( Eq (TokenT src ts t)
  47  , Eq_TokenR src ts (r ': rs)
  48  ) => Eq_TokenR src ts (t ': r ': rs) where
  49         eq_TokenR eq_Loc (TokenZ xl x) (TokenZ yl y) = xl `eq_Loc` yl && x == y
  50         eq_TokenR eq_Loc (TokenS x) (TokenS y) = eq_TokenR eq_Loc x y
  51         eq_TokenR _ _ _ = False
  52 instance
  53  ( Eq (TokenT src ts t)
  54  ) => Eq_TokenR src ts (t ': '[]) where
  55         eq_TokenR eq_Loc (TokenZ xl x) (TokenZ yl y) = xl `eq_Loc` yl && x == y
  56         eq_TokenR _ _ _ = False
  57
  58 -- ** Type 'TestEquality_Token'
  59 type TestEquality_Token  src ts
  60  =   TestEquality_TokenR src ts ts
  61
  62 -- *** Type 'TestEquality_TokenR'
  63 instance
  64  TestEquality_TokenR src ts rs =>
  65  TestEquality (TokenR src ts rs) where
  66         testEquality = testEqualityR
  67 class TestEquality_TokenR src (ts::[*]) (rs::[*]) where
  68         testEqualityR :: TokenR src ts rs x
  69                       -> TokenR src ts rs y
  70                       -> Maybe (x :~: y)
  71 instance
  72  ( Eq src
  73  , Eq (TokenT src ts t)
  74  , TestEquality_TokenR src ts (r ': rs)
  75  ) => TestEquality_TokenR src ts (t ': r ': rs) where
  76         testEqualityR (TokenZ _xl x) (TokenZ _yl y)
  77          | {-xl == yl &&-} x == y
  78          = Just Refl
  79         testEqualityR (TokenS x) (TokenS y) = testEqualityR x y
  80         testEqualityR _ _ = Nothing
  81 instance
  82  ( Eq src
  83  , Eq (TokenT src ts t)
  84  ) => TestEquality_TokenR src ts (t ': '[]) where
  85         testEqualityR (TokenZ _xl x) (TokenZ _yl y)
  86          | {-xl == yl &&-} x == y
  87          = Just Refl
  88         testEqualityR _ _ = Nothing
  89
  90 -- ** Type 'Show_Token'
  91 type Show_Token src ts = Show_TokenR src ts ts
  92
  93 -- *** Type 'Show_TokenR'
  94 instance Show_TokenR src ts rs => Show (TokenR src ts rs t) where
  95         show = show_TokenR
  96 class Show_TokenR src (ts::[*]) (rs::[*]) where
  97         show_TokenR :: TokenR src ts rs x -> String
  98 instance
  99  ( Show src
 100  , Show (TokenT src ts t)
 101  , Show_TokenR src ts (r ': rs)
 102  ) => Show_TokenR src ts (t ': r ': rs) where
 103         show_TokenR (TokenZ m t) = show (m, t)
 104         show_TokenR (TokenS rs) = show_TokenR rs
 105 instance
 106  ( Show src
 107  , Show (TokenT src ts t)
 108  ) => Show_TokenR src ts (t ': '[]) where
 109         show_TokenR (TokenZ m t) = show (m, t)
 110         show_TokenR TokenS{} = error "Oops, the impossible happened..."
 111
 112 -- ** Type 'EToken'
 113 -- | Existential 'Token'.
 114 data EToken src (ts::[*])
 115  = forall t. EToken (Token src ts t)
 116
 117 instance (Eq_Token src ts, Eq src) => Eq (EToken src ts) where
 118         EToken x == EToken y = eq_TokenR (==) x y
 119 instance Show_Token src ts => Show (EToken src ts) where
 120         show (EToken x) = show x
 121 instance Source src => Sourced (EToken src ts) where
 122         type Source_of (EToken src ts) = src
 123         source_of (EToken tok) = source_of tok
 124         source_is (EToken tok) src = EToken $ source_is tok src
 125
 126 -- * Type 'Inj_Token'
 127 -- | Convenient type synonym wrapping 'Inj_TokenP'
 128 -- applied on the correct 'Index'.
 129 type Inj_Token src ts t = Inj_TokenP (Index ts (Proxy t)) src ts ts t
 130
 131 inj_Token
 132  :: forall src ts t.
 133     Inj_Token src ts t
 134  => src
 135  -> TokenT src ts (Proxy t)
 136  -> Token  src ts (Proxy t)
 137 inj_Token = inj_TokenP (Proxy @(Index ts (Proxy t)))
 138
 139 inj_EToken
 140  :: forall src ts t.
 141     Inj_Token src ts t
 142  => src
 143  -> TokenT src ts (Proxy t)
 144  -> EToken src ts
 145 inj_EToken src = EToken . inj_TokenP (Proxy @(Index ts (Proxy t))) src
 146
 147 -- ** Class 'Inj_TokenP'
 148 class Inj_TokenP p src ts rs (t::kt) where
 149         inj_TokenP :: Proxy p -> src
 150          -> TokenT src ts    (Proxy t)
 151          -> TokenR src ts rs (Proxy t)
 152 instance Inj_TokenP Zero src ts (Proxy t ': rs) t where
 153         inj_TokenP _ = TokenZ
 154 instance
 155  Inj_TokenP p src ts rs t =>
 156  Inj_TokenP (Succ p) src ts (not_t ': rs) t where
 157         inj_TokenP _p src = TokenS . inj_TokenP (Proxy @p) src
 158
 159 -- ** Type 'Inj_Tokens'
 160 type Inj_Tokens src ts ts_to_inj
 161  = Concat_Constraints (Inj_TokensR src ts ts_to_inj)
 162
 163 -- *** Type family 'Inj_TokensR'
 164 type family Inj_TokensR src ts ts_to_inj where
 165  Inj_TokensR src ts '[] = '[]
 166  Inj_TokensR src ts (Proxy t ': rs) = Inj_Token src ts t ': Inj_TokensR src ts rs
 167
 168 -- * Class 'Proj_Token'
 169 -- | Convenient type synonym wrapping 'Proj_TokenP'
 170 -- applied on the correct 'Index'.
 171 type Proj_Token ts t = Proj_TokenP (Index ts (Proxy t)) ts ts t
 172
 173 proj_Token :: forall src ts t u.
 174  Proj_Token ts t
 175  => Token src ts u
 176  -> Maybe (Proxy t :~: u, src, TokenT src ts u)
 177 proj_Token = proj_TokenP (Proxy @(Index ts (Proxy t)))
 178
 179 proj_EToken :: forall src ts t.
 180  Proj_Token ts t
 181  => EToken src ts
 182  -> Maybe (src, TokenT src ts (Proxy t))
 183 proj_EToken (EToken (tok::TokenR src ts ts u)) =
 184         case proj_Token tok of
 185          Just (Refl :: Proxy t :~: u, src, to) -> Just (src, to)
 186          Nothing -> Nothing
 187
 188 -- ** Type 'Proj_TokenP'
 189 class Proj_TokenP p ts rs t where
 190         proj_TokenP
 191          :: Proxy p -> TokenR src ts rs u
 192          -> Maybe (Proxy t :~: u, src, TokenT src ts u)
 193 instance Proj_TokenP Zero ts (Proxy t ': rs) t where
 194         proj_TokenP _p (TokenZ src tok) = Just (Refl, src, tok)
 195         proj_TokenP _p TokenS{} = Nothing
 196 instance Proj_TokenP p ts rs t => Proj_TokenP (Succ p) ts (not_t ': rs) t where
 197         proj_TokenP _p TokenZ{}  = Nothing
 198         proj_TokenP _p (TokenS u) = proj_TokenP (Proxy @p) u
 199
 200 -- * Class 'Source'
 201 class Source src where
 202         sourceLess :: src
 203 instance Source () where
 204         sourceLess = ()
 205
 206 -- * Class 'Inj_Source'
 207 class Source src => Inj_Source a src where
 208         inj_Source :: a -> src
 209 instance Inj_Source a () where
 210         inj_Source _ = ()
 211
 212 -- ** Type 'Sourced'
 213 class Source (Source_of a) => Sourced a where
 214         type Source_of a
 215         source_of :: a -> Source_of a
 216         source_is :: a -> Source_of a -> a
 217 infixl 5 `source_is`
 218
 219 source :: (Inj_Source src (Source_of a), Sourced a) => a -> src -> a
 220 source a src = a `source_is` inj_Source src
 221
 222 -- ** Type 'Text_of_Source'
 223 type family Text_of_Source (src :: *) :: *
 224
 225 sourceG :: forall meta src g a.
 226  ( Gram_Meta meta g
 227  , meta ~ Text_of_Source src
 228  , Inj_Source meta src
 229  , Functor g
 230  ) => g (src -> a) -> g a
 231 sourceG g = metaG $ (\f (txt::Text_of_Source src) -> f (inj_Source txt :: src)) <$> g
 232
 233 -- * Type 'At'
 234 -- | Attach a source.
 235 data At src a
 236  =   At src a
 237  deriving (Eq, Show)
 238
 239 instance Functor (At src) where
 240         fmap f (At src a) = At src (f a)
 241 unAt :: At src a -> a
 242 unAt (At _ a) = a
 243
 244 -- * Type 'BinTree'
 245 -- | Binary Tree.
 246 data BinTree a
 247  =   BinTree0 a
 248  |   BinTree1 (BinTree a) (BinTree a)
 249  deriving (Eq, Show)
 250
 251 instance Semigroup (BinTree a) where
 252         (<>) = BinTree1
 253 instance Functor BinTree where
 254         fmap f (BinTree0 a)   = BinTree0 (f a)
 255         fmap f (BinTree1 x y) = BinTree1 (fmap f x) (fmap f y)
 256 instance Applicative BinTree where
 257         pure = BinTree0
 258         BinTree0 f     <*> BinTree0 a   = BinTree0 (f a)
 259         BinTree0 f     <*> BinTree1 x y = BinTree1 (f  <$> x) (f  <$> y)
 260         BinTree1 fx fy <*> a            = BinTree1 (fx <*> a) (fy <*> a)
 261 instance Monad BinTree where
 262         return = BinTree0
 263         BinTree0 a   >>= f = f a
 264         BinTree1 x y >>= f = BinTree1 (x >>= f) (y >>= f)
 265 instance Foldable BinTree where
 266         foldMap f (BinTree0 a)   = f a
 267         foldMap f (BinTree1 x y) = foldMap f x `mappend` foldMap f y
 268         foldr f acc (BinTree0 a)   = f a acc
 269         foldr f acc (BinTree1 x y) = foldr f (foldr f acc y) x
 270         foldl f acc (BinTree0 a)   = f acc a
 271         foldl f acc (BinTree1 x y) = foldl f (foldl f acc x) y
 272 instance Traversable BinTree where
 273         traverse f (BinTree0 a)   = BinTree0 <$> f a
 274         traverse f (BinTree1 x y) = BinTree1 <$> traverse f x <*> traverse f y