{-# 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.Parsing.Grammar
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans
import Language.Symantic.Lib.MonoFunctor (Fam_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 Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
type instance Consts_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 (Proxy @Sym_SemiSequence) intersperse
	cons        = dupI2 (Proxy @Sym_SemiSequence) cons
	snoc        = dupI2 (Proxy @Sym_SemiSequence) snoc
	reverse     = dupI1 (Proxy @Sym_SemiSequence) reverse

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs SemiSequence
 ) => Read_TypeNameR Type_Name cs (Proxy SemiSequence ': rs) where
	read_typenameR _cs (Type_Name "SemiSequence") k = k (ty @SemiSequence)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
	show_const ConstZ{} = "SemiSequence"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs SemiSequence
 , Proj_Consts cs (Consts_imported_by SemiSequence)
 ) => Proj_ConC cs (Proxy SemiSequence) where
	proj_conC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy @SemiSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy @Text) -> Just Con
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy @[]) -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _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_Const (Consts_of_Ifaces is) SemiSequence
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_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_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
			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_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
			check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (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 Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
type instance Consts_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 (Proxy @Sym_IsSequence) filter

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs IsSequence
 ) => Read_TypeNameR Type_Name cs (Proxy IsSequence ': rs) where
	read_typenameR _cs (Type_Name "IsSequence") k = k (ty @IsSequence)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
	show_const ConstZ{} = "IsSequence"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs IsSequence
 , Proj_Consts cs (Consts_imported_by IsSequence)
 ) => Proj_ConC cs (Proxy IsSequence) where
	proj_conC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy @IsSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy @Text) -> Just Con
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy @[]) -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _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_Const (Consts_of_Ifaces is) IsSequence
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_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_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_type
			 (At Nothing (ty @Bool))
			 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_con (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \Con ->
			check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type
			 (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