Language/Symantic/Compiling/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.Compiling.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.Parsing
  18 import Language.Symantic.Parsing.Grammar
  19 import Language.Symantic.Typing
  20 import Language.Symantic.Compiling.Term
  21 import Language.Symantic.Interpreting
  22 import Language.Symantic.Transforming.Trans
  23 import Language.Symantic.Lib.Data.Type.List hiding (Map)
  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 Consts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': Consts_imported_by MonoFunctor
  34 type instance Consts_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  ] ++ Consts_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 (Proxy @Sym_MonoFunctor) omap
  51
  52 instance
  53  ( Read_TypeNameR Type_Name cs rs
  54  , Inj_Const cs MonoFunctor
  55  ) => Read_TypeNameR Type_Name cs (Proxy MonoFunctor ': rs) where
  56         read_typenameR _cs (Type_Name "MonoFunctor") k = k (ty @MonoFunctor)
  57         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  58 instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
  59         show_const ConstZ{} = "MonoFunctor"
  60         show_const (ConstS c) = show_const c
  61
  62 -- * Type 'Fam_MonoElement'
  63 data Fam_MonoElement
  64  =   Fam_MonoElement
  65  deriving (Eq, Show)
  66 type instance Fam Fam_MonoElement '[h] = MT.Element (UnProxy h)
  67
  68 instance -- Constraint
  69  Proj_FamC cs Fam_MonoElement (c::Constraint)
  70 instance -- k -> Constraint
  71  Proj_FamC cs Fam_MonoElement (c::k -> Constraint)
  72 instance -- ()
  73  Proj_FamC cs Fam_MonoElement ()
  74 instance -- Bool
  75  Proj_FamC cs Fam_MonoElement Bool
  76 instance -- Char
  77  Proj_FamC cs Fam_MonoElement Char
  78 instance -- Int
  79  Proj_FamC cs Fam_MonoElement Int
  80 instance -- Integer
  81  Proj_FamC cs Fam_MonoElement Integer
  82 instance -- Text
  83  ( Proj_Const cs Text
  84  , Inj_Const cs (MT.Element Text)
  85  ) => Proj_FamC cs Fam_MonoElement Text where
  86         proj_famC _c _fam (TyConst c `TypesS` TypesZ)
  87          | Just Refl <- eq_skind (kind_of_const c) SKiType
  88          , Just Refl <- proj_const c (Proxy @Text)
  89          = Just (TyConst inj_const::Type cs (MT.Element Text))
  90         proj_famC _c _fam _ty = Nothing
  91 instance -- []
  92  ( Proj_Const cs []
  93  ) => Proj_FamC cs Fam_MonoElement [] where
  94         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  95          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  96          , Just Refl <- proj_const c (Proxy @[])
  97          = Just ty_a
  98         proj_famC _c _fam _ty = Nothing
  99 instance -- IO
 100  ( Proj_Const cs IO
 101  ) => Proj_FamC cs Fam_MonoElement IO where
 102         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 103          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 104          , Just Refl <- proj_const c (Proxy @IO)
 105          = Just ty_a
 106         proj_famC _c _fam _ty = Nothing
 107 instance -- IO.Handle
 108  Proj_FamC cs Fam_MonoElement IO.Handle
 109 instance -- IO.IOMode
 110  Proj_FamC cs Fam_MonoElement IO.IOMode
 111 instance -- Maybe
 112  ( Proj_Const cs Maybe
 113  ) => Proj_FamC cs Fam_MonoElement Maybe where
 114         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 115          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 116          , Just Refl <- proj_const c (Proxy @Maybe)
 117          = Just ty_a
 118         proj_famC _c _fam _ty = Nothing
 119 instance -- (->)
 120  ( Proj_Const cs (->)
 121  ) => Proj_FamC cs Fam_MonoElement (->) where
 122         proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
 123          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 124          , Just Refl <- proj_const c (Proxy @(->))
 125          = Just ty_a
 126         proj_famC _c _fam _ty = Nothing
 127 instance -- (,)
 128  ( Proj_Const cs (,)
 129  ) => Proj_FamC cs Fam_MonoElement (,) where
 130         proj_famC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
 131          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 132          , Just Refl <- proj_const c (Proxy @(,))
 133          = Just ty_b
 134         proj_famC _c _fam _ty = Nothing
 135 instance -- Either
 136  ( Proj_Const cs Either
 137  ) => Proj_FamC cs Fam_MonoElement Either where
 138         proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
 139          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 140          , Just Refl <- proj_const c (Proxy @Either)
 141          = Just ty_r
 142         proj_famC _c _fam _ty = Nothing
 143 instance -- Map
 144  ( Proj_Const cs Map
 145  ) => Proj_FamC cs Fam_MonoElement Map where
 146         proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 147          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 148          , Just Refl <- proj_const c (Proxy @Map)
 149          = Just ty_a
 150         proj_famC _c _fam _ty = Nothing
 151
 152 instance -- Proj_ConC
 153  ( Proj_Const cs MonoFunctor
 154  , Proj_Consts cs (Consts_imported_by MonoFunctor)
 155  ) => Proj_ConC cs (Proxy MonoFunctor) where
 156         proj_conC _ (TyConst q :$ typ)
 157          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 158          , Just Refl <- proj_const q (Proxy @MonoFunctor)
 159          = case typ of
 160                  TyConst c
 161                   | Just Refl <- proj_const c (Proxy @Text) -> Just Con
 162                  TyConst c :$ _a
 163                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 164                   -> case () of
 165                          _ | Just Refl <- proj_const c (Proxy @[])    -> Just Con
 166                            | Just Refl <- proj_const c (Proxy @IO)    -> Just Con
 167                            | Just Refl <- proj_const c (Proxy @Maybe) -> Just Con
 168                          _ -> Nothing
 169                  TyConst c :$ _a :$ _b
 170                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 171                   -> case () of
 172                          _ | Just Refl <- proj_const c (Proxy @(->))   -> Just Con
 173                            | Just Refl <- proj_const c (Proxy @(,))    -> Just Con
 174                            | Just Refl <- proj_const c (Proxy @Either) -> Just Con
 175                            | Just Refl <- proj_const c (Proxy @Map)    -> Just Con
 176                          _ -> Nothing
 177                  _ -> Nothing
 178         proj_conC _c _q = Nothing
 179 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
 180  = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
 181 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
 182 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
 183 instance -- CompileI
 184  ( Inj_Const (Consts_of_Ifaces is) MonoFunctor
 185  , Inj_Const (Consts_of_Ifaces is) (->)
 186  , Proj_Con  (Consts_of_Ifaces is)
 187  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 188  , Compile is
 189  ) => CompileI is (Proxy MonoFunctor) where
 190         compileI tok ctx k =
 191                 case tok of
 192                  Token_Term_MonoFunctor_omap tok_f tok_o ->
 193                         -- omap :: (Element o -> Element o) -> o -> o
 194                         compileO tok_f ctx $ \ty_f (TermO f) ->
 195                         compileO tok_o ctx $ \ty_o (TermO m) ->
 196                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
 197                         check_type
 198                          (At (Just tok_f) ty_f_a)
 199                          (At (Just tok_f) ty_f_b) $ \Refl ->
 200                         check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
 201                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 202                         check_type
 203                          (At Nothing ty_o_e)
 204                          (At (Just tok_f) ty_f_a) $ \Refl ->
 205                         k ty_o $ TermO $
 206                          \c -> omap (f c) (m c)
 207 instance -- TokenizeT
 208  Inj_Token meta ts MonoFunctor =>
 209  TokenizeT meta ts (Proxy MonoFunctor) where
 210         tokenizeT _t = mempty
 211          { tokenizers_infix = tokenizeTMod []
 212                  [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
 213                  ]
 214          }
 215 instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g