Add support for (>=>).

diff --git a/symantic-lib/Language/Symantic/Lib/Monad.hs b/symantic-lib/Language/Symantic/Lib/Monad.hs
index 1ec20a75ac3bcd398652dea94012f7c7a9d7a473..ed194a60c459d6f95f588e715137dea9a34b874b 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Monad.hs
+++ b/symantic-lib/Language/Symantic/Lib/Monad.hs
@@ -14,6 +14,7 @@ import Language.Symantic.Typing
 import Language.Symantic.Compiling
 import Language.Symantic.Interpreting
 import Language.Symantic.Transforming
+import Language.Symantic.Lib.Lambda ((~>))
 import Language.Symantic.Lib.Applicative (Sym_Applicative)
 
 -- * Class 'Sym_Monad'
@@ -22,20 +23,19 @@ class Sym_Applicative term => Sym_Monad term where
        (>>=)  :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
        join   :: Monad m => term (m (m a)) -> term (m a)
        when   :: Applicative f => term Bool -> term (f ()) -> term (f ())
+       (>=>)  :: Monad m => term (a -> m b) -> term (b -> m c) -> term (a -> m c); infixr 1 >=>
        
-       default return :: (Trans t term, Monad m)
-        => t term a -> t term (m a)
-       default (>>=) :: (Trans t term, Monad m)
-        => t term (m a) -> t term (a -> m b) -> t term (m b)
-       default join :: (Trans t term, Monad m)
-        => t term (m (m a)) -> t term (m a)
-       default when :: (Trans t term, Applicative f)
-        => t term Bool -> t term (f ()) -> t term (f ())
+       default return :: (Trans t term, Monad m) => t term a -> t term (m a)
+       default (>>=)  :: (Trans t term, Monad m) => t term (m a) -> t term (a -> m b) -> t term (m b)
+       default join   :: (Trans t term, Monad m) => t term (m (m a)) -> t term (m a)
+       default when   :: (Trans t term, Applicative f) => t term Bool -> t term (f ()) -> t term (f ())
+       default (>=>)  :: (Trans t term, Monad m) => t term (a -> m b) -> t term (b -> m c) -> t term (a -> m c)
        
        return = trans_map1 return
        (>>=)  = trans_map2 (>>=)
        join   = trans_map1 join
        when   = trans_map2 when
+       (>=>)  = trans_map2 (>=>)
 
 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
 type instance TyConsts_of_Iface (Proxy Monad) = Proxy Monad ': TyConsts_imported_by (Proxy Monad)
@@ -50,16 +50,19 @@ instance Sym_Monad HostI where
        (>>=)  = Monad.liftM2 (Monad.>>=)
        join   = Monad.liftM  Monad.join
        when   = Monad.liftM2 Monad.when
+       (>=>)  = Monad.liftM2 (Monad.>=>)
 instance Sym_Monad TextI where
        return = textI1 "return"
        (>>=)  = textI_infix ">>=" (infixL 1)
        join   = textI1 "join"
        when   = textI2 "when"
+       (>=>)  = textI_infix ">=>" (infixR 1)
 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
        return = dupI1 @Sym_Monad return
        (>>=)  = dupI2 @Sym_Monad (>>=)
        join   = dupI1 @Sym_Monad join
        when   = dupI2 @Sym_Monad when
+       (>=>)  = dupI2 @Sym_Monad (>=>)
 
 instance
  ( Read_TyNameR TyName cs rs
@@ -73,21 +76,22 @@ instance Show_TyConst cs => Show_TyConst (Proxy Monad ': cs) where
 
 instance Proj_TyConC cs (Proxy Monad)
 data instance TokenT meta (ts::[*]) (Proxy Monad)
- = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
- | Token_Term_Monad_bind   (EToken meta ts) (EToken meta ts)
- | Token_Term_Monad_join   (EToken meta ts)
- | Token_Term_Monad_when   (EToken meta ts) (EToken meta ts)
+ = Token_Term_Monad_return      (EToken meta '[Proxy Token_Type]) (EToken meta ts)
+ | Token_Term_Monad_bind        (EToken meta ts) (EToken meta ts)
+ | Token_Term_Monad_join        (EToken meta ts)
+ | Token_Term_Monad_when        (EToken meta ts) (EToken meta ts)
+ | Token_Term_Monad_kleisli_l2r (EToken meta ts) (EToken meta ts)
 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
 
 instance -- CompileI
  ( Read_TyName TyName cs
- , Inj_TyConst        cs Monad
- , Inj_TyConst        cs (->)
- , Inj_TyConst        cs ()
- , Inj_TyConst        cs Applicative
- , Inj_TyConst        cs Bool
- , Proj_TyCon         cs
+ , Inj_TyConst cs Monad
+ , Inj_TyConst cs (->)
+ , Inj_TyConst cs ()
+ , Inj_TyConst cs Applicative
+ , Inj_TyConst cs Bool
+ , Proj_TyCon cs
  , Compile cs is
  ) => CompileI cs is (Proxy Monad) where
        compileI tok ctx k =
@@ -134,6 +138,20 @@ instance -- CompileI
                         (At (Just tok_ok) ty_ok_u) $ \Refl ->
                        k ty_ok $ TermO $
                         \c -> when (cond c) (ok c)
+                Token_Term_Monad_kleisli_l2r tok_a2mb tok_b2mc ->
+                       -- (>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
+                       compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
+                       compileO tok_b2mc ctx $ \ty_b2mc (TermO b2mc) ->
+                       check_TyEq2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
+                       check_TyEq2 (ty @(->)) (At (Just tok_b2mc) ty_b2mc) $ \Refl ty_b2mc_b ty_b2mc_mc ->
+                       check_TyCon1 (ty @Monad) (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl TyCon ty_a2mb_mb_m ty_a2mb_mb_b ->
+                       check_TyEq1 ty_a2mb_mb_m (At (Just tok_b2mc) ty_b2mc_mc) $ \Refl _ty_b2mc_mc_c ->
+                       check_TyEq1 ty_a2mb_mb_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
+                       check_TyEq
+                        (At (Just tok_a2mb) ty_a2mb_mb_b)
+                        (At (Just tok_b2mc) ty_b2mc_b) $ \Refl ->
+                       k (ty_a2mb_a ~> ty_b2mc_mc) $ TermO $
+                        \c -> (>=>) (a2mb c) (b2mc c)
 instance -- TokenizeT
  Inj_Token meta ts Monad =>
  TokenizeT meta ts (Proxy Monad) where
@@ -147,6 +165,7 @@ instance -- TokenizeT
                 , tokenize2 ">>="  (infixL 1) Token_Term_Monad_bind
                 , tokenize1 "join" infixN5    Token_Term_Monad_join
                 , tokenize2 "when" infixN5    Token_Term_Monad_when
+                , tokenize2 ">=>"  (infixR 1) Token_Term_Monad_kleisli_l2r
                 ]
         }
 instance Gram_Term_AtomsT meta ts (Proxy Monad) g