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.String (String)
   9 import Data.Type.Equality
  10 import Language.Symantic.Helper.Data.Type.List
  11 import Language.Symantic.Helper.Data.Type.Peano
  12
  13 -- * Type 'Token'
  14 type Token meta ts = TokenR meta ts ts
  15
  16 -- ** Type 'TokenR'
  17 data TokenR meta (ts::[*]) (rs::[*]) (t:: *) where
  18         TokenZ :: meta -> TokenT meta ts t
  19                -> TokenR meta ts (t ': rs) t
  20         TokenS :: TokenR meta ts rs t -> TokenR meta ts (not_t ': rs) t
  21 infixr 5 `TokenS`
  22
  23 -- ** Data family 'TokenT'
  24 data family TokenT meta (ts::[*]) (t:: *) :: *
  25
  26 -- ** Type 'Eq_Token'
  27 type Eq_Token meta ts = Eq_TokenR meta ts ts
  28
  29 -- *** Type 'Eq_TokenR'
  30 instance Eq_TokenR meta ts rs => Eq (TokenR meta ts rs t) where
  31         (==) = eq_TokenR
  32 class Eq_TokenR meta (ts::[*]) (rs::[*]) where
  33         eq_TokenR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Bool
  34 instance
  35  ( Eq meta
  36  , Eq (TokenT meta ts t)
  37  , Eq_TokenR meta ts (r ': rs)
  38  ) => Eq_TokenR meta ts (t ': r ': rs) where
  39         eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
  40         eq_TokenR (TokenS x) (TokenS y) = eq_TokenR x y
  41         eq_TokenR _ _ = False
  42 instance
  43  ( Eq meta
  44  , Eq (TokenT meta ts t)
  45  ) => Eq_TokenR meta ts (t ': '[]) where
  46         eq_TokenR (TokenZ mx x) (TokenZ my y) = mx == my && x == y
  47         eq_TokenR _ _ = False
  48
  49 -- ** Type 'TestEquality_Token'
  50 type TestEquality_Token meta ts = TestEquality_TokenR meta ts ts
  51
  52 -- *** Type 'TestEquality_TokenR'
  53 instance TestEquality_TokenR meta ts rs => TestEquality (TokenR meta ts rs) where
  54         testEquality = testEqualityR
  55 class TestEquality_TokenR meta (ts::[*]) (rs::[*]) where
  56         testEqualityR :: TokenR meta ts rs x -> TokenR meta ts rs y -> Maybe (x :~: y)
  57 instance
  58  ( Eq meta
  59  , Eq (TokenT meta ts t)
  60  , TestEquality_TokenR meta ts (r ': rs)
  61  ) => TestEquality_TokenR meta ts (t ': r ': rs) where
  62         testEqualityR (TokenZ mx x) (TokenZ my y)
  63          | mx == my && x == y
  64          = Just Refl
  65         testEqualityR (TokenS x) (TokenS y) = testEqualityR x y
  66         testEqualityR _ _ = Nothing
  67 instance
  68  ( Eq meta
  69  , Eq (TokenT meta ts t)
  70  ) => TestEquality_TokenR meta ts (t ': '[]) where
  71         testEqualityR (TokenZ mx x) (TokenZ my y)
  72          | mx == my && x == y
  73          = Just Refl
  74         testEqualityR _ _ = Nothing
  75
  76 -- ** Type 'Show_Token'
  77 type Show_Token meta ts = Show_TokenR meta ts ts
  78
  79 -- *** Type 'Show_TokenR'
  80 instance Show_TokenR meta ts rs => Show (TokenR meta ts rs t) where
  81         show = show_TokenR
  82 class Show_TokenR meta (ts::[*]) (rs::[*]) where
  83         show_TokenR :: TokenR meta ts rs x -> String
  84 instance
  85  ( Show meta
  86  , Show (TokenT meta ts t)
  87  , Show_TokenR meta ts (r ': rs)
  88  ) => Show_TokenR meta ts (t ': r ': rs) where
  89         show_TokenR (TokenZ m t) = show (m, t)
  90         show_TokenR (TokenS rs) = show_TokenR rs
  91 instance
  92  ( Show meta
  93  , Show (TokenT meta ts t)
  94  ) => Show_TokenR meta ts (t ': '[]) where
  95         show_TokenR (TokenZ m t) = show (m, t)
  96         show_TokenR TokenS{} = error "Oops, the impossible happened..."
  97
  98 -- ** Type 'EToken'
  99 -- | Existential 'Token'.
 100 data EToken meta (ts::[*]) = forall t. EToken (Token meta ts t)
 101
 102 instance Eq_Token meta ts => Eq (EToken meta ts) where
 103         EToken x == EToken y = eq_TokenR x y
 104 instance Show_Token meta ts => Show (EToken meta ts) where
 105         show (EToken x) = show x
 106
 107 -- * Type 'Inj_Token'
 108 -- | Convenient type synonym wrapping 'Inj_TokenP'
 109 -- applied on the correct 'Index'.
 110 type Inj_Token meta ts t = Inj_TokenP (Index ts (Proxy t)) meta ts ts t
 111
 112 inj_token
 113  :: forall meta ts t.
 114     Inj_Token meta ts t
 115  => meta
 116  -> TokenT meta ts (Proxy t)
 117  -> Token  meta ts (Proxy t)
 118 inj_token = inj_tokenP (Proxy @(Index ts (Proxy t)))
 119
 120 inj_EToken
 121  :: forall meta ts t.
 122     Inj_Token meta ts t
 123  => meta
 124  -> TokenT meta ts (Proxy t)
 125  -> EToken meta ts
 126 inj_EToken meta = EToken . inj_tokenP (Proxy @(Index ts (Proxy t))) meta
 127
 128 -- ** Class 'Inj_TokenP'
 129 class Inj_TokenP p meta ts rs (t::kt) where
 130         inj_tokenP :: Proxy p -> meta
 131          -> TokenT meta ts    (Proxy t)
 132          -> TokenR meta ts rs (Proxy t)
 133 instance Inj_TokenP Zero meta ts (Proxy t ': rs) t where
 134         inj_tokenP _ = TokenZ
 135 instance
 136  Inj_TokenP p meta ts rs t =>
 137  Inj_TokenP (Succ p) meta ts (not_t ': rs) t where
 138         inj_tokenP _p meta = TokenS . inj_tokenP (Proxy @p) meta
 139
 140 -- ** Type 'Inj_Tokens'
 141 type Inj_Tokens meta ts ts_to_inj
 142  = Concat_Constraints (Inj_TokensR meta ts ts_to_inj)
 143
 144 -- *** Type family 'Inj_TokensR'
 145 type family Inj_TokensR meta ts ts_to_inj where
 146  Inj_TokensR meta ts '[] = '[]
 147  Inj_TokensR meta ts (Proxy t ': rs) = Inj_Token meta ts t ': Inj_TokensR meta ts rs
 148
 149 -- * Class 'Proj_Token'
 150 -- | Convenient type synonym wrapping 'Proj_TokenP'
 151 -- applied on the correct 'Index'.
 152 type Proj_Token ts t = Proj_TokenP (Index ts (Proxy t)) ts ts t
 153
 154 proj_token :: forall meta ts t u.
 155  Proj_Token ts t
 156  => Token meta ts u
 157  -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
 158 proj_token = proj_tokenP (Proxy @(Index ts (Proxy t)))
 159
 160 proj_EToken :: forall meta ts t.
 161  Proj_Token ts t
 162  => EToken meta ts
 163  -> Maybe (TokenT meta ts (Proxy t))
 164 proj_EToken (EToken (tok::TokenR meta ts ts u)) =
 165         case proj_token tok of
 166          Just (Refl :: Proxy t :~: u, _meta, tokD) -> Just tokD
 167          Nothing -> Nothing
 168
 169 -- ** Type 'Proj_TokenP'
 170 class Proj_TokenP p ts rs t where
 171         proj_tokenP
 172          :: Proxy p -> TokenR meta ts rs u
 173          -> Maybe (Proxy t :~: u, meta, TokenT meta ts u)
 174 instance Proj_TokenP Zero ts (Proxy t ': rs) t where
 175         proj_tokenP _p (TokenZ meta tok) = Just (Refl, meta, tok)
 176         proj_tokenP _p TokenS{} = Nothing
 177 instance Proj_TokenP p ts rs t => Proj_TokenP (Succ p) ts (not_t ': rs) t where
 178         proj_tokenP _p TokenZ{}  = Nothing
 179         proj_tokenP _p (TokenS u) = proj_tokenP (Proxy @p) u
 180
 181 -- * Type 'At'
 182 -- | Attach a location.
 183 data At meta ts a
 184  =   At (Maybe (EToken meta ts)) a
 185 deriving instance (Eq_Token meta ts, Eq a) => Eq (At meta ts a)
 186 deriving instance (Show_Token meta ts, Show a) => Show (At meta ts a)
 187 instance Functor (At meta ts) where
 188         fmap f (At at a) = At at (f a)
 189 unAt :: At meta ts a -> a
 190 unAt (At _ a) = a
 191
 192 -- * Class 'Meta_of'
 193 class Meta_of tok where
 194         type Meta_Of tok
 195         meta_of :: tok -> Meta_Of tok
 196 instance Meta_of (TokenR meta ts rs t) where
 197         type Meta_Of (TokenR meta ts rs t) = meta
 198         meta_of (TokenZ m _) = m
 199         meta_of (TokenS t) = meta_of t
 200 instance Meta_of (EToken meta ts) where
 201         type Meta_Of (EToken meta ts) = meta
 202         meta_of (EToken t) = meta_of t