Merge pull request #2563 from clash-lang/vecfoldnon1

Drop `1 <= n` constraint from `Foldable (Vec n)` and from `Traversable (Vec n)`.

changelog/2023-08-16T19_26_52+02_00_vec_fold_zero

@@ -0,0 +1,3 @@
+CHANGED: The `Foldable (Vec n)` instance and `Traversable (Vec n)` instance no longer have the `1 <= n` constraint. `Foldable.{foldr1,foldl1,maximum,minimum}` functions now throw an error at run-/simulation-time, and also at HDL-generation time, for vectors of length zero.
+CHANGED: The `maximum` and `minimum` functions exported by `Clash.Prelude` work on non-empty vectors, instead of the more generic version from `Data.Foldable`.
+ADDED: `1 <= n => Foldable1 (Vec n)` instance (`base-4.18+` only)

clash-lib/clash-lib.cabal

@@ -281,7 +281,7 @@ Library
                       Clash.Primitives.GHC.Literal
                       Clash.Primitives.GHC.Word
                       Clash.Primitives.Intel.ClockGen
-                      Clash.Primitives.Prelude
+                      Clash.Primitives.Magic
                       Clash.Primitives.Sized.ToInteger
                       Clash.Primitives.Sized.Signed
                       Clash.Primitives.Sized.Vector

clash-lib/src/Clash/Driver.hs

@@ -139,7 +139,7 @@ import qualified Clash.Primitives.Sized.Vector    as P
 import qualified Clash.Primitives.GHC.Int         as P
 import qualified Clash.Primitives.GHC.Word        as P
 import qualified Clash.Primitives.Intel.ClockGen  as P
-import qualified Clash.Primitives.Prelude         as P
+import qualified Clash.Primitives.Magic           as P
 import qualified Clash.Primitives.Verification    as P
 import qualified Clash.Primitives.Xilinx.ClockGen as P
 import           Clash.Primitives.Types

clash-lib/src/Clash/Primitives/Prelude.hs → clash-lib/src/Clash/Primitives/Magic.hs

@@ -4,12 +4,12 @@
   License     :  BSD2 (see the file LICENSE)
   Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
 
