@@ -26,7 +26,7 @@ module Pipeline.Circuit
2626 ) where
2727
2828
29- import Pipeline.Internal.Common.IFunctor (IFix7 (.. ))
29+ import Pipeline.Internal.Common.IFunctor (IFix5 (.. ))
3030import Pipeline.Internal.Common.IFunctor.Modular ((:<:) (.. ))
3131import Pipeline.Internal.Common.Nat (IsNat , N1 , N2 ,
3232 Nat (.. ), SNat (.. ), (:+) )
@@ -49,8 +49,8 @@ In diagram form it would look like,
4949> |
5050
5151-}
52- id :: (DataStore' '[f ] '[a ]) => AST. Circuitf ] '[a ] '[f a ] '[f ] '[ a ] '[ f a ] N1
53- id = (IIn7 . inj) AST. Id
52+ id :: (DataStore' '[f ] '[a ]) => AST. Circuitf ] '[a ] '[f ] '[a ] N1
53+ id = (IIn5 . inj) AST. Id
5454
5555{-|
5656Duplicates an input.
@@ -60,8 +60,8 @@ In diagram form it would look like,
6060> /\
6161
6262-}
63- replicate2 :: DataStore' '[f ] '[a ] => AST. Circuitf ] '[a ] '[f a ] '[ f , f ] '[a , a ] '[ f a , f a ] N1
64- replicate2 = (IIn7 . inj) AST. Replicate
63+ replicate2 :: DataStore' '[f ] '[a ] => AST. Circuitf ] '[a ] '[f , f ] '[a , a ] N1
64+ replicate2 = (IIn5 . inj) AST. Replicate
6565
6666{-|
6767Usually referred to as \"then\", this operator joins two levels of a circuit together.
@@ -77,10 +77,10 @@ A diagram representing @a \<-\> b@ or \"a then b\" can be seen below,
7777-}
7878(<->)
7979 :: (DataStore' fs as , DataStore' gs bs , DataStore' hs cs )
80- => AST. Circuitfs as ( Apply fs as ) gs bs ( Apply gs bs ) nfs -- ^ First circuit (@a@)
81- -> AST. Circuitgs bs ( Apply gs bs ) hs cs ( Apply hs cs ) ngs -- ^ Second circuit (@b@)
82- -> AST. Circuitfs as ( Apply fs as ) hs cs ( Apply hs cs ) nfs
83- (<->) l r = IIn7 (inj (AST. Then
80+ => AST. Circuitfs as gs bs nfs -- ^ First circuit (@a@)
81+ -> AST. Circuitgs bs hs cs ngs -- ^ Second circuit (@b@)
82+ -> AST. Circuitfs as hs cs nfs
83+ (<->) l r = IIn5 (inj (AST. Then
8484infixr 4 <->
8585
8686
@@ -103,32 +103,24 @@ A diagram representing @a \<\> b@ or \"a next to b\" can be seen below,
103103 , IsNat nfs
104104 , IsNat nhs
105105 , Length fs ~ Length as
106- , Length fs ~ Length (Apply fs as )
107106 , Length gs ~ Length bs
108- , Length gs ~ Length (Apply gs bs )
109107 , Length hs ~ Length cs
110- , Length hs ~ Length (Apply hs cs )
111108 , Length is ~ Length ds
112- , Length is ~ Length (Apply is ds )
113- , Take (Length as ) (Apply fs as :++ Apply hs cs ) ~ Apply fs as
114109 , Take (Length as ) (as :++ cs ) ~ as
115110 , Take (Length as ) (fs :++ hs ) ~ fs
116- , Drop (Length as ) (Apply fs as :++ Apply hs cs ) ~ Apply hs cs
117111 , Drop (Length as ) (as :++ cs ) ~ cs
118112 , Drop (Length as ) (fs :++ hs ) ~ hs
119- , AppendP gs bs ( Apply gs bs ) is ds ( Apply is ds )
113+ , AppendP gs bs is ds
120114 )
121- => AST. Circuitfs as ( Apply fs as ) gs bs ( Apply gs bs ) nfs -- ^ Left circuit
122- -> AST. Circuiths cs ( Apply hs cs ) is ds ( Apply is ds ) nhs -- ^ Right circuit
115+ => AST. Circuitfs as gs bs nfs -- ^ Left circuit
116+ -> AST. Circuiths cs is ds nhs -- ^ Right circuit
123117 -> AST. Circuit
124118 (fs :++ hs )
125119 (as :++ cs )
126- (Apply fs as :++ Apply hs cs )
127120 (gs :++ is )
128121 (bs :++ ds )
129- (Apply gs bs :++ Apply is ds )
130122 (nfs :+ nhs )
131- (<>) l r = IIn7 (inj (AST. Beside
123+ (<>) l r = IIn5 (inj (AST. Beside
132124infixr 5 <>
133125
134126{-|
@@ -142,40 +134,40 @@ In diagram form this would look like,
142134-}
143135swap
144136 :: (DataStore' '[f , g ] '[a , b ])
145- => AST. Circuitf , g ] '[a , b ] '[f a , g b ] '[ g , f ] '[b , a ] '[ g b , f a ] N2
146- swap = (IIn7 . inj) AST. Swap
137+ => AST. Circuitf , g ] '[a , b ] '[g , f ] '[b , a ] N2
138+ swap = (IIn5 . inj) AST. Swap
147139
148140{-|
149141Takes two values as input and drops the left input.
150142-}
151143dropL
152- :: (DataStore' '[f , g ] '[a , b ]) => AST. Circuitf , g ] '[a , b ] '[f a , g b ] '[g ] '[ b ] '[ g b ] N2
153- dropL = (IIn7 . inj) AST. DropL
144+ :: (DataStore' '[f , g ] '[a , b ]) => AST. Circuitf , g ] '[a , b ] '[g ] '[b ] N2
145+ dropL = (IIn5 . inj) AST. DropL
154146
155147{-|
156148Takes two values as input and drops the right input.
157149-}
158150dropR
159- :: (DataStore' '[f , g ] '[a , b ]) => AST. Circuitf , g ] '[a , b ] '[f a , g b ] '[f ] '[ a ] '[ f a ] N2
160- dropR = (IIn7 . inj) AST. DropR
151+ :: (DataStore' '[f , g ] '[a , b ]) => AST. Circuitf , g ] '[a , b ] '[f ] '[a ] N2
152+ dropR = (IIn5 . inj) AST. DropR
161153
162154{-|
163155Maps a circuit on the inputs
164156-}
165157mapC
166158 :: (DataStore' '[f ] '[[a ]], DataStore g [b ], Eq g [b ]), Eq a )
167- => AST. CircuitVar ] '[a ] '[Var a ] '[Var ] '[ b ] '[ Var b ] N1
168- -> AST. Circuitf ] '[[a ]] '[f [ a ]] '[ g ] '[[ b ]] '[ g [b ]] N1
169- mapC c = (IIn7 . inj) (AST. Map
159+ => AST. CircuitVar ] '[a ] '[Var ] '[b ] N1
160+ -> AST. Circuitf ] '[[a ]] '[g ] '[[b ]] N1
161+ mapC c = (IIn5 . inj) (AST. Map
170162
171163class (DataStore f a , Eq f a )) => ReplicateN n f a where
172- replicateN :: SNat n -> AST. Circuitf ] '[a ] '[ f a ] (Replicate n f ) (Replicate n a ) ( Apply ( Replicate n f ) ( Replicate n a )) N1
164+ replicateN :: SNat n -> AST. Circuitf ] '[a ] (Replicate n f ) (Replicate n a ) N1
173165
174166instance (DataStore f a , Eq a , Eq f a )) => ReplicateN ('Succ ('Succ 'Zero)) f a where
175167 replicateN (SSucc (SSucc SZero )) = replicate2
176168
177169instance (DataStore f a , Eq a , Eq f a )) => ReplicateN ('Succ ('Succ ('Succ 'Zero))) f a where
178170 replicateN (SSucc n) = replicate2 <-> id <> replicateN n
179171
180- replicateMany :: SNat m -> AST. Circuitfs as (Apply fs as ) ( fs :++ fs ) (as :++ as ) ( Apply ( fs :++ fs ) ( as :++ as ) ) m
172+ replicateMany :: SNat m -> AST. Circuitfs as (fs :++ fs ) (as :++ as ) m
181173replicateMany = undefined
0 commit comments