]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Maybe.hs
Rename inj_* -> *Inj.
[haskell/symantic.git] / 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'