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 qualified Data.Function as Fun
   8 import Data.Functor (Functor)
   9 import qualified Data.Functor as Functor
  10 import Data.Proxy (Proxy(..))
  11 import Data.Type.Equality
  12 import Prelude hiding (Functor(..))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Parsing.Grammar
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20 import Language.Symantic.Lib.Lambda
  21
  22 -- * Class 'Sym_Functor'
  23 class Sym_Lambda term => Sym_Functor term where
  24         fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
  25         default fmap
  26          :: (Trans t term, Functor f)
  27          => t term (a -> b)
  28          -> t term (f a)
  29          -> t term (f b)
  30         fmap = trans_map2 fmap
  31
  32         (<$) :: Functor f => term a -> term (f b) -> term (f a)
  33         (<$) a = fmap (lam (Fun.const a))
  34
  35 infixl 4 <$
  36
  37 type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
  38 type instance Consts_of_Iface (Proxy Functor) = Proxy Functor ': Consts_imported_by Functor
  39 type instance Consts_imported_by Functor = '[]
  40
  41 instance Sym_Functor HostI where
  42         fmap = liftM2 Functor.fmap
  43         (<$) = liftM2 (Functor.<$)
  44 instance Sym_Functor TextI where
  45         fmap = textI2 "fmap"
  46         (<$) = textI_infix "<$" (infixL 4)
  47 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
  48         fmap = dupI2 (Proxy @Sym_Functor) fmap
  49         (<$) = dupI2 (Proxy @Sym_Functor) (<$)
  50
  51 -- | 'fmap' alias.
  52 (<$>) :: (Sym_Functor term, Functor f)
  53  => term (a -> b) -> term (f a) -> term (f b)
  54 (<$>) = fmap
  55 infixl 4 <$>
  56
  57 instance
  58  ( Read_TypeNameR Type_Name cs rs
  59  , Inj_Const cs Functor
  60  ) => Read_TypeNameR Type_Name cs (Proxy Functor ': rs) where
  61         read_typenameR _cs (Type_Name "Functor") k = k (ty @Functor)
  62         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  63 instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
  64         show_const ConstZ{} = "Functor"
  65         show_const (ConstS c) = show_const c
  66
  67 instance Proj_ConC cs (Proxy Functor)
  68 data instance TokenT meta (ts::[*]) (Proxy Functor)
  69  = Token_Term_Functor_fmap   (EToken meta ts) (EToken meta ts)
  70  | Token_Term_Functor_const (EToken meta ts) (EToken meta ts)
  71 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
  72 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
  73 instance -- CompileI
  74  ( Inj_Const  (Consts_of_Ifaces is) Functor
  75  , Inj_Const  (Consts_of_Ifaces is) (->)
  76  , Proj_Con   (Consts_of_Ifaces is)
  77  , Compile is
  78  ) => CompileI is (Proxy Functor) where
  79         compileI tok ctx k =
  80                 case tok of
  81                  Token_Term_Functor_fmap tok_a2b tok_fa ->
  82                         -- fmap :: Functor f => (a -> b) -> f a -> f b
  83                         compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
  84                         compileO tok_fa  ctx $ \ty_fa  (TermO fa) ->
  85                         check_type2 (ty @(->))
  86                          (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
  87                         check_con1 (ty @Functor)
  88                          (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f ty_fa_a ->
  89                         check_type
  90                          (At (Just tok_a2b) ty_a2b_a)
  91                          (At (Just tok_fa) ty_fa_a) $ \Refl ->
  92                         k (ty_fa_f :$ ty_a2b_b) $ TermO $
  93                          \c -> fmap (a2b c) (fa c)
  94                  Token_Term_Functor_const tok_a tok_fb ->
  95                         -- (<$) :: Functor f => a -> f b -> f a
  96                         compileO tok_a  ctx $ \ty_a  (TermO a) ->
  97                         compileO tok_fb ctx $ \ty_fb (TermO fb) ->
  98                         check_con1 (ty @Functor)
  99                          (At (Just tok_fb) ty_fb) $ \Refl Con ty_fb_f _ty_fb_b ->
 100                         k (ty_fb_f :$ ty_a) $ TermO $
 101                          \c -> (<$) (a c) (fb c)
 102 instance -- TokenizeT
 103  Inj_Token meta ts Functor =>
 104  TokenizeT meta ts (Proxy Functor) where
 105         tokenizeT _t = mempty
 106          { tokenizers_infix = tokenizeTMod []
 107                  [ tokenize2 "fmap" infixN5   Token_Term_Functor_fmap
 108                  , tokenize2 "<$"  (infixL 4) Token_Term_Functor_const
 109                  , tokenize2 "<$>" (infixL 4) Token_Term_Functor_fmap
 110                  ]
 111          }
 112 instance Gram_Term_AtomsT meta ts (Proxy Functor) g