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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Functor'.
   4 module Language.Symantic.Lib.Functor where
   5
   6 import Control.Monad (liftM2)
   7 import Data.Functor (Functor)
   8 import Data.Proxy (Proxy(..))
   9 import Data.Type.Equality
  10 import Prelude hiding (Functor(..))
  11 import qualified Data.Function as Fun
  12 import qualified Data.Functor as Functor
  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 import Language.Symantic.Lib.Lambda
  20
  21 -- * Class 'Sym_Functor'
  22 class Sym_Lambda term => Sym_Functor term where
  23         fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
  24         default fmap
  25          :: (Trans t term, Functor f)
  26          => t term (a -> b)
  27          -> t term (f a)
  28          -> t term (f b)
  29         fmap = trans_map2 fmap
  30
  31         (<$) :: Functor f => term a -> term (f b) -> term (f a); infixl 4 <$
  32         (<$) a = fmap (lam (Fun.const a))
  33
  34
  35 type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
  36 type instance TyConsts_of_Iface (Proxy Functor) = Proxy Functor ': TyConsts_imported_by (Proxy Functor)
  37 type instance TyConsts_imported_by (Proxy Functor) = '[]
  38
  39 instance Sym_Functor HostI where
  40         fmap = liftM2 Functor.fmap
  41         (<$) = liftM2 (Functor.<$)
  42 instance Sym_Functor TextI where
  43         fmap = textI2 "fmap"
  44         (<$) = textI_infix "<$" (infixL 4)
  45 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
  46         fmap = dupI2 @Sym_Functor fmap
  47         (<$) = dupI2 @Sym_Functor (<$)
  48
  49 -- | 'fmap' alias.
  50 (<$>) :: (Sym_Functor term, Functor f)
  51  => term (a -> b) -> term (f a) -> term (f b)
  52 (<$>) = fmap
  53 infixl 4 <$>
  54
  55 instance
  56  ( Read_TyNameR TyName cs rs
  57  , Inj_TyConst cs Functor
  58  ) => Read_TyNameR TyName cs (Proxy Functor ': rs) where
  59         read_TyNameR _cs (TyName "Functor") k = k (ty @Functor)
  60         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  61 instance Show_TyConst cs => Show_TyConst (Proxy Functor ': cs) where
  62         show_TyConst TyConstZ{} = "Functor"
  63         show_TyConst (TyConstS c) = show_TyConst c
  64
  65 instance Proj_TyConC cs (Proxy Functor)
  66 data instance TokenT meta (ts::[*]) (Proxy Functor)
  67  = Token_Term_Functor_fmap   (EToken meta ts) (EToken meta ts)
  68  | Token_Term_Functor_const (EToken meta ts) (EToken meta ts)
  69 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
  70 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
  71
  72 instance -- CompileI
  73  ( Inj_TyConst cs Functor
  74  , Inj_TyConst cs (->)
  75  , Proj_TyCon  cs
  76  , Compile cs is
  77  ) => CompileI cs is (Proxy Functor) where
  78         compileI tok ctx k =
  79                 case tok of
  80                  Token_Term_Functor_fmap tok_a2b tok_fa ->
  81                         -- fmap :: Functor f => (a -> b) -> f a -> f b
  82                         compile tok_a2b ctx $ \ty_a2b (Term a2b) ->
  83                         compile tok_fa  ctx $ \ty_fa  (Term fa) ->
  84                         check_TyEq2 (ty @(->))
  85                          (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
  86                         check_TyCon1 (ty @Functor)
  87                          (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f ty_fa_a ->
  88                         check_TyEq
  89                          (At (Just tok_a2b) ty_a2b_a)
  90                          (At (Just tok_fa) ty_fa_a) $ \Refl ->
  91                         k (ty_fa_f :$ ty_a2b_b) $ Term $
  92                          \c -> fmap (a2b c) (fa c)
  93                  Token_Term_Functor_const tok_a tok_fb ->
  94                         -- (<$) :: Functor f => a -> f b -> f a
  95                         compile tok_a  ctx $ \ty_a  (Term a) ->
  96                         compile tok_fb ctx $ \ty_fb (Term fb) ->
  97                         check_TyCon1 (ty @Functor)
  98                          (At (Just tok_fb) ty_fb) $ \Refl TyCon ty_fb_f _ty_fb_b ->
  99                         k (ty_fb_f :$ ty_a) $ Term $
 100                          \c -> (<$) (a c) (fb c)
 101 instance -- TokenizeT
 102  Inj_Token meta ts Functor =>
 103  TokenizeT meta ts (Proxy Functor) where
 104         tokenizeT _t = mempty
 105          { tokenizers_infix = tokenizeTMod []
 106                  [ tokenize2 "fmap" infixN5   Token_Term_Functor_fmap
 107                  , tokenize2 "<$"  (infixL 4) Token_Term_Functor_const
 108                  , tokenize2 "<$>" (infixL 4) Token_Term_Functor_fmap
 109                  ]
 110          }
 111 instance Gram_Term_AtomsT meta ts (Proxy Functor) g