module Language.Symantic.Lib.Applicative where
import Control.Applicative (Applicative)
+import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
import qualified Control.Applicative as Applicative
-import Control.Monad (liftM, liftM2)
import qualified Data.Function as Fun
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling.Term
-import Language.Symantic.Lib.Lambda
-import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>))
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0, b1)
+import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)
-- * Class 'Sym_Applicative'
+type instance Sym Applicative = Sym_Applicative
class Sym_Functor term => Sym_Applicative term where
pure :: Applicative f => term a -> term (f a)
- (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
+ (<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>
+ (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b); infixl 4 *>
+ (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a); infixl 4 <*
- default pure :: (Trans t term, Applicative f) => t term a -> t term (f a)
- default (<*>) :: (Trans t term, Applicative f)
- => t term (f (a -> b)) -> t term (f a) -> t term (f b)
+ default pure :: Sym_Applicative (UnT term) => Trans term => Applicative f => term a -> term (f a)
+ default (<*>) :: Sym_Applicative (UnT term) => Trans term => Applicative f => term (f (a -> b)) -> term (f a) -> term (f b)
+ default (*>) :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f b)
+ default (<*) :: Sym_Lambda term => Applicative f => term (f a) -> term (f b) -> term (f a)
- pure = trans_map1 pure
- (<*>) = trans_map2 (<*>)
- (*>) :: Applicative f => term (f a) -> term (f b) -> term (f b)
- (<*) :: Applicative f => term (f a) -> term (f b) -> term (f a)
- x *> y = (lam Fun.id <$ x) <*> y
- x <* y = (lam (lam . Fun.const) <$> x) <*> y
+ pure = trans1 pure
+ (<*>) = trans2 (<*>)
+ x *> y = lam1 Fun.id <$ x <*> y
+ x <* y = lam2 Fun.const <$> x <*> y
+
+-- Interpreting
+instance Sym_Applicative Eval where
+ pure = eval1 Applicative.pure
+ (<*>) = eval2 (Applicative.<*>)
+instance Sym_Applicative View where
+ pure = view1 "pure"
+ (<*>) = viewInfix "<*>" (infixL 4)
+ (<* ) = viewInfix "<*" (infixL 4)
+ ( *>) = viewInfix "*>" (infixL 4)
+instance (Sym_Applicative r1, Sym_Applicative r2, Sym_Lambda r1, Sym_Lambda r2) => Sym_Applicative (Dup r1 r2) where
+ pure = dup1 @Sym_Applicative pure
+ (<*>) = dup2 @Sym_Applicative (<*>)
+
+-- Transforming
+instance (Sym_Lambda term, Sym_Applicative term) => Sym_Applicative (BetaT term) where
+ (<*) = trans2 (<*)
+ (*>) = trans2 (*>)
+
+-- Typing
+instance NameTyOf Applicative where
+ nameTyOf _c = ["Applicative"] `Mod` "Applicative"
+instance FixityOf Applicative
+instance ClassInstancesFor Applicative
+instance TypeInstancesFor Applicative
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Applicative
+instance (Source src, SymInj ss Applicative) => ModuleFor src ss Applicative where
+ moduleFor = ["Applicative"] `moduleWhere`
+ [ "<*>" `withInfixL` 4 := teApplicative_app
+ , "<*" `withInfixL` 4 := teApplicative_const
+ , "*>" `withInfixL` 4 := teApplicative_tsnoc
+ ]
-infixl 4 *>
-infixl 4 <*
-infixl 4 <*>
+-- ** 'Type's
+tyApplicative :: Source src => Type src vs a -> Type src vs (Applicative a)
+tyApplicative a = tyConstLen @(K Applicative) @Applicative (lenVars a) `tyApp` a
-type instance Sym_of_Iface (Proxy Applicative) = Sym_Applicative
-type instance TyConsts_of_Iface (Proxy Applicative) = Proxy Applicative ': TyConsts_imported_by Applicative
-type instance TyConsts_imported_by Applicative = '[]
+-- ** 'Term's
+teApplicative_pure :: TermDef Applicative '[Proxy a, Proxy f] (Applicative f #> (a -> f a))
+teApplicative_pure = Term (tyApplicative f1) (a0 ~> f1 `tyApp` a0) $ teSym @Applicative $ lam1 pure
-instance Sym_Applicative HostI where
- pure = liftM Applicative.pure
- (<*>) = liftM2 (Applicative.<*>)
-instance Sym_Applicative TextI where
- pure = textI1 "pure"
- (<*>) = textI_infix "<*>" (infixL 4)
- (<* ) = textI_infix "<*" (infixL 4)
- ( *>) = textI_infix "*>" (infixL 4)
-instance (Sym_Applicative r1, Sym_Applicative r2) => Sym_Applicative (DupI r1 r2) where
- pure = dupI1 (Proxy @Sym_Applicative) pure
- (<*>) = dupI2 (Proxy @Sym_Applicative) (<*>)
+teApplicative_app :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f (a -> b) -> f a -> f b))
+teApplicative_app = Term (tyApplicative f2) (f2 `tyApp` (a0 ~> b1) ~> f2 `tyApp` a0 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (<*>)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Applicative
- ) => Read_TyNameR TyName cs (Proxy Applicative ': rs) where
- read_TyNameR _cs (TyName "Applicative") k = k (ty @Applicative)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Applicative ': cs) where
- show_TyConst TyConstZ{} = "Applicative"
- show_TyConst (TyConstS c) = show_TyConst c
+teApplicative_const :: TermDef Applicative '[Proxy a, Proxy b1, Proxy f] (Applicative f #> (f a -> f b1 -> f a))
+teApplicative_const = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` a0) $ teSym @Applicative $ lam2 (<*)
-instance Proj_TyConC cs (Proxy Applicative)
-data instance TokenT meta (ts::[*]) (Proxy Applicative)
- = Token_Term_Applicative_pure (EToken meta '[Proxy Token_Type]) (EToken meta ts)
- | Token_Term_Applicative_app (EToken meta ts)
- | Token_Term_Applicative_tsnoc (EToken meta ts) (EToken meta ts)
- | Token_Term_Applicative_const (EToken meta ts) (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Applicative))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Applicative))
-instance -- CompileI
- ( Read_TyName TyName (TyConsts_of_Ifaces is)
- , Inj_TyConst (TyConsts_of_Ifaces is) Applicative
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Applicative) where
- compileI tok ctx k =
- case tok of
- Token_Term_Applicative_pure tok_ty_f tok_a ->
- -- pure :: Applicative f => a -> f a
- compile_Type tok_ty_f $ \(ty_f::Type (TyConsts_of_Ifaces is) f) ->
- check_Kind
- (At Nothing $ SKiType `SKiArrow` SKiType)
- (At (Just tok_ty_f) $ kind_of ty_f) $ \Refl ->
- check_TyCon (At (Just tok_ty_f) (ty @Applicative :$ ty_f)) $ \TyCon ->
- compileO tok_a ctx $ \ty_a (TermO a) ->
- k (ty_f :$ ty_a) $ TermO $
- \c -> pure (a c)
- Token_Term_Applicative_app tok_fa2b ->
- -- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
- compileO tok_fa2b ctx $ \ty_fa2b (TermO fa2b) ->
- check_TyCon1 (ty @Applicative)
- (At (Just tok_fa2b) ty_fa2b) $ \Refl TyCon ty_fa2b_f ty_fa2b_a2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_fa2b) ty_fa2b_a2b) $ \Refl ty_fa2b_a ty_fa2b_b ->
- k (ty_fa2b_f :$ ty_fa2b_a ~> ty_fa2b_f :$ ty_fa2b_b) $ TermO $
- \c -> lam $ \fa -> (<*>) (fa2b c) fa
- Token_Term_Applicative_const tok_fa tok_fb ->
- -- (<*) :: Applicative f => f a -> f b -> f a
- compileO tok_fa ctx $ \ty_fa (TermO fa) ->
- compileO tok_fb ctx $ \ty_fb (TermO fb) ->
- check_TyCon1 (ty @Applicative)
- (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
- check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
- k ty_fa $ TermO $
- \c -> (<*) (fa c) (fb c)
- Token_Term_Applicative_tsnoc tok_fa tok_fb ->
- -- (*>) :: Applicative f => f a -> f b -> f b
- compileO tok_fa ctx $ \ty_fa (TermO fa) ->
- compileO tok_fb ctx $ \ty_fb (TermO fb) ->
- check_TyCon1 (ty @Applicative)
- (At (Just tok_fa) ty_fa) $ \Refl TyCon ty_fa_f _ty_fa_a ->
- check_TyEq1 ty_fa_f (At (Just tok_fb) ty_fb) $ \Refl _ty_fb_b ->
- k ty_fb $ TermO $
- \c -> (*>) (fa c) (fb c)
-instance -- TokenizeT
- Inj_Token meta ts Applicative =>
- TokenizeT meta ts (Proxy Applicative) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize1 "<*>" (infixL 4) Token_Term_Applicative_app
- , tokenize2 "<*" (infixL 4) Token_Term_Applicative_const
- , tokenize2 "*>" (infixL 4) Token_Term_Applicative_tsnoc
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Applicative) g
+teApplicative_tsnoc :: TermDef Applicative '[Proxy a, Proxy b, Proxy f] (Applicative f #> (f a -> f b -> f b))
+teApplicative_tsnoc = Term (tyApplicative f2) (f2 `tyApp` a0 ~> f2 `tyApp` b1 ~> f2 `tyApp` b1) $ teSym @Applicative $ lam2 (*>)
sourcephile / git / haskell / symantic.git / blobdiff