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 (Repr_Dup r1 r2) where
  71         foldMap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
  72                 foldMap f1 m1 `Repr_Dup` foldMap f2 m2
  73         length  (f1 `Repr_Dup` f2) = length  f1 `Repr_Dup` length  f2
  74         null    (f1 `Repr_Dup` f2) = null    f1 `Repr_Dup` null    f2
  75         minimum (f1 `Repr_Dup` f2) = minimum f1 `Repr_Dup` minimum f2
  76         maximum (f1 `Repr_Dup` f2) = maximum f1 `Repr_Dup` maximum f2
  77         elem    (a1 `Repr_Dup` a2) (f1 `Repr_Dup` f2) = elem a1 f1 `Repr_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         check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
 111         check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
 112         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 113         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
 114         k ty_f_m $ Forall_Repr_with_Context $
 115          \c -> foldMap (f c) (ta c)
 116
 117 -- | Parse 'length'.
 118 length_from
 119  :: forall root ty ast hs ret.
 120  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 121  , Expr_From ast root
 122  , Type0_Eq ty
 123  , Type0_Lift Type_Int (Type_of_Expr root)
 124  , Type1_Constraint Foldable ty
 125  , Type1_Unlift (Type_of_Expr root)
 126  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 127                    (Error_of_Expr ast root)
 128  , Root_of_Expr root ~ root
 129  ) => ast
 130  -> ExprFrom ast (Expr_Foldable root) hs ret
 131 length_from ast_ta ex ast ctx k =
 132  -- length :: Foldable t => t a -> Int
 133         expr_from (Proxy::Proxy root) ast_ta ctx $
 134          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 135         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 136         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 137         k type_int $ Forall_Repr_with_Context $
 138          \c -> length (ta c)
 139
 140 -- | Parse 'null'.
 141 null_from
 142  :: forall root ty ast hs ret.
 143  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 144  , Expr_From ast root
 145  , Type0_Eq ty
 146  , Type0_Lift Type_Bool (Type_of_Expr root)
 147  , Type1_Constraint Foldable ty
 148  , Type1_Unlift (Type_of_Expr root)
 149  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 150                    (Error_of_Expr ast root)
 151  , Root_of_Expr root ~ root
 152  ) => ast
 153  -> ExprFrom ast (Expr_Foldable root) hs ret
 154 null_from ast_ta ex ast ctx k =
 155  -- null :: Foldable t => t a -> Bool
 156         expr_from (Proxy::Proxy root) ast_ta ctx $
 157          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 158         check_type1 ex ast ty_ta $ \(Type1{}, _) ->
 159         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 160         k type_bool $ Forall_Repr_with_Context $
 161          \c -> null (ta c)
 162
 163 -- | Parse 'minimum'.
 164 minimum_from
 165  :: forall root ty ast hs ret.
 166  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 167  , Expr_From ast root
 168  , Type0_Eq ty
 169  , Type0_Constraint Ord      ty
 170  , Type1_Constraint Foldable ty
 171  , Type1_Unlift (Type_of_Expr root)
 172  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 173                    (Error_of_Expr ast root)
 174  , Root_of_Expr root ~ root
 175  ) => ast
 176  -> ExprFrom ast (Expr_Foldable root) hs ret
 177 minimum_from ast_ta ex ast ctx k =
 178  -- minimum :: (Foldable t, Ord a) => t a -> a
 179         expr_from (Proxy::Proxy root) ast_ta ctx $
 180          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 181         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 182         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 183         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 184         k ty_t_a $ Forall_Repr_with_Context $
 185          \c -> minimum (ta c)
 186
 187 -- | Parse 'maximum'.
 188 maximum_from
 189  :: forall root ty ast hs ret.
 190  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 191  , Expr_From ast root
 192  , Type0_Eq ty
 193  , Type0_Constraint Ord      ty
 194  , Type1_Constraint Foldable ty
 195  , Type1_Unlift (Type_of_Expr root)
 196  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 197                    (Error_of_Expr ast root)
 198  , Root_of_Expr root ~ root
 199  ) => ast
 200  -> ExprFrom ast (Expr_Foldable root) hs ret
 201 maximum_from ast_ta ex ast ctx k =
 202  -- maximum :: (Foldable t, Ord a) => t a -> a
 203         expr_from (Proxy::Proxy root) ast_ta ctx $
 204          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 205         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 206         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 207         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
 208         k ty_t_a $ Forall_Repr_with_Context $
 209          \c -> maximum (ta c)
 210
 211 -- | Parse 'elem'.
 212 elem_from
 213  :: forall root ty ast hs ret.
 214  ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 215  , Expr_From ast root
 216  , Type0_Eq ty
 217  , Type0_Constraint  Eq       ty
 218  , Type0_Lift Type_Bool (Type_of_Expr root)
 219  , Type1_Constraint Foldable ty
 220  , Type1_Unlift (Type_of_Expr root)
 221  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 222                    (Error_of_Expr ast root)
 223  , Root_of_Expr root ~ root
 224  ) => ast -> ast
 225  -> ExprFrom ast (Expr_Foldable root) hs ret
 226 elem_from ast_a ast_ta ex ast ctx k =
 227  -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
 228         expr_from (Proxy::Proxy root) ast_a ctx $
 229          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 230         expr_from (Proxy::Proxy root) ast_ta ctx $
 231          \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
 232         check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
 233         check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
 234         check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
 235         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
 236         k type_bool $ Forall_Repr_with_Context $
 237          \c -> a c `elem` ta c