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 Consts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': Consts_imported_by MonoFunctor
  33 type instance Consts_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  ] ++ Consts_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_TypeNameR Type_Name cs rs
  53  , Inj_Const cs MonoFunctor
  54  ) => Read_TypeNameR Type_Name cs (Proxy MonoFunctor ': rs) where
  55         read_typenameR _cs (Type_Name "MonoFunctor") k = k (ty @MonoFunctor)
  56         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  57 instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
  58         show_const ConstZ{} = "MonoFunctor"
  59         show_const (ConstS c) = show_const c
  60
  61 -- * Type 'Fam_MonoElement'
  62 data Fam_MonoElement
  63  =   Fam_MonoElement
  64  deriving (Eq, Show)
  65 type instance Fam Fam_MonoElement '[h] = MT.Element (UnProxy h)
  66
  67 instance -- Constraint
  68  Proj_FamC cs Fam_MonoElement (c::Constraint)
  69 instance -- k -> Constraint
  70  Proj_FamC cs Fam_MonoElement (c::k -> Constraint)
  71 instance -- ()
  72  Proj_FamC cs Fam_MonoElement ()
  73 instance -- Bool
  74  Proj_FamC cs Fam_MonoElement Bool
  75 instance -- Char
  76  Proj_FamC cs Fam_MonoElement Char
  77 instance -- Int
  78  Proj_FamC cs Fam_MonoElement Int
  79 instance -- Integer
  80  Proj_FamC cs Fam_MonoElement Integer
  81 instance -- Text
  82  ( Proj_Const cs Text
  83  , Inj_Const cs (MT.Element Text)
  84  ) => Proj_FamC cs Fam_MonoElement Text where
  85         proj_famC _c _fam (TyConst c `TypesS` TypesZ)
  86          | Just Refl <- eq_skind (kind_of_const c) SKiType
  87          , Just Refl <- proj_const c (Proxy @Text)
  88          = Just (TyConst inj_const::Type cs (MT.Element Text))
  89         proj_famC _c _fam _ty = Nothing
  90 instance -- []
  91  ( Proj_Const cs []
  92  ) => Proj_FamC cs Fam_MonoElement [] where
  93         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  94          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  95          , Just Refl <- proj_const c (Proxy @[])
  96          = Just ty_a
  97         proj_famC _c _fam _ty = Nothing
  98 instance -- IO
  99  ( Proj_Const cs IO
 100  ) => Proj_FamC cs Fam_MonoElement IO where
 101         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 102          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 103          , Just Refl <- proj_const c (Proxy @IO)
 104          = Just ty_a
 105         proj_famC _c _fam _ty = Nothing
 106 instance -- IO.Handle
 107  Proj_FamC cs Fam_MonoElement IO.Handle
 108 instance -- IO.IOMode
 109  Proj_FamC cs Fam_MonoElement IO.IOMode
 110 instance -- Maybe
 111  ( Proj_Const cs Maybe
 112  ) => Proj_FamC cs Fam_MonoElement Maybe where
 113         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 114          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 115          , Just Refl <- proj_const c (Proxy @Maybe)
 116          = Just ty_a
 117         proj_famC _c _fam _ty = Nothing
 118 instance -- (->)
 119  ( Proj_Const cs (->)
 120  ) => Proj_FamC cs Fam_MonoElement (->) where
 121         proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
 122          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 123          , Just Refl <- proj_const c (Proxy @(->))
 124          = Just ty_a
 125         proj_famC _c _fam _ty = Nothing
 126 instance -- (,)
 127  ( Proj_Const cs (,)
 128  ) => Proj_FamC cs Fam_MonoElement (,) where
 129         proj_famC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
 130          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 131          , Just Refl <- proj_const c (Proxy @(,))
 132          = Just ty_b
 133         proj_famC _c _fam _ty = Nothing
 134 instance -- Either
 135  ( Proj_Const cs Either
 136  ) => Proj_FamC cs Fam_MonoElement Either where
 137         proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
 138          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 139          , Just Refl <- proj_const c (Proxy @Either)
 140          = Just ty_r
 141         proj_famC _c _fam _ty = Nothing
 142 instance -- Map
 143  ( Proj_Const cs Map
 144  ) => Proj_FamC cs Fam_MonoElement Map where
 145         proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 146          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 147          , Just Refl <- proj_const c (Proxy @Map)
 148          = Just ty_a
 149         proj_famC _c _fam _ty = Nothing
 150
 151 instance -- Proj_ConC
 152  ( Proj_Const cs MonoFunctor
 153  , Proj_Consts cs (Consts_imported_by MonoFunctor)
 154  ) => Proj_ConC cs (Proxy MonoFunctor) where
 155         proj_conC _ (TyConst q :$ typ)
 156          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 157          , Just Refl <- proj_const q (Proxy @MonoFunctor)
 158          = case typ of
 159                  TyConst c
 160                   | Just Refl <- proj_const c (Proxy @Text) -> Just Con
 161                  TyConst c :$ _a
 162                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 163                   -> case () of
 164                          _ | Just Refl <- proj_const c (Proxy @[])    -> Just Con
 165                            | Just Refl <- proj_const c (Proxy @IO)    -> Just Con
 166                            | Just Refl <- proj_const c (Proxy @Maybe) -> Just Con
 167                          _ -> Nothing
 168                  TyConst c :$ _a :$ _b
 169                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 170                   -> case () of
 171                          _ | Just Refl <- proj_const c (Proxy @(->))   -> Just Con
 172                            | Just Refl <- proj_const c (Proxy @(,))    -> Just Con
 173                            | Just Refl <- proj_const c (Proxy @Either) -> Just Con
 174                            | Just Refl <- proj_const c (Proxy @Map)    -> Just Con
 175                          _ -> Nothing
 176                  _ -> Nothing
 177         proj_conC _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_Const (Consts_of_Ifaces is) MonoFunctor
 184  , Inj_Const (Consts_of_Ifaces is) (->)
 185  , Proj_Con  (Consts_of_Ifaces is)
 186  , Proj_Fam  (Consts_of_Ifaces is) Fam_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_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
 196                         check_type
 197                          (At (Just tok_f) ty_f_a)
 198                          (At (Just tok_f) ty_f_b) $ \Refl ->
 199                         check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
 200                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 201                         check_type
 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