{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Sequences'.
module Language.Symantic.Lib.Sequences where

import Control.Monad (liftM, liftM2)
import Data.Proxy
import Data.Sequences (SemiSequence, IsSequence)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (filter, reverse)
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class 'Sym_SemiSequence'
class Sym_SemiSequence term where
	intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
	cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s
	snoc        :: SemiSequence s => term s -> term (MT.Element s) -> term s
	reverse     :: SemiSequence s => term s -> term s
	default intersperse :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
	default cons        :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
	default snoc        :: (Trans t term, SemiSequence s) => t term s -> t term (MT.Element s) -> t term s
	default reverse     :: (Trans t term, SemiSequence s) => t term s -> t term s
	intersperse = trans_map2 cons
	cons        = trans_map2 cons
	snoc        = trans_map2 snoc
	reverse     = trans_map1 reverse

type instance Sym_of_Iface (Proxy SemiSequence) = Sym_SemiSequence
type instance TyConsts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': TyConsts_imported_by (Proxy SemiSequence)
type instance TyConsts_imported_by (Proxy SemiSequence) = '[]

instance Sym_SemiSequence HostI where
	intersperse = liftM2 Seqs.intersperse
	cons        = liftM2 Seqs.cons
	snoc        = liftM2 Seqs.snoc
	reverse     = liftM  Seqs.reverse
instance Sym_SemiSequence TextI where
	intersperse = textI2 "intersperse"
	cons        = textI2 "cons"
	snoc        = textI2 "snoc"
	reverse     = textI1 "reverse"
instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (DupI r1 r2) where
	intersperse = dupI2 @Sym_SemiSequence intersperse
	cons        = dupI2 @Sym_SemiSequence cons
	snoc        = dupI2 @Sym_SemiSequence snoc
	reverse     = dupI1 @Sym_SemiSequence reverse

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs SemiSequence
 ) => Read_TyNameR TyName cs (Proxy SemiSequence ': rs) where
	read_TyNameR _cs (TyName "SemiSequence") k = k (ty @SemiSequence)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy SemiSequence ': cs) where
	show_TyConst TyConstZ{} = "SemiSequence"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy SemiSequence)

data instance TokenT meta (ts::[*]) (Proxy SemiSequence)
 = Token_Term_SemiSequence_intersperse (EToken meta ts) (EToken meta ts)
 | Token_Term_SemiSequence_cons        (EToken meta ts) (EToken meta ts)
 | Token_Term_SemiSequence_snoc        (EToken meta ts) (EToken meta ts)
 | Token_Term_SemiSequence_reverse     (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy SemiSequence))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy SemiSequence))
instance -- CompileI
 ( Inj_TyConst cs SemiSequence
 , Proj_TyCon  cs
 , Proj_TyFam  cs TyFam_MonoElement
 , Compile cs is
 ) => CompileI cs is (Proxy SemiSequence) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy SemiSequence)
	 -> CompileT meta ctx ret cs is ls (Proxy SemiSequence ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_SemiSequence_intersperse tok_e tok_s ->
			e2s2s_from tok_e tok_s intersperse
		 Token_Term_SemiSequence_cons tok_e tok_s ->
			e2s2s_from tok_e tok_s cons
		 Token_Term_SemiSequence_snoc tok_s tok_e ->
			e2s2s_from tok_s tok_e (Prelude.flip snoc)
		 Token_Term_SemiSequence_reverse tok_s ->
			-- reverse :: SemiSequence s => s -> s
			compileO tok_s ctx $ \ty_s (TermO s) ->
			check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
			k ty_s $ TermO $
			 \c -> reverse (s c)
		where
		e2s2s_from tok_e tok_s
		 (f::forall term s.
			 (Sym_SemiSequence term, SemiSequence s)
			 => term (MT.Element s) -> term s -> term s) =
		 -- intersperse :: SemiSequence s => MT.Element s -> s -> s
		 -- cons        :: SemiSequence s => MT.Element s -> s -> s
		 -- snoc        :: SemiSequence s => s -> MT.Element s -> s
			compileO tok_e ctx $ \ty_e (TermO e) ->
			compileO tok_s ctx $ \ty_s (TermO s) ->
			check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
			check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
			k ty_s $ TermO $
			 \c -> f (e c) (s c)
instance -- TokenizeT
 Inj_Token meta ts SemiSequence =>
 TokenizeT meta ts (Proxy SemiSequence) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "intersperse" infixN5 Token_Term_SemiSequence_intersperse
		 , tokenize2 "cons"        infixN5 Token_Term_SemiSequence_cons
		 , tokenize2 "snoc"        infixN5 Token_Term_SemiSequence_snoc
		 , tokenize1 "reverse"     infixN5 Token_Term_SemiSequence_reverse
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy SemiSequence) g

-- * Class 'Sym_IsSequence'
class Sym_IsSequence term where
	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
	default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
	filter  = trans_map2 filter

type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
type instance TyConsts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': TyConsts_imported_by (Proxy IsSequence)
type instance TyConsts_imported_by (Proxy IsSequence) =
 [ Proxy IsSequence
 , Proxy (->)
 , Proxy Bool
 ]

instance Sym_IsSequence HostI where
	filter  = liftM2 Seqs.filter
instance Sym_IsSequence TextI where
	filter  = textI2 "filter"
instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
	filter  = dupI2 @Sym_IsSequence filter

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs IsSequence
 ) => Read_TyNameR TyName cs (Proxy IsSequence ': rs) where
	read_TyNameR _cs (TyName "IsSequence") k = k (ty @IsSequence)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy IsSequence ': cs) where
	show_TyConst TyConstZ{} = "IsSequence"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy IsSequence)

data instance TokenT meta (ts::[*]) (Proxy IsSequence)
 = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))

instance -- CompileI
 ( Inj_TyConst cs IsSequence
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Bool
 , Proj_TyCon  cs
 , Proj_TyFam  cs TyFam_MonoElement
 , Compile cs is
 ) => CompileI cs is (Proxy IsSequence) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy IsSequence)
	 -> CompileT meta ctx ret cs is ls (Proxy IsSequence ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_IsSequence_filter tok_e2Bool tok_s ->
			-- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
			compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
			compileO tok_s      ctx $ \ty_s      (TermO s) ->
			check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_TyEq
			 (At Nothing (ty @Bool))
			 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_TyCon (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \TyCon ->
			check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_TyEq
			 (At Nothing ty_s_e)
			 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
			k ty_s $ TermO $
			 \c -> filter (e2Bool c) (s c)
instance -- TokenizeT
 Inj_Token meta ts IsSequence =>
 TokenizeT meta ts (Proxy IsSequence) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "filter" infixN5 Token_Term_IsSequence_filter
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy IsSequence) g