Language/Symantic/Parsing/Token.hs

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