Language/Symantic/Compiling/Monad.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Monad'.
   4 module Language.Symantic.Compiling.Monad where
   5
   6 import Control.Monad (Monad)
   7 import qualified Control.Monad as Monad
   8 import Data.Monoid ((<>))
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (Monad(..))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Compiling.Applicative (Sym_Applicative)
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20
  21 -- * Class 'Sym_Monad'
  22 class Sym_Applicative term => Sym_Monad term where
  23         return :: Monad m => term a -> term (m a)
  24         (>>=)  :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
  25         when   :: Applicative f => term Bool -> term (f ()) -> term (f ())
  26
  27         default return :: (Trans t term, Monad m)
  28          => t term a -> t term (m a)
  29         default (>>=) :: (Trans t term, Monad m)
  30          => t term (m a) -> t term (a -> m b) -> t term (m b)
  31         default when :: (Trans t term, Applicative f)
  32          => t term Bool -> t term (f ()) -> t term (f ())
  33
  34         return = trans_map1 return
  35         (>>=)  = trans_map2 (>>=)
  36         when   = trans_map2 when
  37
  38 infixl 1 >>=
  39
  40 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
  41 type instance Consts_of_Iface (Proxy Monad) = Proxy Monad ': Consts_imported_by Monad
  42 type instance Consts_imported_by Monad =
  43  [ Proxy ()
  44  , Proxy Applicative
  45  , Proxy Bool
  46  ]
  47
  48 instance Sym_Monad HostI where
  49         return = Monad.liftM Monad.return
  50         (>>=)  = Monad.liftM2 (Monad.>>=)
  51         when   = Monad.liftM2 Monad.when
  52 instance Sym_Monad TextI where
  53         return = textI_app1 "return"
  54         (>>=)  = textI_infix ">>=" (Precedence 1)
  55         when (TextI cond) (TextI ok) =
  56                 TextI $ \p v ->
  57                         let p' = Precedence 2 in
  58                         paren p p' $
  59                         "when " <> cond p' v <>
  60                         " " <> ok p' v
  61 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
  62         return = dupI1 (Proxy @Sym_Monad) return
  63         (>>=)  = dupI2 (Proxy @Sym_Monad) (>>=)
  64         when   = dupI2 (Proxy @Sym_Monad) when
  65
  66 instance Const_from Text cs => Const_from Text (Proxy Monad ': cs) where
  67         const_from "Monad" k = k (ConstZ kind)
  68         const_from s k = const_from s $ k . ConstS
  69 instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
  70         show_const ConstZ{} = "Monad"
  71         show_const (ConstS c) = show_const c
  72
  73 instance Proj_ConC cs (Proxy Monad)
  74 data instance TokenT meta (ts::[*]) (Proxy Monad)
  75  = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
  76  | Token_Term_Monad_bind   (EToken meta ts) (EToken meta ts)
  77  | Token_Term_Monad_when   (EToken meta ts) (EToken meta ts)
  78 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
  79 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
  80 instance -- CompileI
  81  ( Const_from Name_LamVar (Consts_of_Ifaces is)
  82  , Inj_Const (Consts_of_Ifaces is) Monad
  83  , Inj_Const (Consts_of_Ifaces is) (->)
  84  , Inj_Const (Consts_of_Ifaces is) ()
  85  , Inj_Const (Consts_of_Ifaces is) Applicative
  86  , Inj_Const (Consts_of_Ifaces is) Bool
  87  , Proj_Con  (Consts_of_Ifaces is)
  88  , Compile is
  89  ) => CompileI is (Proxy Monad) where
  90         compileI tok ctx k =
  91                 case tok of
  92                  Token_Term_Monad_return tok_ty_m tok_a ->
  93                         -- return :: Monad m => a -> m a
  94                         compile_type tok_ty_m $ \(ty_m::Type (Consts_of_Ifaces is) m) ->
  95                         check_kind
  96                          (At Nothing (SKiType `SKiArrow` SKiType))
  97                          (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
  98                         check_con (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \Con ->
  99                         compileO tok_a ctx $ \ty_a (TermO a) ->
 100                         k (ty_m :$ ty_a) $ TermO $
 101                          \c -> return (a c)
 102                  Token_Term_Monad_bind tok_ma tok_a2mb ->
 103                         -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
 104                         compileO tok_ma   ctx $ \ty_ma   (TermO ma) ->
 105                         compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
 106                         check_con1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl Con ty_ma_m ty_ma_a ->
 107                         check_type2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
 108                         check_type1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
 109                         check_type
 110                          (At (Just tok_a2mb) ty_a2mb_a)
 111                          (At (Just tok_ma) ty_ma_a) $ \Refl ->
 112                         k ty_a2mb_mb $ TermO $
 113                          \c -> (>>=) (ma c) (a2mb c)
 114                  Token_Term_Monad_when tok_cond tok_ok ->
 115                         -- when :: Applicative f => Bool -> f () -> f ()
 116                         compileO tok_cond ctx $ \ty_cond (TermO cond) ->
 117                         compileO tok_ok   ctx $ \ty_ok   (TermO ok) ->
 118                         check_con1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl Con _ty_ok_f ty_ok_u ->
 119                         check_type
 120                          (At Nothing (ty @Bool))
 121                          (At (Just tok_cond) ty_cond) $ \Refl ->
 122                         check_type
 123                          (At Nothing (ty @()))
 124                          (At (Just tok_ok) ty_ok_u) $ \Refl ->
 125                         k ty_ok $ TermO $
 126                          \c -> when (cond c) (ok c)