]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Maybe.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Maybe.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
4 -- | Symantic for 'Maybe'.
5 module Language.Symantic.Lib.Maybe where
6
7 import Control.Monad
8 import Data.Proxy
9 import Data.Type.Equality ((:~:)(Refl))
10 import Prelude hiding (maybe)
11 import qualified Data.Function as Fun
12 import qualified Data.Maybe as Maybe
13 import qualified Data.MonoTraversable as MT
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming
20 import Language.Symantic.Lib.Lambda
21 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
22
23 -- * Class 'Sym_Maybe_Lam'
24 class Sym_Maybe term where
25 _Nothing :: term (Maybe a)
26 _Just :: term a -> term (Maybe a)
27 maybe :: term b -> term (a -> b) -> term (Maybe a) -> term b
28
29 default _Nothing :: Trans t term => t term (Maybe a)
30 default _Just :: Trans t term => t term a -> t term (Maybe a)
31 default maybe :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
32
33 _Nothing = trans_lift _Nothing
34 _Just = trans_map1 _Just
35 maybe = trans_map3 maybe
36
37 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
38 type instance TyConsts_of_Iface (Proxy Maybe) = Proxy Maybe ': TyConsts_imported_by (Proxy Maybe)
39 type instance TyConsts_imported_by (Proxy Maybe) =
40 [ Proxy Applicative
41 , Proxy Eq
42 , Proxy Foldable
43 , Proxy Functor
44 , Proxy Monad
45 , Proxy MT.MonoFoldable
46 , Proxy MT.MonoFunctor
47 , Proxy Monoid
48 , Proxy Show
49 , Proxy Traversable
50 ]
51
52 instance Sym_Maybe HostI where
53 _Nothing = HostI Nothing
54 _Just = liftM Just
55 maybe = liftM3 Maybe.maybe
56 instance Sym_Maybe TextI where
57 _Nothing = textI0 "Nothing"
58 _Just = textI1 "Just"
59 maybe = textI3 "maybe"
60 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
61 _Nothing = dupI0 @Sym_Maybe _Nothing
62 _Just = dupI1 @Sym_Maybe _Just
63 maybe = dupI3 @Sym_Maybe maybe
64
65 instance
66 ( Read_TyNameR TyName cs rs
67 , Inj_TyConst cs Maybe
68 ) => Read_TyNameR TyName cs (Proxy Maybe ': rs) where
69 read_TyNameR _cs (TyName "Maybe") k = k (ty @Maybe)
70 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
71 instance Show_TyConst cs => Show_TyConst (Proxy Maybe ': cs) where
72 show_TyConst TyConstZ{} = "Maybe"
73 show_TyConst (TyConstS c) = show_TyConst c
74
75 instance -- Proj_TyFamC TyFam_MonoElement
76 ( Proj_TyConst cs Maybe
77 ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
78 proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
79 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
80 , Just Refl <- proj_TyConst c (Proxy @Maybe)
81 = Just ty_a
82 proj_TyFamC _c _fam _ty = Nothing
83
84 instance -- Proj_TyConC
85 ( Proj_TyConst cs Maybe
86 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Maybe))
87 , Proj_TyCon cs
88 ) => Proj_TyConC cs (Proxy Maybe) where
89 proj_TyConC _ (TyConst q :$ TyConst c)
90 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
91 , Just Refl <- proj_TyConst c (Proxy @Maybe)
92 = case () of
93 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
94 | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
95 | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
96 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
97 | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
98 _ -> Nothing
99 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
100 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
101 , Just Refl <- proj_TyConst c (Proxy @Maybe)
102 = case () of
103 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
104 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
105 | Just Refl <- proj_TyConst q (Proxy @Monoid)
106 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
107 | Just Refl <- proj_TyConst q (Proxy @Show)
108 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
109 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
110 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor) -> Just TyCon
111 _ -> Nothing
112 proj_TyConC _c _q = Nothing
113 data instance TokenT meta (ts::[*]) (Proxy Maybe)
114 = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
115 | Token_Term_Maybe_Just (EToken meta ts)
116 | Token_Term_Maybe_maybe (EToken meta ts) (EToken meta ts)
117 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
118 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
119
120 instance -- CompileI
121 ( Read_TyName TyName cs
122 , Inj_TyConst cs Maybe
123 , Inj_TyConst cs (->)
124 , Compile cs is
125 ) => CompileI cs is (Proxy Maybe) where
126 compileI tok ctx k =
127 case tok of
128 Token_Term_Maybe_Nothing tok_ty_a ->
129 -- Nothing :: Maybe a
130 compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
131 check_Kind
132 (At Nothing SKiType)
133 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
134 k (ty @Maybe :$ ty_a) $ TermO $
135 Fun.const _Nothing
136 Token_Term_Maybe_Just tok_a ->
137 -- Just :: a -> Maybe a
138 compileO tok_a ctx $ \ty_a (TermO a) ->
139 k (ty @Maybe :$ ty_a) $ TermO $
140 \c -> _Just (a c)
141 Token_Term_Maybe_maybe tok_b tok_a2b ->
142 -- maybe :: b -> (a -> b) -> Maybe a -> b
143 compileO tok_b ctx $ \ty_b (TermO b) ->
144 compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
145 check_TyEq2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
146 check_TyEq
147 (At (Just tok_a2b) ty_a2b_b)
148 (At (Just tok_b) ty_b) $ \Refl ->
149 k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermO $
150 \c -> lam $ maybe (b c) (a2b c)
151 instance
152 Inj_Token meta ts Maybe =>
153 TokenizeT meta ts (Proxy Maybe) where
154 tokenizeT _t = mempty
155 { tokenizers_infix = tokenizeTMod []
156 [ (TeName "Nothing",) ProTok_Term
157 { protok_term = \meta -> ProTokPi $ \a ->
158 ProTok $ inj_EToken meta $ Token_Term_Maybe_Nothing a
159 , protok_fixity = infixN5
160 }
161 , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
162 ]
163 }
164 instance Gram_Term_AtomsT meta ts (Proxy Maybe) g