{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Maybe'. 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) -- * Class 'Sym_Maybe' 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 -- Interpreting 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 -- Transforming instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term) -- Typing instance FixityOf Maybe instance ClassInstancesFor Maybe where proveConstraintFor _ (TyApp _ (TyConst _ _ q) c) | Just HRefl <- proj_ConstKiTy @_ @Maybe c = 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 _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a)) | Just HRefl <- proj_ConstKiTy @_ @Maybe c = 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 (TyApp _ c a `TypesS` TypesZ) | Just HRefl <- proj_ConstKi @_ @Element f , Just HRefl <- proj_ConstKiTy @_ @Maybe c = Just a expandFamFor _c _len _fam _as = Nothing -- Compiling instance Gram_Term_AtomsFor src ss g Maybe instance (Source src, Inj_Sym ss Maybe) => ModuleFor src ss Maybe where moduleFor = ["Maybe"] `moduleWhere` [ "Nothing" := teMaybe_Nothing , "Just" := teMaybe_Just , "maybe" := teMaybe_maybe ] -- ** 'Type's tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a) tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`) -- ** 'Term's 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'