symantic-lib/Language/Symantic/Lib/MonoFunctor.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
   4 -- | Symantic for 'MonoFunctor'.
   5 module Language.Symantic.Lib.MonoFunctor where
   6
   7 import Control.Monad (liftM2)
   8 import Data.MonoTraversable (MonoFunctor)
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import GHC.Exts (Constraint)
  12 import qualified Data.MonoTraversable as MT
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming
  19
  20 -- * Class 'Sym_MonoFunctor'
  21 class Sym_MonoFunctor term where
  22         omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
  23         default omap :: (Trans t term, MonoFunctor o)
  24          => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
  25         omap = trans_map2 omap
  26
  27 type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
  28 type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by (Proxy MonoFunctor)
  29 type instance TyConsts_imported_by (Proxy MonoFunctor) = '[ Proxy (->) ]
  30
  31 instance Sym_MonoFunctor HostI where
  32         omap = liftM2 MT.omap
  33 instance Sym_MonoFunctor TextI where
  34         omap = textI2 "omap"
  35 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
  36         omap = dupI2 @Sym_MonoFunctor omap
  37
  38 instance
  39  ( Read_TyNameR TyName cs rs
  40  , Inj_TyConst cs MonoFunctor
  41  ) => Read_TyNameR TyName cs (Proxy MonoFunctor ': rs) where
  42         read_TyNameR _cs (TyName "MonoFunctor") k = k (ty @MonoFunctor)
  43         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  44 instance Show_TyConst cs => Show_TyConst (Proxy MonoFunctor ': cs) where
  45         show_TyConst TyConstZ{} = "MonoFunctor"
  46         show_TyConst (TyConstS c) = show_TyConst c
  47
  48 -- * Type 'TyFam_MonoElement'
  49 data TyFam_MonoElement
  50  =   TyFam_MonoElement
  51  deriving (Eq, Show)
  52 type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
  53
  54 instance -- Constraint
  55  Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
  56 instance -- k -> Constraint
  57  Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
  58
  59 instance Proj_TyConC cs (Proxy MonoFunctor)
  60
  61 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
  62  = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
  63 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
  64 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
  65 instance -- CompileI
  66  ( Inj_TyConst cs MonoFunctor
  67  , Inj_TyConst cs (->)
  68  , Proj_TyCon  cs
  69  , Proj_TyFam  cs TyFam_MonoElement
  70  , Compile cs is
  71  ) => CompileI cs is (Proxy MonoFunctor) where
  72         compileI tok ctx k =
  73                 case tok of
  74                  Token_Term_MonoFunctor_omap tok_f tok_o ->
  75                         -- omap :: (Element o -> Element o) -> o -> o
  76                         compile tok_f ctx $ \ty_f (Term f) ->
  77                         compile tok_o ctx $ \ty_o (Term m) ->
  78                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
  79                         check_TyEq
  80                          (At (Just tok_f) ty_f_a)
  81                          (At (Just tok_f) ty_f_b) $ \Refl ->
  82                         check_TyCon (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \TyCon ->
  83                         check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
  84                         check_TyEq
  85                          (At Nothing ty_o_e)
  86                          (At (Just tok_f) ty_f_a) $ \Refl ->
  87                         k ty_o $ Term $
  88                          \c -> omap (f c) (m c)
  89 instance -- TokenizeT
  90  Inj_Token meta ts MonoFunctor =>
  91  TokenizeT meta ts (Proxy MonoFunctor) where
  92         tokenizeT _t = mempty
  93          { tokenizers_infix = tokenizeTMod []
  94                  [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
  95                  ]
  96          }
  97 instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g