]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Sequences.hs
Rename inj_* -> *Inj.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Sequences.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Sequences'.
4 module Language.Symantic.Lib.Sequences where
5
6 import Data.Sequences (SemiSequence, IsSequence)
7 import Prelude hiding (filter, reverse)
8 import qualified Data.MonoTraversable as MT
9 import qualified Data.Sequences as Seqs
10
11 import Language.Symantic
12 import Language.Symantic.Lib.Function ()
13 import Language.Symantic.Lib.Bool (tyBool)
14 import Language.Symantic.Lib.MonoFunctor (e1, famElement)
15
16 -- * Class 'Sym_SemiSequence'
17 type instance Sym SemiSequence = Sym_SemiSequence
18 class Sym_SemiSequence term where
19 intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
20 cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
21 snoc :: SemiSequence s => term s -> term (MT.Element s) -> term s
22 reverse :: SemiSequence s => term s -> term s
23 default intersperse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
24 default cons :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
25 default snoc :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term (MT.Element s) -> term s
26 default reverse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term s
27 intersperse = trans2 cons
28 cons = trans2 cons
29 snoc = trans2 snoc
30 reverse = trans1 reverse
31
32 -- Interpreting
33 instance Sym_SemiSequence Eval where
34 intersperse = eval2 Seqs.intersperse
35 cons = eval2 Seqs.cons
36 snoc = eval2 Seqs.snoc
37 reverse = eval1 Seqs.reverse
38 instance Sym_SemiSequence View where
39 intersperse = view2 "intersperse"
40 cons = view2 "cons"
41 snoc = view2 "snoc"
42 reverse = view1 "reverse"
43 instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1 r2) where
44 intersperse = dup2 @Sym_SemiSequence intersperse
45 cons = dup2 @Sym_SemiSequence cons
46 snoc = dup2 @Sym_SemiSequence snoc
47 reverse = dup1 @Sym_SemiSequence reverse
48
49 -- Transforming
50 instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
51
52 -- Typing
53 instance FixityOf SemiSequence
54 instance ClassInstancesFor SemiSequence
55 instance TypeInstancesFor SemiSequence
56
57 -- Compiling
58 instance Gram_Term_AtomsFor src ss g SemiSequence
59 instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
60 moduleFor = ["SemiSequence"] `moduleWhere`
61 [ "intersperse" := teSemiSequence_intersperse
62 , "cons" := teSemiSequence_cons
63 , "snoc" := teSemiSequence_snoc
64 , "reverse" := teSemiSequence_reverse
65 ]
66
67 -- ** 'Type's
68 tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
69 tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
70
71 s0 :: Source src => LenInj vs => KindInj (K s) =>
72 Type src (Proxy s ': vs) s
73 s0 = tyVar "s" varZ
74
75 -- ** 'Term's
76 teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))
77 teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse
78
79 teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))
80 teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse
81 teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons
82
83 teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))
84 teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
85
86 -- * Class 'Sym_IsSequence'
87 type instance Sym IsSequence = Sym_IsSequence
88 class Sym_IsSequence term where
89 filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
90 default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
91 filter = trans2 filter
92
93 -- Interpreting
94 instance Sym_IsSequence Eval where
95 filter = eval2 Seqs.filter
96 instance Sym_IsSequence View where
97 filter = view2 "filter"
98 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where
99 filter = dup2 @Sym_IsSequence filter
100
101 -- Transforming
102 instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
103
104 -- Typing
105 instance FixityOf IsSequence
106 instance ClassInstancesFor IsSequence
107 instance TypeInstancesFor IsSequence
108
109 -- Compiling
110 instance Gram_Term_AtomsFor src ss g IsSequence
111 instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
112 moduleFor = ["IsSequence"] `moduleWhere`
113 [ "filter" := teIsSequence_filter
114 ]
115
116 -- ** 'Type's
117 tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
118 tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a
119
120 -- ** 'Term's
121 teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))
122 teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter