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.Typing
  19 import Language.Symantic.Compiling.Term
  20 import Language.Symantic.Interpreting
  21 import Language.Symantic.Transforming.Trans
  22 import Language.Symantic.Lib.Data.Type.List hiding (Map)
  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 Text cs rs
  53  , Inj_Const cs MonoFunctor
  54  ) => Read_TypeNameR Text cs (Proxy MonoFunctor ': rs) where
  55         read_typenameR _cs "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 -- Text
  78  ( Proj_Const cs Text
  79  , Inj_Const cs (MT.Element Text)
  80  ) => Proj_FamC cs Fam_MonoElement Text where
  81         proj_famC _c _fam (TyConst c `TypesS` TypesZ)
  82          | Just Refl <- eq_skind (kind_of_const c) SKiType
  83          , Just Refl <- proj_const c (Proxy::Proxy Text)
  84          = Just (TyConst inj_const::Type cs (MT.Element Text))
  85         proj_famC _c _fam _ty = Nothing
  86 instance -- []
  87  ( Proj_Const cs []
  88  ) => Proj_FamC cs Fam_MonoElement [] where
  89         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  90          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  91          , Just Refl <- proj_const c (Proxy::Proxy [])
  92          = Just ty_a
  93         proj_famC _c _fam _ty = Nothing
  94 instance -- IO
  95  ( Proj_Const cs IO
  96  ) => Proj_FamC cs Fam_MonoElement IO where
  97         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  98          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  99          , Just Refl <- proj_const c (Proxy::Proxy IO)
 100          = Just ty_a
 101         proj_famC _c _fam _ty = Nothing
 102 instance -- IO.Handle
 103  Proj_FamC cs Fam_MonoElement IO.Handle
 104 instance -- IO.IOMode
 105  Proj_FamC cs Fam_MonoElement IO.IOMode
 106 instance -- Maybe
 107  ( Proj_Const cs Maybe
 108  ) => Proj_FamC cs Fam_MonoElement Maybe where
 109         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 110          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 111          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
 112          = Just ty_a
 113         proj_famC _c _fam _ty = Nothing
 114 instance -- (->)
 115  ( Proj_Const cs (->)
 116  ) => Proj_FamC cs Fam_MonoElement (->) where
 117         proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
 118          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 119          , Just Refl <- proj_const c (Proxy::Proxy (->))
 120          = Just ty_a
 121         proj_famC _c _fam _ty = Nothing
 122 instance -- (,)
 123  ( Proj_Const cs (,)
 124  ) => Proj_FamC cs Fam_MonoElement (,) where
 125         proj_famC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
 126          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 127          , Just Refl <- proj_const c (Proxy::Proxy (,))
 128          = Just ty_b
 129         proj_famC _c _fam _ty = Nothing
 130 instance -- Either
 131  ( Proj_Const cs Either
 132  ) => Proj_FamC cs Fam_MonoElement Either where
 133         proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
 134          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 135          , Just Refl <- proj_const c (Proxy::Proxy Either)
 136          = Just ty_r
 137         proj_famC _c _fam _ty = Nothing
 138 instance -- Map
 139  ( Proj_Const cs Map
 140  ) => Proj_FamC cs Fam_MonoElement Map where
 141         proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 142          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 143          , Just Refl <- proj_const c (Proxy::Proxy Map)
 144          = Just ty_a
 145         proj_famC _c _fam _ty = Nothing
 146
 147 instance -- Proj_ConC
 148  ( Proj_Const cs MonoFunctor
 149  , Proj_Consts cs (Consts_imported_by MonoFunctor)
 150  ) => Proj_ConC cs (Proxy MonoFunctor) where
 151         proj_conC _ (TyConst q :$ typ)
 152          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 153          , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
 154          = case typ of
 155                  TyConst c
 156                   | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 157                  TyConst c :$ _a
 158                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 159                   -> case () of
 160                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 161                            | Just Refl <- proj_const c (Proxy::Proxy IO)    -> Just Con
 162                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 163                          _ -> Nothing
 164                  TyConst c :$ _a :$ _b
 165                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 166                   -> case () of
 167                          _ | Just Refl <- proj_const c (Proxy::Proxy (->))   -> Just Con
 168                            | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 169                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 170                            | Just Refl <- proj_const c (Proxy::Proxy Map)    -> Just Con
 171                          _ -> Nothing
 172                  _ -> Nothing
 173         proj_conC _c _q = Nothing
 174 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
 175  = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
 176 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
 177 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
 178 instance -- CompileI
 179  ( Inj_Const (Consts_of_Ifaces is) MonoFunctor
 180  , Inj_Const (Consts_of_Ifaces is) (->)
 181  , Proj_Con  (Consts_of_Ifaces is)
 182  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 183  , Compile is
 184  ) => CompileI is (Proxy MonoFunctor) where
 185         compileI tok ctx k =
 186                 case tok of
 187                  Token_Term_MonoFunctor_omap tok_f tok_o ->
 188                         -- omap :: (Element o -> Element o) -> o -> o
 189                         compileO tok_f ctx $ \ty_f (TermO f) ->
 190                         compileO tok_o ctx $ \ty_o (TermO m) ->
 191                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
 192                         check_type
 193                          (At (Just tok_f) ty_f_a)
 194                          (At (Just tok_f) ty_f_b) $ \Refl ->
 195                         check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
 196                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 197                         check_type
 198                          (At Nothing ty_o_e)
 199                          (At (Just tok_f) ty_f_a) $ \Refl ->
 200                         k ty_o $ TermO $
 201                          \c -> omap (f c) (m c)