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 = textI_app2 "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 Const_from Text cs => Const_from Text (Proxy MonoFunctor ': cs) where
  52         const_from "MonoFunctor" k = k (ConstZ kind)
  53         const_from s k = const_from s $ k . ConstS
  54 instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
  55         show_const ConstZ{} = "MonoFunctor"
  56         show_const (ConstS c) = show_const c
  57
  58 -- * Type 'Fam_MonoElement'
  59 data Fam_MonoElement
  60  =   Fam_MonoElement
  61  deriving (Eq, Show)
  62 type instance Fam Fam_MonoElement '[h] = MT.Element (UnProxy h)
  63
  64 instance -- Constraint
  65  Proj_FamC cs Fam_MonoElement (c::Constraint)
  66 instance -- k -> Constraint
  67  Proj_FamC cs Fam_MonoElement (c::k -> Constraint)
  68 instance -- ()
  69  Proj_FamC cs Fam_MonoElement ()
  70 instance -- Bool
  71  Proj_FamC cs Fam_MonoElement Bool
  72 instance -- Char
  73  Proj_FamC cs Fam_MonoElement Char
  74 instance -- Text
  75  ( Proj_Const cs Text
  76  , Inj_Const cs (MT.Element Text)
  77  ) => Proj_FamC cs Fam_MonoElement Text where
  78         proj_famC _c _fam (TyConst c `TypesS` TypesZ)
  79          | Just Refl <- eq_skind (kind_of_const c) SKiType
  80          , Just Refl <- proj_const c (Proxy::Proxy Text)
  81          = Just (TyConst inj_const::Type cs (MT.Element Text))
  82         proj_famC _c _fam _ty = Nothing
  83 instance -- []
  84  ( Proj_Const cs []
  85  ) => Proj_FamC cs Fam_MonoElement [] where
  86         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
  87          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  88          , Just Refl <- proj_const c (Proxy::Proxy [])
  89          = Just ty_a
  90         proj_famC _c _fam _ty = Nothing
  91 instance -- IO
  92  ( Proj_Const cs IO
  93  ) => Proj_FamC cs Fam_MonoElement IO 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::Proxy IO)
  97          = Just ty_a
  98         proj_famC _c _fam _ty = Nothing
  99 instance -- IO.Handle
 100  Proj_FamC cs Fam_MonoElement IO.Handle
 101 instance -- IO.IOMode
 102  Proj_FamC cs Fam_MonoElement IO.IOMode
 103 instance -- Maybe
 104  ( Proj_Const cs Maybe
 105  ) => Proj_FamC cs Fam_MonoElement Maybe where
 106         proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 107          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 108          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
 109          = Just ty_a
 110         proj_famC _c _fam _ty = Nothing
 111 instance -- (->)
 112  ( Proj_Const cs (->)
 113  ) => Proj_FamC cs Fam_MonoElement (->) where
 114         proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
 115          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 116          , Just Refl <- proj_const c (Proxy::Proxy (->))
 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_a :$ ty_b) `TypesS` TypesZ)
 123          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 124          , Just Refl <- proj_const c (Proxy::Proxy (,))
 125          = Just ty_b
 126         proj_famC _c _fam _ty = Nothing
 127 instance -- Either
 128  ( Proj_Const cs Either
 129  ) => Proj_FamC cs Fam_MonoElement Either where
 130         proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
 131          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 132          , Just Refl <- proj_const c (Proxy::Proxy Either)
 133          = Just ty_r
 134         proj_famC _c _fam _ty = Nothing
 135 instance -- Map
 136  ( Proj_Const cs Map
 137  ) => Proj_FamC cs Fam_MonoElement Map where
 138         proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 139          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 140          , Just Refl <- proj_const c (Proxy::Proxy Map)
 141          = Just ty_a
 142         proj_famC _c _fam _ty = Nothing
 143
 144 instance -- Proj_ConC
 145  ( Proj_Const cs MonoFunctor
 146  , Proj_Consts cs (Consts_imported_by MonoFunctor)
 147  ) => Proj_ConC cs (Proxy MonoFunctor) where
 148         proj_conC _ (TyConst q :$ typ)
 149          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 150          , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
 151          = case typ of
 152                  TyConst c
 153                   | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 154                  TyConst c :$ _a
 155                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 156                   -> case () of
 157                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 158                            | Just Refl <- proj_const c (Proxy::Proxy IO)    -> Just Con
 159                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 160                          _ -> Nothing
 161                  TyConst c :$ _a :$ _b
 162                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 163                   -> case () of
 164                          _ | Just Refl <- proj_const c (Proxy::Proxy (->))   -> Just Con
 165                            | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 166                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 167                            | Just Refl <- proj_const c (Proxy::Proxy Map)    -> Just Con
 168                          _ -> Nothing
 169                  _ -> Nothing
 170         proj_conC _c _q = Nothing
 171 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
 172  = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
 173 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
 174 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
 175 instance -- CompileI
 176  ( Inj_Const (Consts_of_Ifaces is) MonoFunctor
 177  , Inj_Const (Consts_of_Ifaces is) (->)
 178  , Proj_Con  (Consts_of_Ifaces is)
 179  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 180  , Compile is
 181  ) => CompileI is (Proxy MonoFunctor) where
 182         compileI tok ctx k =
 183                 case tok of
 184                  Token_Term_MonoFunctor_omap tok_f tok_o ->
 185                         -- omap :: (Element o -> Element o) -> o -> o
 186                         compileO tok_f ctx $ \ty_f (TermO f) ->
 187                         compileO tok_o ctx $ \ty_o (TermO m) ->
 188                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
 189                         check_type
 190                          (At (Just tok_f) ty_f_a)
 191                          (At (Just tok_f) ty_f_b) $ \Refl ->
 192                         check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
 193                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 194                         check_type
 195                          (At Nothing ty_o_e)
 196                          (At (Just tok_f) ty_f_a) $ \Refl ->
 197                         k ty_o $ TermO $
 198                          \c -> omap (f c) (m c)