symantic/Language/Symantic/Parsing/Token.hs

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