Language/Symantic/Compiling/Applicative.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Applicative'.
   4 module Language.Symantic.Compiling.Applicative where
   5
   6 import Control.Applicative (Applicative)
   7 import qualified Control.Applicative as Applicative
   8 import Control.Monad (liftM, liftM2)
   9 import qualified Data.Function as Fun
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const, Monoid(..))
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Compiling.Functor (Sym_Functor(..), (<$>))
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming.Trans
  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
  27         default pure  :: (Trans t term, Applicative f) => t term a -> t term (f a)
  28         default (<*>) :: (Trans t term, Applicative f)
  29          => t term (f (a -> b)) -> t term (f a) -> t term (f b)
  30
  31         pure = trans_map1 pure
  32         (<*>) = trans_map2 (<*>)
  33         (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b)
  34         (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a)
  35         x *> y = (lam Fun.id <$ x) <*> y
  36         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  37
  38 infixl 4  *>
  39 infixl 4 <*
  40 infixl 4 <*>
  41
  42 type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
  43 type instance Consts_of_Iface (Proxy Applicative) = Proxy Applicative ': Consts_imported_by Applicative
  44 type instance Consts_imported_by Applicative = '[]
  45
  46 instance Sym_Applicative HostI where
  47         pure  = liftM Applicative.pure
  48         (<*>) = liftM2 (Applicative.<*>)
  49 instance Sym_Applicative TextI where
  50         pure  = textI_app1 "pure"
  51         (<*>) = textI_infix "<*>" (Precedence 4)
  52         (<* ) = textI_infix "<*"  (Precedence 4)
  53         ( *>) = textI_infix "*>"  (Precedence 4)
  54 instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
  55         pure  = dupI1 (Proxy @Sym_Applicative) pure
  56         (<*>) = dupI2 (Proxy @Sym_Applicative) (<*>)
  57
  58 instance Const_from Text cs => Const_from Text (Proxy Applicative ': cs) where
  59         const_from "Applicative" k = k (ConstZ kind)
  60         const_from s k = const_from s $ k . ConstS
  61 instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
  62         show_const ConstZ{} = "Applicative"
  63         show_const (ConstS c) = show_const c
  64
  65 instance Proj_ConC 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_ltstargt (EToken meta ts)
  69  | Token_Term_Applicative_stargt   (EToken meta ts) (EToken meta ts)
  70  | Token_Term_Applicative_ltstar   (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 instance -- Term_fromI
  74  ( Const_from Name_LamVar (Consts_of_Ifaces is)
  75  , Inj_Const  (Consts_of_Ifaces is) Applicative
  76  , Inj_Const  (Consts_of_Ifaces is) (->)
  77  , Proj_Con   (Consts_of_Ifaces is)
  78  , Term_from is
  79  ) => Term_fromI is (Proxy Applicative) where
  80         term_fromI tok ctx k =
  81                 case tok of
  82                  Token_Term_Applicative_pure tok_ty_f tok_a ->
  83                         -- pure :: Applicative f => a -> f a
  84                         type_from tok_ty_f $ \(ty_f::Type (Consts_of_Ifaces is) f) ->
  85                         check_kind
  86                          (At Nothing $ SKiType `SKiArrow` SKiType)
  87                          (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
  88                         check_con (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \Con ->
  89                         term_from tok_a ctx $ \ty_a (TermLC a) ->
  90                         k (ty_f :$ ty_a) $ TermLC $
  91                          \c -> pure (a c)
  92                  Token_Term_Applicative_ltstargt tok_fa2b ->
  93                         -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
  94                         term_from tok_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
  95                         check_con1 (ty @Applicative)
  96                          (At (Just tok_fa2b) ty_fa2b) $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
  97                         check_type2 (ty @(->)) (At (Just tok_fa2b) ty_fa2b_a2b) $ \Refl ty_fa2b_a ty_fa2b_b ->
  98                         k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
  99                          \c -> lam $ \fa -> (<*>) (fa2b c) fa
 100                  Token_Term_Applicative_ltstar tok_fa tok_fb ->
 101                         -- (<*) :: Applicative f => f a -> f b -> f a
 102                         term_from tok_fa ctx $ \ty_fa (TermLC fa) ->
 103                         term_from tok_fb ctx $ \ty_fb (TermLC fb) ->
 104                         check_con1 (ty @Applicative)
 105                          (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
 106                         check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
 107                         k ty_fa $ TermLC $
 108                          \c -> (<*) (fa c) (fb c)
 109                  Token_Term_Applicative_stargt tok_fa tok_fb ->
 110                         -- (*>) :: Applicative f => f a -> f b -> f b
 111                         term_from tok_fa ctx $ \ty_fa (TermLC fa) ->
 112                         term_from tok_fb ctx $ \ty_fb (TermLC fb) ->
 113                         check_con1 (ty @Applicative)
 114                          (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
 115                         check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
 116                         k ty_fb $ TermLC $
 117                          \c -> (*>) (fa c) (fb c)