-  Blackbox functions for primitives in one of the @Prelude@ modules.
+  Blackbox functions for primitives in the @Clash.Magic@ module.
 -}
 
 {-# LANGUAGE TemplateHaskellQuotes #-}
 
-module Clash.Primitives.Prelude
+module Clash.Primitives.Magic
   ( clashCompileErrorBBF
   ) where
 

clash-prelude/src/Clash/Explicit/Prelude.hs

@@ -13,8 +13,6 @@ defined in "Clash.Prelude".
 
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE QuasiQuotes #-}
-{-# LANGUAGE TemplateHaskellQuotes #-}
 
 {-# LANGUAGE Unsafe #-}
 
@@ -80,8 +78,6 @@ module Clash.Explicit.Prelude
   , isFalling
   , riseEvery
   , oscillate
-    -- * Static assertions
-  , clashCompileError
     -- * Testbench functions
   , assert
   , stimuliGenerator
@@ -154,8 +150,6 @@ where
 import Control.Applicative
 import Data.Bits
 import Data.Default.Class
-import Data.String.Interpolate (__i)
-import GHC.Stack (HasCallStack, withFrozenCallStack)
 import GHC.TypeLits
 #if MIN_VERSION_base(4,18,0)
   hiding (SNat, SSymbol, fromSNat)
@@ -164,7 +158,6 @@ import GHC.TypeLits.Extra
 import Language.Haskell.TH.Syntax  (Lift(..))
 import Clash.HaskellPrelude
 
-import Clash.Annotations.Primitive (Primitive(..))
 import Clash.Annotations.TopEntity
 import Clash.Class.AutoReg
 import Clash.Class.BitPack
@@ -290,23 +283,3 @@ windowD clk rst en x =
       next = x +>> prev
   in  prev
 {-# INLINABLE windowD #-}
-
--- | Same as 'error' but will make HDL generation fail if included in the
--- final circuit.
---
--- This is useful for the error case of static assertions.
---
--- Note that the error message needs to be a literal, and during HDL generation
--- the error message does not include a stack trace, so it had better be
--- descriptive.
-clashCompileError :: forall a . HasCallStack => String -> a
-clashCompileError msg = withFrozenCallStack $ error msg
--- See: https://github.com/clash-lang/clash-compiler/pull/2511
-{-# CLASH_OPAQUE clashCompileError #-}
-{-# ANN clashCompileError (
-  let primName = 'clashCompileError
-  in InlineYamlPrimitive [minBound..] [__i|
-    BlackBoxHaskell:
-      name: #{primName}
-      templateFunction: Clash.Primitives.Prelude.clashCompileErrorBBF
-    |]) #-}

clash-prelude/src/Clash/HaskellPrelude.hs

@@ -26,7 +26,7 @@ import Prelude hiding
   ((++), (!!), concat, concatMap, drop, even, foldl, foldl1, foldr, foldr1, head, init,
    iterate, last, length, map, odd, repeat, replicate, reverse, scanl, scanl1,
    scanr, scanr1, splitAt, tail, take, unzip, unzip3, zip, zip3, zipWith, zipWith3, undefined,
-   (^), getChar, putChar, getLine, (&&), (||), not)
+   (^), getChar, putChar, getLine, (&&), (||), not, maximum, minimum)
 
 import qualified Prelude
 import GHC.Magic (noinline)

clash-prelude/src/Clash/Magic.hs

@@ -17,6 +17,8 @@ Refer to "Clash.Annotations.TopEntity" for controlling naming of entities
 -}
 
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
 
 module Clash.Magic
   (
@@ -36,12 +38,17 @@ module Clash.Magic
   -- ** Utilities to differentiate between simulation and generating HDL
   , clashSimulation
   , SimOnly (..)
+
+  -- * Static assertions
+  , clashCompileError
   ) where
 
+import Data.String.Interpolate     (__i)
+import GHC.Stack                   (HasCallStack, withFrozenCallStack)
 import Clash.NamedTypes            ((:::))
 import GHC.TypeLits                (Nat,Symbol)
 import Clash.Promoted.Symbol       (SSymbol)
-import Clash.Annotations.Primitive (hasBlackBox)
+import Clash.Annotations.Primitive (Primitive(..), hasBlackBox)
 
 -- | Prefix instance and register names with the given 'Symbol'
 prefixName
@@ -281,3 +288,23 @@ instance Semigroup a => Semigroup (SimOnly a) where
 
 instance Monoid a => Monoid (SimOnly a) where
   mempty = SimOnly mempty
+
+-- | Same as 'error' but will make HDL generation fail if included in the
+-- final circuit.
+--
+-- This is useful for the error case of static assertions.
+--
+-- Note that the error message needs to be a literal, and during HDL generation
+-- the error message does not include a stack trace, so it had better be
+-- descriptive.
+clashCompileError :: forall a . HasCallStack => String -> a
+clashCompileError msg = withFrozenCallStack $ error msg
+-- See: https://github.com/clash-lang/clash-compiler/pull/2511
+{-# CLASH_OPAQUE clashCompileError #-}
+{-# ANN clashCompileError (
+  let primName = 'clashCompileError
+  in InlineYamlPrimitive [minBound..] [__i|
+    BlackBoxHaskell:
+      name: #{primName}
+      templateFunction: Clash.Primitives.Magic.clashCompileErrorBBF
+    |]) #-}

clash-prelude/src/Clash/Prelude.hs

@@ -104,8 +104,6 @@ module Clash.Prelude
   , isFalling
   , riseEvery
   , oscillate
-    -- * Static assertions
-  , clashCompileError
     -- * Tracing
     -- ** Simple
   , traceSignal1
@@ -195,7 +193,6 @@ import           Clash.Class.Num
 import           Clash.Class.Parity
 import           Clash.Class.Resize
 import qualified Clash.Explicit.Prelude      as E
-import           Clash.Explicit.Prelude (clashCompileError)
 import           Clash.Hidden
 import           Clash.Magic
 import           Clash.NamedTypes

clash-prelude/src/Clash/Sized/Vector.hs

@@ -1,7 +1,7 @@
 {-|
 Copyright  :  (C) 2013-2016, University of Twente,
                   2017     , Myrtle Software Ltd
-                  2022     , QBayLogic B.V.
+                  2022-2023, QBayLogic B.V.
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
 -}
@@ -75,7 +75,7 @@ module Clash.Sized.Vector
   , foldr, foldl, foldr1, foldl1, fold
   , ifoldr, ifoldl
     -- ** Specialized folds
-  , dfold, dtfold, vfold
+  , dfold, dtfold, vfold, maximum, minimum
     -- * Prefix sums (scans)
   , scanl, scanl1, scanr, scanr1, postscanl, postscanr
   , mapAccumL, mapAccumR
@@ -107,6 +107,9 @@ import Data.Constraint.Nat        (leZero)
 import Data.Data
   (Data (..), Constr, DataType, Fixity (..), Typeable, mkConstr, mkDataType)
 import Data.Either                (isLeft)
+#if MIN_VERSION_base(4,18,0)
+import qualified Data.Foldable1   as F1
+#endif
 import Data.Default.Class         (Default (..))
 import qualified Data.Foldable    as F
 import Data.Kind                  (Type)
@@ -129,7 +132,7 @@ import Prelude                    hiding ((++), (!!), concat, concatMap, drop,
                                           repeat, replicate, reverse, scanl,
                                           scanl1, scanr, scanr1, splitAt, tail,
                                           take, unzip, unzip3, zip, zip3, zipWith,
-                                          zipWith3)
+                                          zipWith3, maximum, minimum)
 import qualified Data.String.Interpolate as I
 import qualified Prelude          as P
 import Test.QuickCheck
@@ -138,9 +141,13 @@ import Unsafe.Coerce              (unsafeCoerce)
 
 import Clash.Annotations.Primitive
   (Primitive(InlineYamlPrimitive), HDL(..), dontTranslate, hasBlackBox)
+import Clash.Magic (clashCompileError)
 import Clash.Promoted.Nat
-  (SNat (..), SNatLE (..), UNat (..), compareSNat, leToPlus, pow2SNat,
+  (SNat (..), SNatLE (..), UNat (..), compareSNat, pow2SNat,
    snatProxy, snatToInteger, subSNat, withSNat, toUNat, natToInteger)
+#if MIN_VERSION_base(4,18,0)
+import Clash.Promoted.Nat (leToPlus)
+#endif
 import Clash.Promoted.Nat.Literals (d1)
 import Clash.Sized.Internal.BitVector (Bit, BitVector (..), split#)
 import Clash.Sized.Index          (Index)
@@ -317,25 +324,44 @@ instance KnownNat n => Applicative (Vec n) where
 "zipWith$map" forall f xs ys. zipWith (\g a -> g a) (map f xs) ys = zipWith f xs ys
   #-}
 
-instance (KnownNat n, 1 <= n) => F.Foldable (Vec n) where
-  fold      = leToPlus @1 @n $ fold mappend
-  foldMap f = leToPlus @1 @n $ fold mappend . map f
+instance KnownNat n => F.Foldable (Vec n) where
+  fold Nil      = mempty
+  fold z@Cons{} = fold mappend z
+  foldMap _ Nil      = mempty
+  foldMap f z@Cons{} = fold mappend (map f z)
   foldr     = foldr
   foldl     = foldl
-  foldr1 f  = leToPlus @1 @n $ foldr1 f
-  foldl1 f  = leToPlus @1 @n $ foldl1 f
+  foldr1 _ Nil      = clashCompileError "foldr1: empty Vec"
+  foldr1 f z@Cons{} = foldr1 f z
+  foldl1 _ Nil      = clashCompileError "foldl1: empty Vec"
+  foldl1 f z@Cons{} = foldl1 f z
   toList    = toList
+  null Nil  = True
   null _    = False
   length    = length
-  maximum   = leToPlus @1 @n $ fold (\x y -> if x >= y then x else y)
-  minimum   = leToPlus @1 @n $ fold (\x y -> if x <= y then x else y)
-  sum       = leToPlus @1 @n $ fold (+)
-  product   = leToPlus @1 @n $ fold (*)
+  maximum Nil      = clashCompileError "maximum: empty Vec"
+  maximum z@Cons{} = fold (\x y -> if x >= y then x else y) z
+  minimum Nil      = clashCompileError "minimum: empty Vec"
+  minimum z@Cons{} = fold (\x y -> if x <= y then x else y) z
+  sum Nil      = 0
+  sum z@Cons{} = fold (+) z
+  product Nil      = 1
+  product z@Cons{} = fold (*) z
+
+#if MIN_VERSION_base(4,18,0)
+instance (KnownNat n, 1 <= n) => F1.Foldable1 (Vec n) where
+  fold1         = leToPlus @1 @n $ fold (<>)
+  foldMap1 f    = leToPlus @1 @n $ fold (<>) . map f
+  maximum       = leToPlus @1 @n maximum
+  minimum       = leToPlus @1 @n minimum
+  head          = leToPlus @1 @n head
+  last          = leToPlus @1 @n last
+#endif
 
 instance Functor (Vec n) where
   fmap = map
 
-instance (KnownNat n, 1 <= n) => Traversable (Vec n) where
+instance KnownNat n => Traversable (Vec n) where
   traverse = traverse#
 
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -2492,6 +2518,20 @@ vfold :: forall k a b . KnownNat k
 vfold f xs = dfold (Proxy @(VCons b)) f Nil xs
 {-# INLINE vfold #-}
 
+-- | The largest element of a non-empty vector
+maximum ::
+  Ord a =>
+  Vec (n + 1) a ->
+  a
+maximum = fold (\x y -> if x >= y then x else y)
+
+-- | The least element of a non-empty vector
+minimum ::
+  Ord a =>
+  Vec (n + 1) a ->
+  a
+minimum = fold (\x y -> if x <= y then x else y)
+
 -- | Apply a function to every element of a vector and the element's position
 -- (as an 'SNat' value) in the vector.
 --

clash-prelude/src/Clash/Sized/Vector.hs-boot

@@ -13,13 +13,13 @@ Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 module Clash.Sized.Vector where
 
 import Data.Kind (Type)
-import GHC.TypeLits  (KnownNat, Nat, type (<=))
+import GHC.TypeLits  (KnownNat, Nat)
 import {-# SOURCE #-} Clash.Sized.Internal.BitVector (BitVector, Bit)
 
 type role Vec nominal representational
 data Vec :: Nat -> Type -> Type
 
-instance (KnownNat n, 1 <= n) => Foldable (Vec n)
+instance KnownNat n => Foldable (Vec n)
 
 bv2v  :: KnownNat n => BitVector n -> Vec n Bit
 map   :: (a -> b) -> Vec n a -> Vec n b