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.Parsing.Grammar
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20 import Language.Symantic.Lib.Lambda
  21
  22 -- * Class 'Sym_Maybe_Lam'
  23 class Sym_Maybe term where
  24         _Nothing :: term (Maybe a)
  25         _Just    :: term a -> term (Maybe a)
  26         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  27
  28         default _Nothing :: Trans t term => t term (Maybe a)
  29         default _Just    :: Trans t term => t term a -> t term (Maybe a)
  30         default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
  31
  32         _Nothing = trans_lift _Nothing
  33         _Just    = trans_map1 _Just
  34         maybe    = trans_map3 maybe
  35
  36 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
  37 type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
  38 type instance Consts_imported_by Maybe =
  39  [ Proxy Applicative
  40  , Proxy Eq
  41  , Proxy Foldable
  42  , Proxy Functor
  43  , Proxy Monad
  44  , Proxy Monoid
  45  , Proxy Show
  46  , Proxy Traversable
  47  ]
  48
  49 instance Sym_Maybe HostI where
  50         _Nothing = HostI Nothing
  51         _Just    = liftM Just
  52         maybe    = liftM3 Maybe.maybe
  53 instance Sym_Maybe TextI where
  54         _Nothing = textI0 "Nothing"
  55         _Just    = textI1 "Just"
  56         maybe    = textI3 "maybe"
  57 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  58         _Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
  59         _Just    = dupI1 (Proxy @Sym_Maybe) _Just
  60         maybe    = dupI3 (Proxy @Sym_Maybe) maybe
  61
  62 instance
  63  ( Read_TypeNameR Type_Name cs rs
  64  , Inj_Const cs Maybe
  65  ) => Read_TypeNameR Type_Name cs (Proxy Maybe ': rs) where
  66         read_typenameR _cs (Type_Name "Maybe") k = k (ty @Maybe)
  67         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  68 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
  69         show_const ConstZ{} = "Maybe"
  70         show_const (ConstS c) = show_const c
  71
  72 instance -- Proj_ConC
  73  ( Proj_Const cs Maybe
  74  , Proj_Consts cs (Consts_imported_by Maybe)
  75  , Proj_Con cs
  76  ) => Proj_ConC cs (Proxy Maybe) where
  77         proj_conC _ (TyConst q :$ TyConst c)
  78          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  79          , Just Refl <- proj_const c (Proxy @Maybe)
  80          = case () of
  81                  _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
  82                    | Just Refl <- proj_const q (Proxy @Foldable)    -> Just Con
  83                    | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
  84                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
  85                    | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
  86                  _ -> Nothing
  87         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  88          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  89          , Just Refl <- proj_const c (Proxy @Maybe)
  90          = case () of
  91                  _ | Just Refl <- proj_const q (Proxy @Eq)
  92                    , Just Con  <- proj_con (t :$ a) -> Just Con
  93                    | Just Refl <- proj_const q (Proxy @Monoid)
  94                    , Just Con  <- proj_con (t :$ a) -> Just Con
  95                    | Just Refl <- proj_const q (Proxy @Show)
  96                    , Just Con  <- proj_con (t :$ a) -> Just Con
  97                  _ -> Nothing
  98         proj_conC _c _q = Nothing
  99 data instance TokenT meta (ts::[*]) (Proxy Maybe)
 100  = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
 101  | Token_Term_Maybe_Just    (EToken meta ts)
 102  | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
 103 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
 104 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
 105 instance -- CompileI
 106  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 107  , Inj_Const  (Consts_of_Ifaces is) Maybe
 108  , Inj_Const  (Consts_of_Ifaces is) (->)
 109  , Compile is
 110  ) => CompileI is (Proxy Maybe) where
 111         compileI tok ctx k =
 112                 case tok of
 113                  Token_Term_Maybe_Nothing tok_ty_a ->
 114                         -- Nothing :: Maybe a
 115                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 116                         check_kind
 117                          (At Nothing SKiType)
 118                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 119                         k (ty @Maybe :$ ty_a) $ TermO $
 120                                 Fun.const _Nothing
 121                  Token_Term_Maybe_Just tok_a ->
 122                         -- Just :: a -> Maybe a
 123                         compileO tok_a ctx $ \ty_a (TermO a) ->
 124                         k (ty @Maybe :$ ty_a) $ TermO $
 125                          \c -> _Just (a c)
 126                  Token_Term_Maybe_maybe tok_b tok_a2b ->
 127                         -- maybe :: b -> (a -> b) -> Maybe a -> b
 128                         compileO tok_b   ctx $ \ty_b   (TermO b) ->
 129                         compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
 130                         check_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 131                         check_type
 132                          (At (Just tok_a2b) ty_a2b_b)
 133                          (At (Just tok_b) ty_b) $ \Refl ->
 134                         k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermO $
 135                          \c -> lam $ maybe (b c) (a2b c)
 136 instance
 137  Inj_Token meta ts Maybe =>
 138  TokenizeT meta ts (Proxy Maybe) where
 139         tokenizeT _t = mempty
 140          { tokenizers_infix = tokenizeTMod []
 141                  [ (Term_Name "Nothing",) Term_ProTok
 142                          { term_protok = \meta -> ProTokPi $ \a ->
 143                                 ProTok $ inj_etoken meta $ Token_Term_Maybe_Nothing a
 144                          , term_fixity = infixN5
 145                          }
 146                  , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
 147                  ]
 148          }
 149 instance Gram_Term_AtomsT meta ts (Proxy Maybe) g