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.Ratio (Ratio)
  14 import Data.Type.Equality ((:~:)(Refl))
  15 import GHC.Exts (Constraint)
  16 import qualified System.IO as IO
  17
  18 import Language.Symantic.Helper.Data.Type.List hiding (Map)
  19 import Language.Symantic.Parsing
  20 import Language.Symantic.Typing
  21 import Language.Symantic.Compiling
  22 import Language.Symantic.Interpreting
  23 import Language.Symantic.Transforming
  24
  25 -- * Class 'Sym_MonoFunctor'
  26 class Sym_MonoFunctor term where
  27         omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
  28         default omap :: (Trans t term, MonoFunctor o)
  29          => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
  30         omap = trans_map2 omap
  31
  32 type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
  33 type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by MonoFunctor
  34 type instance TyConsts_imported_by MonoFunctor =
  35  [ Proxy (->)
  36  , Proxy (,)
  37  , Proxy []
  38  , Proxy Either
  39  , Proxy IO
  40  , Proxy Map
  41  , Proxy Maybe
  42  , Proxy Text
  43  ] ++ TyConsts_imported_by IO
  44
  45 instance Sym_MonoFunctor HostI where
  46         omap = liftM2 MT.omap
  47 instance Sym_MonoFunctor TextI where
  48         omap = textI2 "omap"
  49 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
  50         omap = dupI2 @Sym_MonoFunctor omap
  51
  52 instance
  53  ( Read_TyNameR TyName cs rs
  54  , Inj_TyConst cs MonoFunctor
  55  ) => Read_TyNameR TyName cs (Proxy MonoFunctor ': rs) where
  56         read_TyNameR _cs (TyName "MonoFunctor") k = k (ty @MonoFunctor)
  57         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  58 instance Show_TyConst cs => Show_TyConst (Proxy MonoFunctor ': cs) where
  59         show_TyConst TyConstZ{} = "MonoFunctor"
  60         show_TyConst (TyConstS c) = show_TyConst c
  61
  62 -- * Type 'TyFam_MonoElement'
  63 data TyFam_MonoElement
  64  =   TyFam_MonoElement
  65  deriving (Eq, Show)
  66 type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
  67
  68 instance -- Constraint
  69  Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
  70 instance -- k -> Constraint
  71  Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
  72 instance -- (->)
  73  ( Proj_TyConst cs (->)
  74  ) => Proj_TyFamC cs TyFam_MonoElement (->) where
  75         proj_TyFamC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
  76          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  77          , Just Refl <- proj_TyConst c (Proxy @(->))
  78          = Just ty_a
  79         proj_TyFamC _c _fam _ty = Nothing
  80 instance -- []
  81  ( Proj_TyConst cs []
  82  ) => Proj_TyFamC cs TyFam_MonoElement [] where
  83         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  84          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
  85          , Just Refl <- proj_TyConst c (Proxy @[])
  86          = Just ty_a
  87         proj_TyFamC _c _fam _ty = Nothing
  88 instance -- ()
  89  Proj_TyFamC cs TyFam_MonoElement ()
  90 instance -- (,)
  91  ( Proj_TyConst cs (,)
  92  ) => Proj_TyFamC cs TyFam_MonoElement (,) where
  93         proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
  94          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  95          , Just Refl <- proj_TyConst c (Proxy @(,))
  96          = Just ty_b
  97         proj_TyFamC _c _fam _ty = Nothing
  98 instance -- Bool
  99  Proj_TyFamC cs TyFam_MonoElement Bool
 100 instance -- Char
 101  Proj_TyFamC cs TyFam_MonoElement Char
 102 instance -- Either
 103  ( Proj_TyConst cs Either
 104  ) => Proj_TyFamC cs TyFam_MonoElement Either where
 105         proj_TyFamC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
 106          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 107          , Just Refl <- proj_TyConst c (Proxy @Either)
 108          = Just ty_r
 109         proj_TyFamC _c _fam _ty = Nothing
 110 instance -- Int
 111  Proj_TyFamC cs TyFam_MonoElement Int
 112 instance -- Integer
 113  Proj_TyFamC cs TyFam_MonoElement Integer
 114 instance -- IO
 115  ( Proj_TyConst cs IO
 116  ) => Proj_TyFamC cs TyFam_MonoElement IO where
 117         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 118          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 119          , Just Refl <- proj_TyConst c (Proxy @IO)
 120          = Just ty_a
 121         proj_TyFamC _c _fam _ty = Nothing
 122 instance -- IO.Handle
 123  Proj_TyFamC cs TyFam_MonoElement IO.Handle
 124 instance -- IO.IOMode
 125  Proj_TyFamC cs TyFam_MonoElement IO.IOMode
 126 instance -- Map
 127  ( Proj_TyConst cs Map
 128  ) => Proj_TyFamC cs TyFam_MonoElement Map where
 129         proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 130          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 131          , Just Refl <- proj_TyConst c (Proxy @Map)
 132          = Just ty_a
 133         proj_TyFamC _c _fam _ty = Nothing
 134 instance -- Maybe
 135  ( Proj_TyConst cs Maybe
 136  ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
 137         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 138          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 139          , Just Refl <- proj_TyConst c (Proxy @Maybe)
 140          = Just ty_a
 141         proj_TyFamC _c _fam _ty = Nothing
 142 instance -- Ordering
 143  Proj_TyFamC cs TyFam_MonoElement Ordering
 144 instance -- Ratio
 145  Proj_TyFamC cs TyFam_MonoElement Ratio
 146 instance -- Text
 147  ( Proj_TyConst cs Text
 148  , Inj_TyConst cs (MT.Element Text)
 149  ) => Proj_TyFamC cs TyFam_MonoElement Text where
 150         proj_TyFamC _c _fam (TyConst c `TypesS` TypesZ)
 151          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
 152          , Just Refl <- proj_TyConst c (Proxy @Text)
 153          = Just (TyConst inj_TyConst::Type cs (MT.Element Text))
 154         proj_TyFamC _c _fam _ty = Nothing
 155
 156 instance -- Proj_TyConC
 157  ( Proj_TyConst cs MonoFunctor
 158  , Proj_TyConsts cs (TyConsts_imported_by MonoFunctor)
 159  ) => Proj_TyConC cs (Proxy MonoFunctor) where
 160         proj_TyConC _ (TyConst q :$ typ)
 161          | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
 162          , Just Refl <- proj_TyConst q (Proxy @MonoFunctor)
 163          = case typ of
 164                  TyConst c
 165                   | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
 166                  TyConst c :$ _a
 167                   | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 168                   -> case () of
 169                          _ | Just Refl <- proj_TyConst c (Proxy @[])    -> Just TyCon
 170                            | Just Refl <- proj_TyConst c (Proxy @IO)    -> Just TyCon
 171                            | Just Refl <- proj_TyConst c (Proxy @Maybe) -> Just TyCon
 172                          _ -> Nothing
 173                  TyConst c :$ _a :$ _b
 174                   | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 175                   -> case () of
 176                          _ | Just Refl <- proj_TyConst c (Proxy @(->))   -> Just TyCon
 177                            | Just Refl <- proj_TyConst c (Proxy @(,))    -> Just TyCon
 178                            | Just Refl <- proj_TyConst c (Proxy @Either) -> Just TyCon
 179                            | Just Refl <- proj_TyConst c (Proxy @Map)    -> Just TyCon
 180                          _ -> Nothing
 181                  _ -> Nothing
 182         proj_TyConC _c _q = Nothing
 183 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
 184  = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
 185 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
 186 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
 187 instance -- CompileI
 188  ( Inj_TyConst cs MonoFunctor
 189  , Inj_TyConst cs (->)
 190  , Proj_TyCon  cs
 191  , Proj_TyFam  cs TyFam_MonoElement
 192  , Compile cs is
 193  ) => CompileI cs is (Proxy MonoFunctor) where
 194         compileI tok ctx k =
 195                 case tok of
 196                  Token_Term_MonoFunctor_omap tok_f tok_o ->
 197                         -- omap :: (Element o -> Element o) -> o -> o
 198                         compileO tok_f ctx $ \ty_f (TermO f) ->
 199                         compileO tok_o ctx $ \ty_o (TermO m) ->
 200                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
 201                         check_TyEq
 202                          (At (Just tok_f) ty_f_a)
 203                          (At (Just tok_f) ty_f_b) $ \Refl ->
 204                         check_TyCon (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \TyCon ->
 205                         check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 206                         check_TyEq
 207                          (At Nothing ty_o_e)
 208                          (At (Just tok_f) ty_f_a) $ \Refl ->
 209                         k ty_o $ TermO $
 210                          \c -> omap (f c) (m c)
 211 instance -- TokenizeT
 212  Inj_Token meta ts MonoFunctor =>
 213  TokenizeT meta ts (Proxy MonoFunctor) where
 214         tokenizeT _t = mempty
 215          { tokenizers_infix = tokenizeTMod []
 216                  [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
 217                  ]
 218          }
 219 instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g