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.Trans.Common
  32
  33 -- * Class 'Sym_Foldable'
  34 -- | Symantic.
  35 class Sym_Foldable repr where
  36         foldMap    :: (Foldable f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
  37         foldr      :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  38         foldr'     :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
  39         foldl      :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  40         foldl'     :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
  41         length     :: Foldable f => repr (f a) -> repr Int
  42         null       :: Foldable f => repr (f a) -> repr Bool
  43         minimum    :: (Foldable f, Ord a) => repr (f a) -> repr a
  44         maximum    :: (Foldable f, Ord a) => repr (f a) -> repr a
  45         elem       :: (Foldable f, Eq  a) => repr a -> repr (f a) -> repr Bool
  46         sum        :: (Foldable f, Num a) => repr (f a) -> repr a
  47         product    :: (Foldable f, Num a) => repr (f a) -> repr a
  48         toList     :: Foldable f => repr (f a) -> repr [a]
  49         all        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
  50         and        :: Foldable f => repr (f Bool) -> repr Bool
  51         any        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
  52         concat     :: Foldable f => repr (f [a]) -> repr [a]
  53         concatMap  :: Foldable f => repr (a -> [b]) -> repr (f a) -> repr [b]
  54         find       :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr (Maybe a)
  55         foldlM     :: (Foldable f, Monad m) => repr (b -> a -> m b) -> repr b -> repr (f a) -> repr (m b)
  56         foldrM     :: (Foldable f, Monad m) => repr (a -> b -> m b) -> repr b -> repr (f a) -> repr (m b)
  57         forM_      :: (Foldable f, Monad m) => repr (f a) -> repr (a -> m b) -> repr (m ())
  58         for_       :: (Foldable f, Applicative p) => repr (f a) -> repr (a -> p b) -> repr (p ())
  59         mapM_      :: (Foldable f, Monad m) => repr (a -> m b) -> repr (f a) -> repr (m ())
  60         maximumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
  61         minimumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
  62         notElem    :: (Foldable f, Eq a) => repr a -> repr (f a) -> repr Bool
  63         or         :: Foldable f => repr (f Bool) -> repr Bool
  64         sequenceA_ :: (Foldable f, Applicative p) => repr (f (p a)) -> repr (p ())
  65         sequence_  :: (Foldable f, Monad m) => repr (f (m a)) -> repr (m ())
  66         traverse_  :: (Foldable f, Applicative p) => repr (a -> p b) -> repr (f a) -> repr (p ())
  67         -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
  68         -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
  69
  70         default foldMap    :: (Trans t repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
  71         default foldr      :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
  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 foldl      :: (Trans t repr, Foldable f) => t repr (b -> a -> 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 length     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
  76         default null       :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
  77         default minimum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  78         default maximum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
  79         default elem       :: (Trans t repr, Foldable f, Eq  a) => t repr a -> t repr (f a) -> t repr Bool
  80         default sum        :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  81         default product    :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
  82         default toList     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
  83         default all        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
  84         default and        :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
  85         default any        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
  86         default concat     :: (Trans t repr, Foldable f) => t repr (f [a]) -> t repr [a]
  87         default concatMap  :: (Trans t repr, Foldable f) => t repr (a -> [b]) -> t repr (f a) -> t repr [b]
  88         default find       :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr (Maybe a)
  89         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)
  90         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)
  91         default forM_      :: (Trans t repr, Foldable f, Monad m) => t repr (f a) -> t repr (a -> m b) -> t repr (m ())
  92         default for_       :: (Trans t repr, Foldable f, Applicative p) => t repr (f a) -> t repr (a -> p b) -> t repr (p ())
  93         default mapM_      :: (Trans t repr, Foldable f, Monad m) => t repr (a -> m b) -> t repr (f a) -> t repr (m ())
  94         default maximumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
  95         default minimumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
  96         default notElem    :: (Trans t repr, Foldable f, Eq a) => t repr a -> t repr (f a) -> t repr Bool
  97         default or         :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
  98         default sequenceA_ :: (Trans t repr, Foldable f, Applicative p) => t repr (f (p a)) -> t repr (p ())
  99         default sequence_  :: (Trans t repr, Foldable f, Monad m) => t repr (f (m a)) -> t repr (m ())
 100         default traverse_  :: (Trans t repr, Foldable f, Applicative p) => t repr (a -> p b) -> t repr (f a) -> t repr (p ())
 101
 102         foldMap    = trans_map2 foldMap
 103         foldr      = trans_map3 foldr
 104         foldr'     = trans_map3 foldr'
 105         foldl      = trans_map3 foldl
 106         foldl'     = trans_map3 foldl'
 107         length     = trans_map1 length
 108         null       = trans_map1 null
 109         minimum    = trans_map1 minimum
 110         maximum    = trans_map1 maximum
 111         elem       = trans_map2 elem
 112         sum        = trans_map1 sum
 113         product    = trans_map1 product
 114         toList     = trans_map1 toList
 115         all        = trans_map2 all
 116         and        = trans_map1 and
 117         any        = trans_map2 any
 118         concat     = trans_map1 concat
 119         concatMap  = trans_map2 concatMap
 120         find       = trans_map2 find
 121         foldlM     = trans_map3 foldlM
 122         foldrM     = trans_map3 foldrM
 123         forM_      = trans_map2 forM_
 124         for_       = trans_map2 for_
 125         mapM_      = trans_map2 mapM_
 126         maximumBy  = trans_map2 maximumBy
 127         minimumBy  = trans_map2 minimumBy
 128         notElem    = trans_map2 notElem
 129         or         = trans_map1 or
 130         sequenceA_ = trans_map1 sequenceA_
 131         sequence_  = trans_map1 sequence_
 132         traverse_  = trans_map2 traverse_
 133 instance Sym_Foldable Repr_Host where
 134         foldMap    = liftM2 Foldable.foldMap
 135         foldr      = liftM3 Foldable.foldr
 136         foldr'     = liftM3 Foldable.foldr'
 137         foldl      = liftM3 Foldable.foldl
 138         foldl'     = liftM3 Foldable.foldl'
 139         null       = liftM  Foldable.null
 140         length     = liftM  Foldable.length
 141         minimum    = liftM  Foldable.minimum
 142         maximum    = liftM  Foldable.maximum
 143         elem       = liftM2 Foldable.elem
 144         sum        = liftM  Foldable.sum
 145         product    = liftM  Foldable.product
 146         toList     = liftM  Foldable.toList
 147         all        = liftM2 Foldable.all
 148         and        = liftM  Foldable.and
 149         any        = liftM2 Foldable.any
 150         concat     = liftM  Foldable.concat
 151         concatMap  = liftM2 Foldable.concatMap
 152         find       = liftM2 Foldable.find
 153         foldlM     = liftM3 Foldable.foldlM
 154         foldrM     = liftM3 Foldable.foldrM
 155         forM_      = liftM2 Foldable.forM_
 156         for_       = liftM2 Foldable.for_
 157         mapM_      = liftM2 Foldable.mapM_
 158         maximumBy  = liftM2 Foldable.maximumBy
 159         minimumBy  = liftM2 Foldable.minimumBy
 160         notElem    = liftM2 Foldable.notElem
 161         or         = liftM  Foldable.or
 162         sequenceA_ = liftM  Foldable.sequenceA_
 163         sequence_  = liftM  Foldable.sequence_
 164         traverse_  = liftM2 Foldable.traverse_
 165 instance Sym_Foldable Repr_Text where
 166         foldMap    = repr_text_app2 "foldMap"
 167         foldr      = repr_text_app3 "foldr"
 168         foldr'     = repr_text_app3 "foldr'"
 169         foldl      = repr_text_app3 "foldl"
 170         foldl'     = repr_text_app3 "foldl'"
 171         null       = repr_text_app1 "null"
 172         length     = repr_text_app1 "length"
 173         minimum    = repr_text_app1 "minimum"
 174         maximum    = repr_text_app1 "maximum"
 175         elem       = repr_text_app2 "elem"
 176         sum        = repr_text_app1 "sum"
 177         product    = repr_text_app1 "product"
 178         toList     = repr_text_app1 "toList"
 179         all        = repr_text_app2 "all"
 180         and        = repr_text_app1 "and"
 181         any        = repr_text_app2 "any"
 182         concat     = repr_text_app1 "concat"
 183         concatMap  = repr_text_app2 "concatMap"
 184         find       = repr_text_app2 "find"
 185         foldlM     = repr_text_app3 "foldlM"
 186         foldrM     = repr_text_app3 "foldrM"
 187         forM_      = repr_text_app2 "forM_"
 188         for_       = repr_text_app2 "for_"
 189         mapM_      = repr_text_app2 "mapM_"
 190         maximumBy  = repr_text_app2 "maximumBy"
 191         minimumBy  = repr_text_app2 "minimumBy"
 192         notElem    = repr_text_app2 "notElem"
 193         or         = repr_text_app1 "or"
 194         sequenceA_ = repr_text_app1 "sequenceA_"
 195         sequence_  = repr_text_app1 "sequence_"
 196         traverse_  = repr_text_app2 "traverse_"
 197 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
 198         foldMap    = repr_dup2 sym_Foldable foldMap
 199         foldr      = repr_dup3 sym_Foldable foldr
 200         foldr'     = repr_dup3 sym_Foldable foldr'
 201         foldl      = repr_dup3 sym_Foldable foldl
 202         foldl'     = repr_dup3 sym_Foldable foldl'
 203         null       = repr_dup1 sym_Foldable null
 204         length     = repr_dup1 sym_Foldable length
 205         minimum    = repr_dup1 sym_Foldable minimum
 206         maximum    = repr_dup1 sym_Foldable maximum
 207         elem       = repr_dup2 sym_Foldable elem
 208         sum        = repr_dup1 sym_Foldable sum
 209         product    = repr_dup1 sym_Foldable product
 210         toList     = repr_dup1 sym_Foldable toList
 211         all        = repr_dup2 sym_Foldable all
 212         and        = repr_dup1 sym_Foldable and
 213         any        = repr_dup2 sym_Foldable any
 214         concat     = repr_dup1 sym_Foldable concat
 215         concatMap  = repr_dup2 sym_Foldable concatMap
 216         find       = repr_dup2 sym_Foldable find
 217         foldlM     = repr_dup3 sym_Foldable foldlM
 218         foldrM     = repr_dup3 sym_Foldable foldrM
 219         forM_      = repr_dup2 sym_Foldable forM_
 220         for_       = repr_dup2 sym_Foldable for_
 221         mapM_      = repr_dup2 sym_Foldable mapM_
 222         maximumBy  = repr_dup2 sym_Foldable maximumBy
 223         minimumBy  = repr_dup2 sym_Foldable minimumBy
 224         notElem    = repr_dup2 sym_Foldable notElem
 225         or         = repr_dup1 sym_Foldable or
 226         sequenceA_ = repr_dup1 sym_Foldable sequenceA_
 227         sequence_  = repr_dup1 sym_Foldable sequence_
 228         traverse_  = repr_dup2 sym_Foldable traverse_
 229
 230 sym_Foldable :: Proxy Sym_Foldable
 231 sym_Foldable = Proxy
 232
 233 -- * Type 'Expr_Foldable'
 234 -- | Expression.
 235 data Expr_Foldable (root:: *)
 236 type instance Root_of_Expr      (Expr_Foldable root)      = root
 237 type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
 238 type instance Sym_of_Expr       (Expr_Foldable root) repr = (Sym_Foldable repr)
 239 type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr
 240
 241 -- | Parse 'foldMap'.
 242 foldMap_from
 243  :: forall root ty ast hs ret.
 244  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 245  , Expr_From ast root
 246  , Type0_Eq ty
 247  , Type0_Lift   Type_Fun (Type_of_Expr root)
 248  , Type0_Unlift Type_Fun (Type_of_Expr root)
 249  , Type0_Constraint Monoid   ty
 250  , Type1_Constraint Foldable ty
 251  , Type1_Unlift (Type_of_Expr root)
 252  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 253                    (Error_of_Expr ast root)
 254  , Root_of_Expr root ~ root
 255  ) => ast -> ast
 256  -> ExprFrom ast (Expr_Foldable root) hs ret
 257 foldMap_from ast_f ast_ta ex ast ctx k =
 258  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 259         expr_from (Proxy::Proxy root) ast_f ctx $
 260          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 261         expr_from (Proxy::Proxy root) ast_ta ctx $
 262          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 263         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_m) ->
 264         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 265         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 266         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 267         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 268         k ty_f_m $ Forall_Repr_with_Context $
 269          \c -> foldMap (f c) (ta c)
 270
 271 -- | Parse 'foldr' or |foldr'|.
 272 foldr_from
 273  :: forall root ty ast hs ret.
 274  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 275  , Expr_From ast root
 276  , Type0_Eq ty
 277  , Type0_Lift   Type_Fun (Type_of_Expr root)
 278  , Type0_Unlift Type_Fun (Type_of_Expr root)
 279  , Type1_Constraint Foldable ty
 280  , Type1_Unlift (Type_of_Expr root)
 281  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 282                    (Error_of_Expr ast root)
 283  , Root_of_Expr root ~ root
 284  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
 285  -> ast -> ast -> ast
 286  -> ExprFrom ast (Expr_Foldable root) hs ret
 287 foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
 288  -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
 289         expr_from (Proxy::Proxy root) ast_f ctx $
 290          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 291         expr_from (Proxy::Proxy root) ast_b ctx $
 292          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 293         expr_from (Proxy::Proxy root) ast_ta ctx $
 294          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 295         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
 296         check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
 297         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 298         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 299         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 300         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 301         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 302         k ty_b $ Forall_Repr_with_Context $
 303          \c -> fold (f c) (b c) (ta c)
 304
 305 -- | Parse 'foldl' or |foldl'|.
 306 foldl_from
 307  :: forall root ty ast hs ret.
 308  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 309  , Expr_From ast root
 310  , Type0_Eq ty
 311  , Type0_Lift   Type_Fun (Type_of_Expr root)
 312  , Type0_Unlift Type_Fun (Type_of_Expr root)
 313  , Type1_Constraint Foldable ty
 314  , Type1_Unlift (Type_of_Expr root)
 315  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 316                    (Error_of_Expr ast root)
 317  , Root_of_Expr root ~ root
 318  ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
 319  -> ast -> ast -> ast
 320  -> ExprFrom ast (Expr_Foldable root) hs ret
 321 foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
 322  -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
 323         expr_from (Proxy::Proxy root) ast_f ctx $
 324          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 325         expr_from (Proxy::Proxy root) ast_b ctx $
 326          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 327         expr_from (Proxy::Proxy root) ast_ta ctx $
 328          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 329         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
 330         check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
 331         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 332         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 333         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 334         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 335         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 336         k ty_b $ Forall_Repr_with_Context $
 337          \c -> fold (f c) (b c) (ta c)
 338
 339 -- | Parse 'length'.
 340 length_from
 341  :: forall root ty ast hs ret.
 342  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 343  , Expr_From ast root
 344  , Type0_Eq ty
 345  , Type0_Lift Type_Int (Type_of_Expr root)
 346  , Type1_Constraint Foldable ty
 347  , Type1_Unlift (Type_of_Expr root)
 348  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 349                    (Error_of_Expr ast root)
 350  , Root_of_Expr root ~ root
 351  ) => ast
 352  -> ExprFrom ast (Expr_Foldable root) hs ret
 353 length_from ast_ta ex ast ctx k =
 354  -- length :: Foldable t => t a -> Int
 355         expr_from (Proxy::Proxy root) ast_ta ctx $
 356          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 357         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 358         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 359         k type_int $ Forall_Repr_with_Context $
 360          \c -> length (ta c)
 361
 362 -- | Parse 'null'.
 363 null_from
 364  :: forall root ty ast hs ret.
 365  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 366  , Expr_From ast root
 367  , Type0_Eq ty
 368  , Type0_Lift Type_Bool (Type_of_Expr root)
 369  , Type1_Constraint Foldable ty
 370  , Type1_Unlift (Type_of_Expr root)
 371  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 372                    (Error_of_Expr ast root)
 373  , Root_of_Expr root ~ root
 374  ) => ast
 375  -> ExprFrom ast (Expr_Foldable root) hs ret
 376 null_from ast_ta ex ast ctx k =
 377  -- null :: Foldable t => t a -> Bool
 378         expr_from (Proxy::Proxy root) ast_ta ctx $
 379          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 380         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 381         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 382         k type_bool $ Forall_Repr_with_Context $
 383          \c -> null (ta c)
 384
 385 -- | Parse 'minimum'.
 386 minimum_from
 387  :: forall root ty ast hs ret.
 388  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 389  , Expr_From ast root
 390  , Type0_Eq ty
 391  , Type0_Constraint Ord      ty
 392  , Type1_Constraint Foldable ty
 393  , Type1_Unlift (Type_of_Expr root)
 394  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 395                    (Error_of_Expr ast root)
 396  , Root_of_Expr root ~ root
 397  ) => ast
 398  -> ExprFrom ast (Expr_Foldable root) hs ret
 399 minimum_from ast_ta ex ast ctx k =
 400  -- minimum :: (Foldable t, Ord a) => t a -> a
 401         expr_from (Proxy::Proxy root) ast_ta ctx $
 402          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 403         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 404         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 405         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 406         k ty_t_a $ Forall_Repr_with_Context $
 407          \c -> minimum (ta c)
 408
 409 -- | Parse 'maximum'.
 410 maximum_from
 411  :: forall root ty ast hs ret.
 412  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 413  , Expr_From ast root
 414  , Type0_Eq ty
 415  , Type0_Constraint Ord      ty
 416  , Type1_Constraint Foldable ty
 417  , Type1_Unlift (Type_of_Expr root)
 418  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 419                    (Error_of_Expr ast root)
 420  , Root_of_Expr root ~ root
 421  ) => ast
 422  -> ExprFrom ast (Expr_Foldable root) hs ret
 423 maximum_from ast_ta ex ast ctx k =
 424  -- maximum :: (Foldable t, Ord a) => t a -> a
 425         expr_from (Proxy::Proxy root) ast_ta ctx $
 426          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 427         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 428         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 429         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 430         k ty_t_a $ Forall_Repr_with_Context $
 431          \c -> maximum (ta c)
 432
 433 -- | Parse 'elem'.
 434 elem_from
 435  :: forall root ty ast hs ret.
 436  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 437  , Expr_From ast root
 438  , Type0_Eq ty
 439  , Type0_Constraint  Eq       ty
 440  , Type0_Lift Type_Bool (Type_of_Expr root)
 441  , Type1_Constraint Foldable ty
 442  , Type1_Unlift (Type_of_Expr root)
 443  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 444                    (Error_of_Expr ast root)
 445  , Root_of_Expr root ~ root
 446  ) => ast -> ast
 447  -> ExprFrom ast (Expr_Foldable root) hs ret
 448 elem_from ast_a ast_ta ex ast ctx k =
 449  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 450         expr_from (Proxy::Proxy root) ast_a ctx $
 451          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 452         expr_from (Proxy::Proxy root) ast_ta ctx $
 453          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 454         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 455         check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
 456         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 457         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 458         k type_bool $ Forall_Repr_with_Context $
 459          \c -> a c `elem` ta c
 460
 461 -- | Parse 'sum'.
 462 sum_from
 463  :: forall root ty ast hs ret.
 464  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 465  , Expr_From ast root
 466  , Type0_Eq ty
 467  , Type0_Constraint Num      ty
 468  , Type1_Constraint Foldable ty
 469  , Type1_Unlift (Type_of_Expr root)
 470  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 471                    (Error_of_Expr ast root)
 472  , Root_of_Expr root ~ root
 473  ) => ast
 474  -> ExprFrom ast (Expr_Foldable root) hs ret
 475 sum_from ast_ta ex ast ctx k =
 476  -- sum :: (Foldable t, Num a) => t a -> a
 477         expr_from (Proxy::Proxy root) ast_ta ctx $
 478          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 479         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 480         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 481         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 482         k ty_t_a $ Forall_Repr_with_Context $
 483          \c -> sum (ta c)
 484
 485 -- | Parse 'product'.
 486 product_from
 487  :: forall root ty ast hs ret.
 488  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 489  , Expr_From ast root
 490  , Type0_Eq ty
 491  , Type0_Constraint Num      ty
 492  , Type1_Constraint Foldable ty
 493  , Type1_Unlift (Type_of_Expr root)
 494  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 495                    (Error_of_Expr ast root)
 496  , Root_of_Expr root ~ root
 497  ) => ast
 498  -> ExprFrom ast (Expr_Foldable root) hs ret
 499 product_from ast_ta ex ast ctx k =
 500  -- product :: (Foldable t, Num a) => t a -> a
 501         expr_from (Proxy::Proxy root) ast_ta ctx $
 502          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 503         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 504         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 505         check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
 506         k ty_t_a $ Forall_Repr_with_Context $
 507          \c -> product (ta c)
 508
 509 -- | Parse 'toList'.
 510 toList_from
 511  :: forall root ty ast hs ret.
 512  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 513  , Expr_From ast root
 514  , Type0_Eq ty
 515  , Type0_Lift Type_List (Type_of_Expr root)
 516  , Type0_Constraint Num      ty
 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)