{-# 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