{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Foldable'.
module Language.Symantic.Expr.Foldable where

import Control.Monad
import Data.Monoid
import Data.Foldable (Foldable)
import qualified Data.Foldable as Foldable
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((<$>), Foldable(..))

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Expr.Lambda
import Language.Symantic.Trans.Common

-- * Class 'Sym_Foldable'
-- | Symantic.
class Sym_Foldable repr where
	foldMap :: (Foldable t, Monoid m) => repr ((->) a m) -> repr (t a) -> repr m
	length  :: Foldable t => repr (t a) -> repr Int
	null    :: Foldable t => repr (t a) -> repr Bool
	minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
	maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
	elem    :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
	default foldMap :: (Trans tr repr, Foldable t, Monoid m)
	 => tr repr ((->) a m) -> tr repr (t a) -> tr repr m
	default length  :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
	default null    :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
	default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
	default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
	default elem    :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
	foldMap = trans_map2 foldMap
	length  = trans_map1 length
	null    = trans_map1 null
	minimum = trans_map1 minimum
	maximum = trans_map1 maximum
	elem    = trans_map2 elem
instance Sym_Foldable Repr_Host where
	foldMap = liftM2 Foldable.foldMap
	null    = liftM Foldable.null
	length  = liftM Foldable.length
	minimum = liftM Foldable.minimum
	maximum = liftM Foldable.maximum
	elem    = liftM2 Foldable.elem
instance Sym_Foldable Repr_Text where
	foldMap = repr_text_app2 "foldMap"
	null    = repr_text_app1 "null"
	length  = repr_text_app1 "length"
	minimum = repr_text_app1 "minimum"
	maximum = repr_text_app1 "maximum"
	elem    = repr_text_app2 "elem"
instance
 ( Sym_Foldable r1
 , Sym_Foldable r2
 ) => Sym_Foldable (Dup r1 r2) where
	foldMap (f1 `Dup` f2) (m1 `Dup` m2) =
		foldMap f1 m1 `Dup` foldMap f2 m2
	length  (f1 `Dup` f2) = length  f1 `Dup` length  f2
	null    (f1 `Dup` f2) = null    f1 `Dup` null    f2
	minimum (f1 `Dup` f2) = minimum f1 `Dup` minimum f2
	maximum (f1 `Dup` f2) = maximum f1 `Dup` maximum f2
	elem    (a1 `Dup` a2) (f1 `Dup` f2) = elem a1 f1 `Dup` elem a2 f2

-- * Type 'Expr_Foldable'
-- | Expression.
data Expr_Foldable (root:: *)
type instance Root_of_Expr      (Expr_Foldable root)      = root
type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
type instance Sym_of_Expr       (Expr_Foldable root) repr = (Sym_Foldable repr)
type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr

-- | Parse 'foldMap'.
foldMap_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Fun (Type_of_Expr root)
 , Unlift_Type Type_Fun (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type Monoid ty
 , Constraint_Type1 Foldable ty
 ) => ast -> ast
 -> Expr_From ast (Expr_Foldable root) hs ret
foldMap_from ast_f ast_ta ex ast ctx k =
 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_m
	 :: Type_Fun ty h_f) ->
	check_type1 ex ast ty_ta $ \(Type_Type1 _t (ty_t_a::ty h_t_a), Lift_Type1 _ty_t) ->
	check_eq_type ex ast ty_f_a ty_t_a $ \Refl ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_constraint_type ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
	k ty_f_m $ Forall_Repr_with_Context $
	 \c -> foldMap (f c) (ta c)

-- | Parse 'length'.
length_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type Type_Int (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type1 Foldable ty
 ) => ast
 -> Expr_From ast (Expr_Foldable root) hs ret
length_from ast_ta ex ast ctx k =
 -- length :: Foldable t => t a -> Int
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_int $ Forall_Repr_with_Context $
	 \c -> length (ta c)

-- | Parse 'null'.
null_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type Type_Bool (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type1 Foldable ty
 ) => ast
 -> Expr_From ast (Expr_Foldable root) hs ret
null_from ast_ta ex ast ctx k =
 -- null :: Foldable t => t a -> Bool
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type_Type1{}, _) ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> null (ta c)

-- | Parse 'minimum'.
minimum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type  Ord      ty
 , Constraint_Type1 Foldable ty
 ) => ast
 -> Expr_From ast (Expr_Foldable root) hs ret
minimum_from ast_ta ex ast ctx k =
 -- minimum :: (Foldable t, Ord a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> minimum (ta c)

-- | Parse 'maximum'.
maximum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type  Ord      ty
 , Constraint_Type1 Foldable ty
 ) => ast
 -> Expr_From ast (Expr_Foldable root) hs ret
maximum_from ast_ta ex ast ctx k =
 -- maximum :: (Foldable t, Ord a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> maximum (ta c)

-- | Parse 'elem'.
elem_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type Type_Bool (Type_of_Expr root)
 , Unlift_Type1 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 , Constraint_Type  Eq       ty
 , Constraint_Type1 Foldable ty
 ) => ast -> ast
 -> Expr_From ast (Expr_Foldable root) hs ret
elem_from ast_a ast_ta ex ast ctx k =
 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type_Type1 _ ty_t_a, _) ->
	check_eq_type ex ast ty_a ty_t_a $ \Refl ->
	check_constraint_type1 ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_constraint_type ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> a c `elem` ta c