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
  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
  23 import Language.Symantic.Type
  24 import Language.Symantic.Repr
  25 import Language.Symantic.Expr.Root
  26 import Language.Symantic.Expr.Error
  27 import Language.Symantic.Expr.From
  28 import Language.Symantic.Expr.Lambda
  29 import Language.Symantic.Trans.Common
  30
  31 -- * Class 'Sym_Foldable'
  32 -- | Symantic.
  33 class Sym_Foldable repr where
  34         foldMap :: (Foldable t, Monoid m) => repr ((->) a m) -> repr (t a) -> repr m
  35         length  :: Foldable t => repr (t a) -> repr Int
  36         null    :: Foldable t => repr (t a) -> repr Bool
  37         minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
  38         maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
  39         elem    :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
  40         default foldMap :: (Trans tr repr, Foldable t, Monoid m)
  41          => tr repr ((->) a m) -> tr repr (t a) -> tr repr m
  42         default length  :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
  43         default null    :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
  44         default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  45         default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
  46         default elem    :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
  47         foldMap = trans_map2 foldMap
  48         length  = trans_map1 length
  49         null    = trans_map1 null
  50         minimum = trans_map1 minimum
  51         maximum = trans_map1 maximum
  52         elem    = trans_map2 elem
  53 instance Sym_Foldable Repr_Host where
  54         foldMap = liftM2 Foldable.foldMap
  55         null    = liftM Foldable.null
  56         length  = liftM Foldable.length
  57         minimum = liftM Foldable.minimum
  58         maximum = liftM Foldable.maximum
  59         elem    = liftM2 Foldable.elem
  60 instance Sym_Foldable Repr_Text where
  61         foldMap = repr_text_app2 "foldMap"
  62         null    = repr_text_app1 "null"
  63         length  = repr_text_app1 "length"
  64         minimum = repr_text_app1 "minimum"
  65         maximum = repr_text_app1 "maximum"
  66         elem    = repr_text_app2 "elem"
  67 instance
  68  ( Sym_Foldable r1
  69  , Sym_Foldable r2
  70  ) => Sym_Foldable (Dup r1 r2) where
  71         foldMap (f1 `Dup` f2) (m1 `Dup` m2) =
  72                 foldMap f1 m1 `Dup` foldMap f2 m2
  73         length  (f1 `Dup` f2) = length  f1 `Dup` length  f2
  74         null    (f1 `Dup` f2) = null    f1 `Dup` null    f2
  75         minimum (f1 `Dup` f2) = minimum f1 `Dup` minimum f2
  76         maximum (f1 `Dup` f2) = maximum f1 `Dup` maximum f2
  77         elem    (a1 `Dup` a2) (f1 `Dup` f2) = elem a1 f1 `Dup` elem a2 f2
  78
  79 -- * Type 'Expr_Foldable'
  80 -- | Expression.
  81 data Expr_Foldable (root:: *)
  82 type instance Root_of_Expr      (Expr_Foldable root)      = root
  83 type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
  84 type instance Sym_of_Expr       (Expr_Foldable root) repr = (Sym_Foldable repr)
  85 type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr
  86
  87 -- | Parse 'foldMap'.
  88 foldMap_from
  89  :: forall root ty ast hs ret.
  90  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
  91  , Eq_Type ty
  92  , Expr_from ast root
  93  , Lift_Type   Type_Fun (Type_of_Expr root)
  94  , Unlift_Type Type_Fun (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_Type Monoid ty
 100  , Constraint_Type1 Foldable ty
 101  ) => ast -> ast
 102  -> Expr_From ast (Expr_Foldable root) hs ret
 103 foldMap_from ast_f ast_ta ex ast ctx k =
 104  -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
 105         expr_from (Proxy::Proxy root) ast_f ctx $
 106          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 107         expr_from (Proxy::Proxy root) ast_ta ctx $
 108          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 109         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_m
 110          :: Type_Fun ty h_f) ->
 111         check_type1 ex ast ty_ta $ \(Type_Type1 _t (ty_t_a::ty h_t_a), Lift_Type1 _ty_t) ->
 112         check_eq_type ex ast ty_f_a ty_t_a $ \Refl ->
 113         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 114         check_constraint_type ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 115         k ty_f_m $ Forall_Repr_with_Context $
 116          \c -> foldMap (f c) (ta c)
 117
 118 -- | Parse 'length'.
 119 length_from
 120  :: forall root ty ast hs ret.
 121  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 122  , Eq_Type ty
 123  , Expr_from ast root
 124  , Lift_Type Type_Int (Type_of_Expr root)
 125  , Unlift_Type1 (Type_of_Expr root)
 126  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 127                    (Error_of_Expr ast root)
 128  , Root_of_Expr root ~ root
 129  , Constraint_Type1 Foldable ty
 130  ) => ast
 131  -> Expr_From ast (Expr_Foldable root) hs ret
 132 length_from ast_ta ex ast ctx k =
 133  -- length :: Foldable t => t a -> Int
 134         expr_from (Proxy::Proxy root) ast_ta ctx $
 135          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 136         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 137         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 138         k type_int $ Forall_Repr_with_Context $
 139          \c -> length (ta c)
 140
 141 -- | Parse 'null'.
 142 null_from
 143  :: forall root ty ast hs ret.
 144  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 145  , Eq_Type ty
 146  , Expr_from ast root
 147  , Lift_Type Type_Bool (Type_of_Expr root)
 148  , Unlift_Type1 (Type_of_Expr root)
 149  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 150                    (Error_of_Expr ast root)
 151  , Root_of_Expr root ~ root
 152  , Constraint_Type1 Foldable ty
 153  ) => ast
 154  -> Expr_From ast (Expr_Foldable root) hs ret
 155 null_from ast_ta ex ast ctx k =
 156  -- null :: Foldable t => t a -> Bool
 157         expr_from (Proxy::Proxy root) ast_ta ctx $
 158          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 159         check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
 160         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 161         k type_bool $ Forall_Repr_with_Context $
 162          \c -> null (ta c)
 163
 164 -- | Parse 'minimum'.
 165 minimum_from
 166  :: forall root ty ast hs ret.
 167  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 168  , Eq_Type ty
 169  , Expr_from ast root
 170  , Unlift_Type1 (Type_of_Expr root)
 171  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 172                    (Error_of_Expr ast root)
 173  , Root_of_Expr root ~ root
 174  , Constraint_Type  Ord      ty
 175  , Constraint_Type1 Foldable ty
 176  ) => ast
 177  -> Expr_From ast (Expr_Foldable root) hs ret
 178 minimum_from ast_ta ex ast ctx k =
 179  -- minimum :: (Foldable t, Ord a) => t a -> a
 180         expr_from (Proxy::Proxy root) ast_ta ctx $
 181          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 182         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 183         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 184         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 185         k ty_t_a $ Forall_Repr_with_Context $
 186          \c -> minimum (ta c)
 187
 188 -- | Parse 'maximum'.
 189 maximum_from
 190  :: forall root ty ast hs ret.
 191  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 192  , Eq_Type ty
 193  , Expr_from ast 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  Ord      ty
 199  , Constraint_Type1 Foldable ty
 200  ) => ast
 201  -> Expr_From ast (Expr_Foldable root) hs ret
 202 maximum_from ast_ta ex ast ctx k =
 203  -- maximum :: (Foldable t, Ord a) => t a -> 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_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 208         check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 209         k ty_t_a $ Forall_Repr_with_Context $
 210          \c -> maximum (ta c)
 211
 212 -- | Parse 'elem'.
 213 elem_from
 214  :: forall root ty ast hs ret.
 215  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 216  , Eq_Type ty
 217  , Expr_from ast root
 218  , Lift_Type Type_Bool (Type_of_Expr root)
 219  , Unlift_Type1 (Type_of_Expr root)
 220  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 221                    (Error_of_Expr ast root)
 222  , Root_of_Expr root ~ root
 223  , Constraint_Type  Eq       ty
 224  , Constraint_Type1 Foldable ty
 225  ) => ast -> ast
 226  -> Expr_From ast (Expr_Foldable root) hs ret
 227 elem_from ast_a ast_ta ex ast ctx k =
 228  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 229         expr_from (Proxy::Proxy root) ast_a ctx $
 230          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 231         expr_from (Proxy::Proxy root) ast_ta ctx $
 232          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 233         check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
 234         check_eq_type ex ast ty_a ty_t_a $ \Refl ->
 235         check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 236         check_constraint_type ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 237         k type_bool $ Forall_Repr_with_Context $
 238          \c -> a c `elem` ta c