dfold_.hs

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}

module DFold_ (dfold_, subMonotone1) where

import Clash.Prelude

import Data.Singletons (TyFun, Apply, type (@@))
import Data.Proxy
import Data.Kind
import Data.Constraint
import Unsafe.Coerce

axiom :: forall a b . Dict (a ~ b)
axiom = unsafeCoerce (Dict @(a ~ a))


subMonotone1 :: forall a b c . (a <= b, c <= a) :- (a - c <= b - c)
subMonotone1 = Sub axiom



dfold_ :: forall p k a . KnownNat k
      => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
      -> (forall l . (l <= k - 1) => SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))
      -- ^ Function to fold.
      --
      -- __NB__: The @SNat l@ is __not__ the index (see (`!!`)) to the
      -- element /a/. @SNat l@ is the number of elements that occur to the
      -- right of /a/.
      -> (p @@ 0) -- ^ Initial element
      -> Vec k a -- ^ Vector to fold over
      -> (p @@ k)
dfold_ _ f z xs = go (snatProxy (asNatProxy xs)) xs
  where
    go :: forall n . (n <= k) => SNat n -> Vec n a -> (p @@ n)
    go _ Nil                        = z
    go s@SNat (y `Cons` (ys :: Vec (n - 1) a)) =
      let s' = s `subSNat` d1
      in  case subMonotone1 @n @k @1 of
            Sub Dict -> f s' y (go s' ys)
{-# NOINLINE dfold_ #-}