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_Lam (Lambda_from_Repr repr) repr => Sym_Foldable repr where
  29         length  :: Foldable t => repr (t a) -> repr Int
  30         null    :: Foldable t => repr (t a) -> repr Bool
  31         minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
  32         maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
  33         elem    :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
  34         default length  :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
  35         default null    :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
  36         default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  37         default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  38         default elem    :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
  39         length  = trans_map1 length
  40         null    = trans_map1 null
  41         minimum = trans_map1 minimum
  42         maximum = trans_map1 maximum
  43         elem    = trans_map2 elem
  44
  45 -- * Class 'Sym_Foldable_Lam'
  46 -- | Symantic requiring a 'Lambda'.
  47 class Sym_Foldable_Lam lam repr where
  48         foldMap :: (Foldable t, Monoid m) => repr (Lambda lam a m) -> repr (t a) -> repr m
  49         default foldMap :: (Trans tr repr, Foldable t, Monoid m)
  50          => tr repr (Lambda lam a m) -> tr repr (t a) -> tr repr m
  51         foldMap = trans_map2 foldMap
  52
  53 -- * Type 'Expr_Foldable'
  54 -- | Expression.
  55 data Expr_Foldable (lam:: * -> *) (root:: *)
  56 type instance Root_of_Expr      (Expr_Foldable lam root)      = root
  57 type instance Type_of_Expr      (Expr_Foldable lam root)      = No_Type
  58 type instance Sym_of_Expr       (Expr_Foldable lam root) repr = (Sym_Foldable repr, Sym_Foldable_Lam lam repr)
  59 type instance Error_of_Expr ast (Expr_Foldable lam root)      = No_Error_Expr
  60
  61 instance Constraint_Type1 Foldable (Type_Type0 px root)
  62 instance Constraint_Type1 Foldable (Type_Var1 root)
  63
  64 -- | Parse 'length'.
  65 length_from
  66  :: forall root ty lam ast hs ret.
  67  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam root)
  68  , Eq_Type ty
  69  , Expr_from ast root
  70  , Lift_Type Type_Int (Type_of_Expr root)
  71  , Unlift_Type1 (Type_of_Expr root)
  72  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  73                    (Error_of_Expr ast root)
  74  , Root_of_Expr root ~ root
  75  , Constraint_Type1 Foldable ty
  76  ) => ast
  77  -> Expr_From ast (Expr_Foldable lam root) hs ret
  78 length_from ast_ta ex ast ctx k =
  79  -- length :: Foldable t => t a -> Int
  80         expr_from (Proxy::Proxy root) ast_ta ctx $
  81          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
  82         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
  83         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
  84         k type_int $ Forall_Repr_with_Context $
  85          \c -> length (ta c)
  86
  87 -- | Parse 'null'.
  88 null_from
  89  :: forall root ty lam ast hs ret.
  90  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam root)
  91  , Eq_Type ty
  92  , Expr_from ast root
  93  , Lift_Type Type_Bool (Type_of_Expr root)
  94  , Unlift_Type1 (Type_of_Expr root)
  95  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  96                    (Error_of_Expr ast root)
  97  , Root_of_Expr root ~ root
  98  , Constraint_Type1 Foldable ty
  99  ) => ast
 100  -> Expr_From ast (Expr_Foldable lam root) hs ret
 101 null_from ast_ta ex ast ctx k =
 102  -- null :: Foldable t => t a -> Bool
 103         expr_from (Proxy::Proxy root) ast_ta ctx $
 104          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 105         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 106         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 107         k type_bool $ Forall_Repr_with_Context $
 108          \c -> null (ta c)
 109
 110 -- | Parse 'minimum'.
 111 minimum_from
 112  :: forall root ty lam ast hs ret.
 113  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam root)
 114  , Eq_Type ty
 115  , Expr_from ast root
 116  , Unlift_Type1 (Type_of_Expr root)
 117  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 118                    (Error_of_Expr ast root)
 119  , Root_of_Expr root ~ root
 120  , Constraint_Type  Ord      ty
 121  , Constraint_Type1 Foldable ty
 122  ) => ast
 123  -> Expr_From ast (Expr_Foldable lam root) hs ret
 124 minimum_from ast_ta ex ast ctx k =
 125  -- minimum :: (Foldable t, Ord a) => t a -> a
 126         expr_from (Proxy::Proxy root) ast_ta ctx $
 127          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 128         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 129         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 130         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 131         k ty_t_a $ Forall_Repr_with_Context $
 132          \c -> minimum (ta c)
 133
 134 -- | Parse 'maximum'.
 135 maximum_from
 136  :: forall root ty lam ast hs ret.
 137  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam 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 lam root) hs ret
 148 maximum_from ast_ta ex ast ctx k =
 149  -- maximum :: (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 -> maximum (ta c)
 157
 158 -- | Parse 'elem'.
 159 elem_from
 160  :: forall root ty lam ast hs ret.
 161  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam root)
 162  , Eq_Type ty
 163  , Expr_from ast root
 164  , Lift_Type Type_Bool (Type_of_Expr 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  Eq       ty
 170  , Constraint_Type1 Foldable ty
 171  ) => ast -> ast
 172  -> Expr_From ast (Expr_Foldable lam root) hs ret
 173 elem_from ast_a ast_ta ex ast ctx k =
 174  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 175         expr_from (Proxy::Proxy root) ast_a ctx $
 176          \(ty_a::ty h_a) (Forall_Repr_with_Context 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_eq_type ex ast ty_a ty_t_a $ \Refl ->
 181         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 182         check_constraint_type ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 183         k type_bool $ Forall_Repr_with_Context $
 184          \c -> a c `elem` ta c
 185
 186 -- | Parse 'foldMap'.
 187 foldMap_from
 188  :: forall root ty lam ast hs ret.
 189  ( ty ~ Type_Root_of_Expr (Expr_Foldable lam root)
 190  , Eq_Type ty
 191  , Expr_from ast root
 192  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 193  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 194  , Unlift_Type1 (Type_of_Expr root)
 195  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 196                    (Error_of_Expr ast root)
 197  , Root_of_Expr root ~ root
 198  , Constraint_Type Monoid ty
 199  , Constraint_Type1 Foldable ty
 200  ) => ast -> ast
 201  -> Expr_From ast (Expr_Foldable lam root) hs ret
 202 foldMap_from ast_f ast_ta ex ast ctx k =
 203  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 204         expr_from (Proxy::Proxy root) ast_f ctx $
 205          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 206         expr_from (Proxy::Proxy root) ast_ta ctx $
 207          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 208         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_m
 209          :: Type_Fun lam ty h_f) ->
 210         check_type1 ex ast ty_ta $ \(Type_Type1 _t (ty_t_a::ty h_t_a), Lift_Type1 _ty_t) ->
 211         check_eq_type ex ast ty_f_a ty_t_a $ \Refl ->
 212         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 213         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 214         k ty_f_m $ Forall_Repr_with_Context $
 215          \c -> foldMap (f c) (ta c)