Use (:>) in favor of Cons

clash-lib/src/Clash/Core/TermLiteral.hs

@@ -52,7 +52,7 @@ import           Clash.Core.Term                 (Term(Literal, Data), collectAr
 import           Clash.Promoted.Nat
 import           Clash.Promoted.Nat.Unsafe
 import           Clash.Sized.Index               (Index)
-import           Clash.Sized.Vector              (Vec (Nil, Cons), fromList)
+import           Clash.Sized.Vector              (Vec (Nil, (:>)), fromList)
 import qualified Clash.Util.Interpolate          as I
 import qualified Clash.Verification.Internal     as Cv
 
@@ -193,7 +193,7 @@ instance (TermLiteral a, KnownNat n) => TermLiteral (Vec n a) where
       case constr of
         Data (MkData{dcName=Name{nameOcc}})
           | nameOcc == showt 'Nil -> Right []
-          | nameOcc == showt 'Cons ->
+          | nameOcc == showt '(:>) ->
             case lefts args of
               [_gadtProof, c0, cs0] -> do
                 c1 <- termToData @a c0

clash-lib/src/Clash/Core/Util.hs

@@ -98,7 +98,7 @@ unsafeCoerceTy =
 
 -- | Create a vector of supplied elements
 mkVec :: DataCon -- ^ The Nil constructor
-      -> DataCon -- ^ The Cons (:>) constructor
+      -> DataCon -- ^ The (:>) constructor
       -> Type    -- ^ Element type
       -> Integer -- ^ Length of the vector
       -> [Term]  -- ^ Elements to put in the vector
@@ -128,7 +128,7 @@ mkVec nilCon consCon resTy = go
                    _ -> error "impossible"
 
 -- | Append elements to the supplied vector
-appendToVec :: DataCon -- ^ The Cons (:>) constructor
+appendToVec :: DataCon -- ^ The (:>) constructor
             -> Type    -- ^ Element type
             -> Term    -- ^ The vector to append the elements to
             -> Integer -- ^ Length of the vector
@@ -161,7 +161,7 @@ extractElems
   -> InScopeSet
   -- ^ (Superset of) in scope variables
   -> DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ The element type
   -> Char
@@ -609,10 +609,10 @@ shouldSplit0 tcm (TyConApp tcNm tyArgs)
   -- Project the n'th value out of a vector
   --
   -- >>> mkVecSelector subj 0
-  -- case subj of Cons x xs -> x
+  -- case subj of x :> xs -> x
   --
   -- >>> mkVecSelector subj 2
-  -- case (case (case subj of Cons x xs -> xs) of Cons x xs -> xs) of Cons x xs -> x
+  -- case (case (case subj of x :> xs -> xs) of x :> xs -> xs) of x :> xs -> x
   mkVecSelector :: forall m . MonadUnique m => InScopeSet -> Term -> Integer -> m Term
   mkVecSelector is0 subj 0 =
     mkSelectorCase ($(curLoc) ++ "mkVecSelector") is0 tcm subj 2 1

clash-lib/src/Clash/Netlist.hs

@@ -1056,10 +1056,10 @@ mkDcApplication declType [dstHType] bndr dc args = do
       Vector 0 _ -> return (HW.DataCon dstHType VecAppend [])
       Vector 1 _ -> case argExprsFiltered of
                       [e] -> return (HW.DataCon dstHType VecAppend [e])
-                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `Cons`: " ++ showPpr args
+                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `(:>)`: " ++ showPpr args
       Vector _ _ -> case argExprsFiltered of
                       [e1,e2] -> return (HW.DataCon dstHType VecAppend [e1,e2])
-                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `Cons`: " ++ showPpr args
+                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `(:>)`: " ++ showPpr args
       MemBlob _ _ ->
         case compare 6 (length argExprsFiltered) of
           EQ -> return (HW.DataCon dstHType (DC (dstHType,0)) argExprsFiltered)

clash-lib/src/Clash/Netlist/Util.hs

@@ -538,7 +538,7 @@ mkADT builtInTranslation reprs m tyString tc args = case tyConDataCons (UniqMap.
 -- data Vec :: Nat -> Type -> Type
 --  where
 --   Nil  :: Vec 0 a
---   Cons :: forall m . (n ~ m + 1) => a -> Vec m a -> Vec n a
+--   (:>) :: forall m . (n ~ m + 1) => a -> Vec m a -> Vec n a
 --
 -- where we can generate a type for `m` when we know `n` (by doing `n-1`).
 --

clash-lib/src/Clash/Normalize/PrimitiveReductions.hs

@@ -184,7 +184,7 @@ vecTailTy vecNm =
 -- vector, the latter the tail.
 extractHeadTail
   :: DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ Element type
   -> Integer
@@ -206,15 +206,15 @@ extractHeadTail consCon elTy n vec =
       in
         ( Case vec elTy [(pat, Var el)]
         , Case vec restTy [(pat, Var rest)] )
-    _ -> error "extractHeadTail: failed to instantiate Cons DC"
+    _ -> error "extractHeadTail: failed to instantiate (:>) DC"
  where
   tys = [(LitTy (NumTy n)), elTy, (LitTy (NumTy (n-1)))]
 
 -- | Create a vector of supplied elements
 mkVecCons
   :: HasCallStack
   => DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ Element type
   -> Integer
@@ -235,7 +235,7 @@ mkVecCons consCon resTy n h t
                             , Left (primCo consCoTy)
                             , Left h
                             , Left t ]
-    _ -> error "mkVecCons: failed to instantiate Cons DC"
+    _ -> error "mkVecCons: failed to instantiate (:>) DC"
 
 -- | Create an empty vector
 mkVecNil
@@ -568,7 +568,7 @@ reduceTraverse n aTy fTy bTy dict fun arg (TransformContext is0 ctx) = do
 -- > (:>) <$> x0 <*> ((:>) <$> x1 <*> pure Nil)
 mkTravVec :: TyConName -- ^ Vec tcon
           -> DataCon   -- ^ Nil con
-          -> DataCon   -- ^ Cons con
+          -> DataCon   -- ^ (:>) con
           -> Term      -- ^ 'pure' term
           -> Term      -- ^ '<*>' term
           -> Term      -- ^ 'fmap' term
@@ -983,7 +983,7 @@ reduceUnconcat unconcatPrimInfo n m aTy _kn sm arg (TransformContext inScope _ct
                                   , Left (snd nextVec)
                                   ]
             -- let (mvec,nextVec) = splitAt sm arg
-            -- in Cons mvec (unconcat sm nextVec)
+            -- in mvec :> (unconcat sm nextVec)
             lBody = mkVecCons consCon innerVecTy n mvec nextUnconcat
             lb = Letrec lbs lBody
 

clash-lib/src/Clash/Normalize/Transformations/Case.hs

@@ -670,24 +670,24 @@ caseOneAlt e = return e
 -- existential should be. For example, consider Vec:
 --
 --    data Vec :: Nat -> Type -> Type where
---      Nil       :: Vec 0 a
---      Cons x xs :: a -> Vec n a -> Vec (n + 1) a
+--      Nil     :: Vec 0 a
+--      x :> xs :: a -> Vec n a -> Vec (n + 1) a
 --
 -- Thus, 'null' (annotated with existentials) could look like:
 --
 --    null :: forall n . Vec n Bool -> Bool
 --    null v =
 --      case v of
 --        Nil  {n ~ 0}                                     -> True
---        Cons {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False
+--        (:>) {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False
 --
 -- When it's applied to a vector of length 5, this becomes:
 --
 --    null :: Vec 5 Bool -> Bool
 --    null v =
 --      case v of
 --        Nil  {5 ~ 0}                                     -> True
---        Cons {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False
+--        (:>) {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False
 --
 -- This function solves 'n1' and replaces every occurrence with its solution. A
 -- very limited number of solutions are currently recognized: only adds (such

clash-lib/src/Clash/Normalize/Transformations/Letrec.hs

@@ -40,7 +40,7 @@ import qualified Data.Text.Extra as Text
 import GHC.Stack (HasCallStack)
 
 import Clash.Annotations.BitRepresentation.Deriving (dontApplyInHDL)
-import Clash.Sized.Vector as Vec (Vec(Cons), splitAt)
+import Clash.Sized.Vector as Vec (Vec((:>)), splitAt)
 
 import Clash.Annotations.Primitive (extractPrim)
 import Clash.Core.DataCon (DataCon(..))
@@ -151,9 +151,9 @@ removeUnusedExpr _ e@(Case _ _ [(DataPat _ [] xs,altExpr)]) =
      else return e
 
 -- Replace any expression that creates a Vector of size 0 within the application
--- of the Cons constructor, by the Nil constructor.
+-- of the (:>) constructor, by the Nil constructor.
 removeUnusedExpr _ e@(collectArgsTicks -> (Data dc, [_,Right aTy,Right nTy,_,Left a,Left nil],ticks))
-  | nameOcc (dcName dc) == Text.showt 'Vec.Cons
+  | nameOcc (dcName dc) == Text.showt '(Vec.:>)
   = do
     tcm <- Lens.view tcCache
     case runExcept (tyNatSize tcm nTy) of

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

@@ -279,9 +279,9 @@ getLine (File fp) (Reg r) = SimIO $ do
   return 0
  where
    rep :: String -> Vec m (Unsigned 8) -> Vec m (Unsigned 8)
-   rep []     vs          = vs
-   rep (x:xs) (Cons _ vs) = Cons (toEnum (fromEnum x)) (rep xs vs)
-   rep _      Nil         = Nil
+   rep []     vs        = vs
+   rep (x:xs) (_ :> vs) = toEnum (fromEnum x) :> rep xs vs
+   rep _      Nil       = Nil
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE getLine #-}
 {-# ANN getLine hasBlackBox #-}

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

@@ -51,7 +51,10 @@ class VecToTuple a where
   -- The following would produce a warning even though we can be sure
   -- no other pattern can ever apply:
   --
-  -- >>> (a :> b :> c :> Nil) = myVec
+  -- >>> :{
+  -- a, b, c :: Int
+  -- (a :> b :> c :> Nil) = myVec
+  -- :}
   --
   -- 'vecToTuple' can be used to work around the warning:
   --

clash-prelude/src/Clash/Tutorial.hs

@@ -2114,8 +2114,8 @@ Here is a list of Haskell features for which the Clash compiler has only
 
         @
         mapV :: (a -> b) -> Vec n a -> Vec n b
-        mapV _ Nil         = Nil
-        mapV f (Cons x xs) = Cons (f x) (mapV f xs)
+        mapV _ Nil       = Nil
+        mapV f (x :> xs) = f x :> mapV f xs
 
         topEntity :: Vec 4 Int -> Vec 4 Int
         topEntity = mapV (+1)

docs/developing-hardware/prelude.rst

@@ -38,16 +38,6 @@ More generally, there is a ``Vec n a`` type which allows collections of
 arbitrary values to be used. These vectors are tagged with their length, to
 prevent out of bounds access at compile-time.
 
-.. warning::
-  The ``Vec n a`` type exports pattern synonyms for inserting at the left and
-  right of a vector. The types of the ``Cons`` constructor and ``(:>)`` pattern
-  are slightly different, and may behave differently in practice.
-
-  The ``Cons`` constructor has a more general type, allowing it to be used in
-  some cases where the pattern cannot be used. However, this additional power
-  comes at the cost of type inference. It is recommended that users use the
-  ``(:>)`` pattern by default, and only use ``Cons`` when necessary.
-
 Synthesis Domains
 -----------------
 
@@ -98,7 +88,7 @@ which can be used to define synchronous circuits. The first of these is
 
 .. _`Mealy machine`: https://en.wikipedia.org/wiki/Mealy_machine
 
-It is also possible to define a `Moore machine`_ using the ``moore`` function 
+It is also possible to define a `Moore machine`_ using the ``moore`` function
 in the Clash prelude. This differs to the Mealy machine by providing output
 based on the previous state (as oppoesd to the newly calculated state), and is
 specified by
@@ -169,4 +159,3 @@ changed to work with undefined values. Currently these are
   library. This allows evaluating values to normal form in code when undefined
   may be present. ``NFData`` can still be used, but will bubble up exceptions
   if undefined is encountered.
-

tests/shouldwork/Basic/T1316.hs

@@ -12,6 +12,6 @@ incr i = if i == maxBound then 0 else i + 1
 topEntity :: Index 10 -> Index 2
 topEntity j = case j < 1 of
   False ->
-    let xs = init (Cons 1 (Cons (incr (head xs)) Nil)) in last xs
+    let xs = init (1 :> (incr (head xs) :> Nil)) in last xs
   True ->
-    let ys = init (Cons 2 (Cons (incr (last ys)) Nil)) in head ys
+    let ys = init (2 :> (incr (last ys) :> Nil)) in head ys

tests/shouldwork/Basic/T1322.hs

@@ -14,18 +14,18 @@ topEntity :: Index 10 -> Index 3
 topEntity j = case j < 1 of
   False ->
     let xs :: Vec 1 (Index 3)
-        xs = init (Cons 1 (Cons (incr (head ys)) Nil))
+        xs = init (1 :> (incr (head ys) :> Nil))
         {-# NOINLINE xs #-}
         ys :: Vec 1 (Index 3)
-        ys = init (Cons 1 (Cons (incr (head xs)) Nil))
+        ys = init (1 :> (incr (head xs) :> Nil))
         {-# NOINLINE ys #-}
     in incr (incr (head xs))
   True ->
     let ys :: Vec 1 (Index 3)
-        ys = init (Cons 2 (Cons (incr (head xs)) Nil))
+        ys = init (2 :> (incr (head xs) :> Nil))
         {-# NOINLINE xs #-}
         xs :: Vec 1 (Index 3)
-        xs = init (Cons 2 (Cons (incr (head ys)) Nil))
+        xs = init (2 :> (incr (head ys) :> Nil))
         {-# NOINLINE ys #-}
     in incr (incr (head ys))
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511

tests/shouldwork/Basic/T1340.hs

@@ -72,18 +72,14 @@ catLayout (BitLayout aBitCount aInFn aOutFn) (BitLayout bBitCount bInFn bOutFn)
   in BitLayout SNat inFn outFn
 
 vecLayout
-  :: forall n n' t
-  .  ( n' ~ (n - 1)
-     , 1 <= n
-     , KnownNat n
-     , KnownNat n' )
+  :: (1 <= n, KnownNat n)
   => Vec n (BitLayout t)
   -> BitLayout (Vec n t)
 vecLayout (BitLayout{..} :> others) = let
   headLayout = BitLayout SNat (headSigFn >>> inFn) (outFn >>> singletonSigFn)
   in case others of
-       Nil -> headLayout
-       _ -> headLayout `catLayout` vecLayout @n' others
+       Nil    -> headLayout
+       _ :> _ -> headLayout `catLayout` vecLayout others
 
 layout :: BitLayout (Vec Lanes Bit)
 layout = mkPos (0 :: Index (Lanes + 1))

tests/shouldwork/Basic/T1354B.hs

@@ -76,18 +76,14 @@ catLayout (BitLayout aBitCount aInFn aOutFn) (BitLayout bBitCount bInFn bOutFn)
   in BitLayout SNat inFn outFn
 
 vecLayout
-  :: forall n n' t
-  .  ( n' ~ (n - 1)
-     , 1 <= n
-     , KnownNat n
-     , KnownNat n' )
+  :: (1 <= n, KnownNat n)
   => Vec n (BitLayout t)
   -> BitLayout (Vec n t)
 vecLayout (BitLayout{..} :> others) = let
   headLayout = BitLayout SNat (headSigFn >>> inFn) (outFn >>> singletonSigFn)
   in case others of
-       Nil -> headLayout
-       _ -> headLayout `catLayout` vecLayout @n' others
+       Nil    -> headLayout
+       _ :> _ -> headLayout `catLayout` vecLayout others
 
 layout :: BitLayout (Vec Lanes Bit)
 layout = mkPos (0 :: Index (Lanes + 1))

tests/shouldwork/GADTs/Head.hs

@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 head' :: Vec (n+1) (Signed 16) -> Signed 16
-head' (Cons x xs) = x
+head' (x :> xs) = x
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE head' #-}
 

tests/shouldwork/GADTs/HeadM.hs

@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 head' :: Vec 3 (Signed 16) -> Signed 16
-head' (Cons x xs) = x
+head' (x :> xs) = x
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE head' #-}
 

tests/shouldwork/GADTs/Tail.hs

@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tail' :: Vec (n+1) (Signed 16) -> Vec n (Signed 16)
-tail' (Cons x xs) = xs
+tail' (x :> xs) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tail' #-}
 

tests/shouldwork/GADTs/TailM.hs

@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tail' :: Vec 3 (Signed 16) -> Vec 2 (Signed 16)
-tail' (Cons x xs) = xs
+tail' (x :> xs) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tail' #-}
 

tests/shouldwork/GADTs/TailOfTail.hs

@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tailOfTail :: Vec (n+2) (Signed 16) -> Vec n (Signed 16)
-tailOfTail (Cons _ (Cons _ xs)) = xs
+tailOfTail (_ :> (_ :> xs)) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tailOfTail #-}
 

tests/shouldwork/Issues/T2542.hs

@@ -9,7 +9,7 @@ import Clash.Prelude
 
 topEntity :: (Index 2, Index 2)
 topEntity = case reverse (indicesI @2) of
-  (a `Cons` b `Cons` Nil) -> (a,b)
+  (a :> b :> Nil) -> (a,b)
 
 assertIn :: String -> String -> IO ()
 assertIn needle haystack

tests/shouldwork/Numbers/HalfAsBlackboxArg.hs

@@ -9,7 +9,7 @@ g :: KnownNat n => Vec n Half -> Half
 g v =
   case v of
     Nil -> Half 5
-    Cons a as -> a
+    a :> as -> a
 
 topEntity =
   ( g (replicate d3 (Half 7))