diff --git a/circuitflow.cabal b/circuitflow.cabal index 6ee33b6..af844df 100644 --- a/circuitflow.cabal +++ b/circuitflow.cabal @@ -73,6 +73,7 @@ library , directory hs-source-dirs: src default-language: Haskell2010 + ghc-options: -fprint-potential-instances -freduction-depth=201 test-suite test default-language: Haskell2010 diff --git a/src/Pipeline/Circuit.hs b/src/Pipeline/Circuit.hs index 615b34f..4e29418 100644 --- a/src/Pipeline/Circuit.hs +++ b/src/Pipeline/Circuit.hs @@ -8,6 +8,8 @@ Maintainer : haskell@rly.rocks This package contains all the constructors needed to build a 'Circuit'. -} + +{-# LANGUAGE UndecidableInstances #-} module Pipeline.Circuit ( -- * Main Type @@ -23,6 +25,7 @@ module Pipeline.Circuit , dropL , dropR , mapC + , replicateInputs ) where @@ -30,8 +33,8 @@ import Pipeline.Internal.Common.IFunctor (IFix5 (..)) import Pipeline.Internal.Common.IFunctor.Modular ((:<:) (..)) import Pipeline.Internal.Common.Nat (IsNat, N1, N2, Nat (..), SNat (..), (:+)) -import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, - Take, Replicate, (:++)) +import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, Swap, Pair, Transpose, Concat, + Take, Replicate, Duplicate, (:++)) import qualified Pipeline.Internal.Core.CircuitAST as AST import Pipeline.Internal.Core.DataStore (DataStore, DataStore', Var) @@ -169,5 +172,91 @@ instance (DataStore f a, Eq a, Eq (f a)) => ReplicateN ('Succ ('Succ 'Zero)) f a instance (DataStore f a, Eq a, Eq (f a)) => ReplicateN ('Succ ('Succ ('Succ 'Zero))) f a where replicateN (SSucc n) = replicate2 <-> id <> replicateN n -replicateMany :: SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m -replicateMany = undefined + +class (DataStore' fs as) => ReplicateInputs m fs as where + replicateInputs :: ( Length fs ~ m + , Length as ~ m + , Length (Duplicate fs) ~ Length (Duplicate as) + , ('Succ 'Zero :+ m) ~ 'Succ m + , IsNat m + ) => SNat m -> AST.Circuit fs as (Duplicate fs) (Duplicate as) m + +instance (DataStore f a, Eq a, Eq (f a)) => ReplicateInputs ('Succ 'Zero) '[f] '[a] where + replicateInputs (SSucc SZero) = replicate2 + +instance ( DataStore f a + , DataStore' fs as + , DataStore' (Duplicate fs) (Duplicate as) + , ReplicateInputs ('Succ n) fs as + , Length fs ~ 'Succ n + , IsNat n + , Eq a + , Eq (f a) + ) => ReplicateInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where + replicateInputs (SSucc (SSucc n)) = replicate2 <> replicateInputs (SSucc n) + +class DataStore' fs as => OrganiseInputs m fs as where + organiseInputs :: SNat m + -> AST.Circuit fs + as + (Concat (Transpose (Pair fs))) + (Concat (Transpose (Pair as))) + (Length fs) + +instance (DataStore f a, DataStore g b, Eq a, Eq (f a), Eq b, Eq (g b)) => OrganiseInputs ('Succ 'Zero) '[f, g] '[a, b] where + organiseInputs (SSucc SZero) = id <> id + +-- Problem with the type as I need it to be something like f ': (fs :++ '[g]) +-- function peels one off each end of the list, which can't do with Haskell list! +-- Any other way to write a function that does the same thing...? +-- Currently its 'centre-recursive', a tail-recursive function would probably avoid the problem +instance (DataStore f a, DataStore' fs as, Eq a, Eq (f a)) => OrganiseInputs ('Succ ('Succ n)) (f ': fs) (a ': as) where + organiseInputs = undefined -- Stuck here + +-- organiseInputs :: (DataStore' fs as) => SNat n +-- -> AST.Circuit fs +-- as +-- (Concat (Transpose (Pair fs))) +-- (Concat (Transpose (Pair as))) +-- (Length fs) +-- organiseInputs (SSucc SZero) = id <> id +-- organiseInputs (SSucc n) = (id <> swapInputs n <> id +-- <-> id <> organiseInputs n <> id) + +class DataStore' fs as => SwapInputs n fs as where + swapInputs :: SNat n -> AST.Circuit fs as (Swap n fs) (Swap n as) (Length fs) + +instance (DataStore f a, DataStore g b, Eq b, Eq (g b), Eq a, Eq (f a)) => SwapInputs ('Succ 'Zero) '[f, g] '[a, b] where + swapInputs (SSucc SZero) = swap + +instance ( DataStore f a + , DataStore g b + , SwapInputs ('Succ n) hs cs + , Length hs ~ Length cs + , Length (Swap ('Succ n) hs) ~ Length (Swap ('Succ n) cs) + , (N2 :+ Length cs) ~ 'Succ ('Succ (Length cs)) + , (DataStore' (Swap ('Succ n) hs) (Swap ('Succ n) cs)) + , IsNat (Length cs) + , Eq b, Eq (g b) + , Eq a, Eq (f a) + ) => SwapInputs ('Succ ('Succ n)) (f ': g ': hs) (a ': b ': cs) where + swapInputs (SSucc n) = swap <> swapInputs n + +replicateMany :: ( 'Succ 'Zero :+ m ~ 'Succ m + , Length fs ~ m + , Length as ~ m + , Length (Apply fs as) ~ m + , Length (Duplicate fs) ~ Length (Duplicate as) + , (as :++ as) ~ Concat (Transpose (Pair (Duplicate as))) + , (fs :++ fs) ~ Concat (Transpose (Pair (Duplicate fs))) + , ReplicateInputs m fs as + , OrganiseInputs m (Duplicate fs) (Duplicate as) + , IsNat m + , DataStore' (Duplicate fs) (Duplicate as) + , DataStore' fs as + , DataStore' (Concat (Transpose (Pair (Duplicate fs)))) (Concat (Transpose (Pair (Duplicate as)))) + ) => SNat m -> AST.Circuit fs as (fs :++ fs) (as :++ as) m +replicateMany n = replicateInputs n + <-> + organiseInputs n + -- where diff --git a/src/Pipeline/Internal/Common/TypeList.hs b/src/Pipeline/Internal/Common/TypeList.hs index 3a210b7..0e7ecc3 100644 --- a/src/Pipeline/Internal/Common/TypeList.hs +++ b/src/Pipeline/Internal/Common/TypeList.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE UndecidableInstances #-} module Pipeline.Internal.Common.TypeList where import Pipeline.Internal.Common.Nat (Nat (..)) @@ -33,3 +34,34 @@ type family Apply (fs :: [Type -> Type]) (as :: [Type]) where type family Replicate (n :: Nat) (a :: k) :: [k] where Replicate 'Zero _ = '[] Replicate ('Succ n) x = x ': Replicate n x + +type family Duplicate (a :: [k]) :: [k] where + Duplicate '[] = '[] + Duplicate (x ': xs) = x ': x ': Duplicate xs + +type family Swap (n :: Nat) (a :: [k]) :: [k] where + Swap n '[] = '[] + Swap 'Zero l = l + Swap ('Succ n) (x ': y ': xs) = y ': x ': Swap n xs + + +type family Pair (xs :: [k]) :: [[k]] where + Pair '[] = '[] + Pair (x ': y ': xs) = '[x, y] ': Pair xs + +type family Concat (xss :: [[k]]) :: [k] where + Concat '[] = '[] + Concat ('[] ': l) = Concat l + Concat ((x ': xs) ': l) = x ': Concat (xs ': l) + +type family Transpose (xss :: [[k]]) :: [[k]] where + Transpose ('[] ': _) = '[] + Transpose xss = Heads xss ': Transpose (Tails xss) + +type family Heads (xss :: [[k]]) :: [k] where + Heads '[] = '[] + Heads ((x ': xs) ': xss) = x ': Heads xss + +type family Tails (xss :: [[k]]) :: [[k]] where + Tails '[] = '[] + Tails ((x ': xs) ': xss) = xs ': Tails xss diff --git a/src/Pipeline/Internal/Core/CircuitAST.hs b/src/Pipeline/Internal/Core/CircuitAST.hs index 6e5604b..c57fc81 100644 --- a/src/Pipeline/Internal/Core/CircuitAST.hs +++ b/src/Pipeline/Internal/Core/CircuitAST.hs @@ -23,8 +23,8 @@ import Pipeline.Internal.Common.IFunctor (IFix5 (..), import Pipeline.Internal.Common.IFunctor.Modular ((:+:) (..)) import Pipeline.Internal.Common.Nat (IsNat (..), N1, N2, Nat (..), (:+), - (:=)) -import Pipeline.Internal.Common.TypeList (Apply, Drop, Length, + (:=), SNat (..)) +import Pipeline.Internal.Common.TypeList (Drop, Length, Take, (:++)) import Pipeline.Internal.Core.DataStore (DataStore, DataStore', Var) @@ -42,6 +42,13 @@ data Replicate (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Na Replicate ::(DataStore' '[f] '[a]) => Replicate iF '[f] '[a] [f, f] '[a, a] N1 +data ReplicateManyN (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Nat -> Type) + (inputsS :: [Type -> Type]) (inputsT :: [Type]) + (outputsS :: [Type -> Type]) (outputsT :: [Type]) (ninputs :: Nat) where + ReplicateManyN ::(DataStore' '[f] '[a]) + => SNat n -> SNat m -> ReplicateManyN iF '[f] '[a] [f, f] '[a, a] N1 + + data Then (iF :: [Type -> Type] -> [Type] -> [Type -> Type] -> [Type] -> Nat -> Type) (inputsS :: [Type -> Type]) (inputsT :: [Type]) (outputsS :: [Type -> Type]) (outputsT :: [Type]) (ninputs :: Nat) where diff --git a/tests/Pipeline/Network/MinimalTests.hs b/tests/Pipeline/Network/MinimalTests.hs index c8d9102..e67ef3a 100644 --- a/tests/Pipeline/Network/MinimalTests.hs +++ b/tests/Pipeline/Network/MinimalTests.hs @@ -25,6 +25,7 @@ minimalTests = testGroup "Minimal Examples" [ idTests , replicate2Tests + , replicate3Tests , thenTests , besideTests , swapTests @@ -33,6 +34,7 @@ minimalTests = testGroup , functionTaskTests , multiInputTaskTests , mapTests + , replicateInputsTests ] @@ -84,7 +86,7 @@ replicate2Tests = testGroup out <- fetch' o out @?= HCons 0 (HCons 0 HNil) ] - + replicate3Circuit :: Circuit '[Var] @@ -104,6 +106,28 @@ replicate3Tests = testGroup out <- fetch' o out @?= HCons 0 (HCons 0 (HCons 0 HNil)) ] + + +replicateInputsCircuit + :: Circuit + '[Var , Var] + '[Int , Int] + '[Var , Var , Var , Var] + '[Int , Int , Int , Int] + N2 +replicateInputsCircuit = replicateInputs (SSucc (SSucc SZero)) + +replicateInputsTests :: TestTree +replicateInputsTests = testGroup + "(replicateN 3) should" + [ testCase "return a trupled input value" $ do + var1 <- varWith 0 + var2 <- varWith 2 + let i = HCons' var1 (HCons' var2 HNil') + (Right o) <- singleInputTest replicateInputsCircuit i + out <- fetch' o + out @?= HCons 0 (HCons 0 (HCons 2 (HCons 2 HNil))) + ] -- Tests for the 'Then' constructor thenCircuit