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)
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
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
instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
instance NameTyOf SemiSequence where
nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
instance FixityOf SemiSequence
instance ClassInstancesFor SemiSequence
instance TypeInstancesFor SemiSequence
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
]
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
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
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
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
instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
instance NameTyOf IsSequence where
nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
instance FixityOf IsSequence
instance ClassInstancesFor IsSequence
instance TypeInstancesFor IsSequence
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
]
tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a
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