]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/NonNull.hs
Fix time&space explosion of GHC's typechecker.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / NonNull.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
4 -- | Symantic for 'NonNull'.
5 module Language.Symantic.Lib.NonNull where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.MonoTraversable (MonoFoldable)
9 import qualified Data.MonoTraversable as MT
10 import Data.NonNull (NonNull)
11 import qualified Data.NonNull as NonNull
12 import Data.Proxy
13 import Data.Sequences (IsSequence, SemiSequence)
14 import Data.Type.Equality ((:~:)(Refl))
15 import Prelude hiding (head, init, last, tail)
16
17 import Language.Symantic.Parsing
18 import Language.Symantic.Typing
19 import Language.Symantic.Compiling
20 import Language.Symantic.Interpreting
21 import Language.Symantic.Transforming
22 import Language.Symantic.Lib.MonoFunctor
23
24 -- * Class 'Sym_NonNull'
25 class Sym_NonNull term where
26 fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
27 toNullable :: MonoFoldable o => term (NonNull o) -> term o
28 ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
29 nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
30 head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
31 last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
32 tail :: IsSequence s => term (NonNull s) -> term s
33 init :: IsSequence s => term (NonNull s) -> term s
34 nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
35 default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
36 default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
37 default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
38 default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
39 default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
40 default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
41 default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
42 default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
43 default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
44 fromNullable = trans_map1 fromNullable
45 toNullable = trans_map1 toNullable
46 ncons = trans_map2 ncons
47 nuncons = trans_map1 nuncons
48 head = trans_map1 head
49 last = trans_map1 last
50 tail = trans_map1 tail
51 init = trans_map1 init
52 nfilter = trans_map2 nfilter
53
54 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
55 type instance TyConsts_of_Iface (Proxy NonNull) = Proxy NonNull ': TyConsts_imported_by NonNull
56 type instance TyConsts_imported_by NonNull =
57 [ Proxy (->)
58 , Proxy (,)
59 , Proxy Eq
60 , Proxy Maybe
61 , Proxy Ord
62 , Proxy MT.MonoFoldable
63 , Proxy MT.MonoFunctor
64 , Proxy IsSequence
65 , Proxy SemiSequence
66 , Proxy Show
67 ]
68
69 instance Sym_NonNull HostI where
70 fromNullable = liftM NonNull.fromNullable
71 toNullable = liftM NonNull.toNullable
72 ncons = liftM2 NonNull.ncons
73 nuncons = liftM NonNull.nuncons
74 head = liftM NonNull.head
75 last = liftM NonNull.last
76 tail = liftM NonNull.tail
77 init = liftM NonNull.init
78 nfilter = liftM2 NonNull.nfilter
79 instance Sym_NonNull TextI where
80 fromNullable = textI1 "fromNullable"
81 toNullable = textI1 "toNullable"
82 ncons = textI2 "ncons"
83 nuncons = textI1 "nuncons"
84 head = textI1 "head"
85 last = textI1 "last"
86 tail = textI1 "tail"
87 init = textI1 "init"
88 nfilter = textI2 "nfilter"
89 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
90 fromNullable = dupI1 @Sym_NonNull fromNullable
91 toNullable = dupI1 @Sym_NonNull toNullable
92 ncons = dupI2 @Sym_NonNull ncons
93 nuncons = dupI1 @Sym_NonNull nuncons
94 head = dupI1 @Sym_NonNull head
95 last = dupI1 @Sym_NonNull last
96 tail = dupI1 @Sym_NonNull tail
97 init = dupI1 @Sym_NonNull init
98 nfilter = dupI2 @Sym_NonNull nfilter
99
100 instance
101 ( Read_TyNameR TyName cs rs
102 , Inj_TyConst cs NonNull
103 ) => Read_TyNameR TyName cs (Proxy NonNull ': rs) where
104 read_TyNameR _cs (TyName "NonNull") k = k (ty @NonNull)
105 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
106 instance Show_TyConst cs => Show_TyConst (Proxy NonNull ': cs) where
107 show_TyConst TyConstZ{} = "NonNull"
108 show_TyConst (TyConstS c) = show_TyConst c
109
110 instance -- TyFam_MonoElement
111 ( Proj_TyConst cs NonNull
112 , Proj_TyFam cs TyFam_MonoElement
113 ) => Proj_TyFamC cs TyFam_MonoElement NonNull where
114 proj_TyFamC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
115 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
116 , Just Refl <- proj_TyConst c (Proxy @NonNull)
117 = proj_TyFam TyFam_MonoElement (ty_o `TypesS` TypesZ)
118 proj_TyFamC _c _fam _ty = Nothing
119 instance -- Proj_TyConC
120 ( Proj_TyConst cs NonNull
121 , Proj_TyConsts cs (TyConsts_imported_by NonNull)
122 , Proj_TyCon cs
123 ) => Proj_TyConC cs (Proxy NonNull) where
124 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ o))
125 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
126 , Just Refl <- proj_TyConst c (Proxy @NonNull)
127 = case () of
128 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
129 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
130 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)
131 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
132 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)
133 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
134 | Just Refl <- proj_TyConst q (Proxy @Ord)
135 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
136 | Just Refl <- proj_TyConst q (Proxy @SemiSequence)
137 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
138 | Just Refl <- proj_TyConst q (Proxy @Show)
139 , Just TyCon <- proj_TyCon (t :$ o) -> Just TyCon
140 _ -> Nothing
141 proj_TyConC _c _q = Nothing
142 data instance TokenT meta (ts::[*]) (Proxy NonNull)
143 = Token_Term_NonNull_fromNullable (EToken meta ts)
144 | Token_Term_NonNull_toNullable (EToken meta ts)
145 | Token_Term_NonNull_ncons (EToken meta ts) (EToken meta ts)
146 | Token_Term_NonNull_nuncons (EToken meta ts)
147 | Token_Term_NonNull_head (EToken meta ts)
148 | Token_Term_NonNull_last (EToken meta ts)
149 | Token_Term_NonNull_tail (EToken meta ts)
150 | Token_Term_NonNull_init (EToken meta ts)
151 | Token_Term_NonNull_nfilter (EToken meta ts) (EToken meta ts)
152 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy NonNull))
153 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy NonNull))
154 instance -- CompileI
155 ( Inj_TyConst cs NonNull
156 , Inj_TyConst cs (->)
157 , Inj_TyConst cs (,)
158 , Inj_TyConst cs Bool
159 , Inj_TyConst cs Maybe
160 , Inj_TyConst cs MonoFoldable
161 , Inj_TyConst cs IsSequence
162 , Inj_TyConst cs SemiSequence
163 , Proj_TyCon cs
164 , Proj_TyFam cs TyFam_MonoElement
165 , Compile cs is
166 ) => CompileI cs is (Proxy NonNull) where
167 compileI
168 :: forall meta ctx ret ls rs.
169 TokenT meta is (Proxy NonNull)
170 -> CompileT meta ctx ret cs is ls (Proxy NonNull ': rs)
171 compileI tok ctx k =
172 case tok of
173 Token_Term_NonNull_fromNullable tok_o ->
174 -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
175 compileO tok_o ctx $ \ty_o (TermO o) ->
176 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
177 k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermO $
178 \c -> fromNullable (o c)
179 Token_Term_NonNull_toNullable tok_n ->
180 -- toNullable :: MonoFoldable o => NonNull o -> o
181 compileO tok_n ctx $ \ty_n (TermO n) ->
182 check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
183 check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
184 k ty_o $ TermO $
185 \c -> toNullable (n c)
186 Token_Term_NonNull_ncons tok_e tok_s ->
187 -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
188 compileO tok_e ctx $ \ty_e (TermO e) ->
189 compileO tok_s ctx $ \ty_s (TermO s) ->
190 check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
191 check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
192 check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
193 k (ty @NonNull :$ ty_s) $ TermO $
194 \c -> ncons (e c) (s c)
195 Token_Term_NonNull_nuncons tok_n ->
196 -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
197 compileO tok_n ctx $ \ty_n (TermO n) ->
198 check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
199 check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
200 check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
201 check_TyEq
202 (At Nothing ty_s_e)
203 (At (Just tok_n) ty_s_e) $ \Refl ->
204 k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermO $
205 \c -> nuncons (n c)
206 Token_Term_NonNull_head tok_n -> n2e_from tok_n head
207 Token_Term_NonNull_last tok_n -> n2e_from tok_n last
208 Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
209 Token_Term_NonNull_init tok_n -> n2s_from tok_n init
210 Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
211 -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
212 compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
213 compileO tok_n ctx $ \ty_n (TermO s) ->
214 check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
215 check_TyEq
216 (At Nothing (ty @Bool))
217 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
218 check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
219 check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
220 check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
221 check_TyEq
222 (At Nothing ty_s_e)
223 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
224 k ty_s $ TermO $
225 \c -> nfilter (e2Bool c) (s c)
226 where
227 n2e_from tok_n
228 (f::forall term o.
229 (Sym_NonNull term, MonoFoldable o)
230 => term (NonNull o) -> term (MT.Element o)) =
231 -- head :: MonoFoldable o => NonNull o -> MT.Element o
232 -- last :: MonoFoldable o => NonNull o -> MT.Element o
233 compileO tok_n ctx $ \ty_n (TermO n) ->
234 check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
235 check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
236 check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
237 k ty_o_e $ TermO $
238 \c -> f (n c)
239 n2s_from tok_n
240 (f::forall term s.
241 (Sym_NonNull term, IsSequence s)
242 => term (NonNull s) -> term s) =
243 -- tail :: IsSequence s => NonNull s -> s
244 -- init :: IsSequence s => NonNull s -> s
245 compileO tok_n ctx $ \ty_n (TermO n) ->
246 check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
247 check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
248 k ty_s $ TermO $
249 \c -> f (n c)
250 instance -- TokenizeT
251 Inj_Token meta ts NonNull =>
252 TokenizeT meta ts (Proxy NonNull) where
253 tokenizeT _t = mempty
254 { tokenizers_infix = tokenizeTMod []
255 [ tokenize1 "fromNullable" infixN5 Token_Term_NonNull_fromNullable
256 , tokenize1 "toNullable" infixN5 Token_Term_NonNull_toNullable
257 , tokenize2 "ncons" infixN5 Token_Term_NonNull_ncons
258 , tokenize1 "nuncons" infixN5 Token_Term_NonNull_nuncons
259 , tokenize1 "head" infixN5 Token_Term_NonNull_head
260 , tokenize1 "last" infixN5 Token_Term_NonNull_last
261 , tokenize1 "tail" infixN5 Token_Term_NonNull_tail
262 , tokenize1 "init" infixN5 Token_Term_NonNull_init
263 , tokenize2 "nfilter" infixN5 Token_Term_NonNull_nfilter
264 ]
265 }
266 instance Gram_Term_AtomsT meta ts (Proxy NonNull) g