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 FixityOf Maybe
  49 instance ClassInstancesFor Maybe where
  50         proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
  51          | Just HRefl <- proj_ConstKiTy @_ @Maybe c
  52          = case () of
  53                  _ | Just Refl <- proj_Const @Applicative q -> Just Dict
  54                    | Just Refl <- proj_Const @Foldable q    -> Just Dict
  55                    | Just Refl <- proj_Const @Functor q     -> Just Dict
  56                    | Just Refl <- proj_Const @Monad q       -> Just Dict
  57                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  58                  _ -> Nothing
  59         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
  60          | Just HRefl <- proj_ConstKiTy @_ @Maybe c
  61          = case () of
  62                  _ | Just Refl <- proj_Const @Eq q
  63                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  64                    | Just Refl <- proj_Const @Monoid q
  65                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  66                    | Just Refl <- proj_Const @Show q
  67                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
  68                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  69                    | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
  70                  _ -> Nothing
  71         proveConstraintFor _c _q = Nothing
  72 instance TypeInstancesFor Maybe where
  73         expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
  74          | Just HRefl <- proj_ConstKi @_ @Element f
  75          , Just HRefl <- proj_ConstKiTy @_ @Maybe c
  76          = Just a
  77         expandFamFor _c _len _fam _as = Nothing
  78
  79 -- Compiling
  80 instance Gram_Term_AtomsFor src ss g Maybe
  81 instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
  82         moduleFor = ["Maybe"] `moduleWhere`
  83          [ "Nothing" := teMaybe_Nothing
  84          , "Just"    := teMaybe_Just
  85          , "maybe"   := teMaybe_maybe
  86          ]
  87
  88 -- ** 'Type's
  89 tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
  90 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
  91
  92 -- ** 'Term's
  93 teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
  94 teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
  95
  96 teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
  97 teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
  98
  99 teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
 100 teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'