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  , Expr_From ast root
  92  , Type0_Eq ty
  93  , Type0_Lift   Type_Fun (Type_of_Expr root)
  94  , Type0_Unlift Type_Fun (Type_of_Expr root)
  95  , Type0_Constraint Monoid   ty
  96  , Type1_Constraint Foldable ty
  97  , Type1_Unlift (Type_of_Expr root)
  98  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  99                    (Error_of_Expr ast root)
 100  , Root_of_Expr root ~ root
 101  ) => ast -> ast
 102  -> ExprFrom 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 $ \(Type2 Proxy ty_f_a ty_f_m
 110          :: Type_Fun ty h_f) ->
 111         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 112         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 113         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 114         check_type0_constraint 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  , Expr_From ast root
 123  , Type0_Eq ty
 124  , Type0_Lift Type_Int (Type_of_Expr root)
 125  , Type1_Constraint Foldable ty
 126  , Type1_Unlift (Type_of_Expr root)
 127  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 128                    (Error_of_Expr ast root)
 129  , Root_of_Expr root ~ root
 130  ) => ast
 131  -> ExprFrom 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 $ \(Type1{}, _) ->
 137         check_type1_constraint 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  , Expr_From ast root
 146  , Type0_Eq ty
 147  , Type0_Lift Type_Bool (Type_of_Expr root)
 148  , Type1_Constraint Foldable ty
 149  , Type1_Unlift (Type_of_Expr root)
 150  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 151                    (Error_of_Expr ast root)
 152  , Root_of_Expr root ~ root
 153  ) => ast
 154  -> ExprFrom 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 $ \(Type1{}, _) ->
 160         check_type1_constraint 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  , Expr_From ast root
 169  , Type0_Eq ty
 170  , Type0_Constraint Ord      ty
 171  , Type1_Constraint Foldable ty
 172  , Type1_Unlift (Type_of_Expr root)
 173  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 174                    (Error_of_Expr ast root)
 175  , Root_of_Expr root ~ root
 176  ) => ast
 177  -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
 183         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 184         check_type0_constraint 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  , Expr_From ast root
 193  , Type0_Eq ty
 194  , Type0_Constraint Ord      ty
 195  , Type1_Constraint Foldable ty
 196  , Type1_Unlift (Type_of_Expr root)
 197  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 198                    (Error_of_Expr ast root)
 199  , Root_of_Expr root ~ root
 200  ) => ast
 201  -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
 207         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 208         check_type0_constraint 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  , Expr_From ast root
 217  , Type0_Eq ty
 218  , Type0_Constraint  Eq       ty
 219  , Type0_Lift Type_Bool (Type_of_Expr root)
 220  , Type1_Constraint Foldable ty
 221  , Type1_Unlift (Type_of_Expr root)
 222  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 223                    (Error_of_Expr ast root)
 224  , Root_of_Expr root ~ root
 225  ) => ast -> ast
 226  -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
 234         check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
 235         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 236         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 237         k type_bool $ Forall_Repr_with_Context $
 238          \c -> a c `elem` ta c