]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Applicative.hs
Cosmetic cleanup.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Applicative.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Applicative'.
4 module Language.Symantic.Lib.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.Type.Equality ((:~:)(Refl))
12 import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
13
14 import Language.Symantic.Parsing
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling.Term
17 import Language.Symantic.Lib.Lambda
18 import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>))
19 import Language.Symantic.Interpreting
20 import Language.Symantic.Transforming
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 infixl 4 <*>
27
28 default pure :: (Trans t term, Applicative f) => t term a -> t term (f a)
29 default (<*>) :: (Trans t term, Applicative f)
30 => t term (f (a -> b)) -> t term (f a) -> t term (f b)
31
32 pure = trans_map1 pure
33 (<*>) = trans_map2 (<*>)
34 (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>
35 (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
36 x *> y = (lam Fun.id <$ x) <*> y
37 x <* y = (lam (lam . Fun.const) <$> x) <*> y
38
39 type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
40 type instance TyConsts_of_Iface (Proxy Applicative) = Proxy Applicative ': TyConsts_imported_by Applicative
41 type instance TyConsts_imported_by Applicative = '[]
42
43 instance Sym_Applicative HostI where
44 pure = liftM Applicative.pure
45 (<*>) = liftM2 (Applicative.<*>)
46 instance Sym_Applicative TextI where
47 pure = textI1 "pure"
48 (<*>) = textI_infix "<*>" (infixL 4)
49 (<* ) = textI_infix "<*" (infixL 4)
50 ( *>) = textI_infix "*>" (infixL 4)
51 instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
52 pure = dupI1 @Sym_Applicative pure
53 (<*>) = dupI2 @Sym_Applicative (<*>)
54
55 instance
56 ( Read_TyNameR TyName cs rs
57 , Inj_TyConst cs Applicative
58 ) => Read_TyNameR TyName cs (Proxy Applicative ': rs) where
59 read_TyNameR _cs (TyName "Applicative") k = k (ty @Applicative)
60 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
61 instance Show_TyConst cs => Show_TyConst (Proxy Applicative ': cs) where
62 show_TyConst TyConstZ{} = "Applicative"
63 show_TyConst (TyConstS c) = show_TyConst c
64
65 instance Proj_TyConC 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_app (EToken meta ts)
69 | Token_Term_Applicative_tsnoc (EToken meta ts) (EToken meta ts)
70 | Token_Term_Applicative_const (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 -- CompileI
74 ( Read_TyName TyName (TyConsts_of_Ifaces is)
75 , Inj_TyConst (TyConsts_of_Ifaces is) Applicative
76 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
77 , Proj_TyCon (TyConsts_of_Ifaces is)
78 , Compile is
79 ) => CompileI is (Proxy Applicative) where
80 compileI 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 compile_Type tok_ty_f $ \(ty_f::Type (TyConsts_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_TyCon (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \TyCon ->
89 compileO tok_a ctx $ \ty_a (TermO a) ->
90 k (ty_f :$ ty_a) $ TermO $
91 \c -> pure (a c)
92 Token_Term_Applicative_app tok_fa2b ->
93 -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
94 compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
95 check_TyCon1 (ty @Applicative)
96 (At (Just tok_fa2b) ty_fa2b) $ \Refl TyCon ty_fa2b_f ty_fa2b_a2b ->
97 check_TyEq2 (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) $ TermO $
99 \c -> lam $ \fa -> (<*>) (fa2b c) fa
100 Token_Term_Applicative_const tok_fa tok_fb ->
101 -- (<*) :: Applicative f => f a -> f b -> f a
102 compileO tok_fa ctx $ \ty_fa (TermO fa) ->
103 compileO tok_fb ctx $ \ty_fb (TermO fb) ->
104 check_TyCon1 (ty @Applicative)
105 (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
106 check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
107 k ty_fa $ TermO $
108 \c -> (<*) (fa c) (fb c)
109 Token_Term_Applicative_tsnoc tok_fa tok_fb ->
110 -- (*>) :: Applicative f => f a -> f b -> f b
111 compileO tok_fa ctx $ \ty_fa (TermO fa) ->
112 compileO tok_fb ctx $ \ty_fb (TermO fb) ->
113 check_TyCon1 (ty @Applicative)
114 (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
115 check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
116 k ty_fb $ TermO $
117 \c -> (*>) (fa c) (fb c)
118 instance -- TokenizeT
119 Inj_Token meta ts Applicative =>
120 TokenizeT meta ts (Proxy Applicative) where
121 tokenizeT _t = mempty
122 { tokenizers_infix = tokenizeTMod []
123 [ tokenize1 "<*>" (infixL 4) Token_Term_Applicative_app
124 , tokenize2 "<*" (infixL 4) Token_Term_Applicative_const
125 , tokenize2 "*>" (infixL 4) Token_Term_Applicative_tsnoc
126 ]
127 }
128 instance Gram_Term_AtomsT meta ts (Proxy Applicative) g