module Language.Symantic.Lib.Maybe where
import Control.Monad
import Prelude hiding (maybe)
import qualified Data.Maybe as Maybe
import qualified Data.MonoTraversable as MT
import Language.Symantic
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.MonoFunctor (Element)
type instance Sym Maybe = Sym_Maybe
class Sym_Maybe term where
_Nothing :: term (Maybe a)
_Just :: term a -> term (Maybe a)
maybe :: term b -> term (a -> b) -> term (Maybe a) -> term b
default _Nothing :: Sym_Maybe (UnT term) => Trans term => term (Maybe a)
default _Just :: Sym_Maybe (UnT term) => Trans term => term a -> term (Maybe a)
default maybe :: Sym_Maybe (UnT term) => Trans term => term b -> term (a -> b) -> term (Maybe a) -> term b
_Nothing = trans _Nothing
_Just = trans1 _Just
maybe = trans3 maybe
instance Sym_Maybe Eval where
_Nothing = Eval Nothing
_Just = eval1 Just
maybe = eval3 Maybe.maybe
instance Sym_Maybe View where
_Nothing = view0 "Nothing"
_Just = view1 "Just"
maybe = view3 "maybe"
instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
_Nothing = dup0 @Sym_Maybe _Nothing
_Just = dup1 @Sym_Maybe _Just
maybe = dup3 @Sym_Maybe maybe
instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
instance NameTyOf Maybe where
nameTyOf _c = ["Maybe"] `Mod` "Maybe"
instance FixityOf Maybe
instance ClassInstancesFor Maybe where
proveConstraintFor _ (TyConst _ _ q :$ m)
| Just HRefl <- proj_ConstKiTy @_ @Maybe m
= case () of
_ | Just Refl <- proj_Const @Applicative q -> Just Dict
| Just Refl <- proj_Const @Foldable q -> Just Dict
| Just Refl <- proj_Const @Functor q -> Just Dict
| Just Refl <- proj_Const @Monad q -> Just Dict
| Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@a)
| Just HRefl <- proj_ConstKiTy @_ @Maybe m
= case () of
_ | Just Refl <- proj_Const @Eq q
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Monoid q
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Show q
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
| Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Maybe where
expandFamFor _c _len f (m:@a `TypesS` TypesZ)
| Just HRefl <- proj_ConstKi @_ @Element f
, Just HRefl <- proj_ConstKiTy @_ @Maybe m
= Just a
expandFamFor _c _len _fam _as = Nothing
instance Gram_Term_AtomsFor src ss g Maybe
instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
moduleFor = ["Maybe"] `moduleWhere`
[ "Nothing" := teMaybe_Nothing
, "Just" := teMaybe_Just
, "maybe" := teMaybe_maybe
]
tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'