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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Maybe'.
   4 module Language.Symantic.Lib.Maybe where
   5
   6 import Control.Monad
   7 import Prelude hiding (maybe)
   8 import qualified Data.Maybe as Maybe
   9 import qualified Data.MonoTraversable as MT
  10
  11 import Language.Symantic
  12 import Language.Symantic.Lib.Function (a0, b1)
  13 import Language.Symantic.Lib.MonoFunctor (Element)
  14
  15 -- * Class 'Sym_Maybe'
  16 type instance Sym Maybe = Sym_Maybe
  17 class Sym_Maybe term where
  18         _Nothing :: term (Maybe a)
  19         _Just    :: term a -> term (Maybe a)
  20         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  21
  22         default _Nothing :: Sym_Maybe (UnT term) => Trans term => term (Maybe a)
  23         default _Just    :: Sym_Maybe (UnT term) => Trans term => term a -> term (Maybe a)
  24         default maybe    :: Sym_Maybe (UnT term) => Trans term => term b -> term (a -> b) -> term (Maybe a) -> term b
  25
  26         _Nothing = trans _Nothing
  27         _Just    = trans1 _Just
  28         maybe    = trans3 maybe
  29
  30 -- Interpreting
  31 instance Sym_Maybe Eval where
  32         _Nothing = Eval  Nothing
  33         _Just    = eval1 Just
  34         maybe    = eval3 Maybe.maybe
  35 instance Sym_Maybe View where
  36         _Nothing = view0 "Nothing"
  37         _Just    = view1 "Just"
  38         maybe    = view3 "maybe"
  39 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
  40         _Nothing = dup0 @Sym_Maybe _Nothing
  41         _Just    = dup1 @Sym_Maybe _Just
  42         maybe    = dup3 @Sym_Maybe maybe
  43
  44 -- Transforming
  45 instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
  46
  47 -- Typing
  48 instance NameTyOf Maybe where
  49         nameTyOf _c = ["Maybe"] `Mod` "Maybe"
  50 instance FixityOf Maybe
  51 instance ClassInstancesFor Maybe where
  52         proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
  53          | Just HRefl <- proj_ConstKiTy @_ @Maybe c
  54          = case () of
  55                  _ | Just Refl <- proj_Const @Applicative q -> Just Dict
  56                    | Just Refl <- proj_Const @Foldable q    -> Just Dict
  57                    | Just Refl <- proj_Const @Functor q     -> Just Dict
  58                    | Just Refl <- proj_Const @Monad q       -> Just Dict
  59                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  60                  _ -> Nothing
  61         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
  62          | Just HRefl <- proj_ConstKiTy @_ @Maybe c
  63          = case () of
  64                  _ | Just Refl <- proj_Const @Eq q
  65                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  66                    | Just Refl <- proj_Const @Monoid q
  67                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  68                    | Just Refl <- proj_Const @Show q
  69                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  70                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  71                    | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
  72                  _ -> Nothing
  73         proveConstraintFor _c _q = Nothing
  74 instance TypeInstancesFor Maybe where
  75         expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
  76          | Just HRefl <- proj_ConstKi @_ @Element f
  77          , Just HRefl <- proj_ConstKiTy @_ @Maybe c
  78          = Just a
  79         expandFamFor _c _len _fam _as = Nothing
  80
  81 -- Compiling
  82 instance Gram_Term_AtomsFor src ss g Maybe
  83 instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
  84         moduleFor = ["Maybe"] `moduleWhere`
  85          [ "Nothing" := teMaybe_Nothing
  86          , "Just"    := teMaybe_Just
  87          , "maybe"   := teMaybe_maybe
  88          ]
  89
  90 -- ** 'Type's
  91 tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
  92 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
  93
  94 -- ** 'Term's
  95 teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
  96 teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
  97
  98 teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
  99 teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
 100
 101 teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
 102 teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'