Language/Symantic/Expr/Applicative.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   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 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Applicative'.
  13 module Language.Symantic.Expr.Applicative where
  14
  15 import Control.Applicative (Applicative)
  16 import qualified Control.Applicative as Applicative
  17 import Control.Monad
  18 import qualified Data.Function as Fun
  19 import Data.Monoid
  20 import Data.Proxy (Proxy(..))
  21 import Data.Type.Equality ((:~:)(Refl))
  22 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
  23
  24 import Language.Symantic.Type
  25 import Language.Symantic.Repr
  26 import Language.Symantic.Trans.Common
  27 import Language.Symantic.Expr.Root
  28 import Language.Symantic.Expr.Error
  29 import Language.Symantic.Expr.From
  30 import Language.Symantic.Expr.Lambda
  31 import Language.Symantic.Expr.Functor
  32
  33 -- * Class 'Sym_Applicative'
  34 -- | Symantic.
  35 class Sym_Functor repr => Sym_Applicative repr where
  36         pure  :: Applicative f => repr a -> repr (f a)
  37         (<*>) :: Applicative f => repr (f ((->) a b)) -> repr (f a) -> repr (f b)
  38         default pure  :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
  39         default (<*>) :: (Trans t repr, Applicative f)
  40          => t repr (f ((->) a b)) -> t repr (f a) -> t repr (f b)
  41         pure = trans_map1 pure
  42         (<*>) = trans_map2 (<*>)
  43         (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
  44         (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
  45         x *> y = (lam Fun.id <$ x) <*> y
  46         x <* y = (lam (lam . Fun.const) <$> x) <*> y
  47 infixl 4  *>
  48 infixl 4 <*
  49 infixl 4 <*>
  50 instance Sym_Applicative Repr_Host where
  51         pure  = liftM Applicative.pure
  52         (<*>) = liftM2 (Applicative.<*>)
  53 instance Sym_Applicative Repr_Text where
  54         pure = repr_text_app1 "pure"
  55         (<*>) (Repr_Text fg) (Repr_Text fa) =
  56                 Repr_Text $ \p v ->
  57                         let p' = precedence_LtStarGt in
  58                         paren p p' $ fg p' v <> " <*> " <> fa p' v
  59 instance
  60  ( Sym_Applicative r1
  61  , Sym_Applicative r2
  62  ) => Sym_Applicative (Dup r1 r2) where
  63         pure (a1 `Dup` a2) =
  64                 pure a1 `Dup` pure a2
  65         (<*>) (f1 `Dup` f2) (m1 `Dup` m2) =
  66                 (<*>) f1 m1 `Dup` (<*>) f2 m2
  67
  68 -- * Type 'Expr_Applicative'
  69 -- | Expression.
  70 data Expr_Applicative (root:: *)
  71 type instance Root_of_Expr      (Expr_Applicative root)      = root
  72 type instance Type_of_Expr      (Expr_Applicative root)      = No_Type
  73 type instance Sym_of_Expr       (Expr_Applicative root) repr = (Sym_Applicative repr)
  74 type instance Error_of_Expr ast (Expr_Applicative root)      = No_Error_Expr
  75
  76 -- | Parse 'pure'.
  77 pure_from
  78  :: forall root ty ast hs ret.
  79  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
  80  , Eq_Type ty
  81  , Type1_from ast ty
  82  , Expr_from ast root
  83  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  84                    (Error_of_Expr ast root)
  85  , Root_of_Expr root ~ root
  86  , Constraint_Type1 Applicative ty
  87  ) => ast -> ast
  88  -> Expr_From ast (Expr_Applicative root) hs ret
  89 pure_from ast_f ast_a ex ast ctx k =
  90  -- pure :: Applicative f => a -> f a
  91         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  92         type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
  93                 expr_from (Proxy::Proxy root) ast_a ctx $
  94                  \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  95                 let ty_fa = ty_f ty_a in
  96                 check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
  97                 k ty_fa $ Forall_Repr_with_Context $
  98                  \c -> pure (a c)
  99
 100 -- | Parse '<*>'.
 101 ltstargt_from
 102  :: forall root ty ast hs ret.
 103  ( ty ~ Type_Root_of_Expr (Expr_Applicative root)
 104  , Eq_Type  ty
 105  , Eq_Type1 ty
 106  , Expr_from ast root
 107  , Lift_Type   Type_Fun (Type_of_Expr root)
 108  , Unlift_Type Type_Fun (Type_of_Expr root)
 109  , Unlift_Type1 (Type_of_Expr root)
 110  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 111                    (Error_of_Expr ast root)
 112  , Root_of_Expr root ~ root
 113  , Constraint_Type1 Applicative ty
 114  ) => ast -> ast
 115  -> Expr_From ast (Expr_Applicative root) hs ret
 116 ltstargt_from ast_fg ast_fa ex ast ctx k =
 117  -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
 118         expr_from (Proxy::Proxy root) ast_fg ctx $
 119          \(ty_fg::ty h_fg) (Forall_Repr_with_Context fg) ->
 120         expr_from (Proxy::Proxy root) ast_fa ctx $
 121          \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
 122         check_type1 ex ast ty_fg $ \(Type_Type1 _f (ty_g::ty h_g), _) ->
 123         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 ty_f) ->
 124         check_eq_type1 ex ast ty_fg ty_fa $ \Refl ->
 125         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
 126          :: Type_Fun ty h_g) ->
 127         check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_fa $ \Dict ->
 128         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
 129         k (Type_Root $ ty_f $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
 130          \c -> (<*>) (fg c) (fa c)