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