+{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Functor'.
module Language.Symantic.Lib.Functor where
-import Control.Monad (liftM2)
-import qualified Data.Function as Fun
import Data.Functor (Functor)
+import Prelude hiding (Functor(..), (<$>))
+import qualified Data.Function as Fun
import qualified Data.Functor as Functor
-import Data.Proxy (Proxy(..))
-import Data.Type.Equality
-import Prelude hiding (Functor(..))
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0, b1)
-- * Class 'Sym_Functor'
-class Sym_Lambda term => Sym_Functor term where
+type instance Sym Functor = Sym_Functor
+class Sym_Functor term where
fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
- default fmap
- :: (Trans t term, Functor f)
- => t term (a -> b)
- -> t term (f a)
- -> t term (f b)
- fmap = trans_map2 fmap
+ default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b)
+ fmap = trans2 fmap
+
+ (<$>) :: (Sym_Functor term, Functor f) => term (a -> b) -> term (f a) -> term (f b); infixl 4 <$>
+ (<$>) = fmap
(<$) :: Functor f => term a -> term (f b) -> term (f a); infixl 4 <$
- (<$) a = fmap (lam (Fun.const a))
+ default (<$) :: Sym_Lambda term => Functor f => term a -> term (f b) -> term (f a)
+ (<$) x = fmap (lam (Fun.const x))
+
+-- Interpreting
+instance Sym_Functor Eval where
+ fmap = eval2 Functor.fmap
+ (<$) = eval2 (Functor.<$)
+instance Sym_Functor View where
+ fmap = view2 "fmap"
+ (<$>) = viewInfix "<$>" (infixL 4)
+ (<$) = viewInfix "<$" (infixL 4)
+instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (Dup r1 r2) where
+ fmap = dup2 @Sym_Functor fmap
+ (<$) = dup2 @Sym_Functor (<$)
+
+-- Transforming
+instance (Sym_Functor term, Sym_Lambda term) => Sym_Functor (BetaT term) where
+ (<$>) = trans2 (<$>)
+ (<$) = trans2 (<$)
+
+-- Typing
+instance NameTyOf Functor where
+ nameTyOf _c = ["Functor"] `Mod` "Functor"
+instance FixityOf Functor
+instance ClassInstancesFor Functor
+instance TypeInstancesFor Functor
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Functor
+instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where
+ moduleFor = ["Functor"] `moduleWhere`
+ [ "fmap" := teFunctor_fmap
+ , "<$" `withInfixL` 4 := teFunctor_const
+ , "<$>" `withInfixL` 4 := teFunctor_fmap_infix
+ ]
-type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
-type instance TyConsts_of_Iface (Proxy Functor) = Proxy Functor ': TyConsts_imported_by Functor
-type instance TyConsts_imported_by Functor = '[]
+-- ** 'Type's
+tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a)
+tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a
-instance Sym_Functor HostI where
- fmap = liftM2 Functor.fmap
- (<$) = liftM2 (Functor.<$)
-instance Sym_Functor TextI where
- fmap = textI2 "fmap"
- (<$) = textI_infix "<$" (infixL 4)
-instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
- fmap = dupI2 @Sym_Functor fmap
- (<$) = dupI2 @Sym_Functor (<$)
+f1 :: Source src => LenInj vs => KindInj (K f) =>
+ Type src (a ': Proxy f ': vs) f
+f1 = tyVar "f" $ VarS varZ
--- | 'fmap' alias.
-(<$>) :: (Sym_Functor term, Functor f)
- => term (a -> b) -> term (f a) -> term (f b)
-(<$>) = fmap
-infixl 4 <$>
+f2 :: Source src => LenInj vs => KindInj (K f) =>
+ Type src (a ': b ': Proxy f ': vs) f
+f2 = tyVar "f" $ VarS $ VarS varZ
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Functor
- ) => Read_TyNameR TyName cs (Proxy Functor ': rs) where
- read_TyNameR _cs (TyName "Functor") k = k (ty @Functor)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Functor ': cs) where
- show_TyConst TyConstZ{} = "Functor"
- show_TyConst (TyConstS c) = show_TyConst c
+-- ** 'Term's
+teFunctor_fmap, teFunctor_fmap_infix :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> ((a -> b) -> f a -> f b))
+teFunctor_fmap = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 fmap
+teFunctor_fmap_infix = Term (tyFunctor f2) ((a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Functor $ lam2 (<$>)
-instance Proj_TyConC cs (Proxy Functor)
-data instance TokenT meta (ts::[*]) (Proxy Functor)
- = Token_Term_Functor_fmap (EToken meta ts) (EToken meta ts)
- | Token_Term_Functor_const (EToken meta ts) (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Functor
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Functor) where
- compileI tok ctx k =
- case tok of
- Token_Term_Functor_fmap tok_a2b tok_fa ->
- -- fmap :: Functor f => (a -> b) -> f a -> f b
- compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
- compileO tok_fa ctx $ \ty_fa (TermO fa) ->
- check_TyEq2 (ty @(->))
- (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
- check_TyCon1 (ty @Functor)
- (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f ty_fa_a ->
- check_TyEq
- (At (Just tok_a2b) ty_a2b_a)
- (At (Just tok_fa) ty_fa_a) $ \Refl ->
- k (ty_fa_f :$ ty_a2b_b) $ TermO $
- \c -> fmap (a2b c) (fa c)
- Token_Term_Functor_const tok_a tok_fb ->
- -- (<$) :: Functor f => a -> f b -> f a
- compileO tok_a ctx $ \ty_a (TermO a) ->
- compileO tok_fb ctx $ \ty_fb (TermO fb) ->
- check_TyCon1 (ty @Functor)
- (At (Just tok_fb) ty_fb) $ \Refl TyCon ty_fb_f _ty_fb_b ->
- k (ty_fb_f :$ ty_a) $ TermO $
- \c -> (<$) (a c) (fb c)
-instance -- TokenizeT
- Inj_Token meta ts Functor =>
- TokenizeT meta ts (Proxy Functor) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "fmap" infixN5 Token_Term_Functor_fmap
- , tokenize2 "<$" (infixL 4) Token_Term_Functor_const
- , tokenize2 "<$>" (infixL 4) Token_Term_Functor_fmap
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Functor) g
+teFunctor_const :: TermDef Functor '[Proxy a, Proxy b, Proxy f] (Functor f #> (a -> f b -> f a))
+teFunctor_const = Term (tyFunctor f2) (a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Functor $ lam2 (<$)
sourcephile / git / haskell / symantic.git / blobdiff