Language/Symantic/Compiling/Functor.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Functor'.
   4 module Language.Symantic.Compiling.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.Text (Text)
  12 import Data.Type.Equality
  13 import Prelude hiding (Functor(..))
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  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)
  32         (<$) a = fmap (lam (Fun.const a))
  33
  34 infixl 4 <$
  35
  36 type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
  37 type instance Consts_of_Iface (Proxy Functor) = Proxy Functor ': Consts_imported_by Functor
  38 type instance Consts_imported_by Functor = '[]
  39
  40 instance Sym_Functor HostI where
  41         fmap = liftM2 Functor.fmap
  42         (<$) = liftM2 (Functor.<$)
  43 instance Sym_Functor TextI where
  44         fmap = textI_app2 "fmap"
  45         (<$) = textI_infix "<$" (Precedence 4)
  46 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
  47         fmap = dupI2 (Proxy @Sym_Functor) fmap
  48         (<$) = dupI2 (Proxy @Sym_Functor) (<$)
  49
  50 -- | 'fmap' alias.
  51 (<$>) :: (Sym_Functor term, Functor f)
  52  => term (a -> b) -> term (f a) -> term (f b)
  53 (<$>) = fmap
  54 infixl 4 <$>
  55
  56 instance Const_from Text cs => Const_from Text (Proxy Functor ': cs) where
  57         const_from "Functor" k = k (ConstZ kind)
  58         const_from s k = const_from s $ k . ConstS
  59 instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
  60         show_const ConstZ{} = "Functor"
  61         show_const (ConstS c) = show_const c
  62
  63 instance Proj_ConC cs (Proxy Functor)
  64 data instance TokenT meta (ts::[*]) (Proxy Functor)
  65  = Token_Term_Functor_fmap     (EToken meta ts) (EToken meta ts)
  66  | Token_Term_Functor_ltdollar (EToken meta ts) (EToken meta ts)
  67 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
  68 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
  69 instance -- Term_fromI
  70  ( Inj_Const  (Consts_of_Ifaces is) Functor
  71  , Inj_Const  (Consts_of_Ifaces is) (->)
  72  , Proj_Con   (Consts_of_Ifaces is)
  73  , Term_from is
  74  ) => Term_fromI is (Proxy Functor) where
  75         term_fromI tok ctx k =
  76                 case tok of
  77                  Token_Term_Functor_fmap tok_a2b tok_fa ->
  78                         -- fmap :: Functor f => (a -> b) -> f a -> f b
  79                         term_from tok_a2b ctx $ \ty_a2b (TermLC a2b) ->
  80                         term_from tok_fa  ctx $ \ty_fa  (TermLC fa) ->
  81                         check_type2 (ty @(->))
  82                          (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
  83                         check_con1 (ty @Functor)
  84                          (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f ty_fa_a ->
  85                         check_type
  86                          (At (Just tok_a2b) ty_a2b_a)
  87                          (At (Just tok_fa) ty_fa_a) $ \Refl ->
  88                         k (ty_fa_f :$ ty_a2b_b) $ TermLC $
  89                          \c -> fmap (a2b c) (fa c)
  90                  Token_Term_Functor_ltdollar tok_a tok_fb ->
  91                         -- (<$) :: Functor f => a -> f b -> f a
  92                         term_from tok_a  ctx $ \ty_a  (TermLC a) ->
  93                         term_from tok_fb ctx $ \ty_fb (TermLC fb) ->
  94                         check_con1 (ty @Functor)
  95                          (At (Just tok_fb) ty_fb) $ \Refl Con ty_fb_f _ty_fb_b ->
  96                         k (ty_fb_f :$ ty_a) $ TermLC $
  97                          \c -> (<$) (a c) (fb c)