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 String
  63  , Proxy Text
  64  ]
  65
  66 instance Sym_MonoFoldable HostI where
  67         ofoldMap = liftM2 MT.ofoldMap
  68         ofoldr   = liftM3 MT.ofoldr
  69         ofoldl'  = liftM3 MT.ofoldl'
  70         olength  = liftM  MT.olength
  71         onull    = liftM  MT.onull
  72         oall     = liftM2 MT.oall
  73         oany     = liftM2 MT.oany
  74         otoList  = liftM  MT.otoList
  75 instance Sym_MonoFoldable TextI where
  76         ofoldMap = textI_app2 "ofoldMap"
  77         ofoldr   = textI_app3 "ofoldr"
  78         ofoldl'  = textI_app3 "ofoldl'"
  79         olength  = textI_app1 "olength"
  80         onull    = textI_app1 "onull"
  81         oall     = textI_app2 "oall"
  82         oany     = textI_app2 "oany"
  83         otoList  = textI_app1 "otoList"
  84 instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
  85         ofoldMap = dupI2 (Proxy @Sym_MonoFoldable) ofoldMap
  86         ofoldr   = dupI3 (Proxy @Sym_MonoFoldable) ofoldr
  87         ofoldl'  = dupI3 (Proxy @Sym_MonoFoldable) ofoldl'
  88         olength  = dupI1 (Proxy @Sym_MonoFoldable) olength
  89         onull    = dupI1 (Proxy @Sym_MonoFoldable) onull
  90         oall     = dupI2 (Proxy @Sym_MonoFoldable) oall
  91         oany     = dupI2 (Proxy @Sym_MonoFoldable) oany
  92         otoList  = dupI1 (Proxy @Sym_MonoFoldable) otoList
  93
  94 instance Const_from Text cs => Const_from Text (Proxy MonoFoldable ': cs) where
  95         const_from "MonoFoldable" k = k (ConstZ kind)
  96         const_from s k = const_from s $ k . ConstS
  97 instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
  98         show_const ConstZ{} = "MonoFoldable"
  99         show_const (ConstS c) = show_const c
 100
 101 instance -- Proj_ConC
 102  ( Proj_Const cs MonoFoldable
 103  , Proj_Consts cs (Consts_imported_by MonoFoldable)
 104  ) => Proj_ConC cs (Proxy MonoFoldable) where
 105         proj_conC _ (TyConst q :$ typ)
 106          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 107          , Just Refl <- proj_const q (Proxy::Proxy MonoFoldable)
 108          = case typ of
 109                  TyConst c
 110                   | Just Refl <- proj_const c (Proxy::Proxy String) -> Just Con
 111                   | Just Refl <- proj_const c (Proxy::Proxy Text)   -> Just Con
 112                  TyConst c :$ _a
 113                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 114                   -> case () of
 115                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 116                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 117                          _ -> Nothing
 118                  TyConst c :$ _a :$ _b
 119                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 120                   -> case () of
 121                          _ | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 122                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 123                          _ -> Nothing
 124                  _ -> Nothing
 125         proj_conC _c _q = Nothing
 126 data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
 127  = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
 128  | Token_Term_MonoFoldable_ofoldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 129  | Token_Term_MonoFoldable_ofoldl'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 130  | Token_Term_MonoFoldable_olength  (EToken meta ts)
 131  | Token_Term_MonoFoldable_onull    (EToken meta ts)
 132  | Token_Term_MonoFoldable_oall     (EToken meta ts) (EToken meta ts)
 133  | Token_Term_MonoFoldable_oany     (EToken meta ts) (EToken meta ts)
 134  | Token_Term_MonoFoldable_otoList  (EToken meta ts)
 135 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
 136 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
 137 instance -- Term_fromI
 138  ( Inj_Const (Consts_of_Ifaces is) MonoFoldable
 139  , Inj_Const (Consts_of_Ifaces is) (->)
 140  , Inj_Const (Consts_of_Ifaces is) []
 141  , Inj_Const (Consts_of_Ifaces is) Monoid
 142  , Inj_Const (Consts_of_Ifaces is) Bool
 143  , Inj_Const (Consts_of_Ifaces is) Int
 144  , Proj_Con  (Consts_of_Ifaces is)
 145  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 146  , Term_from is
 147  ) => Term_fromI is (Proxy MonoFoldable) where
 148         term_fromI
 149          :: forall meta ctx ret ls rs.
 150          TokenT meta is (Proxy MonoFoldable)
 151          -> Term_fromT meta ctx ret is ls (Proxy MonoFoldable ': rs)
 152         term_fromI tok ctx k =
 153                 case tok of
 154                  Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
 155                         -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
 156                         term_from tok_f ctx $ \ty_f (TermLC f) ->
 157                         term_from tok_o ctx $ \ty_o (TermLC o) ->
 158                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
 159                         check_con (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 160                         check_con (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \Con ->
 161                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 162                         check_type
 163                          (At Nothing ty_o_e)
 164                          (At (Just tok_f) ty_f_a) $ \Refl ->
 165                         k ty_m $ TermLC $
 166                          \c -> ofoldMap (f c) (o c)
 167                  Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
 168                         ofoldr_from tok_e2b2b tok_b tok_o ofoldr
 169                  Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
 170                         ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
 171                  Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
 172                  Token_Term_MonoFoldable_onull   tok_o -> o2ty_from tok_o onull
 173                  Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
 174                  Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
 175                  Token_Term_MonoFoldable_otoList tok_o ->
 176                  -- otoList :: MonoFoldable o => o -> [MT.Element o]
 177                         term_from tok_o ctx $ \ty_o (TermLC o) ->
 178                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 179                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 180                         k (ty @[] :$ ty_o_e) $ TermLC $
 181                          \c -> otoList (o c)
 182                 where
 183                 ofoldr_from tok_e2b2b tok_b tok_o
 184                  (fold::forall term o b.
 185                          (Sym_MonoFoldable term, MonoFoldable o)
 186                          => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
 187                  -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
 188                         term_from tok_e2b2b ctx $ \ty_e2b2b (TermLC e2b2b) ->
 189                         term_from tok_b     ctx $ \ty_b     (TermLC b) ->
 190                         term_from tok_o     ctx $ \ty_o     (TermLC o) ->
 191                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
 192                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
 193                         check_type
 194                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 195                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
 196                         check_type
 197                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 198                          (At (Just tok_b) ty_b) $ \Refl ->
 199                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 200                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 201                         check_type
 202                          (At (Just tok_e2b2b) ty_e2b2b_e)
 203                          (At (Just tok_o) ty_o_e) $ \Refl ->
 204                         k ty_b $ TermLC $
 205                          \c -> fold (e2b2b c) (b c) (o c)
 206                 ofoldl_from tok_b2e2b tok_b tok_o
 207                  (fold::forall term o b.
 208                          (Sym_MonoFoldable term, MonoFoldable o)
 209                          => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
 210                         -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
 211                         term_from tok_b2e2b ctx $ \ty_b2e2b (TermLC b2e2b) ->
 212                         term_from tok_b     ctx $ \ty_b     (TermLC b) ->
 213                         term_from tok_o     ctx $ \ty_o     (TermLC o) ->
 214                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
 215                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
 216                         check_type
 217                          (At (Just tok_b2e2b) ty_b2e2b_b)
 218                          (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
 219                         check_type
 220                          (At (Just tok_b2e2b) ty_b2e2b_b)
 221                          (At (Just tok_b) ty_b) $ \Refl ->
 222                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 223                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 224                         check_type
 225                          (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
 226                          (At (Just tok_o) ty_o_e) $ \Refl ->
 227                         k ty_b $ TermLC $
 228                          \c -> fold (b2e2b c) (b c) (o c)
 229                 o2ty_from
 230                  :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
 231                  => EToken meta is
 232                  -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
 233                  -> Either (Error_Term meta is) ret
 234                 o2ty_from tok_o f =
 235                         -- olength :: MonoFoldable o => o -> Int
 236                         -- onull   :: MonoFoldable o => o -> Bool
 237                         term_from tok_o ctx $ \ty_o (TermLC o) ->
 238                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 239                         k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermLC $
 240                          \c -> f (o c)
 241                 oalloany_from
 242                  tok_e2Bool tok_o
 243                  (g::forall term o.
 244                          (Sym_MonoFoldable term, MonoFoldable o)
 245                          => term (MT.Element o -> Bool) -> term o -> term Bool) =
 246                  -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 247                  -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 248                         term_from tok_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
 249                         term_from tok_o ctx $ \ty_o (TermLC o) ->
 250                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 251                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 252                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 253                         check_type
 254                          (At (Just tok_e2Bool) ty_e2Bool_e)
 255                          (At (Just tok_o) ty_o_e) $ \Refl ->
 256                         check_type
 257                          (At Nothing (ty @Bool))
 258                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 259                         k (ty @Bool) $ TermLC $
 260                          \c -> g (e2Bool c) (o c)