Language/Symantic/Compiling/Applicative.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Applicative'.
  14 module Language.Symantic.Compiling.Applicative where
  15
  16 import Control.Applicative (Applicative)
  17 import qualified Control.Applicative as Applicative
  18 import Control.Monad (liftM, liftM2)
  19 import qualified Data.Function as Fun
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const, Monoid(..))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Functor (Sym_Functor(..), (<$>))
  29 import Language.Symantic.Interpreting
  30 import Language.Symantic.Transforming.Trans
  31
  32 -- * Class 'Sym_Applicative'
  33 class Sym_Functor term => Sym_Applicative term where
  34         pure  :: Applicative f => term a -> term (f a)
  35         (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
  36
  37         default pure  :: (Trans t term, Applicative f) => t term a -> t term (f a)
  38         default (<*>) :: (Trans t term, Applicative f)
  39          => t term (f (a -> b)) -> t term (f a) -> t term (f b)
  40
  41         pure = trans_map1 pure
  42         (<*>) = trans_map2 (<*>)
  43         (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b)
  44         (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a)
  45         x *> y = (lam Fun.id <$ x) <*> y
  46         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  47
  48 infixl 4  *>
  49 infixl 4 <*
  50 infixl 4 <*>
  51
  52 type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
  53 type instance Consts_of_Iface (Proxy Applicative) = Proxy Applicative ': Consts_imported_by Applicative
  54 type instance Consts_imported_by Applicative = '[]
  55
  56 instance Sym_Applicative HostI where
  57         pure  = liftM Applicative.pure
  58         (<*>) = liftM2 (Applicative.<*>)
  59 instance Sym_Applicative TextI where
  60         pure  = textI_app1 "pure"
  61         (<*>) = textI_infix "<*>" (Precedence 4)
  62         (<* ) = textI_infix "<*"  (Precedence 4)
  63         ( *>) = textI_infix "*>"  (Precedence 4)
  64 instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
  65         pure  = dupI1 sym_Applicative pure
  66         (<*>) = dupI2 sym_Applicative (<*>)
  67
  68 instance Const_from Text cs => Const_from Text (Proxy Applicative ': cs) where
  69         const_from "Applicative" k = k (ConstZ kind)
  70         const_from s k = const_from s $ k . ConstS
  71 instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
  72         show_const ConstZ{} = "Applicative"
  73         show_const (ConstS c) = show_const c
  74
  75 instance -- Proj_ConC
  76  Proj_ConC cs (Proxy Applicative)
  77 instance -- Term_fromI
  78  ( AST ast
  79  , Lexem ast ~ LamVarName
  80  , Const_from (Lexem ast) (Consts_of_Ifaces is)
  81  , Inj_Const  (Consts_of_Ifaces is) Applicative
  82  , Inj_Const  (Consts_of_Ifaces is) (->)
  83  , Proj_Con   (Consts_of_Ifaces is)
  84  , Term_from is ast
  85  ) => Term_fromI is (Proxy Applicative) ast where
  86         term_fromI ast ctx k =
  87                 case ast_lexem ast of
  88                  "pure" -> pure_from
  89                  "<*>"  -> ltstargt_from
  90                  "*>"   -> stargt_from
  91                  "<*"   -> ltstar_from
  92                  _ -> Left $ Error_Term_unsupported
  93                 where
  94                 pure_from =
  95                  -- pure :: Applicative f => a -> f a
  96                         from_ast2 ast $ \ast_ty_f ast_a as ->
  97                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
  98                         type_from ast_ty_f $ \ty_f -> Right $
  99                         check_kind ast (SKiType `SKiArrow` SKiType) (At (Just ast_ty_f) ty_f) $ \Refl ->
 100                         check_constraint (At (Just ast_ty_f) (tyApplicative :$ ty_f)) $ \Con ->
 101                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 102                         k as (ty_f :$ ty_a) $ TermLC $
 103                          \c -> pure (a c)
 104                 ltstargt_from =
 105                  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 106                         from_ast1 ast $ \ast_fa2b as ->
 107                         term_from ast_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
 108                         check_constraint1 tyApplicative ast_fa2b ty_fa2b $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
 109                         check_type2 tyFun ast_fa2b ty_fa2b_a2b $ \Refl ty_fa2b_a ty_fa2b_b ->
 110                         k as (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
 111                          \c -> lam $ \fa -> (<*>) (fa2b c) fa
 112                 stargt_from =
 113                  -- (*>) :: Applicative f => f a -> f b -> f b
 114                         from_ast2 ast $ \ast_fa ast_fb as ->
 115                         term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
 116                         term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
 117                         check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
 118                         check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
 119                         k as ty_fb $ TermLC $
 120                          \c -> (*>) (fa c) (fb c)
 121                 ltstar_from =
 122                  -- (<*) :: Applicative f => f a -> f b -> f a
 123                         from_ast2 ast $ \ast_fa ast_fb as ->
 124                         term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
 125                         term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
 126                         check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
 127                         check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
 128                         k as ty_fa $ TermLC $
 129                          \c -> (<*) (fa c) (fb c)
 130
 131 -- | The 'Applicative' 'Type'
 132 tyApplicative :: Inj_Const cs Applicative => Type cs Applicative
 133 tyApplicative = TyConst inj_const
 134
 135 sym_Applicative :: Proxy Sym_Applicative
 136 sym_Applicative = Proxy
 137
 138 syApplicative :: IsString a => [Syntax a] -> Syntax a
 139 syApplicative = Syntax "Applicative"