Language/Symantic/Compiling/Foldable.hs

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