symantic-lib/Language/Symantic/Lib/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.Lib.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.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (maybe)
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming
  19 import Language.Symantic.Lib.Lambda
  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 TyConsts_of_Iface (Proxy Maybe) = Proxy Maybe ': TyConsts_imported_by Maybe
  37 type instance TyConsts_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 @Sym_Maybe _Nothing
  58         _Just    = dupI1 @Sym_Maybe _Just
  59         maybe    = dupI3 @Sym_Maybe maybe
  60
  61 instance
  62  ( Read_TyNameR TyName cs rs
  63  , Inj_TyConst cs Maybe
  64  ) => Read_TyNameR TyName cs (Proxy Maybe ': rs) where
  65         read_TyNameR _cs (TyName "Maybe") k = k (ty @Maybe)
  66         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  67 instance Show_TyConst cs => Show_TyConst (Proxy Maybe ': cs) where
  68         show_TyConst TyConstZ{} = "Maybe"
  69         show_TyConst (TyConstS c) = show_TyConst c
  70
  71 instance -- Proj_TyConC
  72  ( Proj_TyConst cs Maybe
  73  , Proj_TyConsts cs (TyConsts_imported_by Maybe)
  74  , Proj_TyCon cs
  75  ) => Proj_TyConC cs (Proxy Maybe) where
  76         proj_TyConC _ (TyConst q :$ TyConst c)
  77          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  78          , Just Refl <- proj_TyConst c (Proxy @Maybe)
  79          = case () of
  80                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
  81                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
  82                    | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
  83                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
  84                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
  85                  _ -> Nothing
  86         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
  87          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  88          , Just Refl <- proj_TyConst c (Proxy @Maybe)
  89          = case () of
  90                  _ | Just Refl  <- proj_TyConst q (Proxy @Eq)
  91                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
  92                    | Just Refl <- proj_TyConst q (Proxy @Monoid)
  93                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
  94                    | Just Refl <- proj_TyConst q (Proxy @Show)
  95                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
  96                  _ -> Nothing
  97         proj_TyConC _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_TyName TyName cs
 106  , Inj_TyConst        cs Maybe
 107  , Inj_TyConst        cs (->)
 108  , Compile cs is
 109  ) => CompileI cs 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 cs 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_TyEq2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 130                         check_TyEq
 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)
 135 instance
 136  Inj_Token meta ts Maybe =>
 137  TokenizeT meta ts (Proxy Maybe) where
 138         tokenizeT _t = mempty
 139          { tokenizers_infix = tokenizeTMod []
 140                  [ (TeName "Nothing",) ProTok_Term
 141                          { protok_term = \meta -> ProTokPi $ \a ->
 142                                 ProTok $ inj_EToken meta $ Token_Term_Maybe_Nothing a
 143                          , protok_fixity = infixN5
 144                          }
 145                  , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
 146                  ]
 147          }
 148 instance Gram_Term_AtomsT meta ts (Proxy Maybe) g