Language/Symantic/Expr/Foldable.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 -- | Expression for 'Foldable'.
  12 module Language.Symantic.Expr.Foldable where
  13
  14 import Data.Foldable (Foldable)
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import Prelude hiding ((<$>), Foldable(..))
  18
  19 import Language.Symantic.Type
  20 import Language.Symantic.Trans.Common
  21 import Language.Symantic.Expr.Root
  22 import Language.Symantic.Expr.Error
  23 import Language.Symantic.Expr.From
  24 import Language.Symantic.Expr.Lambda
  25
  26 -- * Class 'Sym_Foldable'
  27 -- | Symantic.
  28 class Sym_Foldable repr where
  29         foldMap :: (Foldable t, Monoid m) => repr ((->) a m) -> repr (t a) -> repr m
  30         length  :: Foldable t => repr (t a) -> repr Int
  31         null    :: Foldable t => repr (t a) -> repr Bool
  32         minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
  33         maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
  34         elem    :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
  35         default foldMap :: (Trans tr repr, Foldable t, Monoid m)
  36          => tr repr ((->) a m) -> tr repr (t a) -> tr repr m
  37         default length  :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
  38         default null    :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
  39         default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  40         default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  41         default elem    :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
  42         foldMap = trans_map2 foldMap
  43         length  = trans_map1 length
  44         null    = trans_map1 null
  45         minimum = trans_map1 minimum
  46         maximum = trans_map1 maximum
  47         elem    = trans_map2 elem
  48
  49 -- * Type 'Expr_Foldable'
  50 -- | Expression.
  51 data Expr_Foldable (root:: *)
  52 type instance Root_of_Expr      (Expr_Foldable root)      = root
  53 type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
  54 type instance Sym_of_Expr       (Expr_Foldable root) repr = (Sym_Foldable repr)
  55 type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr
  56
  57 instance Constraint_Type1 Foldable (Type_Type0 px root)
  58 instance Constraint_Type1 Foldable (Type_Var1 root)
  59
  60 -- | Parse 'foldMap'.
  61 foldMap_from
  62  :: forall root ty ast hs ret.
  63  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
  64  , Eq_Type ty
  65  , Expr_from ast root
  66  , Lift_Type   Type_Fun (Type_of_Expr root)
  67  , Unlift_Type Type_Fun (Type_of_Expr root)
  68  , Unlift_Type1 (Type_of_Expr root)
  69  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  70                    (Error_of_Expr ast root)
  71  , Root_of_Expr root ~ root
  72  , Constraint_Type Monoid ty
  73  , Constraint_Type1 Foldable ty
  74  ) => ast -> ast
  75  -> Expr_From ast (Expr_Foldable root) hs ret
  76 foldMap_from ast_f ast_ta ex ast ctx k =
  77  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
  78         expr_from (Proxy::Proxy root) ast_f ctx $
  79          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
  80         expr_from (Proxy::Proxy root) ast_ta ctx $
  81          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
  82         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_m
  83          :: Type_Fun ty h_f) ->
  84         check_type1 ex ast ty_ta $ \(Type_Type1 _t (ty_t_a::ty h_t_a), Lift_Type1 _ty_t) ->
  85         check_eq_type ex ast ty_f_a ty_t_a $ \Refl ->
  86         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
  87         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
  88         k ty_f_m $ Forall_Repr_with_Context $
  89          \c -> foldMap (f c) (ta c)
  90
  91 -- | Parse 'length'.
  92 length_from
  93  :: forall root ty ast hs ret.
  94  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
  95  , Eq_Type ty
  96  , Expr_from ast root
  97  , Lift_Type Type_Int (Type_of_Expr root)
  98  , Unlift_Type1 (Type_of_Expr root)
  99  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 100                    (Error_of_Expr ast root)
 101  , Root_of_Expr root ~ root
 102  , Constraint_Type1 Foldable ty
 103  ) => ast
 104  -> Expr_From ast (Expr_Foldable root) hs ret
 105 length_from ast_ta ex ast ctx k =
 106  -- length :: Foldable t => t a -> Int
 107         expr_from (Proxy::Proxy root) ast_ta ctx $
 108          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 109         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 110         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 111         k type_int $ Forall_Repr_with_Context $
 112          \c -> length (ta c)
 113
 114 -- | Parse 'null'.
 115 null_from
 116  :: forall root ty ast hs ret.
 117  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 118  , Eq_Type ty
 119  , Expr_from ast root
 120  , Lift_Type Type_Bool (Type_of_Expr root)
 121  , Unlift_Type1 (Type_of_Expr root)
 122  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 123                    (Error_of_Expr ast root)
 124  , Root_of_Expr root ~ root
 125  , Constraint_Type1 Foldable ty
 126  ) => ast
 127  -> Expr_From ast (Expr_Foldable root) hs ret
 128 null_from ast_ta ex ast ctx k =
 129  -- null :: Foldable t => t a -> Bool
 130         expr_from (Proxy::Proxy root) ast_ta ctx $
 131          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 132         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 133         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 134         k type_bool $ Forall_Repr_with_Context $
 135          \c -> null (ta c)
 136
 137 -- | Parse 'minimum'.
 138 minimum_from
 139  :: forall root ty ast hs ret.
 140  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 141  , Eq_Type ty
 142  , Expr_from ast root
 143  , Unlift_Type1 (Type_of_Expr root)
 144  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 145                    (Error_of_Expr ast root)
 146  , Root_of_Expr root ~ root
 147  , Constraint_Type  Ord      ty
 148  , Constraint_Type1 Foldable ty
 149  ) => ast
 150  -> Expr_From ast (Expr_Foldable root) hs ret
 151 minimum_from ast_ta ex ast ctx k =
 152  -- minimum :: (Foldable t, Ord a) => t a -> a
 153         expr_from (Proxy::Proxy root) ast_ta ctx $
 154          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 155         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 156         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 157         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 158         k ty_t_a $ Forall_Repr_with_Context $
 159          \c -> minimum (ta c)
 160
 161 -- | Parse 'maximum'.
 162 maximum_from
 163  :: forall root ty ast hs ret.
 164  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 165  , Eq_Type ty
 166  , Expr_from ast root
 167  , Unlift_Type1 (Type_of_Expr root)
 168  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 169                    (Error_of_Expr ast root)
 170  , Root_of_Expr root ~ root
 171  , Constraint_Type  Ord      ty
 172  , Constraint_Type1 Foldable ty
 173  ) => ast
 174  -> Expr_From ast (Expr_Foldable root) hs ret
 175 maximum_from ast_ta ex ast ctx k =
 176  -- maximum :: (Foldable t, Ord a) => t a -> a
 177         expr_from (Proxy::Proxy root) ast_ta ctx $
 178          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 179         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 180         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 181         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 182         k ty_t_a $ Forall_Repr_with_Context $
 183          \c -> maximum (ta c)
 184
 185 -- | Parse 'elem'.
 186 elem_from
 187  :: forall root ty ast hs ret.
 188  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 189  , Eq_Type ty
 190  , Expr_from ast root
 191  , Lift_Type Type_Bool (Type_of_Expr root)
 192  , Unlift_Type1 (Type_of_Expr root)
 193  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 194                    (Error_of_Expr ast root)
 195  , Root_of_Expr root ~ root
 196  , Constraint_Type  Eq       ty
 197  , Constraint_Type1 Foldable ty
 198  ) => ast -> ast
 199  -> Expr_From ast (Expr_Foldable root) hs ret
 200 elem_from ast_a ast_ta ex ast ctx k =
 201  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 202         expr_from (Proxy::Proxy root) ast_a ctx $
 203          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 204         expr_from (Proxy::Proxy root) ast_ta ctx $
 205          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 206         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 207         check_eq_type ex ast ty_a ty_t_a $ \Refl ->
 208         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 209         check_constraint_type ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 210         k type_bool $ Forall_Repr_with_Context $
 211          \c -> a c `elem` ta c