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