]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Applicative.hs
Add Parsing.Grammar.
[haskell/symantic.git] / 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 = textI1 "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
59 ( Read_TypeNameR Text cs rs
60 , Inj_Const cs Applicative
61 ) => Read_TypeNameR Text cs (Proxy Applicative ': rs) where
62 read_typenameR _cs "Applicative" k = k (ty @Applicative)
63 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
64 instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
65 show_const ConstZ{} = "Applicative"
66 show_const (ConstS c) = show_const c
67
68 instance Proj_ConC cs (Proxy Applicative)
69 data instance TokenT meta (ts::[*]) (Proxy Applicative)
70 = Token_Term_Applicative_pure (EToken meta '[Proxy Token_Type]) (EToken meta ts)
71 | Token_Term_Applicative_app (EToken meta ts)
72 | Token_Term_Applicative_stargt (EToken meta ts) (EToken meta ts)
73 | Token_Term_Applicative_ltstar (EToken meta ts) (EToken meta ts)
74 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Applicative))
75 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Applicative))
76 instance -- CompileI
77 ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
78 , Inj_Const (Consts_of_Ifaces is) Applicative
79 , Inj_Const (Consts_of_Ifaces is) (->)
80 , Proj_Con (Consts_of_Ifaces is)
81 , Compile is
82 ) => CompileI is (Proxy Applicative) where
83 compileI tok ctx k =
84 case tok of
85 Token_Term_Applicative_pure tok_ty_f tok_a ->
86 -- pure :: Applicative f => a -> f a
87 compile_type tok_ty_f $ \(ty_f::Type (Consts_of_Ifaces is) f) ->
88 check_kind
89 (At Nothing $ SKiType `SKiArrow` SKiType)
90 (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
91 check_con (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \Con ->
92 compileO tok_a ctx $ \ty_a (TermO a) ->
93 k (ty_f :$ ty_a) $ TermO $
94 \c -> pure (a c)
95 Token_Term_Applicative_app tok_fa2b ->
96 -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
97 compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
98 check_con1 (ty @Applicative)
99 (At (Just tok_fa2b) ty_fa2b) $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
100 check_type2 (ty @(->)) (At (Just tok_fa2b) ty_fa2b_a2b) $ \Refl ty_fa2b_a ty_fa2b_b ->
101 k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermO $
102 \c -> lam $ \fa -> (<*>) (fa2b c) fa
103 Token_Term_Applicative_ltstar tok_fa tok_fb ->
104 -- (<*) :: Applicative f => f a -> f b -> f a
105 compileO tok_fa ctx $ \ty_fa (TermO fa) ->
106 compileO tok_fb ctx $ \ty_fb (TermO fb) ->
107 check_con1 (ty @Applicative)
108 (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
109 check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
110 k ty_fa $ TermO $
111 \c -> (<*) (fa c) (fb c)
112 Token_Term_Applicative_stargt tok_fa tok_fb ->
113 -- (*>) :: Applicative f => f a -> f b -> f b
114 compileO tok_fa ctx $ \ty_fa (TermO fa) ->
115 compileO tok_fb ctx $ \ty_fb (TermO fb) ->
116 check_con1 (ty @Applicative)
117 (At (Just tok_fa) ty_fa) $ \Refl Con ty_fa_f _ty_fa_a ->
118 check_type1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
119 k ty_fb $ TermO $
120 \c -> (*>) (fa c) (fb c)