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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Applicative'.
   4 module Language.Symantic.Lib.Applicative where
   5
   6 import Control.Applicative (Applicative)
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
  11 import qualified Control.Applicative as Applicative
  12 import qualified Data.Function as Fun
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Lib.Lambda
  18 import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>))
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming
  21
  22 -- * Class 'Sym_Applicative'
  23 class Sym_Functor term => Sym_Applicative term where
  24         pure  :: Applicative f => term a -> term (f a)
  25         (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
  26         infixl 4 <*>
  27
  28         default pure  :: (Trans t term, Applicative f) => t term a -> t term (f a)
  29         default (<*>) :: (Trans t term, Applicative f)
  30          => t term (f (a -> b)) -> t term (f a) -> t term (f b)
  31
  32         pure = trans_map1 pure
  33         (<*>) = trans_map2 (<*>)
  34         (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>
  35         (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
  36         x *> y = (lam Fun.id <$ x) <*> y
  37         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  38
  39 type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
  40 type instance TyConsts_of_Iface (Proxy Applicative) = Proxy Applicative ': TyConsts_imported_by (Proxy Applicative)
  41 type instance TyConsts_imported_by (Proxy Applicative) = '[]
  42
  43 instance Sym_Applicative HostI where
  44         pure  = liftM Applicative.pure
  45         (<*>) = liftM2 (Applicative.<*>)
  46 instance Sym_Applicative TextI where
  47         pure  = textI1 "pure"
  48         (<*>) = textI_infix "<*>" (infixL 4)
  49         (<* ) = textI_infix "<*"  (infixL 4)
  50         ( *>) = textI_infix "*>"  (infixL 4)
  51 instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
  52         pure  = dupI1 @Sym_Applicative pure
  53         (<*>) = dupI2 @Sym_Applicative (<*>)
  54
  55 instance
  56  ( Read_TyNameR TyName cs rs
  57  , Inj_TyConst cs Applicative
  58  ) => Read_TyNameR TyName cs (Proxy Applicative ': rs) where
  59         read_TyNameR _cs (TyName "Applicative") k = k (ty @Applicative)
  60         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  61 instance Show_TyConst cs => Show_TyConst (Proxy Applicative ': cs) where
  62         show_TyConst TyConstZ{} = "Applicative"
  63         show_TyConst (TyConstS c) = show_TyConst c
  64
  65 instance Proj_TyConC cs (Proxy Applicative)
  66 data instance TokenT meta (ts::[*]) (Proxy Applicative)
  67  = Token_Term_Applicative_pure  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  68  | Token_Term_Applicative_app   (EToken meta ts)
  69  | Token_Term_Applicative_tsnoc (EToken meta ts) (EToken meta ts)
  70  | Token_Term_Applicative_const (EToken meta ts) (EToken meta ts)
  71 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Applicative))
  72 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Applicative))
  73
  74 instance -- CompileI
  75  ( Read_TyName TyName cs
  76  , Inj_TyConst        cs Applicative
  77  , Inj_TyConst        cs (->)
  78  , Proj_TyCon         cs
  79  , Compile cs is
  80  ) => CompileI cs is (Proxy Applicative) where
  81         compileI tok ctx k =
  82                 case tok of
  83                  Token_Term_Applicative_pure tok_ty_f tok_a ->
  84                         -- pure :: Applicative f => a -> f a
  85                         compile_Type tok_ty_f $ \(ty_f::Type cs f) ->
  86                         check_Kind
  87                          (At Nothing $ SKiType `SKiArrow` SKiType)
  88                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
  89                         check_TyCon (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \TyCon ->
  90                         compileO tok_a ctx $ \ty_a (TermO a) ->
  91                         k (ty_f :$ ty_a) $ TermO $
  92                          \c -> pure (a c)
  93                  Token_Term_Applicative_app tok_fa2b ->
  94                         -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
  95                         compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
  96                         check_TyCon1 (ty @Applicative)
  97                          (At (Just tok_fa2b) ty_fa2b) $ \Refl TyCon ty_fa2b_f ty_fa2b_a2b ->
  98                         check_TyEq2 (ty @(->)) (At (Just tok_fa2b) ty_fa2b_a2b) $ \Refl ty_fa2b_a ty_fa2b_b ->
  99                         k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermO $
 100                          \c -> lam $ \fa -> (<*>) (fa2b c) fa
 101                  Token_Term_Applicative_const tok_fa tok_fb ->
 102                         -- (<*) :: Applicative f => f a -> f b -> f a
 103                         compileO tok_fa ctx $ \ty_fa (TermO fa) ->
 104                         compileO tok_fb ctx $ \ty_fb (TermO fb) ->
 105                         check_TyCon1 (ty @Applicative)
 106                          (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
 107                         check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
 108                         k ty_fa $ TermO $
 109                          \c -> (<*) (fa c) (fb c)
 110                  Token_Term_Applicative_tsnoc tok_fa tok_fb ->
 111                         -- (*>) :: Applicative f => f a -> f b -> f b
 112                         compileO tok_fa ctx $ \ty_fa (TermO fa) ->
 113                         compileO tok_fb ctx $ \ty_fb (TermO fb) ->
 114                         check_TyCon1 (ty @Applicative)
 115                          (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
 116                         check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
 117                         k ty_fb $ TermO $
 118                          \c -> (*>) (fa c) (fb c)
 119 instance -- TokenizeT
 120  Inj_Token meta ts Applicative =>
 121  TokenizeT meta ts (Proxy Applicative) where
 122         tokenizeT _t = mempty
 123          { tokenizers_infix = tokenizeTMod []
 124                  [ tokenize1 "<*>" (infixL 4) Token_Term_Applicative_app
 125                  , tokenize2 "<*"  (infixL 4) Token_Term_Applicative_const
 126                  , tokenize2 "*>"  (infixL 4) Token_Term_Applicative_tsnoc
 127                  ]
 128          }
 129 instance Gram_Term_AtomsT meta ts (Proxy Applicative) g