Language/Symantic/Compiling/Foldable.hs

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