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