1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Maybe'.
4 module Language.Symantic.Lib.Maybe where
7 import Prelude hiding (maybe)
8 import qualified Data.Maybe as Maybe
9 import qualified Data.MonoTraversable as MT
11 import Language.Symantic
12 import Language.Symantic.Lib.Function (a0, b1)
13 import Language.Symantic.Lib.MonoFunctor (Element)
15 -- * Class 'Sym_Maybe'
16 type instance Sym (Proxy 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
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
26 _Nothing = trans _Nothing
31 instance Sym_Maybe Eval where
32 _Nothing = Eval Nothing
34 maybe = eval3 Maybe.maybe
35 instance Sym_Maybe View where
36 _Nothing = view0 "Nothing"
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
45 instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
48 instance FixityOf Maybe
49 instance ClassInstancesFor Maybe where
50 proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
51 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
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
59 proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
60 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
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
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
77 expandFamFor _c _len _fam _as = Nothing
80 instance Gram_Term_AtomsFor src ss g Maybe
81 instance (Source src, Inj_Sym ss Maybe) => Module src ss Maybe where
82 module_ _s = [] `moduleWhere`
83 [ "Nothing" := teMaybe_Nothing
84 , "Just" := teMaybe_Just
85 , "maybe" := teMaybe_maybe
89 tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)
90 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
93 teMaybe_Nothing :: TermDef Maybe '[Proxy a] (Maybe a)
94 teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
96 teMaybe_Just :: TermDef Maybe '[Proxy a] (a -> Maybe a)
97 teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
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'