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 -- | Parse 'foldMap'.
  58 foldMap_from
  59  :: forall root ty ast hs ret.
  60  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
  61  , Eq_Type ty
  62  , Expr_from ast root
  63  , Lift_Type   Type_Fun (Type_of_Expr root)
  64  , Unlift_Type Type_Fun (Type_of_Expr root)
  65  , Unlift_Type1 (Type_of_Expr root)
  66  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  67                    (Error_of_Expr ast root)
  68  , Root_of_Expr root ~ root
  69  , Constraint_Type Monoid ty
  70  , Constraint_Type1 Foldable ty
  71  ) => ast -> ast
  72  -> Expr_From ast (Expr_Foldable root) hs ret
  73 foldMap_from ast_f ast_ta ex ast ctx k =
  74  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
  75         expr_from (Proxy::Proxy root) ast_f ctx $
  76          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
  77         expr_from (Proxy::Proxy root) ast_ta ctx $
  78          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
  79         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_m
  80          :: Type_Fun ty h_f) ->
  81         check_type1 ex ast ty_ta $ \(Type_Type1 _t (ty_t_a::ty h_t_a), Lift_Type1 _ty_t) ->
  82         check_eq_type ex ast ty_f_a ty_t_a $ \Refl ->
  83         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
  84         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
  85         k ty_f_m $ Forall_Repr_with_Context $
  86          \c -> foldMap (f c) (ta c)
  87
  88 -- | Parse 'length'.
  89 length_from
  90  :: forall root ty ast hs ret.
  91  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
  92  , Eq_Type ty
  93  , Expr_from ast root
  94  , Lift_Type Type_Int (Type_of_Expr root)
  95  , Unlift_Type1 (Type_of_Expr root)
  96  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  97                    (Error_of_Expr ast root)
  98  , Root_of_Expr root ~ root
  99  , Constraint_Type1 Foldable ty
 100  ) => ast
 101  -> Expr_From ast (Expr_Foldable root) hs ret
 102 length_from ast_ta ex ast ctx k =
 103  -- length :: Foldable t => t a -> Int
 104         expr_from (Proxy::Proxy root) ast_ta ctx $
 105          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 106         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 107         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 108         k type_int $ Forall_Repr_with_Context $
 109          \c -> length (ta c)
 110
 111 -- | Parse 'null'.
 112 null_from
 113  :: forall root ty ast hs ret.
 114  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 115  , Eq_Type ty
 116  , Expr_from ast root
 117  , Lift_Type Type_Bool (Type_of_Expr root)
 118  , Unlift_Type1 (Type_of_Expr root)
 119  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 120                    (Error_of_Expr ast root)
 121  , Root_of_Expr root ~ root
 122  , Constraint_Type1 Foldable ty
 123  ) => ast
 124  -> Expr_From ast (Expr_Foldable root) hs ret
 125 null_from ast_ta ex ast ctx k =
 126  -- null :: Foldable t => t a -> Bool
 127         expr_from (Proxy::Proxy root) ast_ta ctx $
 128          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 129         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 130         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 131         k type_bool $ Forall_Repr_with_Context $
 132          \c -> null (ta c)
 133
 134 -- | Parse 'minimum'.
 135 minimum_from
 136  :: forall root ty ast hs ret.
 137  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 138  , Eq_Type ty
 139  , Expr_from ast root
 140  , Unlift_Type1 (Type_of_Expr root)
 141  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 142                    (Error_of_Expr ast root)
 143  , Root_of_Expr root ~ root
 144  , Constraint_Type  Ord      ty
 145  , Constraint_Type1 Foldable ty
 146  ) => ast
 147  -> Expr_From ast (Expr_Foldable root) hs ret
 148 minimum_from ast_ta ex ast ctx k =
 149  -- minimum :: (Foldable t, Ord a) => t a -> a
 150         expr_from (Proxy::Proxy root) ast_ta ctx $
 151          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 152         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 153         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 154         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 155         k ty_t_a $ Forall_Repr_with_Context $
 156          \c -> minimum (ta c)
 157
 158 -- | Parse 'maximum'.
 159 maximum_from
 160  :: forall root ty ast hs ret.
 161  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 162  , Eq_Type ty
 163  , Expr_from ast root
 164  , Unlift_Type1 (Type_of_Expr root)
 165  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 166                    (Error_of_Expr ast root)
 167  , Root_of_Expr root ~ root
 168  , Constraint_Type  Ord      ty
 169  , Constraint_Type1 Foldable ty
 170  ) => ast
 171  -> Expr_From ast (Expr_Foldable root) hs ret
 172 maximum_from ast_ta ex ast ctx k =
 173  -- maximum :: (Foldable t, Ord a) => t a -> a
 174         expr_from (Proxy::Proxy root) ast_ta ctx $
 175          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 176         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 177         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 178         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 179         k ty_t_a $ Forall_Repr_with_Context $
 180          \c -> maximum (ta c)
 181
 182 -- | Parse 'elem'.
 183 elem_from
 184  :: forall root ty ast hs ret.
 185  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 186  , Eq_Type ty
 187  , Expr_from ast root
 188  , Lift_Type Type_Bool (Type_of_Expr root)
 189  , Unlift_Type1 (Type_of_Expr root)
 190  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 191                    (Error_of_Expr ast root)
 192  , Root_of_Expr root ~ root
 193  , Constraint_Type  Eq       ty
 194  , Constraint_Type1 Foldable ty
 195  ) => ast -> ast
 196  -> Expr_From ast (Expr_Foldable root) hs ret
 197 elem_from ast_a ast_ta ex ast ctx k =
 198  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 199         expr_from (Proxy::Proxy root) ast_a ctx $
 200          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 201         expr_from (Proxy::Proxy root) ast_ta ctx $
 202          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 203         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 204         check_eq_type ex ast ty_a ty_t_a $ \Refl ->
 205         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 206         check_constraint_type ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 207         k type_bool $ Forall_Repr_with_Context $
 208          \c -> a c `elem` ta c