symantic-lib/Language/Symantic/Lib/Maybe.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
   4 -- | Symantic for 'Maybe'.
   5 module Language.Symantic.Lib.Maybe where
   6
   7 import Control.Monad
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (maybe)
  11 import qualified Data.Function as Fun
  12 import qualified Data.Maybe as Maybe
  13 import qualified Data.MonoTraversable as MT
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming
  20 import Language.Symantic.Lib.Lambda
  21 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
  22
  23 -- * Class 'Sym_Maybe_Lam'
  24 class Sym_Maybe term where
  25         _Nothing :: term (Maybe a)
  26         _Just    :: term a -> term (Maybe a)
  27         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  28
  29         default _Nothing :: Trans t term => t term (Maybe a)
  30         default _Just    :: Trans t term => t term a -> t term (Maybe a)
  31         default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
  32
  33         _Nothing = trans_lift _Nothing
  34         _Just    = trans_map1 _Just
  35         maybe    = trans_map3 maybe
  36
  37 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
  38 type instance TyConsts_of_Iface (Proxy Maybe) = Proxy Maybe ': TyConsts_imported_by (Proxy Maybe)
  39 type instance TyConsts_imported_by (Proxy Maybe) =
  40  [ Proxy Applicative
  41  , Proxy Eq
  42  , Proxy Foldable
  43  , Proxy Functor
  44  , Proxy Monad
  45  , Proxy MT.MonoFoldable
  46  , Proxy MT.MonoFunctor
  47  , Proxy Monoid
  48  , Proxy Show
  49  , Proxy Traversable
  50  ]
  51
  52 instance Sym_Maybe HostI where
  53         _Nothing = HostI Nothing
  54         _Just    = liftM Just
  55         maybe    = liftM3 Maybe.maybe
  56 instance Sym_Maybe TextI where
  57         _Nothing = textI0 "Nothing"
  58         _Just    = textI1 "Just"
  59         maybe    = textI3 "maybe"
  60 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  61         _Nothing = dupI0 @Sym_Maybe _Nothing
  62         _Just    = dupI1 @Sym_Maybe _Just
  63         maybe    = dupI3 @Sym_Maybe maybe
  64
  65 instance
  66  ( Read_TyNameR TyName cs rs
  67  , Inj_TyConst cs Maybe
  68  ) => Read_TyNameR TyName cs (Proxy Maybe ': rs) where
  69         read_TyNameR _cs (TyName "Maybe") k = k (ty @Maybe)
  70         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  71 instance Show_TyConst cs => Show_TyConst (Proxy Maybe ': cs) where
  72         show_TyConst TyConstZ{} = "Maybe"
  73         show_TyConst (TyConstS c) = show_TyConst c
  74
  75 instance -- Proj_TyFamC TyFam_MonoElement
  76  ( Proj_TyConst cs Maybe
  77  ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
  78         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  79          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  80          , Just Refl <- proj_TyConst c (Proxy @Maybe)
  81          = Just ty_a
  82         proj_TyFamC _c _fam _ty = Nothing
  83
  84 instance -- Proj_TyConC
  85  ( Proj_TyConst cs Maybe
  86  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Maybe))
  87  , Proj_TyCon cs
  88  ) => Proj_TyConC cs (Proxy Maybe) where
  89         proj_TyConC _ (TyConst q :$ TyConst c)
  90          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  91          , Just Refl <- proj_TyConst c (Proxy @Maybe)
  92          = case () of
  93                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
  94                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
  95                    | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
  96                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
  97                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
  98                  _ -> Nothing
  99         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
 100          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 101          , Just Refl <- proj_TyConst c (Proxy @Maybe)
 102          = case () of
 103                  _ | Just Refl  <- proj_TyConst q (Proxy @Eq)
 104                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 105                    | Just Refl <- proj_TyConst q (Proxy @Monoid)
 106                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 107                    | Just Refl <- proj_TyConst q (Proxy @Show)
 108                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 109                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
 110                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)  -> Just TyCon
 111                  _ -> Nothing
 112         proj_TyConC _c _q = Nothing
 113 data instance TokenT meta (ts::[*]) (Proxy Maybe)
 114  = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
 115  | Token_Term_Maybe_Just    (EToken meta ts)
 116  | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
 117 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
 118 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
 119
 120 instance -- CompileI
 121  ( Read_TyName TyName cs
 122  , Inj_TyConst        cs Maybe
 123  , Inj_TyConst        cs (->)
 124  , Compile cs is
 125  ) => CompileI cs is (Proxy Maybe) where
 126         compileI tok ctx k =
 127                 case tok of
 128                  Token_Term_Maybe_Nothing tok_ty_a ->
 129                         -- Nothing :: Maybe a
 130                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
 131                         check_Kind
 132                          (At Nothing SKiType)
 133                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 134                         k (ty @Maybe :$ ty_a) $ Term $
 135                                 Fun.const _Nothing
 136                  Token_Term_Maybe_Just tok_a ->
 137                         -- Just :: a -> Maybe a
 138                         compile tok_a ctx $ \ty_a (Term a) ->
 139                         k (ty @Maybe :$ ty_a) $ Term $
 140                          \c -> _Just (a c)
 141                  Token_Term_Maybe_maybe tok_b tok_a2b ->
 142                         -- maybe :: b -> (a -> b) -> Maybe a -> b
 143                         compile tok_b   ctx $ \ty_b   (Term b) ->
 144                         compile tok_a2b ctx $ \ty_a2b (Term a2b) ->
 145                         check_TyEq2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 146                         check_TyEq
 147                          (At (Just tok_a2b) ty_a2b_b)
 148                          (At (Just tok_b) ty_b) $ \Refl ->
 149                         k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ Term $
 150                          \c -> lam $ maybe (b c) (a2b c)
 151 instance
 152  Inj_Token meta ts Maybe =>
 153  TokenizeT meta ts (Proxy Maybe) where
 154         tokenizeT _t = mempty
 155          { tokenizers_infix = tokenizeTMod []
 156                  [ (TeName "Nothing",) ProTok_Term
 157                          { protok_term = \meta -> ProTokPi $ \a ->
 158                                 ProTok $ inj_EToken meta $ Token_Term_Maybe_Nothing a
 159                          , protok_fixity = infixN5
 160                          }
 161                  , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
 162                  ]
 163          }
 164 instance Gram_Term_AtomsT meta ts (Proxy Maybe) g