Language/Symantic/Expr/Foldable.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Foldable'.
  13 module Language.Symantic.Expr.Foldable where
  14
  15 import Control.Monad (liftM, liftM2, liftM3)
  16 import Data.Monoid
  17 import Data.Foldable (Foldable)
  18 import qualified Data.Foldable as Foldable
  19 import Data.Proxy (Proxy(..))
  20 import Data.Type.Equality ((:~:)(Refl))
  21 import Prelude hiding ((<$>), Foldable(..)
  22  , all, and, any, concat, concatMap, mapM_
  23  , notElem, or, sequence_)
  24
  25 import Language.Symantic.Type
  26 import Language.Symantic.Repr
  27 import Language.Symantic.Expr.Root
  28 import Language.Symantic.Expr.Error
  29 import Language.Symantic.Expr.From
  30 import Language.Symantic.Expr.Lambda
  31 import Language.Symantic.Expr.List
  32 import Language.Symantic.Trans.Common
  33
  34 -- * Class 'Sym_Foldable'
  35 -- | Symantic.
  36 class Sym_Foldable repr where
  37         foldMap    :: (Foldable f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
  38         foldr      :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  39         foldr'     :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  40         foldl      :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  41         foldl'     :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  42         length     :: Foldable f => repr (f a) -> repr Int
  43         null       :: Foldable f => repr (f a) -> repr Bool
  44         minimum    :: (Foldable f, Ord a) => repr (f a) -> repr a
  45         maximum    :: (Foldable f, Ord a) => repr (f a) -> repr a
  46         elem       :: (Foldable f, Eq  a) => repr a -> repr (f a) -> repr Bool
  47         sum        :: (Foldable f, Num a) => repr (f a) -> repr a
  48         product    :: (Foldable f, Num a) => repr (f a) -> repr a
  49         toList     :: Foldable f => repr (f a) -> repr [a]
  50         all        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
  51         and        :: Foldable f => repr (f Bool) -> repr Bool
  52         any        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
  53         concat     :: Foldable f => repr (f [a]) -> repr [a]
  54         concatMap  :: Foldable f => repr (a -> [b]) -> repr (f a) -> repr [b]
  55         find       :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr (Maybe a)
  56         foldlM     :: (Foldable f, Monad m) => repr (b -> a -> m b) -> repr b -> repr (f a) -> repr (m b)
  57         foldrM     :: (Foldable f, Monad m) => repr (a -> b -> m b) -> repr b -> repr (f a) -> repr (m b)
  58         forM_      :: (Foldable f, Monad m) => repr (f a) -> repr (a -> m b) -> repr (m ())
  59         for_       :: (Foldable f, Applicative p) => repr (f a) -> repr (a -> p b) -> repr (p ())
  60         mapM_      :: (Foldable f, Monad m) => repr (a -> m b) -> repr (f a) -> repr (m ())
  61         maximumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
  62         minimumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
  63         notElem    :: (Foldable f, Eq a) => repr a -> repr (f a) -> repr Bool
  64         or         :: Foldable f => repr (f Bool) -> repr Bool
  65         sequenceA_ :: (Foldable f, Applicative p) => repr (f (p a)) -> repr (p ())
  66         sequence_  :: (Foldable f, Monad m) => repr (f (m a)) -> repr (m ())
  67         traverse_  :: (Foldable f, Applicative p) => repr (a -> p b) -> repr (f a) -> repr (p ())
  68         -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
  69         -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
  70
  71         default foldMap    :: (Trans t repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
  72         default foldr      :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
  73         default foldr'     :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
  74         default foldl      :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
  75         default foldl'     :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
  76         default length     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
  77         default null       :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
  78         default minimum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  79         default maximum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  80         default elem       :: (Trans t repr, Foldable f, Eq  a) => t repr a -> t repr (f a) -> t repr Bool
  81         default sum        :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  82         default product    :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  83         default toList     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
  84         default all        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
  85         default and        :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
  86         default any        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
  87         default concat     :: (Trans t repr, Foldable f) => t repr (f [a]) -> t repr [a]
  88         default concatMap  :: (Trans t repr, Foldable f) => t repr (a -> [b]) -> t repr (f a) -> t repr [b]
  89         default find       :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr (Maybe a)
  90         default foldlM     :: (Trans t repr, Foldable f, Monad m) => t repr (b -> a -> m b) -> t repr b -> t repr (f a) -> t repr (m b)
  91         default foldrM     :: (Trans t repr, Foldable f, Monad m) => t repr (a -> b -> m b) -> t repr b -> t repr (f a) -> t repr (m b)
  92         default forM_      :: (Trans t repr, Foldable f, Monad m) => t repr (f a) -> t repr (a -> m b) -> t repr (m ())
  93         default for_       :: (Trans t repr, Foldable f, Applicative p) => t repr (f a) -> t repr (a -> p b) -> t repr (p ())
  94         default mapM_      :: (Trans t repr, Foldable f, Monad m) => t repr (a -> m b) -> t repr (f a) -> t repr (m ())
  95         default maximumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
  96         default minimumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
  97         default notElem    :: (Trans t repr, Foldable f, Eq a) => t repr a -> t repr (f a) -> t repr Bool
  98         default or         :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
  99         default sequenceA_ :: (Trans t repr, Foldable f, Applicative p) => t repr (f (p a)) -> t repr (p ())
 100         default sequence_  :: (Trans t repr, Foldable f, Monad m) => t repr (f (m a)) -> t repr (m ())
 101         default traverse_  :: (Trans t repr, Foldable f, Applicative p) => t repr (a -> p b) -> t repr (f a) -> t repr (p ())
 102
 103         foldMap    = trans_map2 foldMap
 104         foldr      = trans_map3 foldr
 105         foldr'     = trans_map3 foldr'
 106         foldl      = trans_map3 foldl
 107         foldl'     = trans_map3 foldl'
 108         length     = trans_map1 length
 109         null       = trans_map1 null
 110         minimum    = trans_map1 minimum
 111         maximum    = trans_map1 maximum
 112         elem       = trans_map2 elem
 113         sum        = trans_map1 sum
 114         product    = trans_map1 product
 115         toList     = trans_map1 toList
 116         all        = trans_map2 all
 117         and        = trans_map1 and
 118         any        = trans_map2 any
 119         concat     = trans_map1 concat
 120         concatMap  = trans_map2 concatMap
 121         find       = trans_map2 find
 122         foldlM     = trans_map3 foldlM
 123         foldrM     = trans_map3 foldrM
 124         forM_      = trans_map2 forM_
 125         for_       = trans_map2 for_
 126         mapM_      = trans_map2 mapM_
 127         maximumBy  = trans_map2 maximumBy
 128         minimumBy  = trans_map2 minimumBy
 129         notElem    = trans_map2 notElem
 130         or         = trans_map1 or
 131         sequenceA_ = trans_map1 sequenceA_
 132         sequence_  = trans_map1 sequence_
 133         traverse_  = trans_map2 traverse_
 134 instance Sym_Foldable Repr_Host where
 135         foldMap    = liftM2 Foldable.foldMap
 136         foldr      = liftM3 Foldable.foldr
 137         foldr'     = liftM3 Foldable.foldr'
 138         foldl      = liftM3 Foldable.foldl
 139         foldl'     = liftM3 Foldable.foldl'
 140         null       = liftM  Foldable.null
 141         length     = liftM  Foldable.length
 142         minimum    = liftM  Foldable.minimum
 143         maximum    = liftM  Foldable.maximum
 144         elem       = liftM2 Foldable.elem
 145         sum        = liftM  Foldable.sum
 146         product    = liftM  Foldable.product
 147         toList     = liftM  Foldable.toList
 148         all        = liftM2 Foldable.all
 149         and        = liftM  Foldable.and
 150         any        = liftM2 Foldable.any
 151         concat     = liftM  Foldable.concat
 152         concatMap  = liftM2 Foldable.concatMap
 153         find       = liftM2 Foldable.find
 154         foldlM     = liftM3 Foldable.foldlM
 155         foldrM     = liftM3 Foldable.foldrM
 156         forM_      = liftM2 Foldable.forM_
 157         for_       = liftM2 Foldable.for_
 158         mapM_      = liftM2 Foldable.mapM_
 159         maximumBy  = liftM2 Foldable.maximumBy
 160         minimumBy  = liftM2 Foldable.minimumBy
 161         notElem    = liftM2 Foldable.notElem
 162         or         = liftM  Foldable.or
 163         sequenceA_ = liftM  Foldable.sequenceA_
 164         sequence_  = liftM  Foldable.sequence_
 165         traverse_  = liftM2 Foldable.traverse_
 166 instance Sym_Foldable Repr_Text where
 167         foldMap    = repr_text_app2 "foldMap"
 168         foldr      = repr_text_app3 "foldr"
 169         foldr'     = repr_text_app3 "foldr'"
 170         foldl      = repr_text_app3 "foldl"
 171         foldl'     = repr_text_app3 "foldl'"
 172         null       = repr_text_app1 "null"
 173         length     = repr_text_app1 "length"
 174         minimum    = repr_text_app1 "minimum"
 175         maximum    = repr_text_app1 "maximum"
 176         elem       = repr_text_app2 "elem"
 177         sum        = repr_text_app1 "sum"
 178         product    = repr_text_app1 "product"
 179         toList     = repr_text_app1 "toList"
 180         all        = repr_text_app2 "all"
 181         and        = repr_text_app1 "and"
 182         any        = repr_text_app2 "any"
 183         concat     = repr_text_app1 "concat"
 184         concatMap  = repr_text_app2 "concatMap"
 185         find       = repr_text_app2 "find"
 186         foldlM     = repr_text_app3 "foldlM"
 187         foldrM     = repr_text_app3 "foldrM"
 188         forM_      = repr_text_app2 "forM_"
 189         for_       = repr_text_app2 "for_"
 190         mapM_      = repr_text_app2 "mapM_"
 191         maximumBy  = repr_text_app2 "maximumBy"
 192         minimumBy  = repr_text_app2 "minimumBy"
 193         notElem    = repr_text_app2 "notElem"
 194         or         = repr_text_app1 "or"
 195         sequenceA_ = repr_text_app1 "sequenceA_"
 196         sequence_  = repr_text_app1 "sequence_"
 197         traverse_  = repr_text_app2 "traverse_"
 198 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
 199         foldMap    = repr_dup2 sym_Foldable foldMap
 200         foldr      = repr_dup3 sym_Foldable foldr
 201         foldr'     = repr_dup3 sym_Foldable foldr'
 202         foldl      = repr_dup3 sym_Foldable foldl
 203         foldl'     = repr_dup3 sym_Foldable foldl'
 204         null       = repr_dup1 sym_Foldable null
 205         length     = repr_dup1 sym_Foldable length
 206         minimum    = repr_dup1 sym_Foldable minimum
 207         maximum    = repr_dup1 sym_Foldable maximum
 208         elem       = repr_dup2 sym_Foldable elem
 209         sum        = repr_dup1 sym_Foldable sum
 210         product    = repr_dup1 sym_Foldable product
 211         toList     = repr_dup1 sym_Foldable toList
 212         all        = repr_dup2 sym_Foldable all
 213         and        = repr_dup1 sym_Foldable and
 214         any        = repr_dup2 sym_Foldable any
 215         concat     = repr_dup1 sym_Foldable concat
 216         concatMap  = repr_dup2 sym_Foldable concatMap
 217         find       = repr_dup2 sym_Foldable find
 218         foldlM     = repr_dup3 sym_Foldable foldlM
 219         foldrM     = repr_dup3 sym_Foldable foldrM
 220         forM_      = repr_dup2 sym_Foldable forM_
 221         for_       = repr_dup2 sym_Foldable for_
 222         mapM_      = repr_dup2 sym_Foldable mapM_
 223         maximumBy  = repr_dup2 sym_Foldable maximumBy
 224         minimumBy  = repr_dup2 sym_Foldable minimumBy
 225         notElem    = repr_dup2 sym_Foldable notElem
 226         or         = repr_dup1 sym_Foldable or
 227         sequenceA_ = repr_dup1 sym_Foldable sequenceA_
 228         sequence_  = repr_dup1 sym_Foldable sequence_
 229         traverse_  = repr_dup2 sym_Foldable traverse_
 230
 231 sym_Foldable :: Proxy Sym_Foldable
 232 sym_Foldable = Proxy
 233
 234 -- * Type 'Expr_Foldable'
 235 -- | Expression.
 236 data Expr_Foldable (root:: *)
 237 type instance Root_of_Expr      (Expr_Foldable root)      = root
 238 type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
 239 type instance Sym_of_Expr       (Expr_Foldable root) repr = Sym_Foldable repr
 240 type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr
 241
 242 -- | Parse 'foldMap'.
 243 foldMap_from
 244  :: forall root ty ast hs ret.
 245  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 246  , Expr_From ast root
 247  , Type0_Eq ty
 248  , Type0_Lift   Type_Fun (Type_of_Expr root)
 249  , Type0_Unlift Type_Fun (Type_of_Expr root)
 250  , Type0_Constraint Monoid   ty
 251  , Type1_Constraint Foldable ty
 252  , Type1_Unlift (Type_of_Expr root)
 253  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 254                    (Error_of_Expr ast root)
 255  , Root_of_Expr root ~ root
 256  ) => ast -> ast
 257  -> ExprFrom ast (Expr_Foldable root) hs ret
 258 foldMap_from ast_f ast_ta ex ast ctx k =
 259  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 260         expr_from (Proxy::Proxy root) ast_f ctx $
 261          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 262         expr_from (Proxy::Proxy root) ast_ta ctx $
 263          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 264         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_m) ->
 265         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 266         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 267         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 268         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 269         k ty_f_m $ Forall_Repr_with_Context $
 270          \c -> foldMap (f c) (ta c)
 271
 272 -- | Parse 'foldr' or |foldr'|.
 273 foldr_from
 274  :: forall root ty ast hs ret.
 275  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 276  , Expr_From ast root
 277  , Type0_Eq ty
 278  , Type0_Lift   Type_Fun (Type_of_Expr root)
 279  , Type0_Unlift Type_Fun (Type_of_Expr root)
 280  , Type1_Constraint Foldable ty
 281  , Type1_Unlift (Type_of_Expr root)
 282  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 283                    (Error_of_Expr ast root)
 284  , Root_of_Expr root ~ root
 285  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
 286  -> ast -> ast -> ast
 287  -> ExprFrom ast (Expr_Foldable root) hs ret
 288 foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
 289  -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
 290         expr_from (Proxy::Proxy root) ast_f ctx $
 291          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 292         expr_from (Proxy::Proxy root) ast_b ctx $
 293          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 294         expr_from (Proxy::Proxy root) ast_ta ctx $
 295          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 296         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
 297         check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
 298         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 299         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 300         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 301         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 302         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 303         k ty_b $ Forall_Repr_with_Context $
 304          \c -> fold (f c) (b c) (ta c)
 305
 306 -- | Parse 'foldl' or |foldl'|.
 307 foldl_from
 308  :: forall root ty ast hs ret.
 309  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 310  , Expr_From ast root
 311  , Type0_Eq ty
 312  , Type0_Lift   Type_Fun (Type_of_Expr root)
 313  , Type0_Unlift Type_Fun (Type_of_Expr root)
 314  , Type1_Constraint Foldable ty
 315  , Type1_Unlift (Type_of_Expr root)
 316  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 317                    (Error_of_Expr ast root)
 318  , Root_of_Expr root ~ root
 319  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
 320  -> ast -> ast -> ast
 321  -> ExprFrom ast (Expr_Foldable root) hs ret
 322 foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
 323  -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
 324         expr_from (Proxy::Proxy root) ast_f ctx $
 325          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 326         expr_from (Proxy::Proxy root) ast_b ctx $
 327          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 328         expr_from (Proxy::Proxy root) ast_ta ctx $
 329          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 330         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
 331         check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
 332         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 333         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 334         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 335         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 336         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 337         k ty_b $ Forall_Repr_with_Context $
 338          \c -> fold (f c) (b c) (ta c)
 339
 340 -- | Parse 'length'.
 341 length_from
 342  :: forall root ty ast hs ret.
 343  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 344  , Expr_From ast root
 345  , Type0_Eq ty
 346  , Type0_Lift Type_Int (Type_of_Expr root)
 347  , Type1_Constraint Foldable ty
 348  , Type1_Unlift (Type_of_Expr root)
 349  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 350                    (Error_of_Expr ast root)
 351  , Root_of_Expr root ~ root
 352  ) => ast
 353  -> ExprFrom ast (Expr_Foldable root) hs ret
 354 length_from ast_ta ex ast ctx k =
 355  -- length :: Foldable t => t a -> Int
 356         expr_from (Proxy::Proxy root) ast_ta ctx $
 357          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 358         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 359         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 360         k type_int $ Forall_Repr_with_Context $
 361          \c -> length (ta c)
 362
 363 -- | Parse 'null'.
 364 null_from
 365  :: forall root ty ast hs ret.
 366  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 367  , Expr_From ast root
 368  , Type0_Eq ty
 369  , Type0_Lift Type_Bool (Type_of_Expr root)
 370  , Type1_Constraint Foldable ty
 371  , Type1_Unlift (Type_of_Expr root)
 372  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 373                    (Error_of_Expr ast root)
 374  , Root_of_Expr root ~ root
 375  ) => ast
 376  -> ExprFrom ast (Expr_Foldable root) hs ret
 377 null_from ast_ta ex ast ctx k =
 378  -- null :: Foldable t => t a -> Bool
 379         expr_from (Proxy::Proxy root) ast_ta ctx $
 380          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 381         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 382         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 383         k type_bool $ Forall_Repr_with_Context $
 384          \c -> null (ta c)
 385
 386 -- | Parse 'minimum'.
 387 minimum_from
 388  :: forall root ty ast hs ret.
 389  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 390  , Expr_From ast root
 391  , Type0_Eq ty
 392  , Type0_Constraint Ord      ty
 393  , Type1_Constraint Foldable ty
 394  , Type1_Unlift (Type_of_Expr root)
 395  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 396                    (Error_of_Expr ast root)
 397  , Root_of_Expr root ~ root
 398  ) => ast
 399  -> ExprFrom ast (Expr_Foldable root) hs ret
 400 minimum_from ast_ta ex ast ctx k =
 401  -- minimum :: (Foldable t, Ord a) => t a -> a
 402         expr_from (Proxy::Proxy root) ast_ta ctx $
 403          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 404         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 405         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 406         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 407         k ty_t_a $ Forall_Repr_with_Context $
 408          \c -> minimum (ta c)
 409
 410 -- | Parse 'maximum'.
 411 maximum_from
 412  :: forall root ty ast hs ret.
 413  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 414  , Expr_From ast root
 415  , Type0_Eq ty
 416  , Type0_Constraint Ord      ty
 417  , Type1_Constraint Foldable ty
 418  , Type1_Unlift (Type_of_Expr root)
 419  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 420                    (Error_of_Expr ast root)
 421  , Root_of_Expr root ~ root
 422  ) => ast
 423  -> ExprFrom ast (Expr_Foldable root) hs ret
 424 maximum_from ast_ta ex ast ctx k =
 425  -- maximum :: (Foldable t, Ord a) => t a -> a
 426         expr_from (Proxy::Proxy root) ast_ta ctx $
 427          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 428         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 429         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 430         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 431         k ty_t_a $ Forall_Repr_with_Context $
 432          \c -> maximum (ta c)
 433
 434 -- | Parse 'elem'.
 435 elem_from
 436  :: forall root ty ast hs ret.
 437  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 438  , Expr_From ast root
 439  , Type0_Eq ty
 440  , Type0_Constraint  Eq       ty
 441  , Type0_Lift Type_Bool (Type_of_Expr root)
 442  , Type1_Constraint Foldable ty
 443  , Type1_Unlift (Type_of_Expr root)
 444  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 445                    (Error_of_Expr ast root)
 446  , Root_of_Expr root ~ root
 447  ) => ast -> ast
 448  -> ExprFrom ast (Expr_Foldable root) hs ret
 449 elem_from ast_a ast_ta ex ast ctx k =
 450  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 451         expr_from (Proxy::Proxy root) ast_a ctx $
 452          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 453         expr_from (Proxy::Proxy root) ast_ta ctx $
 454          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 455         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 456         check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
 457         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 458         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 459         k type_bool $ Forall_Repr_with_Context $
 460          \c -> a c `elem` ta c
 461
 462 -- | Parse 'sum'.
 463 sum_from
 464  :: forall root ty ast hs ret.
 465  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 466  , Expr_From ast root
 467  , Type0_Eq ty
 468  , Type0_Constraint Num      ty
 469  , Type1_Constraint Foldable ty
 470  , Type1_Unlift (Type_of_Expr root)
 471  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 472                    (Error_of_Expr ast root)
 473  , Root_of_Expr root ~ root
 474  ) => ast
 475  -> ExprFrom ast (Expr_Foldable root) hs ret
 476 sum_from ast_ta ex ast ctx k =
 477  -- sum :: (Foldable t, Num a) => t a -> a
 478         expr_from (Proxy::Proxy root) ast_ta ctx $
 479          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 480         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 481         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 482         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 483         k ty_t_a $ Forall_Repr_with_Context $
 484          \c -> sum (ta c)
 485
 486 -- | Parse 'product'.
 487 product_from
 488  :: forall root ty ast hs ret.
 489  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 490  , Expr_From ast root
 491  , Type0_Eq ty
 492  , Type0_Constraint Num      ty
 493  , Type1_Constraint Foldable ty
 494  , Type1_Unlift (Type_of_Expr root)
 495  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 496                    (Error_of_Expr ast root)
 497  , Root_of_Expr root ~ root
 498  ) => ast
 499  -> ExprFrom ast (Expr_Foldable root) hs ret
 500 product_from ast_ta ex ast ctx k =
 501  -- product :: (Foldable t, Num a) => t a -> a
 502         expr_from (Proxy::Proxy root) ast_ta ctx $
 503          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 504         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 505         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 506         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 507         k ty_t_a $ Forall_Repr_with_Context $
 508          \c -> product (ta c)
 509
 510 -- | Parse 'toList'.
 511 toList_from
 512  :: forall root ty ast hs ret.
 513  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 514  , Expr_From ast root
 515  , Type0_Eq ty
 516  , Type0_Lift Type_List (Type_of_Expr root)
 517  , Type1_Constraint Foldable ty
 518  , Type1_Unlift (Type_of_Expr root)
 519  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 520                    (Error_of_Expr ast root)
 521  , Root_of_Expr root ~ root
 522  ) => ast
 523  -> ExprFrom ast (Expr_Foldable root) hs ret
 524 toList_from ast_ta ex ast ctx k =
 525  -- toList :: Foldable t => t a -> [a]
 526         expr_from (Proxy::Proxy root) ast_ta ctx $
 527          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 528         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 529         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 530         k (type_list ty_t_a) $ Forall_Repr_with_Context $
 531          \c -> toList (ta c)
 532
 533 -- | Parse 'all'.
 534 all_from
 535  :: forall root ty ast hs ret.
 536  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 537  , Expr_From ast root
 538  , Type0_Eq ty
 539  , Type0_Lift   Type_Bool (Type_of_Expr root)
 540  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 541  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 542  , Type1_Constraint Foldable ty
 543  , Type1_Unlift (Type_of_Expr root)
 544  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 545                    (Error_of_Expr ast root)
 546  , Root_of_Expr root ~ root
 547  ) => ast -> ast
 548  -> ExprFrom ast (Expr_Foldable root) hs ret
 549 all_from ast_f ast_ta ex ast ctx k =
 550  -- all :: Foldable t => (a -> Bool) -> t a -> Bool
 551         expr_from (Proxy::Proxy root) ast_f ctx $
 552          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 553         expr_from (Proxy::Proxy root) ast_ta ctx $
 554          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 555         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
 556         check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
 557         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 558         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 559         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 560         k type_bool $ Forall_Repr_with_Context $
 561          \c -> all (f c) (ta c)
 562
 563 -- | Parse 'any'.
 564 any_from
 565  :: forall root ty ast hs ret.
 566  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 567  , Expr_From ast root
 568  , Type0_Eq ty
 569  , Type0_Lift   Type_Bool (Type_of_Expr root)
 570  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 571  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 572  , Type0_Constraint Num      ty
 573  , Type1_Constraint Foldable ty
 574  , Type1_Unlift (Type_of_Expr root)
 575  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 576                    (Error_of_Expr ast root)
 577  , Root_of_Expr root ~ root
 578  ) => ast -> ast
 579  -> ExprFrom ast (Expr_Foldable root) hs ret
 580 any_from ast_f ast_ta ex ast ctx k =
 581  -- any :: Foldable t => (a -> Bool) -> t a -> Bool
 582         expr_from (Proxy::Proxy root) ast_f ctx $
 583          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 584         expr_from (Proxy::Proxy root) ast_ta ctx $
 585          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 586         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
 587         check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
 588         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 589         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 590         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 591         k type_bool $ Forall_Repr_with_Context $
 592          \c -> any (f c) (ta c)
 593
 594 -- | Parse 'and'.
 595 and_from
 596  :: forall root ty ast hs ret.
 597  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 598  , Expr_From ast root
 599  , Type0_Eq ty
 600  , Type0_Lift Type_Bool (Type_of_Expr root)
 601  , Type1_Constraint Foldable ty
 602  , Type1_Unlift (Type_of_Expr root)
 603  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 604                    (Error_of_Expr ast root)
 605  , Root_of_Expr root ~ root
 606  ) => ast
 607  -> ExprFrom ast (Expr_Foldable root) hs ret
 608 and_from ast_ta ex ast ctx k =
 609  -- and :: Foldable t => t Bool -> Bool
 610         expr_from (Proxy::Proxy root) ast_ta ctx $
 611          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 612         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 613         check_type0_eq ex ast type_bool ty_t_a $ \Refl ->
 614         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 615         k type_bool $ Forall_Repr_with_Context $
 616          \c -> and (ta c)
 617
 618 -- | Parse 'or'.
 619 or_from
 620  :: forall root ty ast hs ret.
 621  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 622  , Expr_From ast root
 623  , Type0_Eq ty
 624  , Type0_Lift Type_Bool (Type_of_Expr root)
 625  , Type1_Constraint Foldable ty
 626  , Type1_Unlift (Type_of_Expr root)
 627  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 628                    (Error_of_Expr ast root)
 629  , Root_of_Expr root ~ root
 630  ) => ast
 631  -> ExprFrom ast (Expr_Foldable root) hs ret
 632 or_from ast_ta ex ast ctx k =
 633  -- or :: Foldable t => t Bool -> Bool
 634         expr_from (Proxy::Proxy root) ast_ta ctx $
 635          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 636         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 637         check_type0_eq ex ast type_bool ty_t_a $ \Refl ->
 638         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 639         k type_bool $ Forall_Repr_with_Context $
 640          \c -> or (ta c)
 641
 642 -- | Parse 'concat'.
 643 concat_from
 644  :: forall root ty ast hs ret.
 645  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 646  , Expr_From ast root
 647  , Type0_Eq ty
 648  , Type0_Lift   Type_List (Type_of_Expr root)
 649  , Type0_Unlift Type_List (Type_of_Expr root)
 650  , Type1_Constraint Foldable ty
 651  , Type1_Unlift (Type_of_Expr root)
 652  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 653                    (Error_of_Expr ast root)
 654  , Root_of_Expr root ~ root
 655  ) => ast
 656  -> ExprFrom ast (Expr_Foldable root) hs ret
 657 concat_from ast_ta ex ast ctx k =
 658  -- concat :: Foldable t => t [a] -> [a]
 659         expr_from (Proxy::Proxy root) ast_ta ctx $
 660          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 661         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 662         check_type_list ex ast ty_t_a $ \Type1{} ->
 663         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 664         k ty_t_a $ Forall_Repr_with_Context $
 665          \c -> concat (ta c)