]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Applicative.hs
Add tests for Compiling.
[haskell/symantic.git] / 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 as ->
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 as (ty_f :$ ty_a) $ TermLC $
103 \c -> pure (a c)
104 ltstargt_from =
105 -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
106 from_ast1 ast $ \ast_fa2b as ->
107 term_from ast_fa2b ctx $ \ty_fa2b (TermLC fa2b) ->
108 check_constraint1 tyApplicative ast_fa2b ty_fa2b $ \Refl Con ty_fa2b_f ty_fa2b_a2b ->
109 check_type2 tyFun ast_fa2b ty_fa2b_a2b $ \Refl ty_fa2b_a ty_fa2b_b ->
110 k as (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermLC $
111 \c -> lam $ \fa -> (<*>) (fa2b c) fa
112 stargt_from =
113 -- (*>) :: Applicative f => f a -> f b -> f b
114 from_ast2 ast $ \ast_fa ast_fb as ->
115 term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
116 term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
117 check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
118 check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
119 k as ty_fb $ TermLC $
120 \c -> (*>) (fa c) (fb c)
121 ltstar_from =
122 -- (<*) :: Applicative f => f a -> f b -> f a
123 from_ast2 ast $ \ast_fa ast_fb as ->
124 term_from ast_fa ctx $ \ty_fa (TermLC fa) ->
125 term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
126 check_constraint1 tyApplicative ast_fa ty_fa $ \Refl Con ty_fa_f _ty_fa_a ->
127 check_type1 ty_fa_f ast_fb ty_fb $ \Refl _ty_fb_b ->
128 k as ty_fa $ TermLC $
129 \c -> (<*) (fa c) (fb c)
130
131 -- | The 'Applicative' 'Type'
132 tyApplicative :: Inj_Const cs Applicative => Type cs Applicative
133 tyApplicative = TyConst inj_const
134
135 sym_Applicative :: Proxy Sym_Applicative
136 sym_Applicative = Proxy
137
138 syApplicative :: IsString a => [Syntax a] -> Syntax a
139 syApplicative = Syntax "Applicative"