symantic-lib/Language/Symantic/Lib/MonoFunctor.hs

   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
   6
   7 import Control.Monad (liftM2)
   8 import Data.Map.Strict (Map)
   9 import Data.MonoTraversable (MonoFunctor)
  10 import qualified Data.MonoTraversable as MT
  11 import Data.Proxy
  12 import Data.Text (Text)
  13 import Data.Type.Equality ((:~:)(Refl))
  14 import GHC.Exts (Constraint)
  15 import qualified System.IO as IO
  16
  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
  23
  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
  30
  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 =
  34  [ Proxy (->)
  35  , Proxy (,)
  36  , Proxy []
  37  , Proxy Either
  38  , Proxy IO
  39  , Proxy Map
  40  , Proxy Maybe
  41  , Proxy Text
  42  ] ++ TyConsts_imported_by IO
  43
  44 instance Sym_MonoFunctor HostI where
  45         omap = liftM2 MT.omap
  46 instance Sym_MonoFunctor TextI where
  47         omap = textI2 "omap"
  48 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
  49         omap = dupI2 (Proxy @Sym_MonoFunctor) omap
  50
  51 instance
  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
  60
  61 -- * Type 'TyFam_MonoElement'
  62 data TyFam_MonoElement
  63  =   TyFam_MonoElement
  64  deriving (Eq, Show)
  65 type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
  66
  67 instance -- Constraint
  68  Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
  69 instance -- k -> Constraint
  70  Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
  71 instance -- ()
  72  Proj_TyFamC cs TyFam_MonoElement ()
  73 instance -- Bool
  74  Proj_TyFamC cs TyFam_MonoElement Bool
  75 instance -- Char
  76  Proj_TyFamC cs TyFam_MonoElement Char
  77 instance -- Int
  78  Proj_TyFamC cs TyFam_MonoElement Int
  79 instance -- Integer
  80  Proj_TyFamC cs TyFam_MonoElement Integer
  81 instance -- Text
  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
  90 instance -- []
  91  ( Proj_TyConst cs []
  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 @[])
  96          = Just ty_a
  97         proj_TyFamC _c _fam _ty = Nothing
  98 instance -- IO
  99  ( Proj_TyConst cs IO
 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)
 104          = Just ty_a
 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
 110 instance -- Maybe
 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)
 116          = Just ty_a
 117         proj_TyFamC _c _fam _ty = Nothing
 118 instance -- (->)
 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 @(->))
 124          = Just ty_a
 125         proj_TyFamC _c _fam _ty = Nothing
 126 instance -- (,)
 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 @(,))
 132          = Just ty_b
 133         proj_TyFamC _c _fam _ty = Nothing
 134 instance -- Either
 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)
 140          = Just ty_r
 141         proj_TyFamC _c _fam _ty = Nothing
 142 instance -- Map
 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)
 148          = Just ty_a
 149         proj_TyFamC _c _fam _ty = Nothing
 150
 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)
 158          = case typ of
 159                  TyConst c
 160                   | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
 161                  TyConst c :$ _a
 162                   | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 163                   -> case () of
 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
 167                          _ -> Nothing
 168                  TyConst c :$ _a :$ _b
 169                   | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 170                   -> case () of
 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
 175                          _ -> Nothing
 176                  _ -> Nothing
 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))
 182 instance -- CompileI
 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
 187  , Compile is
 188  ) => CompileI is (Proxy MonoFunctor) where
 189         compileI tok ctx k =
 190                 case tok of
 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 ->
 196                         check_TyEq
 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 ->
 201                         check_TyEq
 202                          (At Nothing ty_o_e)
 203                          (At (Just tok_f) ty_f_a) $ \Refl ->
 204                         k ty_o $ TermO $
 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
 212                  ]
 213          }
 214 instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g