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

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

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 SemiSequence
type instance TyConsts_imported_by SemiSequence =
 [ Proxy SemiSequence
 , Proxy []
 , Proxy Text
 ]

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
 ( Proj_TyConst cs SemiSequence
 , Proj_TyConsts cs (TyConsts_imported_by SemiSequence)
 ) => Proj_TyConC cs (Proxy SemiSequence) where
	proj_TyConC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_TyConst q (Proxy @SemiSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_TyConst c) SKiType ->
			case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
			 _ -> Nothing
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
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 (TyConsts_of_Ifaces is) SemiSequence
 , Proj_TyCon  (TyConsts_of_Ifaces is)
 , Proj_TyFam  (TyConsts_of_Ifaces is) TyFam_MonoElement
 , Compile is
 ) => CompileI is (Proxy SemiSequence) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy SemiSequence)
	 -> CompileT meta ctx ret 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 IsSequence
type instance TyConsts_imported_by IsSequence =
 [ Proxy IsSequence
 , Proxy (->)
 , Proxy []
 , Proxy Text
 , 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
 ( Proj_TyConst cs IsSequence
 , Proj_TyConsts cs (TyConsts_imported_by IsSequence)
 ) => Proj_TyConC cs (Proxy IsSequence) where
	proj_TyConC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_TyConst q (Proxy @IsSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_TyConst c) SKiType ->
			case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
			 _ -> Nothing
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
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 (TyConsts_of_Ifaces is) IsSequence
 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 , Inj_TyConst (TyConsts_of_Ifaces is) Bool
 , Proj_TyCon  (TyConsts_of_Ifaces is)
 , Proj_TyFam  (TyConsts_of_Ifaces is) TyFam_MonoElement
 , Compile is
 ) => CompileI is (Proxy IsSequence) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy IsSequence)
	 -> CompileT meta ctx ret 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