{-# 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 f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
	foldr   :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
	foldr'  :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
	foldl   :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
	foldl'  :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
	length  :: Foldable f => repr (f a) -> repr Int
	null    :: Foldable f => repr (f a) -> repr Bool
	minimum :: (Foldable f, Ord a) => repr (f a) -> repr a
	maximum :: (Foldable f, Ord a) => repr (f a) -> repr a
	elem    :: (Foldable f, Eq  a) => repr a -> repr (f a) -> repr Bool
	sum     :: (Foldable f, Num a) => repr (f a) -> repr a
	product :: (Foldable f, Num a) => repr (f a) -> repr a
	toList  :: Foldable f => repr (f a) -> repr [a]
	default foldMap :: (Trans t repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
	default foldr   :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldr'  :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldl   :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldl'  :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
	default length  :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
	default null    :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
	default minimum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
	default maximum :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
	default elem    :: (Trans t repr, Foldable f, Eq  a) => t repr a -> t repr (f a) -> t repr Bool
	default sum     :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
	default product :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
	default toList  :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
	foldMap = trans_map2 foldMap
	foldr   = trans_map3 foldr
	foldr'  = trans_map3 foldr'
	foldl   = trans_map3 foldl
	foldl'  = trans_map3 foldl'
	length  = trans_map1 length
	null    = trans_map1 null
	minimum = trans_map1 minimum
	maximum = trans_map1 maximum
	elem    = trans_map2 elem
	sum     = trans_map1 sum
	product = trans_map1 product
	toList  = trans_map1 toList
instance Sym_Foldable Repr_Host where
	foldMap = liftM2 Foldable.foldMap
	foldr   = liftM3 Foldable.foldr
	foldr'  = liftM3 Foldable.foldr'
	foldl   = liftM3 Foldable.foldl
	foldl'  = liftM3 Foldable.foldl'
	null    = liftM  Foldable.null
	length  = liftM  Foldable.length
	minimum = liftM  Foldable.minimum
	maximum = liftM  Foldable.maximum
	elem    = liftM2 Foldable.elem
	sum     = liftM  Foldable.sum
	product = liftM  Foldable.product
	toList  = liftM  Foldable.toList
instance Sym_Foldable Repr_Text where
	foldMap = repr_text_app2 "foldMap"
	foldr   = repr_text_app3 "foldr"
	foldr'  = repr_text_app3 "foldr'"
	foldl   = repr_text_app3 "foldl"
	foldl'  = repr_text_app3 "foldl'"
	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"
	sum     = repr_text_app1 "sum"
	product = repr_text_app1 "product"
	toList  = repr_text_app1 "toList"
instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
	foldMap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
		foldMap f1 m1 `Repr_Dup` foldMap f2 m2
	foldr (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
		foldr f1 a1 m1 `Repr_Dup` foldr f2 a2 m2
	foldr' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
		foldr' f1 a1 m1 `Repr_Dup` foldr' f2 a2 m2
	foldl (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
		foldl f1 a1 m1 `Repr_Dup` foldl f2 a2 m2
	foldl' (f1 `Repr_Dup` f2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
		foldl' f1 a1 m1 `Repr_Dup` foldl' f2 a2 m2
	length  (f1 `Repr_Dup` f2) = length  f1 `Repr_Dup` length  f2
	null    (f1 `Repr_Dup` f2) = null    f1 `Repr_Dup` null    f2
	minimum (f1 `Repr_Dup` f2) = minimum f1 `Repr_Dup` minimum f2
	maximum (f1 `Repr_Dup` f2) = maximum f1 `Repr_Dup` maximum f2
	elem    (a1 `Repr_Dup` a2) (f1 `Repr_Dup` f2) = elem a1 f1 `Repr_Dup` elem a2 f2
	sum     (f1 `Repr_Dup` f2) = sum f1 `Repr_Dup` sum f2
	product (f1 `Repr_Dup` f2) = product f1 `Repr_Dup` product f2
	toList  (f1 `Repr_Dup` f2) = toList f1 `Repr_Dup` toList 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)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type0_Constraint Monoid   ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom 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 $ \(Type2 Proxy ty_f_a ty_f_m) ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
	k ty_f_m $ Forall_Repr_with_Context $
	 \c -> foldMap (f c) (ta c)

-- | Parse 'foldr' or |foldr'|.
foldr_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
 -> ast -> ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
 -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	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 $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
	check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
	check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
	check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> fold (f c) (b c) (ta c)

-- | Parse 'foldl' or |foldl'|.
foldl_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
 -> ast -> ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
 -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	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 $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
	check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
	check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
	check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> fold (f c) (b c) (ta c)

-- | Parse 'length'.
length_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Int (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom 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 $ \(Type1{}, _) ->
	check_type1_constraint 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)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom 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 $ \(Type1{}, _) ->
	check_type1_constraint 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)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Ord      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint 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)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Ord      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint 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)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint  Eq       ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom 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 $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> a c `elem` ta c

-- | Parse 'sum'.
sum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
sum_from ast_ta ex ast ctx k =
 -- sum :: (Foldable t, Num 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 $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> sum (ta c)

-- | Parse 'product'.
product_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
product_from ast_ta ex ast ctx k =
 -- product :: (Foldable t, Num 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 $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> product (ta c)

-- | Parse 'toList'.
toList_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_List (Type_of_Expr root)
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
toList_from ast_ta ex ast ctx k =
 -- toList :: Foldable t => 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 $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k (type_list ty_t_a) $ Forall_Repr_with_Context $
	 \c -> toList (ta c)