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
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
13 import Data.Sequences (IsSequence, SemiSequence)
14 import Data.Type.Equality ((:~:)(Refl))
15 import Prelude hiding (head, init, last, tail)
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
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
54 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
55 type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
56 type instance Consts_imported_by NonNull =
62 , Proxy MT.MonoFoldable
63 , Proxy MT.MonoFunctor
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"
88 nfilter = textI2 "nfilter"
89 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
90 fromNullable = dupI1 (Proxy @Sym_NonNull) fromNullable
91 toNullable = dupI1 (Proxy @Sym_NonNull) toNullable
92 ncons = dupI2 (Proxy @Sym_NonNull) ncons
93 nuncons = dupI1 (Proxy @Sym_NonNull) nuncons
94 head = dupI1 (Proxy @Sym_NonNull) head
95 last = dupI1 (Proxy @Sym_NonNull) last
96 tail = dupI1 (Proxy @Sym_NonNull) tail
97 init = dupI1 (Proxy @Sym_NonNull) init
98 nfilter = dupI2 (Proxy @Sym_NonNull) nfilter
101 ( Read_TypeNameR Type_Name cs rs
102 , Inj_Const cs NonNull
103 ) => Read_TypeNameR Type_Name cs (Proxy NonNull ': rs) where
104 read_typenameR _cs (Type_Name "NonNull") k = k (ty @NonNull)
105 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
106 instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
107 show_const ConstZ{} = "NonNull"
108 show_const (ConstS c) = show_const c
110 instance -- Fam_MonoElement
111 ( Proj_Const cs NonNull
112 , Proj_Fam cs Fam_MonoElement
113 ) => Proj_FamC cs Fam_MonoElement NonNull where
114 proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
115 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
116 , Just Refl <- proj_const c (Proxy @NonNull)
117 = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
118 proj_famC _c _fam _ty = Nothing
119 instance -- Proj_ConC
120 ( Proj_Const cs NonNull
121 , Proj_Consts cs (Consts_imported_by NonNull)
123 ) => Proj_ConC cs (Proxy NonNull) where
124 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
125 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
126 , Just Refl <- proj_const c (Proxy @NonNull)
128 _ | Just Refl <- proj_const q (Proxy @Eq)
129 , Just Con <- proj_con (t :$ o) -> Just Con
130 | Just Refl <- proj_const q (Proxy @MT.MonoFoldable)
131 , Just Con <- proj_con (t :$ o) -> Just Con
132 | Just Refl <- proj_const q (Proxy @MT.MonoFunctor)
133 , Just Con <- proj_con (t :$ o) -> Just Con
134 | Just Refl <- proj_const q (Proxy @Ord)
135 , Just Con <- proj_con (t :$ o) -> Just Con
136 | Just Refl <- proj_const q (Proxy @SemiSequence)
137 , Just Con <- proj_con (t :$ o) -> Just Con
138 | Just Refl <- proj_const q (Proxy @Show)
139 , Just Con <- proj_con (t :$ o) -> Just Con
141 proj_conC _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))
155 ( Inj_Const (Consts_of_Ifaces is) NonNull
156 , Inj_Const (Consts_of_Ifaces is) (->)
157 , Inj_Const (Consts_of_Ifaces is) (,)
158 , Inj_Const (Consts_of_Ifaces is) Bool
159 , Inj_Const (Consts_of_Ifaces is) Maybe
160 , Inj_Const (Consts_of_Ifaces is) MonoFoldable
161 , Inj_Const (Consts_of_Ifaces is) IsSequence
162 , Inj_Const (Consts_of_Ifaces is) SemiSequence
163 , Proj_Con (Consts_of_Ifaces is)
164 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
166 ) => CompileI is (Proxy NonNull) where
168 :: forall meta ctx ret ls rs.
169 TokenT meta is (Proxy NonNull)
170 -> CompileT meta ctx ret is ls (Proxy NonNull ': rs)
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_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
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_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
183 check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
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_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
191 check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
192 check_type (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_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
199 check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
200 check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \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 $
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_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
216 (At Nothing (ty @Bool))
217 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
218 check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
219 check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
220 check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
223 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
225 \c -> nfilter (e2Bool c) (s c)
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_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
235 check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
236 check_fam (At (Just tok_n) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
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_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
247 check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
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
266 instance Gram_Term_AtomsT meta ts (Proxy NonNull) g