]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Applicative.hs
Sync with ghc-8.2.2 and megaparsec-6.3.0.
[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 Prelude hiding (Functor(..), (<$>), Applicative(..))
8 import qualified Control.Applicative as Applicative
9 import qualified Data.Function as Fun
10
11 import Language.Symantic
12 import Language.Symantic.Lib.Function (a0, b1)
13 import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)
14
15 -- * Class 'Sym_Applicative'
16 type instance Sym Applicative = Sym_Applicative
17 class Sym_Functor term => Sym_Applicative term where
18 pure :: Applicative f => term a -> term (f a)
19 (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>
20 (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>
21 (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
22
23 default pure :: Sym_Applicative (UnT term) => Trans term => Applicative f => term a -> term (f a)
24 default (<*>) :: Sym_Applicative (UnT term) => Trans term => Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
25 default (*>) :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f b)
26 default (<*) :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f a)
27
28 pure = trans1 pure
29 (<*>) = trans2 (<*>)
30 x *> y = lam1 Fun.id <$ x <*> y
31 x <* y = lam2 Fun.const <$> x <*> y
32
33 -- Interpreting
34 instance Sym_Applicative Eval where
35 pure = eval1 Applicative.pure
36 (<*>) = eval2 (Applicative.<*>)
37 instance Sym_Applicative View where
38 pure = view1 "pure"
39 (<*>) = viewInfix "<*>" (infixL 4)
40 (<* ) = viewInfix "<*" (infixL 4)
41 ( *>) = viewInfix "*>" (infixL 4)
42 instance (Sym_Applicative r1, Sym_Applicative r2, Sym_Lambda r1, Sym_Lambda r2) => Sym_Applicative (Dup r1 r2) where
43 pure = dup1 @Sym_Applicative pure
44 (<*>) = dup2 @Sym_Applicative (<*>)
45
46 -- Transforming
47 instance (Sym_Lambda term, Sym_Applicative term) => Sym_Applicative (BetaT term) where
48 (<*) = trans2 (<*)
49 (*>) = trans2 (*>)
50
51 -- Typing
52 instance NameTyOf Applicative where
53 nameTyOf _c = ["Applicative"] `Mod` "Applicative"
54 instance FixityOf Applicative
55 instance ClassInstancesFor Applicative
56 instance TypeInstancesFor Applicative
57
58 -- Compiling
59 instance Gram_Term_AtomsFor src ss g Applicative
60 instance (Source src, SymInj ss Applicative) => ModuleFor src ss Applicative where
61 moduleFor = ["Applicative"] `moduleWhere`
62 [ "<*>" `withInfixL` 4 := teApplicative_app
63 , "<*" `withInfixL` 4 := teApplicative_const
64 , "*>" `withInfixL` 4 := teApplicative_tsnoc
65 ]
66
67 -- ** 'Type's
68 tyApplicative :: Source src => Type src vs a -> Type src vs (Applicative a)
69 tyApplicative a = tyConstLen @(K Applicative) @Applicative (lenVars a) `tyApp` a
70
71 -- ** 'Term's
72 teApplicative_pure :: TermDef Applicative '[Proxy a, Proxy f] (Applicative f #> (a -> f a))
73 teApplicative_pure = Term (tyApplicative f1) (a0 ~> f1 `tyApp` a0) $ teSym @Applicative $ lam1 pure
74
75 teApplicative_app :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f (a -> b) -> f a -> f b))
76 teApplicative_app = Term (tyApplicative f2) (f2 `tyApp` (a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (<*>)
77
78 teApplicative_const :: TermDef Applicative '[Proxy a, Proxy b1, Proxy f] (Applicative f #> (f a -> f b1 -> f a))
79 teApplicative_const = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Applicative $ lam2 (<*)
80
81 teApplicative_tsnoc :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f a -> f b -> f b))
82 teApplicative_tsnoc = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (*>)