symantic-lib/Language/Symantic/Lib/Foldable.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 -- | Symantic for 'Foldable'.
   5 module Language.Symantic.Lib.Foldable where
   6
   7 import Data.Foldable (Foldable)
   8 import qualified Data.Foldable as Foldable
   9 import Control.Monad (liftM, liftM2, liftM3)
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (Foldable(..)
  13  , all, and, any, concat, concatMap
  14  , mapM_, notElem, or, sequence, sequence_)
  15
  16 import Language.Symantic.Parsing hiding (any)
  17 import Language.Symantic.Typing
  18 import Language.Symantic.Compiling
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming
  21
  22 -- * Class 'Sym_Foldable'
  23 class Sym_Foldable term where
  24         foldMap    :: (Foldable f, Monoid m) => term (a -> m) -> term (f a) -> term m
  25         foldr      :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
  26         foldr'     :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
  27         foldl      :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
  28         foldl'     :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
  29         length     :: Foldable f => term (f a) -> term Int
  30         null       :: Foldable f => term (f a) -> term Bool
  31         minimum    :: (Foldable f, Ord a) => term (f a) -> term a
  32         maximum    :: (Foldable f, Ord a) => term (f a) -> term a
  33         elem       :: (Foldable f, Eq  a) => term a -> term (f a) -> term Bool; infix 4 `elem`
  34         sum        :: (Foldable f, Num a) => term (f a) -> term a
  35         product    :: (Foldable f, Num a) => term (f a) -> term a
  36         toList     :: Foldable f => term (f a) -> term [a]
  37         all        :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
  38         and        :: Foldable f => term (f Bool) -> term Bool
  39         any        :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
  40         concat     :: Foldable f => term (f [a]) -> term [a]
  41         concatMap  :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
  42         find       :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
  43         foldlM     :: (Foldable f, Monad m) => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
  44         foldrM     :: (Foldable f, Monad m) => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
  45         forM_      :: (Foldable f, Monad m) => term (f a) -> term (a -> m b) -> term (m ())
  46         for_       :: (Foldable f, Applicative p) => term (f a) -> term (a -> p b) -> term (p ())
  47         mapM_      :: (Foldable f, Monad m) => term (a -> m b) -> term (f a) -> term (m ())
  48         maximumBy  :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
  49         minimumBy  :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
  50         notElem    :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
  51         or         :: Foldable f => term (f Bool) -> term Bool
  52         sequenceA_ :: (Foldable f, Applicative p) => term (f (p a)) -> term (p ())
  53         sequence_  :: (Foldable f, Monad m) => term (f (m a)) -> term (m ())
  54         traverse_  :: (Foldable f, Applicative p) => term (a -> p b) -> term (f a) -> term (p ())
  55         -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
  56         -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
  57
  58         default foldMap    :: (Trans t term, Foldable f, Monoid m) => t term (a -> m) -> t term (f a) -> t term m
  59         default foldr      :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
  60         default foldr'     :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
  61         default foldl      :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
  62         default foldl'     :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
  63         default length     :: (Trans t term, Foldable f) => t term (f a) -> t term Int
  64         default null       :: (Trans t term, Foldable f) => t term (f a) -> t term Bool
  65         default minimum    :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
  66         default maximum    :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
  67         default elem       :: (Trans t term, Foldable f, Eq  a) => t term a -> t term (f a) -> t term Bool
  68         default sum        :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
  69         default product    :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
  70         default toList     :: (Trans t term, Foldable f) => t term (f a) -> t term [a]
  71         default all        :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
  72         default and        :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
  73         default any        :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
  74         default concat     :: (Trans t term, Foldable f) => t term (f [a]) -> t term [a]
  75         default concatMap  :: (Trans t term, Foldable f) => t term (a -> [b]) -> t term (f a) -> t term [b]
  76         default find       :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term (Maybe a)
  77         default foldlM     :: (Trans t term, Foldable f, Monad m) => t term (b -> a -> m b) -> t term b -> t term (f a) -> t term (m b)
  78         default foldrM     :: (Trans t term, Foldable f, Monad m) => t term (a -> b -> m b) -> t term b -> t term (f a) -> t term (m b)
  79         default forM_      :: (Trans t term, Foldable f, Monad m) => t term (f a) -> t term (a -> m b) -> t term (m ())
  80         default for_       :: (Trans t term, Foldable f, Applicative p) => t term (f a) -> t term (a -> p b) -> t term (p ())
  81         default mapM_      :: (Trans t term, Foldable f, Monad m) => t term (a -> m b) -> t term (f a) -> t term (m ())
  82         default maximumBy  :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
  83         default minimumBy  :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
  84         default notElem    :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
  85         default or         :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
  86         default sequenceA_ :: (Trans t term, Foldable f, Applicative p) => t term (f (p a)) -> t term (p ())
  87         default sequence_  :: (Trans t term, Foldable f, Monad m) => t term (f (m a)) -> t term (m ())
  88         default traverse_  :: (Trans t term, Foldable f, Applicative p) => t term (a -> p b) -> t term (f a) -> t term (p ())
  89
  90         foldMap    = trans_map2 foldMap
  91         foldr      = trans_map3 foldr
  92         foldr'     = trans_map3 foldr'
  93         foldl      = trans_map3 foldl
  94         foldl'     = trans_map3 foldl'
  95         length     = trans_map1 length
  96         null       = trans_map1 null
  97         minimum    = trans_map1 minimum
  98         maximum    = trans_map1 maximum
  99         elem       = trans_map2 elem
 100         sum        = trans_map1 sum
 101         product    = trans_map1 product
 102         toList     = trans_map1 toList
 103         all        = trans_map2 all
 104         and        = trans_map1 and
 105         any        = trans_map2 any
 106         concat     = trans_map1 concat
 107         concatMap  = trans_map2 concatMap
 108         find       = trans_map2 find
 109         foldlM     = trans_map3 foldlM
 110         foldrM     = trans_map3 foldrM
 111         forM_      = trans_map2 forM_
 112         for_       = trans_map2 for_
 113         mapM_      = trans_map2 mapM_
 114         maximumBy  = trans_map2 maximumBy
 115         minimumBy  = trans_map2 minimumBy
 116         notElem    = trans_map2 notElem
 117         or         = trans_map1 or
 118         sequenceA_ = trans_map1 sequenceA_
 119         sequence_  = trans_map1 sequence_
 120         traverse_  = trans_map2 traverse_
 121
 122 type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
 123 type instance TyConsts_of_Iface (Proxy Foldable) = Proxy Foldable ': TyConsts_imported_by Foldable
 124 type instance TyConsts_imported_by Foldable = '[]
 125
 126 instance Sym_Foldable HostI where
 127         foldMap    = liftM2 Foldable.foldMap
 128         foldr      = liftM3 Foldable.foldr
 129         foldr'     = liftM3 Foldable.foldr'
 130         foldl      = liftM3 Foldable.foldl
 131         foldl'     = liftM3 Foldable.foldl'
 132         null       = liftM  Foldable.null
 133         length     = liftM  Foldable.length
 134         minimum    = liftM  Foldable.minimum
 135         maximum    = liftM  Foldable.maximum
 136         elem       = liftM2 Foldable.elem
 137         sum        = liftM  Foldable.sum
 138         product    = liftM  Foldable.product
 139         toList     = liftM  Foldable.toList
 140         all        = liftM2 Foldable.all
 141         and        = liftM  Foldable.and
 142         any        = liftM2 Foldable.any
 143         concat     = liftM  Foldable.concat
 144         concatMap  = liftM2 Foldable.concatMap
 145         find       = liftM2 Foldable.find
 146         foldlM     = liftM3 Foldable.foldlM
 147         foldrM     = liftM3 Foldable.foldrM
 148         forM_      = liftM2 Foldable.forM_
 149         for_       = liftM2 Foldable.for_
 150         mapM_      = liftM2 Foldable.mapM_
 151         maximumBy  = liftM2 Foldable.maximumBy
 152         minimumBy  = liftM2 Foldable.minimumBy
 153         notElem    = liftM2 Foldable.notElem
 154         or         = liftM  Foldable.or
 155         sequenceA_ = liftM  Foldable.sequenceA_
 156         sequence_  = liftM  Foldable.sequence_
 157         traverse_  = liftM2 Foldable.traverse_
 158 instance Sym_Foldable TextI where
 159         foldMap    = textI2 "foldMap"
 160         foldr      = textI3 "foldr"
 161         foldr'     = textI3 "foldr'"
 162         foldl      = textI3 "foldl"
 163         foldl'     = textI3 "foldl'"
 164         null       = textI1 "null"
 165         length     = textI1 "length"
 166         minimum    = textI1 "minimum"
 167         maximum    = textI1 "maximum"
 168         elem       = textI2 "elem"
 169         sum        = textI1 "sum"
 170         product    = textI1 "product"
 171         toList     = textI1 "toList"
 172         all        = textI2 "all"
 173         and        = textI1 "and"
 174         any        = textI2 "any"
 175         concat     = textI1 "concat"
 176         concatMap  = textI2 "concatMap"
 177         find       = textI2 "find"
 178         foldlM     = textI3 "foldlM"
 179         foldrM     = textI3 "foldrM"
 180         forM_      = textI2 "forM_"
 181         for_       = textI2 "for_"
 182         mapM_      = textI2 "mapM_"
 183         maximumBy  = textI2 "maximumBy"
 184         minimumBy  = textI2 "minimumBy"
 185         notElem    = textI2 "notElem"
 186         or         = textI1 "or"
 187         sequenceA_ = textI1 "sequenceA_"
 188         sequence_  = textI1 "sequence_"
 189         traverse_  = textI2 "traverse_"
 190 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where
 191         foldMap    = dupI2 @Sym_Foldable foldMap
 192         foldr      = dupI3 @Sym_Foldable foldr
 193         foldr'     = dupI3 @Sym_Foldable foldr'
 194         foldl      = dupI3 @Sym_Foldable foldl
 195         foldl'     = dupI3 @Sym_Foldable foldl'
 196         null       = dupI1 @Sym_Foldable null
 197         length     = dupI1 @Sym_Foldable length
 198         minimum    = dupI1 @Sym_Foldable minimum
 199         maximum    = dupI1 @Sym_Foldable maximum
 200         elem       = dupI2 @Sym_Foldable elem
 201         sum        = dupI1 @Sym_Foldable sum
 202         product    = dupI1 @Sym_Foldable product
 203         toList     = dupI1 @Sym_Foldable toList
 204         all        = dupI2 @Sym_Foldable all
 205         and        = dupI1 @Sym_Foldable and
 206         any        = dupI2 @Sym_Foldable any
 207         concat     = dupI1 @Sym_Foldable concat
 208         concatMap  = dupI2 @Sym_Foldable concatMap
 209         find       = dupI2 @Sym_Foldable find
 210         foldlM     = dupI3 @Sym_Foldable foldlM
 211         foldrM     = dupI3 @Sym_Foldable foldrM
 212         forM_      = dupI2 @Sym_Foldable forM_
 213         for_       = dupI2 @Sym_Foldable for_
 214         mapM_      = dupI2 @Sym_Foldable mapM_
 215         maximumBy  = dupI2 @Sym_Foldable maximumBy
 216         minimumBy  = dupI2 @Sym_Foldable minimumBy
 217         notElem    = dupI2 @Sym_Foldable notElem
 218         or         = dupI1 @Sym_Foldable or
 219         sequenceA_ = dupI1 @Sym_Foldable sequenceA_
 220         sequence_  = dupI1 @Sym_Foldable sequence_
 221         traverse_  = dupI2 @Sym_Foldable traverse_
 222
 223 instance
 224  ( Read_TyNameR TyName cs rs
 225  , Inj_TyConst cs Foldable
 226  ) => Read_TyNameR TyName cs (Proxy Foldable ': rs) where
 227         read_TyNameR _cs (TyName "Foldable") k = k (ty @Foldable)
 228         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 229 instance Show_TyConst cs => Show_TyConst (Proxy Foldable ': cs) where
 230         show_TyConst TyConstZ{} = "Foldable"
 231         show_TyConst (TyConstS c) = show_TyConst c
 232
 233 instance Proj_TyConC cs (Proxy Foldable)
 234 data instance TokenT meta (ts::[*]) (Proxy Foldable)
 235  = Token_Term_Foldable_foldMap (EToken meta ts) (EToken meta ts)
 236  | Token_Term_Foldable_foldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 237  | Token_Term_Foldable_foldr'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 238  | Token_Term_Foldable_foldl   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 239  | Token_Term_Foldable_elem    (EToken meta ts) (EToken meta ts)
 240  | Token_Term_Foldable_null    (EToken meta ts)
 241  | Token_Term_Foldable_length  (EToken meta ts)
 242  | Token_Term_Foldable_minimum (EToken meta ts)
 243  | Token_Term_Foldable_maximum (EToken meta ts)
 244  | Token_Term_Foldable_sum     (EToken meta ts)
 245  | Token_Term_Foldable_product (EToken meta ts)
 246  | Token_Term_Foldable_toList  (EToken meta ts)
 247  | Token_Term_Foldable_all     (EToken meta ts) (EToken meta ts)
 248  | Token_Term_Foldable_any     (EToken meta ts) (EToken meta ts)
 249  | Token_Term_Foldable_and     (EToken meta ts)
 250  | Token_Term_Foldable_or      (EToken meta ts)
 251  | Token_Term_Foldable_concat  (EToken meta ts)
 252 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Foldable))
 253 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Foldable))
 254 instance -- CompileI
 255  ( Inj_TyConst cs Foldable
 256  , Inj_TyConst cs Monoid
 257  , Inj_TyConst cs (->)
 258  , Inj_TyConst cs Int
 259  , Inj_TyConst cs Bool
 260  , Inj_TyConst cs Eq
 261  , Inj_TyConst cs Ord
 262  , Inj_TyConst cs Num
 263  , Inj_TyConst cs []
 264  , Proj_TyCon  cs
 265  , Compile cs is
 266  ) => CompileI cs is (Proxy Foldable) where
 267         compileI
 268          :: forall meta ctx ret ls rs.
 269          TokenT meta is (Proxy Foldable)
 270          -> CompileT meta ctx ret cs is ls (Proxy Foldable ': rs)
 271         compileI tok ctx k =
 272                 case tok of
 273                  Token_Term_Foldable_foldMap tok_a2m tok_ta ->
 274                         -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 275                         compileO tok_a2m ctx $ \ty_a2m (TermO a2m) ->
 276                         compileO tok_ta  ctx $ \ty_ta  (TermO ta) ->
 277                         check_TyEq2 (ty @(->)) (At (Just tok_a2m) ty_a2m) $ \Refl ty_a2m_a ty_a2m_m ->
 278                         check_TyCon (At (Just tok_a2m) (ty @Monoid :$ ty_a2m_m)) $ \TyCon ->
 279                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 280                         check_TyEq
 281                          (At (Just tok_a2m) ty_a2m_a)
 282                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
 283                         k ty_a2m_m $ TermO $
 284                          \c -> foldMap (a2m c) (ta c)
 285                  Token_Term_Foldable_foldr   tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr
 286                  Token_Term_Foldable_foldr'  tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr'
 287                  Token_Term_Foldable_foldl   tok_b2a2b tok_b tok_ta -> foldl_from tok_b2a2b tok_b tok_ta foldl
 288                  Token_Term_Foldable_elem tok_a tok_ta ->
 289                         -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 290                         compileO tok_a  ctx $ \ty_a  (TermO a) ->
 291                         compileO tok_ta ctx $ \ty_ta (TermO ta) ->
 292                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 293                         check_TyCon (At (Just tok_ta) (ty @Eq :$ ty_ta_a)) $ \TyCon ->
 294                         check_TyEq
 295                          (At (Just tok_a) ty_a)
 296                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
 297                         k (ty @Bool) $ TermO $
 298                          \c -> a c `elem` ta c
 299                  Token_Term_Foldable_null    tok_ta -> ta2ty_from tok_ta null
 300                  Token_Term_Foldable_length  tok_ta -> ta2ty_from tok_ta length
 301                  Token_Term_Foldable_minimum tok_ta -> ta2a_from tok_ta (ty @Ord) minimum
 302                  Token_Term_Foldable_maximum tok_ta -> ta2a_from tok_ta (ty @Ord) maximum
 303                  Token_Term_Foldable_sum     tok_ta -> ta2a_from tok_ta (ty @Num) sum
 304                  Token_Term_Foldable_product tok_ta -> ta2a_from tok_ta (ty @Num) product
 305                  Token_Term_Foldable_toList  tok_ta ->
 306                         -- toList :: Foldable t => t a -> [a]
 307                         compileO tok_ta ctx $ \ty_ta (TermO ta) ->
 308                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 309                         k (ty @[] :$ ty_ta_a) $ TermO $
 310                          \c -> toList (ta c)
 311                  Token_Term_Foldable_all tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta all
 312                  Token_Term_Foldable_any tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta any
 313                  Token_Term_Foldable_and tok_tBool -> andor_from tok_tBool and
 314                  Token_Term_Foldable_or  tok_tBool -> andor_from tok_tBool or
 315                  Token_Term_Foldable_concat tok_tla ->
 316                         -- concat :: Foldable t => t [a] -> [a]
 317                         compileO tok_tla ctx $ \ty_tla (TermO tla) ->
 318                         check_TyCon1 (ty @Foldable) (At (Just tok_tla) ty_tla) $ \Refl TyCon _ty_tla_t ty_tla_la ->
 319                         check_TyEq1 (ty @[]) (At (Just tok_tla) ty_tla_la) $ \Refl ty_tla_la_a ->
 320                         k (ty @[] :$ ty_tla_la_a) $ TermO $
 321                          \c -> concat (tla c)
 322                 where
 323                 foldr_from tok_a2b2b tok_b tok_ta
 324                  (fold::forall term f a b.
 325                          (Sym_Foldable term, Foldable f)
 326                          => term (a -> b -> b) -> term b -> term (f a) -> term b) =
 327                  -- foldr  :: Foldable t => (a -> b -> b) -> b -> t a -> b
 328                  -- foldr' :: Foldable t => (a -> b -> b) -> b -> t a -> b
 329                         compileO tok_a2b2b ctx $ \ty_a2b2b (TermO a2b2b) ->
 330                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 331                         compileO tok_ta    ctx $ \ty_ta    (TermO ta) ->
 332                         check_TyEq2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b) $ \Refl ty_a2b2b_a ty_a2b2b_b2b ->
 333                         check_TyEq2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b_b2b) $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 ->
 334                         check_TyEq
 335                          (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
 336                          (At (Just tok_a2b2b) ty_a2b2b_b2b_b1) $ \Refl ->
 337                         check_TyEq
 338                          (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
 339                          (At (Just tok_b) ty_b) $ \Refl ->
 340                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 341                         check_TyEq
 342                          (At (Just tok_a2b2b) ty_a2b2b_a)
 343                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
 344                         k ty_b $ TermO $
 345                          \c -> fold (a2b2b c) (b c) (ta c)
 346                 foldl_from tok_b2a2b tok_b tok_ta
 347                  (fold::forall term f a b.
 348                          (Sym_Foldable term, Foldable f)
 349                          => term (b -> a -> b) -> term b -> term (f a) -> term b) =
 350                  -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
 351                         compileO tok_b2a2b ctx $ \ty_b2a2b (TermO b2a2b) ->
 352                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 353                         compileO tok_ta    ctx $ \ty_ta    (TermO ta) ->
 354                         check_TyEq2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b) $ \Refl ty_b2a2b_b ty_b2a2b_a2b ->
 355                         check_TyEq2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b_a2b) $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b ->
 356                         check_TyEq
 357                          (At (Just tok_b2a2b) ty_b2a2b_b)
 358                          (At (Just tok_b2a2b) ty_b2a2b_a2b_b) $ \Refl ->
 359                         check_TyEq
 360                          (At (Just tok_b2a2b) ty_b2a2b_b)
 361                          (At (Just tok_b) ty_b) $ \Refl ->
 362                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 363                         check_TyEq
 364                          (At (Just tok_b2a2b) ty_b2a2b_a2b_a)
 365                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
 366                         k ty_b $ TermO $
 367                          \c -> fold (b2a2b c) (b c) (ta c)
 368                 ta2ty_from
 369                  :: forall typ. Inj_TyConst cs typ
 370                  => EToken meta is
 371                  -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ)
 372                  -> Either (Error_Term meta cs is) ret
 373                 ta2ty_from tok_ta f =
 374                  -- length :: Foldable t => t a -> Int
 375                  -- null   :: Foldable t => t a -> Bool
 376                         compileO tok_ta ctx $ \ty_ta (TermO ta) ->
 377                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t _ty_ta_a ->
 378                         k (TyConst inj_TyConst::Type cs typ) $ TermO $
 379                          \c -> f (ta c)
 380                 ta2a_from
 381                  :: forall con.
 382                     EToken meta is
 383                  -> Type cs con
 384                  -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
 385                  -> Either (Error_Term meta cs is) ret
 386                 ta2a_from tok_ta q f =
 387                  -- minimum :: (Foldable t, Ord a) => t a -> a
 388                  -- maximum :: (Foldable t, Ord a) => t a -> a
 389                  -- sum     :: (Foldable t, Num a) => t a -> a
 390                  -- product :: (Foldable t, Num a) => t a -> a
 391                         compileO tok_ta ctx $ \ty_ta (TermO ta) ->
 392                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 393                         check_TyCon (At (Just tok_ta) (q :$ ty_ta_a)) $ \TyCon ->
 394                         k ty_ta_a $ TermO $
 395                          \c -> f (ta c)
 396                 allany_from tok_a2Bool tok_ta
 397                  (g::forall term f a.
 398                          (Sym_Foldable term, Foldable f)
 399                          => term (a -> Bool) -> term (f a) -> term Bool) =
 400                  -- all :: Foldable t => (a -> Bool) -> t a -> Bool
 401                  -- any :: Foldable t => (a -> Bool) -> t a -> Bool
 402                         compileO tok_a2Bool ctx $ \ty_a2Bool (TermO a2Bool) ->
 403                         compileO tok_ta ctx $ \ty_ta (TermO ta) ->
 404                         check_TyEq2 (ty @(->)) (At (Just tok_a2Bool) ty_a2Bool) $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
 405                         check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
 406                         check_TyEq
 407                          (At (Just tok_a2Bool) ty_a2Bool_a)
 408                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
 409                         check_TyEq
 410                          (At Nothing (ty @Bool))
 411                          (At (Just tok_a2Bool) ty_a2Bool_Bool) $ \Refl ->
 412                         k (ty @Bool) $ TermO $
 413                          \c -> g (a2Bool c) (ta c)
 414                 andor_from tok_tBool
 415                  (g::forall term f.
 416                          (Sym_Foldable term, Foldable f)
 417                          => term (f Bool) -> term Bool) =
 418                  -- and :: Foldable t => t Bool -> Bool
 419                  -- or  :: Foldable t => t Bool -> Bool
 420                         compileO tok_tBool ctx $ \ty_tBool (TermO tBool) ->
 421                         check_TyCon1 (ty @Foldable) (At (Just tok_tBool) ty_tBool) $ \Refl TyCon _ty_tBool_t ty_tBool_Bool ->
 422                         check_TyEq
 423                          (At Nothing (ty @Bool))
 424                          (At (Just tok_tBool) ty_tBool_Bool) $ \Refl ->
 425                         k (ty @Bool) $ TermO $
 426                          \c -> g (tBool c)
 427 instance -- TokenizeT
 428  Inj_Token meta ts Foldable =>
 429  TokenizeT meta ts (Proxy Foldable) where
 430         tokenizeT _t = mempty
 431          { tokenizers_infix = tokenizeTMod []
 432                  [ tokenize2 "foldMap" infixN5 Token_Term_Foldable_foldMap
 433                  , tokenize3 "foldr"   infixN5 Token_Term_Foldable_foldr
 434                  , tokenize3 "foldr'"  infixN5 Token_Term_Foldable_foldr'
 435                  , tokenize3 "foldl"   infixN5 Token_Term_Foldable_foldl
 436                  , tokenize2 "elem"    (infixN 4) Token_Term_Foldable_elem
 437                  , tokenize1 "sum"     infixN5 Token_Term_Foldable_sum
 438                  , tokenize1 "product" infixN5 Token_Term_Foldable_product
 439                  , tokenize1 "toList"  infixN5 Token_Term_Foldable_toList
 440                  , tokenize2 "all"     infixN5 Token_Term_Foldable_all
 441                  , tokenize2 "any"     infixN5 Token_Term_Foldable_any
 442                  , tokenize1 "and"     infixN5 Token_Term_Foldable_and
 443                  , tokenize1 "or"      infixN5 Token_Term_Foldable_or
 444                  , tokenize1 "concat"  infixN5 Token_Term_Foldable_concat
 445                  ]
 446          }
 447 instance Gram_Term_AtomsT meta ts (Proxy Foldable) g