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