{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Traversable'.
module Language.Symantic.Compiling.Traversable where

import Control.Monad (liftM2)
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import qualified Data.Traversable as Traversable
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (traverse)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Applicative (Sym_Applicative, tyApplicative)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Traversable'
class Sym_Applicative term => Sym_Traversable term where
	traverse :: (Traversable t, Applicative f)
	 => term (a -> f b) -> term (t a) -> term (f (t b))
	default traverse :: (Trans tr term, Traversable t, Applicative f)
	 => tr term (a -> f b) -> tr term (t a) -> tr term (f (t b))
	traverse = trans_map2 traverse

type instance Sym_of_Iface (Proxy Traversable) = Sym_Traversable
type instance Consts_of_Iface (Proxy Traversable) = Proxy Traversable ': Consts_imported_by Traversable
type instance Consts_imported_by Traversable = '[]

instance Sym_Traversable HostI where
	traverse = liftM2 Traversable.traverse
instance Sym_Traversable TextI where
	traverse = textI_app2 "traverse"
instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
	traverse = dupI2 sym_Traversable traverse

instance Const_from Text cs => Const_from Text (Proxy Traversable ': cs) where
	const_from "Traversable" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
	show_const ConstZ{} = "Traversable"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 Proj_ConC cs (Proxy Traversable)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Traversable
 , Inj_Const (Consts_of_Ifaces is) Applicative
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Proj_Con  (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Traversable) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "traverse" -> traverse_from
		 _ -> Left $ Error_Term_unsupported
		where
		traverse_from =
		 -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
			from_ast2 ast $ \ast_a2fb ast_ta as ->
			term_from ast_a2fb ctx $ \ty_a2fb (TermLC a2fb) ->
			term_from ast_ta   ctx $ \ty_ta   (TermLC ta) ->
			check_type2 tyFun ast_a2fb ty_a2fb $ \Refl ty_a2fb_a ty_a2fb_fb ->
			check_constraint1 tyApplicative ast_a2fb ty_a2fb_fb $ \Refl Con ty_a2fb_fb_f ty_a2fb_fb_b ->
			check_constraint1 tyTraversable ast_ta   ty_ta      $ \Refl Con ty_ta_t ty_ta_a ->
			check_type (At (Just ast_a2fb) ty_a2fb_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
			k as (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermLC $
			 \c -> traverse (a2fb c) (ta c)

-- | The 'Traversable' 'Type'
tyTraversable :: Inj_Const cs Traversable => Type cs Traversable
tyTraversable = TyConst inj_const

sym_Traversable :: Proxy Sym_Traversable
sym_Traversable = Proxy

syTraversable :: IsString a => [Syntax a] -> Syntax a
syTraversable = Syntax "Traversable"