Language/Symantic/Compiling/Monad.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 'Monad'.
  14 module Language.Symantic.Compiling.Monad where
  15
  16 import Control.Monad (Monad)
  17 import qualified Control.Monad as Monad
  18 import qualified Data.Function as Fun
  19 import Data.Monoid ((<>))
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (Monad(..))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Applicative (Sym_Applicative, tyApplicative)
  29 import Language.Symantic.Compiling.Bool (tyBool)
  30 import Language.Symantic.Interpreting
  31 import Language.Symantic.Transforming.Trans
  32
  33 -- * Class 'Sym_Monad'
  34 class Sym_Applicative term => Sym_Monad term where
  35         return :: Monad m => term a -> term (m a)
  36         (>>=)  :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
  37         when   :: Applicative f => term Bool -> term (f ()) -> term (f ())
  38
  39         default return :: (Trans t term, Monad m)
  40          => t term a -> t term (m a)
  41         default (>>=) :: (Trans t term, Monad m)
  42          => t term (m a) -> t term (a -> m b) -> t term (m b)
  43         default when :: (Trans t term, Applicative f)
  44          => t term Bool -> t term (f ()) -> t term (f ())
  45
  46         return = trans_map1 return
  47         (>>=)  = trans_map2 (>>=)
  48         when   = trans_map2 when
  49
  50 infixl 1 >>=
  51
  52 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
  53 type instance Consts_of_Iface (Proxy Monad) = Proxy Monad ': Consts_imported_by Monad
  54 type instance Consts_imported_by Monad =
  55  [ Proxy ()
  56  , Proxy Applicative
  57  , Proxy Bool
  58  ]
  59
  60 instance Sym_Monad HostI where
  61         return = Monad.liftM Monad.return
  62         (>>=)  = Monad.liftM2 (Monad.>>=)
  63         when   = Monad.liftM2 Monad.when
  64 instance Sym_Monad TextI where
  65         return = textI_app1 "return"
  66         (>>=)  = textI_infix ">>=" (Precedence 1)
  67         when (TextI cond) (TextI ok) =
  68                 TextI $ \p v ->
  69                         let p' = Precedence 2 in
  70                         paren p p' $
  71                         "when " <> cond p' v <>
  72                         " " <> ok p' v
  73 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
  74         return = dupI1 sym_Monad return
  75         (>>=)  = dupI2 sym_Monad (>>=)
  76         when   = dupI2 sym_Monad when
  77
  78 instance Const_from Text cs => Const_from Text (Proxy Monad ': cs) where
  79         const_from "Monad" k = k (ConstZ kind)
  80         const_from s k = const_from s $ k . ConstS
  81 instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
  82         show_const ConstZ{} = "Monad"
  83         show_const (ConstS c) = show_const c
  84
  85 instance -- Proj_ConC
  86  Proj_ConC cs (Proxy Monad)
  87 instance -- Term_fromI
  88  ( AST ast
  89  , Lexem ast ~ LamVarName
  90  , Const_from (Lexem ast) (Consts_of_Ifaces is)
  91  , Inj_Const (Consts_of_Ifaces is) Monad
  92  , Inj_Const (Consts_of_Ifaces is) (->)
  93  , Inj_Const (Consts_of_Ifaces is) ()
  94  , Inj_Const (Consts_of_Ifaces is) Applicative
  95  , Inj_Const (Consts_of_Ifaces is) Bool
  96  , Proj_Con  (Consts_of_Ifaces is)
  97  , Term_from is ast
  98  ) => Term_fromI is (Proxy Monad) ast where
  99         term_fromI ast ctx k =
 100                 case ast_lexem ast of
 101                  "return" -> return_from
 102                  ">>="    -> bind_from
 103                  "when"   -> when_from
 104                  _ -> Left $ Error_Term_unsupported
 105                 where
 106                 return_from =
 107                  -- return :: Monad m => a -> m a
 108                         from_ast2 ast $ \ast_ty_m ast_a ->
 109                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 110                         type_from ast_ty_m $ \ty_m -> Right $
 111                         check_kind ast (SKiType `SKiArrow` SKiType) (At (Just ast_ty_m) ty_m) $ \Refl ->
 112                         check_constraint (At (Just ast_ty_m) (tyMonad :$ ty_m)) $ \Con ->
 113                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 114                         k (ty_m :$ ty_a) $ TermLC $
 115                          \c -> return (a c)
 116                 bind_from =
 117                  -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
 118                         from_ast2 ast $ \ast_ma ast_a2mb ->
 119                         term_from ast_ma   ctx $ \ty_ma   (TermLC ma) ->
 120                         term_from ast_a2mb ctx $ \ty_a2mb (TermLC a2mb) ->
 121                         check_constraint1 tyMonad ast_ma ty_ma $ \Refl Con ty_ma_m ty_ma_a ->
 122                         check_type2 tyFun ast_a2mb ty_a2mb $ \Refl ty_a2mb_a ty_a2mb_mb ->
 123                         check_type1 ty_ma_m ast_a2mb ty_a2mb_mb $ \Refl _ty_a2mb_mb_b ->
 124                         check_type (At (Just ast_a2mb) ty_a2mb_a) (At (Just ast_ma) ty_ma_a) $ \Refl ->
 125                         k ty_a2mb_mb $ TermLC $
 126                          \c -> (>>=) (ma c) (a2mb c)
 127                 when_from =
 128                  -- when :: Applicative f => Bool -> f () -> f ()
 129                         case ast_nodes ast of
 130                          [] -> Left $ Error_Term_Syntax $
 131                                 Error_Syntax_more_arguments_needed $ At (Just ast) 2
 132                          [ast_cond, ast_ok] ->
 133                                 term_from ast_cond ctx $ \ty_cond (TermLC cond) ->
 134                                 term_from ast_ok   ctx $ \ty_ok   (TermLC ok) ->
 135                                 check_constraint1 tyApplicative ast_ok ty_ok $ \Refl Con _ty_ok_f ty_ok_u ->
 136                                 check_type (At Nothing tyBool) (At (Just ast_cond) ty_cond) $ \Refl ->
 137                                 check_type (At Nothing tyUnit) (At (Just ast_ok) ty_ok_u) $ \Refl ->
 138                                 k ty_ok $ TermLC $
 139                                  \c -> when (cond c) (ok c)
 140                          _ -> Left $ Error_Term_Syntax $
 141                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 142
 143 -- | The 'Monad' 'Type'
 144 tyMonad :: Inj_Const cs Monad => Type cs Monad
 145 tyMonad = TyConst inj_const
 146
 147 sym_Monad :: Proxy Sym_Monad
 148 sym_Monad = Proxy
 149
 150 syMonad :: IsString a => [Syntax a] -> Syntax a
 151 syMonad = Syntax "Monad"
 152
 153 syWhen :: IsString a => Syntax a -> Syntax a -> Syntax a
 154 syWhen cond ok = Syntax "when" [cond, ok]