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