Language/Symantic/Compiling/MonoFoldable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
   4 -- | Symantic for 'MonoFoldable'.
   5 module Language.Symantic.Compiling.MonoFoldable where
   6
   7 import Control.Monad (liftM, liftM2, liftM3)
   8 import Data.MonoTraversable (MonoFoldable)
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Compiling.MonoFunctor
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20
  21 -- * Class 'Sym_MonoFoldable'
  22 class Sym_MonoFunctor term => Sym_MonoFoldable term where
  23         ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
  24         ofoldr :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
  25         ofoldl' :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
  26         olength :: MonoFoldable o => term o -> term Int
  27         onull :: MonoFoldable o => term o -> term Bool
  28         oall :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  29         oany :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  30         otoList :: MonoFoldable o => term o -> term [MT.Element o]
  31         default ofoldMap :: (Trans t term, MonoFoldable o, Monoid m)
  32          => t term (MT.Element o -> m) -> t term o -> t term m
  33         default ofoldr :: (Trans t term, MonoFoldable o)
  34          => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
  35         default ofoldl' :: (Trans t term, MonoFoldable o)
  36          => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
  37         default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
  38         default onull :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
  39         default oall :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  40         default oany :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  41         default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
  42         ofoldMap = trans_map2 ofoldMap
  43         ofoldr   = trans_map3 ofoldr
  44         ofoldl'  = trans_map3 ofoldl'
  45         olength  = trans_map1 olength
  46         onull    = trans_map1 onull
  47         oall     = trans_map2 oall
  48         oany     = trans_map2 oany
  49         otoList  = trans_map1 otoList
  50
  51 type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
  52 type instance Consts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': Consts_imported_by MonoFoldable
  53 type instance Consts_imported_by MonoFoldable =
  54  [ Proxy (->)
  55  , Proxy (,)
  56  , Proxy []
  57  , Proxy Bool
  58  , Proxy Either
  59  , Proxy Int
  60  , Proxy Maybe
  61  , Proxy Monoid
  62  , Proxy Text
  63  ]
  64
  65 instance Sym_MonoFoldable HostI where
  66         ofoldMap = liftM2 MT.ofoldMap
  67         ofoldr   = liftM3 MT.ofoldr
  68         ofoldl'  = liftM3 MT.ofoldl'
  69         olength  = liftM  MT.olength
  70         onull    = liftM  MT.onull
  71         oall     = liftM2 MT.oall
  72         oany     = liftM2 MT.oany
  73         otoList  = liftM  MT.otoList
  74 instance Sym_MonoFoldable TextI where
  75         ofoldMap = textI2 "ofoldMap"
  76         ofoldr   = textI3 "ofoldr"
  77         ofoldl'  = textI3 "ofoldl'"
  78         olength  = textI1 "olength"
  79         onull    = textI1 "onull"
  80         oall     = textI2 "oall"
  81         oany     = textI2 "oany"
  82         otoList  = textI1 "otoList"
  83 instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
  84         ofoldMap = dupI2 (Proxy @Sym_MonoFoldable) ofoldMap
  85         ofoldr   = dupI3 (Proxy @Sym_MonoFoldable) ofoldr
  86         ofoldl'  = dupI3 (Proxy @Sym_MonoFoldable) ofoldl'
  87         olength  = dupI1 (Proxy @Sym_MonoFoldable) olength
  88         onull    = dupI1 (Proxy @Sym_MonoFoldable) onull
  89         oall     = dupI2 (Proxy @Sym_MonoFoldable) oall
  90         oany     = dupI2 (Proxy @Sym_MonoFoldable) oany
  91         otoList  = dupI1 (Proxy @Sym_MonoFoldable) otoList
  92
  93 instance
  94  ( Read_TypeNameR Text cs rs
  95  , Inj_Const cs MonoFoldable
  96  ) => Read_TypeNameR Text cs (Proxy MonoFoldable ': rs) where
  97         read_typenameR _cs "MonoFoldable" k = k (ty @MonoFoldable)
  98         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  99 instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
 100         show_const ConstZ{} = "MonoFoldable"
 101         show_const (ConstS c) = show_const c
 102
 103 instance -- Proj_ConC
 104  ( Proj_Const cs MonoFoldable
 105  , Proj_Consts cs (Consts_imported_by MonoFoldable)
 106  ) => Proj_ConC cs (Proxy MonoFoldable) where
 107         proj_conC _ (TyConst q :$ typ)
 108          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 109          , Just Refl <- proj_const q (Proxy::Proxy MonoFoldable)
 110          = case typ of
 111                  TyConst c
 112                   | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 113                  TyConst c :$ _a
 114                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 115                   -> case () of
 116                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 117                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 118                          _ -> Nothing
 119                  TyConst c :$ _a :$ _b
 120                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 121                   -> case () of
 122                          _ | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 123                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 124                          _ -> Nothing
 125                  _ -> Nothing
 126         proj_conC _c _q = Nothing
 127 data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
 128  = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
 129  | Token_Term_MonoFoldable_ofoldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 130  | Token_Term_MonoFoldable_ofoldl'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 131  | Token_Term_MonoFoldable_olength  (EToken meta ts)
 132  | Token_Term_MonoFoldable_onull    (EToken meta ts)
 133  | Token_Term_MonoFoldable_oall     (EToken meta ts) (EToken meta ts)
 134  | Token_Term_MonoFoldable_oany     (EToken meta ts) (EToken meta ts)
 135  | Token_Term_MonoFoldable_otoList  (EToken meta ts)
 136 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
 137 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
 138 instance -- CompileI
 139  ( Inj_Const (Consts_of_Ifaces is) MonoFoldable
 140  , Inj_Const (Consts_of_Ifaces is) (->)
 141  , Inj_Const (Consts_of_Ifaces is) []
 142  , Inj_Const (Consts_of_Ifaces is) Monoid
 143  , Inj_Const (Consts_of_Ifaces is) Bool
 144  , Inj_Const (Consts_of_Ifaces is) Int
 145  , Proj_Con  (Consts_of_Ifaces is)
 146  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 147  , Compile is
 148  ) => CompileI is (Proxy MonoFoldable) where
 149         compileI
 150          :: forall meta ctx ret ls rs.
 151          TokenT meta is (Proxy MonoFoldable)
 152          -> CompileT meta ctx ret is ls (Proxy MonoFoldable ': rs)
 153         compileI tok ctx k =
 154                 case tok of
 155                  Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
 156                         -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
 157                         compileO tok_f ctx $ \ty_f (TermO f) ->
 158                         compileO tok_o ctx $ \ty_o (TermO o) ->
 159                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
 160                         check_con (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 161                         check_con (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \Con ->
 162                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 163                         check_type
 164                          (At Nothing ty_o_e)
 165                          (At (Just tok_f) ty_f_a) $ \Refl ->
 166                         k ty_m $ TermO $
 167                          \c -> ofoldMap (f c) (o c)
 168                  Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
 169                         ofoldr_from tok_e2b2b tok_b tok_o ofoldr
 170                  Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
 171                         ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
 172                  Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
 173                  Token_Term_MonoFoldable_onull   tok_o -> o2ty_from tok_o onull
 174                  Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
 175                  Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
 176                  Token_Term_MonoFoldable_otoList tok_o ->
 177                  -- otoList :: MonoFoldable o => o -> [MT.Element o]
 178                         compileO tok_o ctx $ \ty_o (TermO o) ->
 179                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 180                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 181                         k (ty @[] :$ ty_o_e) $ TermO $
 182                          \c -> otoList (o c)
 183                 where
 184                 ofoldr_from tok_e2b2b tok_b tok_o
 185                  (fold::forall term o b.
 186                          (Sym_MonoFoldable term, MonoFoldable o)
 187                          => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
 188                  -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
 189                         compileO tok_e2b2b ctx $ \ty_e2b2b (TermO e2b2b) ->
 190                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 191                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 192                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
 193                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
 194                         check_type
 195                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 196                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
 197                         check_type
 198                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 199                          (At (Just tok_b) ty_b) $ \Refl ->
 200                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 201                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 202                         check_type
 203                          (At (Just tok_e2b2b) ty_e2b2b_e)
 204                          (At (Just tok_o) ty_o_e) $ \Refl ->
 205                         k ty_b $ TermO $
 206                          \c -> fold (e2b2b c) (b c) (o c)
 207                 ofoldl_from tok_b2e2b tok_b tok_o
 208                  (fold::forall term o b.
 209                          (Sym_MonoFoldable term, MonoFoldable o)
 210                          => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
 211                         -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
 212                         compileO tok_b2e2b ctx $ \ty_b2e2b (TermO b2e2b) ->
 213                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 214                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 215                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
 216                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
 217                         check_type
 218                          (At (Just tok_b2e2b) ty_b2e2b_b)
 219                          (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
 220                         check_type
 221                          (At (Just tok_b2e2b) ty_b2e2b_b)
 222                          (At (Just tok_b) ty_b) $ \Refl ->
 223                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 224                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 225                         check_type
 226                          (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
 227                          (At (Just tok_o) ty_o_e) $ \Refl ->
 228                         k ty_b $ TermO $
 229                          \c -> fold (b2e2b c) (b c) (o c)
 230                 o2ty_from
 231                  :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
 232                  => EToken meta is
 233                  -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
 234                  -> Either (Error_Term meta is) ret
 235                 o2ty_from tok_o f =
 236                         -- olength :: MonoFoldable o => o -> Int
 237                         -- onull   :: MonoFoldable o => o -> Bool
 238                         compileO tok_o ctx $ \ty_o (TermO o) ->
 239                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 240                         k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $
 241                          \c -> f (o c)
 242                 oalloany_from
 243                  tok_e2Bool tok_o
 244                  (g::forall term o.
 245                          (Sym_MonoFoldable term, MonoFoldable o)
 246                          => term (MT.Element o -> Bool) -> term o -> term Bool) =
 247                  -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 248                  -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 249                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 250                         compileO tok_o ctx $ \ty_o (TermO o) ->
 251                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 252                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 253                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 254                         check_type
 255                          (At (Just tok_e2Bool) ty_e2Bool_e)
 256                          (At (Just tok_o) ty_o_e) $ \Refl ->
 257                         check_type
 258                          (At Nothing (ty @Bool))
 259                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 260                         k (ty @Bool) $ TermO $
 261                          \c -> g (e2Bool c) (o c)