Language/Symantic/Compiling/Maybe.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Maybe'.
   5 module Language.Symantic.Compiling.Maybe where
   6
   7 import Control.Monad
   8 import qualified Data.Function as Fun
   9 import qualified Data.Maybe as Maybe
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (maybe)
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20
  21 -- * Class 'Sym_Maybe_Lam'
  22 class Sym_Maybe term where
  23         _Nothing :: term (Maybe a)
  24         _Just    :: term a -> term (Maybe a)
  25         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  26
  27         default _Nothing :: Trans t term => t term (Maybe a)
  28         default _Just    :: Trans t term => t term a -> t term (Maybe a)
  29         default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
  30
  31         _Nothing = trans_lift _Nothing
  32         _Just    = trans_map1 _Just
  33         maybe    = trans_map3 maybe
  34
  35 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
  36 type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
  37 type instance Consts_imported_by Maybe =
  38  [ Proxy Applicative
  39  , Proxy Eq
  40  , Proxy Foldable
  41  , Proxy Functor
  42  , Proxy Monad
  43  , Proxy Monoid
  44  , Proxy Show
  45  , Proxy Traversable
  46  ]
  47
  48 instance Sym_Maybe HostI where
  49         _Nothing = HostI Nothing
  50         _Just    = liftM Just
  51         maybe    = liftM3 Maybe.maybe
  52 instance Sym_Maybe TextI where
  53         _Nothing = textI0 "Nothing"
  54         _Just    = textI1 "Just"
  55         maybe    = textI3 "maybe"
  56 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  57         _Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
  58         _Just    = dupI1 (Proxy @Sym_Maybe) _Just
  59         maybe    = dupI3 (Proxy @Sym_Maybe) maybe
  60
  61 instance
  62  ( Read_TypeNameR Text cs rs
  63  , Inj_Const cs Maybe
  64  ) => Read_TypeNameR Text cs (Proxy Maybe ': rs) where
  65         read_typenameR _cs "Maybe" k = k (ty @Maybe)
  66         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  67 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
  68         show_const ConstZ{} = "Maybe"
  69         show_const (ConstS c) = show_const c
  70
  71 instance -- Proj_ConC
  72  ( Proj_Const cs Maybe
  73  , Proj_Consts cs (Consts_imported_by Maybe)
  74  , Proj_Con cs
  75  ) => Proj_ConC cs (Proxy Maybe) where
  76         proj_conC _ (TyConst q :$ TyConst c)
  77          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  78          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  79          = case () of
  80                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  81                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  82                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  83                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  84                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  85                  _ -> Nothing
  86         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  87          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  88          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  89          = case () of
  90                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  91                    , Just Con  <- proj_con (t :$ a) -> Just Con
  92                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
  93                    , Just Con  <- proj_con (t :$ a) -> Just Con
  94                    | Just Refl <- proj_const q (Proxy::Proxy Show)
  95                    , Just Con  <- proj_con (t :$ a) -> Just Con
  96                  _ -> Nothing
  97         proj_conC _c _q = Nothing
  98 data instance TokenT meta (ts::[*]) (Proxy Maybe)
  99  = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
 100  | Token_Term_Maybe_Just    (EToken meta ts)
 101  | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
 102 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
 103 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
 104 instance -- CompileI
 105  ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
 106  , Inj_Const  (Consts_of_Ifaces is) Maybe
 107  , Inj_Const  (Consts_of_Ifaces is) (->)
 108  , Compile is
 109  ) => CompileI is (Proxy Maybe) where
 110         compileI tok ctx k =
 111                 case tok of
 112                  Token_Term_Maybe_Nothing tok_ty_a ->
 113                         -- Nothing :: Maybe a
 114                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 115                         check_kind
 116                          (At Nothing SKiType)
 117                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 118                         k (ty @Maybe :$ ty_a) $ TermO $
 119                                 Fun.const _Nothing
 120                  Token_Term_Maybe_Just tok_a ->
 121                         -- Just :: a -> Maybe a
 122                         compileO tok_a ctx $ \ty_a (TermO a) ->
 123                         k (ty @Maybe :$ ty_a) $ TermO $
 124                          \c -> _Just (a c)
 125                  Token_Term_Maybe_maybe tok_b tok_a2b ->
 126                         -- maybe :: b -> (a -> b) -> Maybe a -> b
 127                         compileO tok_b   ctx $ \ty_b   (TermO b) ->
 128                         compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
 129                         check_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 130                         check_type
 131                          (At (Just tok_a2b) ty_a2b_b)
 132                          (At (Just tok_b) ty_b) $ \Refl ->
 133                         k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermO $
 134                          \c -> lam $ maybe (b c) (a2b c)