{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Sequences'.
module Language.Symantic.Compiling.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.Term
import Language.Symantic.Compiling.MonoFunctor (Fam_MonoElement(..))
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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 = textI_app2 "intersperse"
	cons        = textI_app2 "cons"
	snoc        = textI_app2 "snoc"
	reverse     = textI_app1 "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 Const_from Text cs => Const_from Text (Proxy SemiSequence ': cs) where
	const_from "SemiSequence" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
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::Proxy SemiSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::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::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 -- Term_fromI
 ( Inj_Const (Consts_of_Ifaces is) SemiSequence
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is
 ) => Term_fromI is (Proxy SemiSequence) where
	term_fromI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy SemiSequence)
	 -> Term_fromT meta ctx ret is ls (Proxy SemiSequence ': rs)
	term_fromI 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
			term_from tok_s ctx $ \ty_s (TermLC s) ->
			check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
			k ty_s $ TermLC $
			 \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
			term_from tok_e ctx $ \ty_e (TermLC e) ->
			term_from tok_s ctx $ \ty_s (TermLC 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 $ TermLC $
			 \c -> f (e c) (s c)

-- * 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  = textI_app2 "filter"
instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
	filter  = dupI2 (Proxy @Sym_IsSequence) filter

instance Const_from Text cs => Const_from Text (Proxy IsSequence ': cs) where
	const_from "IsSequence" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
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::Proxy IsSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::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::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 -- Term_fromI
 ( 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
 , Term_from is
 ) => Term_fromI is (Proxy IsSequence) where
	term_fromI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy IsSequence)
	 -> Term_fromT meta ctx ret is ls (Proxy IsSequence ': rs)
	term_fromI tok ctx k =
		case tok of
		 Token_Term_IsSequence_filter tok_e2Bool tok_s ->
			-- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
			term_from tok_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
			term_from tok_s      ctx $ \ty_s      (TermLC 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 $ TermLC $
			 \c -> filter (e2Bool c) (s c)