Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions circuitflow.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
97 changes: 93 additions & 4 deletions src/Pipeline/Circuit.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -23,15 +25,16 @@ module Pipeline.Circuit
, dropL
, dropR
, mapC
, replicateInputs
) where


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)
Expand Down Expand Up @@ -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
32 changes: 32 additions & 0 deletions src/Pipeline/Internal/Common/TypeList.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE UndecidableInstances #-}
module Pipeline.Internal.Common.TypeList where

import Pipeline.Internal.Common.Nat (Nat (..))
Expand Down Expand Up @@ -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
11 changes: 9 additions & 2 deletions src/Pipeline/Internal/Core/CircuitAST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down
26 changes: 25 additions & 1 deletion tests/Pipeline/Network/MinimalTests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ minimalTests = testGroup
"Minimal Examples"
[ idTests
, replicate2Tests
, replicate3Tests
, thenTests
, besideTests
, swapTests
Expand All @@ -33,6 +34,7 @@ minimalTests = testGroup
, functionTaskTests
, multiInputTaskTests
, mapTests
, replicateInputsTests
]


Expand Down Expand Up @@ -84,7 +86,7 @@ replicate2Tests = testGroup
out <- fetch' o
out @?= HCons 0 (HCons 0 HNil)
]

replicate3Circuit
:: Circuit
'[Var]
Expand All @@ -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
Expand Down