symantic/Language/Symantic/Compiling/Term/Grammar.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DeriveFunctor #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   5 {-# LANGUAGE PolyKinds #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 module Language.Symantic.Compiling.Term.Grammar where
   9
  10 import Control.Arrow (left)
  11 import Control.Monad (foldM, void, (=<<))
  12 import qualified Data.Char as Char
  13 import qualified Data.Function as Fun
  14 import           Data.Map.Strict (Map)
  15 import qualified Data.Map.Strict as Map
  16 import Data.Proxy (Proxy(..))
  17 import Data.Semigroup (Semigroup(..))
  18 import Data.String (IsString(..))
  19 import Data.Text (Text)
  20 import qualified Data.Text as Text
  21 import Prelude hiding (mod, not, any)
  22
  23 import Language.Symantic.Parsing
  24 import Language.Symantic.Typing
  25
  26 -- * Type 'TeName'
  27 newtype TeName = TeName Text
  28  deriving (Eq, Ord, Show)
  29 instance IsString TeName where
  30         fromString = TeName . fromString
  31
  32 -- * Type 'ProTok'
  33 -- | Proto 'EToken'. It's almost like a free monad,
  34 -- but with more constructors to avoid the need
  35 -- for sub constructors when requiring a type rather than a term.
  36 --
  37 -- NOTE: this type may one day be removed
  38 -- if proper polymorphic types are implemented.
  39 -- In the meantime it is used to require
  40 -- term or type arguments needed to build
  41 -- the 'EToken's of polymorphic terms.
  42 data ProTok meta ts
  43  =   ProTokLam (EToken meta ts -> ProTok meta ts)
  44      -- ^ Require a term argument.
  45  |   ProTokPi  (EToken meta '[Proxy Token_Type] -> ProTok meta ts)
  46      -- ^ Require a type argument.
  47  |   ProTokTe  (EToken meta ts)
  48      -- ^ Immediat term, no need for any argument.
  49  |   ProTokTy  (EToken meta '[Proxy Token_Type])
  50      -- ^ Immediat type, no need for any argument.
  51  |   ProTokApp
  52      -- ^ Require a term argument to perform a 'Token_Term_App'.
  53      --
  54      -- Useful to make the term application symbolized by a space
  55      -- be an operator, and thus be integrated with the other operators.
  56      -- This enables prefix and postfix operators to be applied
  57      -- before the term application.
  58 instance (Show_Token meta ts, Show meta) => Show (ProTok meta ts) where
  59         showsPrec n ProTokLam{}    = showParen (n > 10) $ showString "ProTokLam"
  60         showsPrec n ProTokPi{}     = showParen (n > 10) $ showString "ProTokPi"
  61         showsPrec n (ProTokTe tok) = showParen (n > 10) $ showString "ProTokTe " . showsPrec 11 tok
  62         showsPrec n (ProTokTy typ) = showParen (n > 10) $ showString "ProTokTe " . showsPrec 11 typ
  63         showsPrec n ProTokApp      = showParen (n > 10) $ showString "ProTokApp"
  64
  65 -- | Declared here and not in @Compiling.Lambda@
  66 -- to be able to use 'Token_Term_Var'.
  67 data instance TokenT meta (ts::[*]) (Proxy (->))
  68  = Token_Term_Abst    TeName (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  69  | Token_Term_App            (EToken meta ts) (EToken meta ts)
  70  | Token_Term_Let     TeName (EToken meta ts) (EToken meta ts)
  71  | Token_Term_Var     TeName
  72  | Token_Term_Compose        (EToken meta ts) (EToken meta ts)
  73
  74 -- * Class 'Tokenize'
  75 type Tokenize  meta ts
  76  =   TokenizeR meta ts ts
  77
  78 -- ** Type 'Tokenizers'
  79 data Tokenizers meta ts
  80  =   Tokenizers
  81  {   tokenizers_prefix  :: Map Mod_Path (Map TeName (ProTok_Term Unifix meta ts))
  82  ,   tokenizers_infix   :: Map Mod_Path (Map TeName (ProTok_Term Infix  meta ts))
  83  ,   tokenizers_postfix :: Map Mod_Path (Map TeName (ProTok_Term Unifix meta ts))
  84  }
  85 deriving instance
  86  ( Show (ProTok_Term Unifix meta ts)
  87  , Show (ProTok_Term Infix  meta ts)
  88  ) => Show (Tokenizers meta ts)
  89 instance Semigroup (Tokenizers meta ts) where
  90         x <> y =
  91                 Tokenizers
  92                  (Map.unionWith Map.union
  93                          (tokenizers_prefix x)
  94                          (tokenizers_prefix y))
  95                  (Map.unionWith Map.union
  96                          (tokenizers_infix x)
  97                          (tokenizers_infix y))
  98                  (Map.unionWith Map.union
  99                          (tokenizers_postfix x)
 100                          (tokenizers_postfix y))
 101 instance Monoid (Tokenizers meta ts) where
 102         mempty  = Tokenizers Map.empty Map.empty Map.empty
 103         mappend = (<>)
 104
 105 -- ** Type 'ProTok_Term'
 106 data ProTok_Term fixy meta ts
 107  =   ProTok_Term
 108  {   protok_term   :: meta -> ProTok meta ts
 109  ,   protok_fixity :: fixy
 110  }
 111
 112 tokenizers :: forall meta ts. Tokenize meta ts => Tokenizers meta ts
 113 tokenizers = tokenizeR (Proxy @ts)
 114
 115 unProTok
 116  :: ProTok meta ts
 117  -> Either Error_Term_Gram (EToken meta ts)
 118 unProTok (ProTokTe t) = Right t
 119 unProTok (ProTokTy _) = Left $ Error_Term_Gram_Type_applied_to_nothing
 120 unProTok _tok         = Left $ Error_Term_Gram_Term_incomplete
 121
 122 -- | Lookup the given 'Mod' 'TeName' into the given 'Tokenizers',
 123 -- returning an error or a 'ProTok' constructor for prefix, infix and postfix positions.
 124 protok_lookup
 125  :: Inj_Token meta ts (->)
 126  => Mod TeName
 127  -> Tokenizers meta ts
 128  -> Either Error_Term_Gram
 129            ( Maybe (ProTok_Term Unifix meta ts)
 130            , Maybe (ProTok_Term Infix  meta ts)
 131            , Maybe (ProTok_Term Unifix meta ts)
 132            )
 133 protok_lookup mn@(mod `Mod` n) (Tokenizers pres ins posts) = do
 134         let pre  = Map.lookup mod pres  >>= Map.lookup n
 135         let post = Map.lookup mod posts >>= Map.lookup n
 136         let in_ =
 137                 case mn of
 138                  [] `Mod` " " -> Just
 139                         ProTok_Term
 140                          { protok_term = \_meta -> ProTokApp
 141                          , protok_fixity = Infix (Just AssocL) 9
 142                          }
 143                  _ -> Map.lookup mod ins >>= Map.lookup n
 144         return (pre, in_, post)
 145
 146 -- | Apply a proto-token to another.
 147 --
 148 -- This is required because polymorphic types are not implemented (yet),
 149 -- therefore tokens for polymorphic types must have enough 'EToken's
 150 -- to make them monomorphic types.
 151 protok_app
 152  :: Inj_Token meta ts (->)
 153  => ProTok meta ts
 154  -> ProTok meta ts
 155  -> Either Error_Term_Gram (ProTok meta ts)
 156 protok_app (ProTokLam f) (ProTokTe a) = Right $ f a
 157 protok_app (ProTokPi  f) (ProTokTy a) = Right $ f a
 158 protok_app (ProTokTe f) (ProTokTe a) =
 159         Right $ ProTokTe $ inj_EToken (meta_of f) $ -- TODO: merge (meta_of a)
 160         f `Token_Term_App` a
 161 protok_app ProTokApp f@ProTokLam{} = Right f
 162 protok_app ProTokApp f@ProTokPi{}  = Right f
 163 protok_app ProTokApp (ProTokTe f) =
 164         Right $ ProTokLam $ \a ->
 165         ProTokTe $ inj_EToken (meta_of f) $ -- TODO: merge (meta_of a)
 166         f `Token_Term_App` a
 167 protok_app ProTokLam{} _ = Left $ Error_Term_Gram_application_mismatch
 168 protok_app ProTokPi{}  _ = Left $ Error_Term_Gram_application_mismatch
 169 protok_app ProTokTe{}  _ = Left $ Error_Term_Gram_not_applicable
 170 protok_app ProTokTy{}  _ = Left $ Error_Term_Gram_not_applicable
 171 protok_app ProTokApp{} _ = Left $ Error_Term_Gram_application
 172
 173 -- ** Class 'TokenizeR'
 174 class TokenizeR meta (ts::[*]) (rs::[*]) where
 175         tokenizeR :: Proxy rs -> Tokenizers meta ts
 176 instance TokenizeR meta ts '[] where
 177         tokenizeR _rs = mempty
 178 instance
 179  ( TokenizeT meta ts t
 180  , TokenizeR meta ts rs
 181  ) => TokenizeR meta ts (t ': rs) where
 182         tokenizeR _ =
 183                 tokenizeR (Proxy @rs) <>
 184                 tokenizeT (Proxy @t)
 185
 186 -- ** Class 'TokenizeT'
 187 class TokenizeT meta ts t where
 188         tokenizeT :: Proxy t -> Tokenizers meta ts
 189         -- tokenizeT _t = [] `Mod` []
 190         tokenizeT _t = mempty
 191
 192 tokenizeTMod
 193  :: Mod_Path
 194  -> [(TeName, ProTok_Term fix meta ts)]
 195  -> Map Mod_Path (Map TeName (ProTok_Term fix meta ts))
 196 tokenizeTMod mod tbl = Map.singleton mod $ Map.fromList tbl
 197
 198 tokenize0
 199  :: Inj_Token meta ts t
 200  => Text -> fixity -> TokenT meta ts (Proxy t)
 201  -> (TeName, ProTok_Term fixity meta ts)
 202 tokenize0 n protok_fixity tok =
 203         (TeName n,) ProTok_Term
 204          { protok_term = \meta -> ProTokTe $ inj_EToken meta $ tok
 205          , protok_fixity }
 206
 207 tokenize1
 208  :: Inj_Token meta ts t
 209  => Text -> fixity
 210  -> (EToken meta ts -> TokenT meta ts (Proxy t))
 211  -> (TeName, ProTok_Term fixity meta ts)
 212 tokenize1 n protok_fixity tok =
 213         (TeName n,) ProTok_Term
 214          { protok_term = \meta ->
 215                 ProTokLam $ \a ->
 216                 ProTokTe $ inj_EToken meta $ tok a
 217          , protok_fixity }
 218
 219 tokenize2
 220  :: Inj_Token meta ts t
 221  => Text -> fixity
 222  -> (EToken meta ts -> EToken meta ts -> TokenT meta ts (Proxy t))
 223  -> (TeName, ProTok_Term fixity meta ts)
 224 tokenize2 n protok_fixity tok =
 225         (TeName n,) ProTok_Term
 226          { protok_term = \meta ->
 227                 ProTokLam $ \a -> ProTokLam $ \b ->
 228                 ProTokTe $ inj_EToken meta $ tok a b
 229          , protok_fixity
 230          }
 231
 232 tokenize3
 233  :: Inj_Token meta ts t
 234  => Text -> fixity
 235  -> (EToken meta ts -> EToken meta ts -> EToken meta ts -> TokenT meta ts (Proxy t))
 236  -> (TeName, ProTok_Term fixity meta ts)
 237 tokenize3 n protok_fixity tok =
 238         (TeName n,) ProTok_Term
 239          { protok_term = \meta ->
 240                 ProTokLam $ \a -> ProTokLam $ \b -> ProTokLam $ \c ->
 241                 ProTokTe $ inj_EToken meta $ tok a b c
 242          , protok_fixity
 243          }
 244
 245 -- * Type 'Mod'
 246 type Mod_Path = [Mod_Name]
 247 newtype Mod_Name = Mod_Name Text
 248  deriving (Eq, Ord, Show)
 249 data Mod a = Mod Mod_Path a
 250  deriving (Eq, Functor, Ord, Show)
 251
 252 -- * Class 'Gram_Name'
 253 class
 254  ( Alt g
 255  , Alter g
 256  , Alter g
 257  , App g
 258  , Try g
 259  , Gram_CF g
 260  , Gram_Op g
 261  , Gram_Lexer g
 262  , Gram_RegL g
 263  , Gram_Rule g
 264  , Gram_Terminal g
 265  ) => Gram_Name g where
 266         g_mod_path :: CF g Mod_Path
 267         g_mod_path = rule "mod_path" $
 268                 infixrG
 269                  (pure <$> g_mod_name)
 270                  (op <$ char '.')
 271                 where op = (<>)
 272         g_mod_name :: CF g Mod_Name
 273         g_mod_name = rule "mod_name" $
 274                 (Mod_Name . Text.pack <$>) $
 275                 (identG `minus`) $
 276                 Fun.const
 277                  <$> g_term_keywords
 278                  <*. (any `but` g_term_idname_tail)
 279                 where
 280                 identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
 281                 headG  = unicat $ Unicat Char.UppercaseLetter
 282
 283         g_term_mod_name :: CF g (Mod TeName)
 284         g_term_mod_name = rule "term_mod_name" $
 285                 lexeme $
 286                         g_term_mod_idname <+>
 287                         parens g_term_mod_opname
 288         g_term_name :: CF g TeName
 289         g_term_name = rule "term_name" $
 290                 lexeme $
 291                         g_term_idname <+>
 292                         parens g_term_opname
 293
 294         g_term_mod_idname :: CF g (Mod TeName)
 295         g_term_mod_idname = rule "term_mod_idname" $
 296                 Mod
 297                  <$> option [] (try $ g_mod_path <* char '.')
 298                  <*> g_term_idname
 299         g_term_idname :: CF g TeName
 300         g_term_idname = rule "term_idname" $
 301                 (TeName . Text.pack <$>) $
 302                 (identG `minus`) $
 303                 Fun.const
 304                  <$> g_term_keywords
 305                  <*. (any `but` g_term_idname_tail)
 306                 where
 307                 identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
 308                 headG  = unicat $ Unicat_Letter
 309         g_term_idname_tail :: Terminal g Char
 310         g_term_idname_tail = rule "term_idname_tail" $
 311                 unicat Unicat_Letter <+>
 312                 unicat Unicat_Number
 313         g_term_keywords :: Reg rl g String
 314         g_term_keywords = rule "term_keywords" $
 315                 choice $ string <$> ["in", "let"]
 316
 317         g_term_mod_opname :: CF g (Mod TeName)
 318         g_term_mod_opname = rule "term_mod_opname" $
 319                 Mod
 320                  <$> option [] (try $ g_mod_path <* char '.')
 321                  <*> g_term_opname
 322         g_term_opname :: CF g TeName
 323         g_term_opname = rule "term_opname" $
 324                 (TeName . Text.pack <$>) $
 325                 (symG `minus`) $
 326                 Fun.const
 327                  <$> g_term_keysyms
 328                  <*. (any `but` g_term_opname_ok)
 329                 where
 330                 symG = some $ cf_of_Terminal g_term_opname_ok
 331         g_term_opname_ok :: Terminal g Char
 332         g_term_opname_ok = rule "term_opname_ok" $
 333                 choice (unicat <$>
 334                  [ Unicat_Symbol
 335                  , Unicat_Punctuation
 336                  , Unicat_Mark
 337                  ]) `but` koG
 338                 where
 339                 koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])
 340         g_term_keysyms :: Reg rl g String
 341         g_term_keysyms = rule "term_keysyms" $
 342                 choice $ string <$> ["\\", "->", "=", "@"]
 343
 344 deriving instance Gram_Name g => Gram_Name (CF g)
 345 instance Gram_Name EBNF
 346 instance Gram_Name RuleDef
 347
 348 -- * Class 'Gram_Term_Type'
 349 class
 350  ( Alt g
 351  , Alter g
 352  , App g
 353  , Gram_CF g
 354  , Gram_Lexer g
 355  , Gram_Meta meta g
 356  , Gram_Rule g
 357  , Gram_Terminal g
 358  , Gram_Name g
 359  , Gram_Type meta g
 360  ) => Gram_Term_Type meta g where
 361         g_term_abst_decl
 362          :: CF g (TeName, TokType meta)
 363         g_term_abst_decl = rule "term_abst_decl" $
 364                 parens $ (,)
 365                  <$> g_term_name
 366                  <*  symbol ":"
 367                  <*> g_type
 368
 369 deriving instance Gram_Term_Type meta g => Gram_Term_Type meta (CF g)
 370 instance Gram_Term_Type meta EBNF
 371 instance Gram_Term_Type meta RuleDef
 372
 373 -- * Class 'Gram_Error'
 374 class Gram_Error g where
 375         term_unError :: CF g (Either Error_Term_Gram a) -> CF g a
 376 deriving instance Gram_Error g => Gram_Error (CF g)
 377 instance Gram_Error EBNF where
 378         term_unError (CF (EBNF g)) = CF $ EBNF g
 379 instance Gram_Error RuleDef where
 380         term_unError (CF (RuleDef (EBNF g))) =
 381                 CF $ RuleDef $ EBNF g
 382
 383 -- ** Type 'Error_Term_Gram'
 384 data Error_Term_Gram
 385  =   Error_Term_Gram_Fixity Error_Fixity
 386  |   Error_Term_Gram_Cannot_apply_term
 387  |   Error_Term_Gram_Cannot_apply_type
 388  |   Error_Term_Gram_Undefined_term
 389  |   Error_Term_Gram_Term_incomplete
 390  |   Error_Term_Gram_Type_applied_to_nothing
 391  |   Error_Term_Gram_not_applicable
 392  |   Error_Term_Gram_application
 393  |   Error_Term_Gram_application_mismatch
 394  deriving (Eq, Show)
 395
 396 -- * Class 'Gram_Term'
 397 class
 398  ( Alt g
 399  , Alter g
 400  , App g
 401  , Gram_CF g
 402  , Gram_Lexer g
 403  , Gram_Meta meta g
 404  , Gram_Rule g
 405  , Gram_Terminal g
 406  , Gram_Error g
 407  , Gram_Term_AtomsR meta ts ts g
 408  , Gram_Name g
 409  , Gram_Term_Type meta g
 410  , Gram_Type meta g
 411  , Inj_Token meta ts (->)
 412  ) => Gram_Term ts meta g where
 413         tokenizers_get :: CF g (Tokenizers meta ts -> a) -> CF g a
 414         tokenizers_put :: CF g (Tokenizers meta ts, a) -> CF g a
 415
 416         g_term
 417          :: Inj_Tokens meta ts '[Proxy (->)]
 418          => CF g (EToken meta ts)
 419         g_term = rule "term" $
 420                 choice
 421                  [ try g_term_abst
 422                  , g_term_operators
 423                  , g_term_let
 424                  ]
 425         g_term_operators
 426          :: Inj_Tokens meta ts '[Proxy (->)]
 427          => CF g (EToken meta ts)
 428         g_term_operators = rule "term_operators" $
 429                 term_unError $
 430                 ((unProTok =<<) <$>) $
 431                 term_unError $
 432                 left Error_Term_Gram_Fixity <$>
 433                 ops
 434                 where
 435                 ops :: CF g (Either Error_Fixity
 436                                     (Either Error_Term_Gram (ProTok meta ts)))
 437                 ops =
 438                         operators
 439                          (Right <$> g_term_atom)
 440                          (term_unError $ metaG $ tokenizers_get $ op_prefix  <$> g_term_op_prefix)
 441                          (term_unError $ metaG $ tokenizers_get $ op_infix   <$> g_term_op_infix)
 442                          (term_unError $ metaG $ tokenizers_get $ op_postfix <$> g_term_op_postfix)
 443                 op_infix
 444                  :: Mod TeName
 445                  -> Tokenizers meta ts
 446                  -> meta
 447                  -> Either Error_Term_Gram
 448                            ( Infix
 449                            ,    Either Error_Term_Gram (ProTok meta ts)
 450                              -> Either Error_Term_Gram (ProTok meta ts)
 451                              -> Either Error_Term_Gram (ProTok meta ts) )
 452                 op_infix name toks meta = do
 453                         (_pre, in_, _post) <- protok_lookup name toks
 454                         case in_ of
 455                          Nothing -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedInfix
 456                          Just p ->
 457                                 Right $ (protok_fixity p,) $ \ma mb -> do
 458                                         a <- ma
 459                                         b <- mb
 460                                         foldM protok_app (protok_term p meta) [a, b]
 461                 op_prefix, op_postfix
 462                  :: Mod TeName
 463                  -> Tokenizers meta ts
 464                  -> meta
 465                  -> Either Error_Term_Gram
 466                            ( Unifix
 467                            ,    Either Error_Term_Gram (ProTok meta ts)
 468                              -> Either Error_Term_Gram (ProTok meta ts) )
 469                 op_prefix name toks meta = do
 470                         (pre, _in_, _post) <- protok_lookup name toks
 471                         case pre of
 472                          Nothing -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedPrefix
 473                          Just p ->
 474                                 Right $ (protok_fixity p,) $ \ma -> do
 475                                         a <- ma
 476                                         protok_term p meta `protok_app` a
 477                 op_postfix name toks meta = do
 478                         (_pre, _in_, post) <- protok_lookup name toks
 479                         case post of
 480                          Nothing -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedPostfix
 481                          Just p ->
 482                                 Right $ (protok_fixity p,) $ \ma -> do
 483                                         a <- ma
 484                                         protok_term p meta `protok_app` a
 485                 g_term_op_postfix :: CF g (Mod TeName)
 486                 g_term_op_postfix = rule "term_op_postfix" $
 487                         lexeme $
 488                                 g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote)
 489                                 g_term_mod_opname
 490                 g_term_op_infix :: CF g (Mod TeName)
 491                 g_term_op_infix = rule "term_op_infix" $
 492                         lexeme $
 493                                 between g_backquote g_backquote g_term_mod_idname <+>
 494                                 try (Fun.const <$> g_term_mod_opname <*> (string " " <+> string "\n")) <+>
 495                                 pure (Mod [] " ")
 496                 g_term_op_prefix :: CF g (Mod TeName)
 497                 g_term_op_prefix = rule "term_op_prefix" $
 498                         lexeme $
 499                                 g_term_mod_idname <* g_backquote <+>
 500                                 g_term_mod_opname
 501                 g_backquote :: Gram_Terminal g' => g' Char
 502                 g_backquote = char '`'
 503
 504         g_term_atom
 505          :: Inj_Tokens meta ts '[Proxy (->)]
 506          => CF g (ProTok meta ts)
 507         g_term_atom =
 508                 choice $
 509                  (try (ProTokTy <$ char '@' <*> g_type) :) $
 510                  try <$> gs_term_atomsR (Proxy @ts) <>
 511                  [ try $
 512                         metaG $ term_unError $ tokenizers_get $
 513                         (\mn toks -> do
 514                                 (_, in_, _) <- protok_lookup mn toks
 515                                 case in_ of
 516                                  Nothing ->
 517                                         case mn of
 518                                          [] `Mod` n -> Right $ \meta ->
 519                                                 ProTokTe $ inj_EToken meta $ Token_Term_Var n
 520                                          _ -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedInfix
 521                                  Just p  -> Right $ protok_term p
 522                          ) <$> g_term_mod_name
 523                  , ProTokTe <$> g_term_group
 524                  ]
 525         g_term_group
 526          :: Inj_Tokens meta ts '[Proxy (->)]
 527          => CF g (EToken meta ts)
 528         g_term_group = rule "term_group" $ parens g_term
 529         g_term_abst
 530          :: Inj_Tokens meta ts '[Proxy (->)]
 531          => CF g (EToken meta ts)
 532         g_term_abst = rule "term_abst" $
 533                 metaG $
 534                 ((\(xs, te) meta ->
 535                         foldr (\(x, ty_x) ->
 536                                 inj_EToken meta .
 537                                 Token_Term_Abst x ty_x) te xs) <$>) $
 538                 g_term_abst_args_body
 539                  (symbol "\\" *> some g_term_abst_decl <* symbol "->")
 540                  g_term
 541         g_term_abst_args_body
 542          :: CF g [(TeName, TokType meta)]
 543          -> CF g (EToken meta ts)
 544          -> CF g ([(TeName, TokType meta)], EToken meta ts)
 545         -- g_term_abst_args_body args body = (,) <$> args <*> body
 546         g_term_abst_args_body cf_args cf_body =
 547                 tokenizers_put $ tokenizers_get $
 548                 (\a b (toks::Tokenizers meta ts) -> (toks, (a, b)))
 549                  <$> (tokenizers_put $ tokenizers_get $
 550                         (\args (toks::Tokenizers meta ts) -> (,args)
 551                                 Tokenizers
 552                                  { tokenizers_prefix  = del (tokenizers_prefix  toks) args
 553                                  , tokenizers_infix   = ins (tokenizers_infix   toks) args
 554                                  , tokenizers_postfix = del (tokenizers_postfix toks) args
 555                                  }) <$> cf_args)
 556                  <*> cf_body
 557                 where
 558                 del = foldr $ \(n, _) -> Map.adjust (Map.delete n) []
 559                 ins = foldr $ \(n, _) ->
 560                         Map.insertWith (<>) [] $
 561                         Map.singleton n
 562                         ProTok_Term
 563                          { protok_term   = \meta -> ProTokTe $ inj_EToken meta $ Token_Term_Var n
 564                          , protok_fixity = infixN5
 565                          }
 566         g_term_let
 567          :: Inj_Tokens meta ts '[Proxy (->)]
 568          => CF g (EToken meta ts)
 569         g_term_let = rule "term_let" $
 570                 metaG $
 571                 (\name args bound body meta ->
 572                         inj_EToken meta $
 573                         Token_Term_Let name
 574                          (foldr (\(x, ty_x) ->
 575                                 inj_EToken meta . Token_Term_Abst x ty_x) bound args) body)
 576                  <$  symbol "let"
 577                  <*> g_term_name
 578                  <*> many g_term_abst_decl
 579                  <*  symbol "="
 580                  <*> g_term
 581                  <*  symbol "in"
 582                  <*> g_term
 583
 584 deriving instance
 585  ( Gram_Term ts meta g
 586  , Gram_Term_AtomsR meta ts ts (CF g)
 587  ) => Gram_Term ts meta (CF g)
 588 instance
 589  ( Gram_Term_AtomsR meta ts ts EBNF
 590  , Inj_Token meta ts (->)
 591  ) => Gram_Term ts meta EBNF where
 592         tokenizers_get (CF (EBNF g)) = CF $ EBNF g
 593         tokenizers_put (CF (EBNF g)) = CF $ EBNF g
 594 instance
 595  ( Gram_Term_AtomsR meta ts ts RuleDef
 596  , Inj_Token meta ts (->)
 597  ) => Gram_Term ts meta RuleDef where
 598         tokenizers_get (CF (RuleDef (EBNF g))) = CF $ RuleDef $ EBNF g
 599         tokenizers_put (CF (RuleDef (EBNF g))) = CF $ RuleDef $ EBNF g
 600
 601 -- ** Class 'Gram_Term_AtomsR'
 602 class Gram_Term_AtomsR meta (ts::[*]) (rs::[*]) g where
 603         gs_term_atomsR :: Proxy rs -> [CF g (ProTok meta ts)]
 604 instance Gram_Term_AtomsR meta ts '[] g where
 605         gs_term_atomsR _rs = []
 606 instance
 607  ( Gram_Term_AtomsT meta ts t  g
 608  , Gram_Term_AtomsR meta ts rs g
 609  ) => Gram_Term_AtomsR meta ts (t ': rs) g where
 610         gs_term_atomsR _ =
 611                 gs_term_atomsT (Proxy @t) <>
 612                 gs_term_atomsR (Proxy @rs)
 613
 614 -- ** Class 'Gram_Term_AtomsT'
 615 class Gram_Term_AtomsT meta ts t g where
 616         gs_term_atomsT :: Proxy t -> [CF g (ProTok meta ts)]
 617         gs_term_atomsT _t = []
 618 -- instance Gram_Term_AtomsT meta ts t RuleDef
 619
 620 gram_term
 621  :: forall g.
 622  ( Gram_Term '[Proxy (->), Proxy Integer] () g
 623  ) => [CF g ()]
 624 gram_term =
 625  [ ue g_term
 626  , ue g_term_operators
 627  , up g_term_atom
 628  , ue g_term_group
 629  , ue g_term_abst
 630  , void (g_term_abst_decl::CF g (TeName, TokType ()))
 631  , ue g_term_let
 632  , void g_term_mod_name
 633  , void g_term_name
 634  , void g_term_idname
 635  , void $ cf_of_Terminal g_term_idname_tail
 636  , void $ cf_of_Reg g_term_keywords
 637  , void g_term_mod_opname
 638  , void g_term_opname
 639  , void $ cf_of_Terminal g_term_opname_ok
 640  , void $ cf_of_Reg g_term_keysyms
 641  ] where
 642         up :: CF g (ProTok () '[Proxy (->), Proxy Integer]) -> CF g ()
 643         up = (() <$)
 644         ue :: CF g (EToken () '[Proxy (->), Proxy Integer]) -> CF g ()
 645         ue = (() <$)