1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
4 -- | Symantic for 'MonoFunctor'.
5 module Language.Symantic.Lib.MonoFunctor where
7 import Control.Monad (liftM2)
8 import Data.Map.Strict (Map)
9 import Data.MonoTraversable (MonoFunctor)
10 import qualified Data.MonoTraversable as MT
12 import Data.Text (Text)
13 import Data.Type.Equality ((:~:)(Refl))
14 import GHC.Exts (Constraint)
15 import qualified System.IO as IO
17 import Language.Symantic.Helper.Data.Type.List hiding (Map)
18 import Language.Symantic.Parsing
19 import Language.Symantic.Typing
20 import Language.Symantic.Compiling
21 import Language.Symantic.Interpreting
22 import Language.Symantic.Transforming
24 -- * Class 'Sym_MonoFunctor'
25 class Sym_MonoFunctor term where
26 omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
27 default omap :: (Trans t term, MonoFunctor o)
28 => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
29 omap = trans_map2 omap
31 type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
32 type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by MonoFunctor
33 type instance TyConsts_imported_by MonoFunctor =
42 ] ++ TyConsts_imported_by IO
44 instance Sym_MonoFunctor HostI where
46 instance Sym_MonoFunctor TextI where
48 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
49 omap = dupI2 @Sym_MonoFunctor omap
52 ( Read_TyNameR TyName cs rs
53 , Inj_TyConst cs MonoFunctor
54 ) => Read_TyNameR TyName cs (Proxy MonoFunctor ': rs) where
55 read_TyNameR _cs (TyName "MonoFunctor") k = k (ty @MonoFunctor)
56 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
57 instance Show_TyConst cs => Show_TyConst (Proxy MonoFunctor ': cs) where
58 show_TyConst TyConstZ{} = "MonoFunctor"
59 show_TyConst (TyConstS c) = show_TyConst c
61 -- * Type 'TyFam_MonoElement'
62 data TyFam_MonoElement
65 type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
67 instance -- Constraint
68 Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
69 instance -- k -> Constraint
70 Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
72 Proj_TyFamC cs TyFam_MonoElement ()
74 Proj_TyFamC cs TyFam_MonoElement Bool
76 Proj_TyFamC cs TyFam_MonoElement Char
78 Proj_TyFamC cs TyFam_MonoElement Int
80 Proj_TyFamC cs TyFam_MonoElement Integer
82 ( Proj_TyConst cs Text
83 , Inj_TyConst cs (MT.Element Text)
84 ) => Proj_TyFamC cs TyFam_MonoElement Text where
85 proj_TyFamC _c _fam (TyConst c `TypesS` TypesZ)
86 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
87 , Just Refl <- proj_TyConst c (Proxy @Text)
88 = Just (TyConst inj_TyConst::Type cs (MT.Element Text))
89 proj_TyFamC _c _fam _ty = Nothing
92 ) => Proj_TyFamC cs TyFam_MonoElement [] where
93 proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
94 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
95 , Just Refl <- proj_TyConst c (Proxy @[])
97 proj_TyFamC _c _fam _ty = Nothing
100 ) => Proj_TyFamC cs TyFam_MonoElement IO where
101 proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
102 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
103 , Just Refl <- proj_TyConst c (Proxy @IO)
105 proj_TyFamC _c _fam _ty = Nothing
106 instance -- IO.Handle
107 Proj_TyFamC cs TyFam_MonoElement IO.Handle
108 instance -- IO.IOMode
109 Proj_TyFamC cs TyFam_MonoElement IO.IOMode
111 ( Proj_TyConst cs Maybe
112 ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
113 proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
114 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
115 , Just Refl <- proj_TyConst c (Proxy @Maybe)
117 proj_TyFamC _c _fam _ty = Nothing
119 ( Proj_TyConst cs (->)
120 ) => Proj_TyFamC cs TyFam_MonoElement (->) where
121 proj_TyFamC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
122 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
123 , Just Refl <- proj_TyConst c (Proxy @(->))
125 proj_TyFamC _c _fam _ty = Nothing
127 ( Proj_TyConst cs (,)
128 ) => Proj_TyFamC cs TyFam_MonoElement (,) where
129 proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
130 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
131 , Just Refl <- proj_TyConst c (Proxy @(,))
133 proj_TyFamC _c _fam _ty = Nothing
135 ( Proj_TyConst cs Either
136 ) => Proj_TyFamC cs TyFam_MonoElement Either where
137 proj_TyFamC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
138 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
139 , Just Refl <- proj_TyConst c (Proxy @Either)
141 proj_TyFamC _c _fam _ty = Nothing
143 ( Proj_TyConst cs Map
144 ) => Proj_TyFamC cs TyFam_MonoElement Map where
145 proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
146 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
147 , Just Refl <- proj_TyConst c (Proxy @Map)
149 proj_TyFamC _c _fam _ty = Nothing
151 instance -- Proj_TyConC
152 ( Proj_TyConst cs MonoFunctor
153 , Proj_TyConsts cs (TyConsts_imported_by MonoFunctor)
154 ) => Proj_TyConC cs (Proxy MonoFunctor) where
155 proj_TyConC _ (TyConst q :$ typ)
156 | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
157 , Just Refl <- proj_TyConst q (Proxy @MonoFunctor)
160 | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
162 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
164 _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
165 | Just Refl <- proj_TyConst c (Proxy @IO) -> Just TyCon
166 | Just Refl <- proj_TyConst c (Proxy @Maybe) -> Just TyCon
168 TyConst c :$ _a :$ _b
169 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
171 _ | Just Refl <- proj_TyConst c (Proxy @(->)) -> Just TyCon
172 | Just Refl <- proj_TyConst c (Proxy @(,)) -> Just TyCon
173 | Just Refl <- proj_TyConst c (Proxy @Either) -> Just TyCon
174 | Just Refl <- proj_TyConst c (Proxy @Map) -> Just TyCon
177 proj_TyConC _c _q = Nothing
178 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
179 = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
180 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
181 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
183 ( Inj_TyConst (TyConsts_of_Ifaces is) MonoFunctor
184 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
185 , Proj_TyCon (TyConsts_of_Ifaces is)
186 , Proj_TyFam (TyConsts_of_Ifaces is) TyFam_MonoElement
188 ) => CompileI is (Proxy MonoFunctor) where
191 Token_Term_MonoFunctor_omap tok_f tok_o ->
192 -- omap :: (Element o -> Element o) -> o -> o
193 compileO tok_f ctx $ \ty_f (TermO f) ->
194 compileO tok_o ctx $ \ty_o (TermO m) ->
195 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
197 (At (Just tok_f) ty_f_a)
198 (At (Just tok_f) ty_f_b) $ \Refl ->
199 check_TyCon (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \TyCon ->
200 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
203 (At (Just tok_f) ty_f_a) $ \Refl ->
205 \c -> omap (f c) (m c)
206 instance -- TokenizeT
207 Inj_Token meta ts MonoFunctor =>
208 TokenizeT meta ts (Proxy MonoFunctor) where
209 tokenizeT _t = mempty
210 { tokenizers_infix = tokenizeTMod []
211 [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
214 instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g