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