Creating a fold that allows the type to change after each repeated function call, in order to call a function n times without recursion
Your base
case was wrong; it should be
base :: (Ord a) => SplitHalf a @@ 0
base = (id, bitonicMerge id)
Putting it all together, here's a fully working version, tested on GHC 8.0.2 (but it should work all the same on a GHC 8.0.2-based CLaSH, modulo the Prelude
import stuff). It turns out the operationList
thing is not used except for its spine, so we can use a Vec n ()
instead.
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-redundant-constraints #-}
{-# LANGUAGE NoImplicitPrelude #-}
import Prelude (Integer, (+), Num, ($), undefined, id, fst, Int, otherwise)
import CLaSH.Sized.Vector
import CLaSH.Promoted.Nat
import Data.Singletons
import GHC.TypeLits
import Data.Ord
type ExpVec k a = Vec (2 ^ k) a
data SplitHalf (a :: *) (f :: TyFun Nat *) :: *
type instance Apply (SplitHalf a) k = (ExpVec k a -> ExpVec k a, ExpVec (k + 1) a -> ExpVec (k + 1) a)
generateBitonicSortN2 :: forall k a . (Ord a, KnownNat k) => SNat k -> ExpVec k a -> ExpVec k a
generateBitonicSortN2 k = fst $ dfold (Proxy :: Proxy (SplitHalf a)) step base (replicate k ())
where
step :: SNat l -> () -> SplitHalf a @@ l -> SplitHalf a @@ (l+1)
step SNat _ (sort, merge) = (bitonicSort sort merge, bitonicMerge merge)
base = (id, bitonicMerge id)
This works as expected, e.g.:
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec2
<9,2>
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec4
<9,8,6,2>
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec8
<9,8,7,6,3,2,1,0>
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec16
<9,8,8,7,7,6,6,5,4,3,3,2,2,1,0,0>
*Main>