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 ->
  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 (ty_f :$ ty_a) $ TermLC $
 103                          \c -> pure (a c)
 104                 ltstargt_from =
 105                  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 106                         case ast_nodes ast of
 107                          [] -> Left $ Error_Term_Syntax $
 108                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 109                          [ast_fa2b] ->
 110                                 term_from ast_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
 111                                 check_constraint1 tyApplicative ast_fa2b ty_fa2b $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
 112                                 check_type2 tyFun ast_fa2b ty_fa2b_a2b $ \Refl ty_fa2b_a ty_fa2b_b ->
 113                                 k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
 114                                  \c -> lam $ \fa -> (<*>) (fa2b c) fa
 115                          [ast_fa2b, ast_fa] ->
 116                                 term_from ast_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
 117                                 term_from ast_fa   ctx $ \ty_fa   (TermLC fa) ->
 118                                 check_constraint1 tyApplicative ast_fa2b ty_fa2b $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
 119                                 check_type2 tyFun ast_fa2b ty_fa2b_a2b $ \Refl ty_fa2b_a ty_fa2b_b ->
 120                                 check_type1 ty_fa2b_f ast_fa ty_fa $ \Refl ty_fa_a ->
 121                                 check_type (At (Just ast_fa2b) ty_fa2b_a) (At (Just ast_fa) ty_fa_a) $ \Refl ->
 122                                 k (ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
 123                                  \c -> (<*>) (fa2b c) (fa c)
 124                          _ -> Left $ Error_Term_Syntax $
 125                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 126                 stargt_from =
 127                  -- (*>) :: Applicative f => f a -> f b -> f b
 128                         from_ast2 ast $ \ast_fa ast_fb ->
 129                         term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
 130                         term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
 131                         check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
 132                         check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
 133                         k ty_fb $ TermLC $
 134                          \c -> (*>) (fa c) (fb c)
 135                 ltstar_from =
 136                  -- (<*) :: Applicative f => f a -> f b -> f a
 137                         from_ast2 ast $ \ast_fa ast_fb ->
 138                         term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
 139                         term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
 140                         check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
 141                         check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
 142                         k ty_fa $ TermLC $
 143                          \c -> (<*) (fa c) (fb c)
 144
 145 -- | The 'Applicative' 'Type'
 146 tyApplicative :: Inj_Const cs Applicative => Type cs Applicative
 147 tyApplicative = TyConst inj_const
 148
 149 sym_Applicative :: Proxy Sym_Applicative
 150 sym_Applicative = Proxy
 151
 152 syApplicative :: IsString a => [Syntax a] -> Syntax a
 153 syApplicative = Syntax "Applicative"