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

import Data.Sequences (SemiSequence, IsSequence)
import Prelude hiding (filter, reverse)
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs

import Language.Symantic
import Language.Symantic.Lib.Function ()
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.MonoFunctor (e1, famElement)

-- * Class 'Sym_SemiSequence'
type instance Sym SemiSequence = 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 :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
	default cons        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
	default snoc        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term (MT.Element s) -> term s
	default reverse     :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term s
	intersperse = trans2 cons
	cons        = trans2 cons
	snoc        = trans2 snoc
	reverse     = trans1 reverse

-- Interpreting
instance Sym_SemiSequence Eval where
	intersperse = eval2 Seqs.intersperse
	cons        = eval2 Seqs.cons
	snoc        = eval2 Seqs.snoc
	reverse     = eval1 Seqs.reverse
instance Sym_SemiSequence View where
	intersperse = view2 "intersperse"
	cons        = view2 "cons"
	snoc        = view2 "snoc"
	reverse     = view1 "reverse"
instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1 r2) where
	intersperse = dup2 @Sym_SemiSequence intersperse
	cons        = dup2 @Sym_SemiSequence cons
	snoc        = dup2 @Sym_SemiSequence snoc
	reverse     = dup1 @Sym_SemiSequence reverse

-- Transforming
instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)

-- Typing
instance NameTyOf SemiSequence where
	nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
instance FixityOf SemiSequence
instance ClassInstancesFor SemiSequence
instance TypeInstancesFor SemiSequence

-- Compiling
instance Gram_Term_AtomsFor src ss g SemiSequence
instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
	moduleFor = ["SemiSequence"] `moduleWhere`
	 [ "intersperse" := teSemiSequence_intersperse
	 , "cons"        := teSemiSequence_cons
	 , "snoc"        := teSemiSequence_snoc
	 , "reverse"     := teSemiSequence_reverse
	 ]

-- ** 'Type's
tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a

s0 :: Source src => LenInj vs => KindInj (K s) =>
      Type src (Proxy s ': vs) s
s0 = tyVar "s" varZ

-- ** 'Term's
teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))
teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse

teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))
teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse
teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons

teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))
teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc

-- * Class 'Sym_IsSequence'
type instance Sym IsSequence = Sym_IsSequence
class Sym_IsSequence term where
	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
	default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
	filter = trans2 filter

-- Interpreting
instance Sym_IsSequence Eval where
	filter  = eval2 Seqs.filter
instance Sym_IsSequence View where
	filter  = view2 "filter"
instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where
	filter  = dup2 @Sym_IsSequence filter

-- Transforming
instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)

-- Typing
instance NameTyOf IsSequence where
	nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
instance FixityOf IsSequence
instance ClassInstancesFor IsSequence
instance TypeInstancesFor IsSequence

-- Compiling
instance Gram_Term_AtomsFor src ss g IsSequence
instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
	moduleFor = ["IsSequence"] `moduleWhere`
	 [ "filter" := teIsSequence_filter
	 ]

-- ** 'Type's
tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a

-- ** 'Term's
teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))
teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter