clash-prelude 1.2.5 → 1.4.0

raw patch · 78 files changed

+4942/−1244 lines, 78 filesdep +arrowsdep +ghc-bignumdep +tasty-thdep ~deepseqdep ~doctestdep ~ghc-primsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: arrows, ghc-bignum, tasty-th

Dependency ranges changed: deepseq, doctest, ghc-prim, ghc-typelits-extra, hedgehog, integer-gmp, lens, template-haskell, text-show

API changes (from Hackage documentation)

Files

• CHANGELOG.md +88/−0
• Setup.hs +4/−2
• clash-prelude.cabal +39/−16
• src/Clash/Annotations/BitRepresentation/Deriving.hs +6/−0
• src/Clash/Annotations/Primitive.hs +71/−43
• src/Clash/Annotations/TH.hs +25/−13
• src/Clash/Class/AutoReg/Internal.hs +24/−8
• src/Clash/Class/BitPack.hs +3/−0
• src/Clash/Class/Exp.hs +8/−6
• src/Clash/Class/HasDomain/Common.hs +3/−0
• src/Clash/Class/HasDomain/HasSingleDomain.hs +3/−0
• src/Clash/Class/HasDomain/HasSpecificDomain.hs +6/−3
• src/Clash/Class/Resize.hs +75/−2
• src/Clash/Examples.hs +10/−1
• src/Clash/Explicit/BlockRam.hs +35/−31
• src/Clash/Explicit/BlockRam/File.hs +1/−1
• src/Clash/Explicit/DDR.hs +1/−1
• src/Clash/Explicit/Prelude.hs +4/−5
• src/Clash/Explicit/Prelude/Safe.hs +1/−5
• src/Clash/Explicit/ROM/File.hs +1/−1
• src/Clash/Explicit/Reset.hs +293/−0
• src/Clash/Explicit/Signal.hs +8/−129
• src/Clash/Explicit/Signal/Delayed.hs +4/−2
• src/Clash/Explicit/SimIO.hs +38/−1
• src/Clash/Explicit/Testbench.hs +8/−15
• src/Clash/Explicit/Verification.hs +266/−0
• src/Clash/Magic.hs +36/−3
• src/Clash/Prelude.hs +7/−8
• src/Clash/Prelude/BlockRam.hs +45/−40
• src/Clash/Prelude/DataFlow.hs +2/−2
• src/Clash/Prelude/ROM/File.hs +1/−1
• src/Clash/Prelude/Safe.hs +1/−4
• src/Clash/Prelude/Testbench.hs +1/−3
• src/Clash/Promoted/Nat.hs +6/−6
• src/Clash/Promoted/Nat/Literals.hs +3/−2
• src/Clash/Promoted/Symbol.hs +3/−1
• src/Clash/Signal.hs +71/−38
• src/Clash/Signal/BiSignal.hs +50/−6
• src/Clash/Signal/Bundle.hs +18/−13
• src/Clash/Signal/Delayed.hs +2/−1
• src/Clash/Signal/Delayed/Bundle.hs +4/−4
• src/Clash/Signal/Delayed/Internal.hs +15/−4
• src/Clash/Signal/Internal.hs +206/−67
• src/Clash/Signal/Trace.hs +2/−1
• src/Clash/Sized/Fixed.hs +218/−21
• src/Clash/Sized/Internal/BitVector.hs +225/−18
• src/Clash/Sized/Internal/BitVector.hs-boot +1/−1
• src/Clash/Sized/Internal/Index.hs +40/−3
• src/Clash/Sized/Internal/Index.hs-boot +1/−1
• src/Clash/Sized/Internal/Mod.hs +163/−1
• src/Clash/Sized/Internal/Signed.hs +77/−16
• src/Clash/Sized/Internal/Unsigned.hs +173/−7
• src/Clash/Sized/RTree.hs +113/−88
• src/Clash/Sized/Vector.hs +369/−191
• src/Clash/Tutorial.hs +31/−30
• src/Clash/Verification.hs +79/−0
• src/Clash/Verification/DSL.hs +42/−0
• src/Clash/Verification/Internal.hs +151/−0
• src/Clash/Verification/PrettyPrinters.hs +244/−0
• src/Clash/XException.hs +138/−316
• src/Clash/XException.hs-boot +16/−0
• src/Clash/XException/Internal.hs +350/−0
• src/Clash/XException/TH.hs +1/−0
• src/Language/Haskell/TH/Compat.hs +4/−1
• tests/Clash/Tests/AutoReg.hs +0/−1
• tests/Clash/Tests/BitVector.hs +8/−7
• tests/Clash/Tests/Fixed.hs +365/−51
• tests/Clash/Tests/FixedExhaustive.hs +151/−0
• tests/Clash/Tests/Laws/Enum.hs +65/−0
• tests/Clash/Tests/Laws/SaturatingNum.hs +202/−0
• tests/Clash/Tests/NFDataX.hs +2/−1
• tests/Clash/Tests/Reset.hs +59/−0
• tests/Clash/Tests/Resize.hs +53/−0
• tests/Clash/Tests/TopEntityGeneration.hs +0/−1
• tests/Hedgehog/Extra.hs +17/−0
• tests/Test/QuickCheck/Extra.hs +39/−0
• tests/Test/Tasty/HUnit/Extra.hs +34/−0
• tests/unittests.hs +13/−0

@@ -1,5 +1,90 @@ # Changelog for the Clash project+## 1.4.0 *March 12th 2020*+Highlighted changes (repeated in other categories): +  * Clash no longer disables the monomorphism restriction. See [#1270](https://github.com/clash-lang/clash-compiler/issues/1270), and mentioned issues, as to why. This can cause, among other things, certain eta-reduced descriptions of sequential circuits to no longer type-check. See [#1349](https://github.com/clash-lang/clash-compiler/pull/1349) for code hints on what kind of changes to make to your own code in case it no longer type-checks due to this change.+  * Type arguments of `Clash.Sized.Vector.fold` swapped: before `forall a n . (a -> a -> a) -> Vec (n+1) a -> a`, after `forall n a . (a -> a -> a) -> Vec (n+1) a`. This makes it easier to use `fold` in a `1 <= n` context so you can "simply" do `fold @(n-1)`+  * `Fixed` now obeys the laws for `Enum` as set out in the Haskell Report, and it is now consistent with the documentation for the `Enum` class on Hackage. As `Fixed` is also `Bounded`, the rule in the Report that `succ maxBound` and `pred minBound` should result in a runtime error is interpreted as meaning that `succ` and `pred` result in a runtime error whenever the result cannot be represented, not merely for `minBound` and `maxBound` alone.+  * Primitives should now be stored in `*.primitives` files instead of `*.json`. While primitive files very much look like JSON files, they're not actually spec complaint as they use newlines in strings. This has recently been brought to our attention by Aeson fixing an oversight in their parser implementation. We've therefore decided to rename the extension to prevent confusion.++Fixed:+  * Result of `Clash.Class.Exp.(^)` has enough bits in order to deal with `x^0`.+  * Resizes to `Signed 0` (e.g., `resize @(Signed n) @(Signed 0)`) don't throw an error anymore+  * `satMul` now correctly handles arguments of type `Index 2`+  * `Clash.Explicit.Reset.resetSynchronizer` now synchronizes on synchronous domains too [#1567](https://github.com/clash-lang/clash-compiler/pull/1567).+  * `Clash.Explicit.Reset.convertReset`: now converts synchronous domains too, if necessary [#1567](https://github.com/clash-lang/clash-compiler/pull/1567).+  * `inlineWorkFree` now never inlines a topentity. It previously only respected this invariant in one of the two cases [#1587](https://github.com/clash-lang/clash-compiler/pull/1587).+  * Clash now reduces recursive type families [#1591](https://github.com/clash-lang/clash-compiler/issues/1591)+  * Primitive template warning is now retained when a `PrimitiveGuard` annotation is present [#1625](https://github.com/clash-lang/clash-compiler/issues/1625)+  * `signum` and `RealFrac` for `Fixed` now give the correct results.+  * Fixed a memory leak in register when used on asynchronous domains. Although the memory leak has always been there, it was only triggered on asserted resets. These periods are typically short, hence typically unnoticable.+  * `createDomain` will not override user definitions of types, helping users who strive for complete documentation coverage [#1674] https://github.com/clash-lang/clash-compiler/issues/1674+  * `fromSNat` is now properly constrained [#1692](https://github.com/clash-lang/clash-compiler/issues/1692)+  * As part of an internal overhaul on netlist identifier generation [#1265](https://github.com/clash-lang/clash-compiler/pull/1265):+    * Clash no longer produces "name conflicts" between basic and extended identifiers. I.e., `\x\` and `x` are now considered the same variable in VHDL (likewise for other HDLs). Although the VHDL spec considers them distinct variables, some HDL tools - like Quartus - don't.+    * Capitalization of Haskell names are now preserved in VHDL. Note that VHDL is a case insensitive languages, so there are measures in place to prevent Clash from generating both `Foo` and `fOO`. This used to be handled by promoting every capitalized identifier to an extended one and wasn't handled for basic ones.+    * Names generated for testbenches can no longer cause collisions with previously generated entities.+    * Names generated for components can no longer cause collisions with user specified top entity names.+    * For (System)Verilog, variables can no longer cause collisions with (to be) generated entity names.+    * HO blackboxes can no longer cause collisions with identifiers declared in their surrounding architecture block.+++Changed:+  * Treat enable lines specially in generated HDL [#1171](https://github.com/clash-lang/clash-compiler/issues/1171)+  * `Signed`, `Unsigned`, `SFixed`, and `UFixed` now correctly implement the `Enum` law specifying that the predecessor of `minBound` and the successor of `maxBound` should result in an error [#1495](https://github.com/clash-lang/clash-compiler/pull/1495).+  * `Fixed` now obeys the laws for `Enum` as set out in the Haskell Report, and it is now consistent with the documentation for the `Enum` class on Hackage. As `Fixed` is also `Bounded`, the rule in the Report that `succ maxBound` and `pred minBound` should result in a runtime error is interpreted as meaning that `succ` and `pred` result in a runtime error whenever the result cannot be represented, not merely for `minBound` and `maxBound` alone.+  * Type arguments of `Clash.Sized.Vector.fold` swapped: before `forall a n . (a -> a -> a) -> Vec (n+1) a -> a`, after `forall n a . (a -> a -> a) -> Vec (n+1) a`. This makes it easier to use `fold` in a `1 <= n` context so you can "simply" do `fold @(n-1)`+  * Moved `Clash.Core.Evaluator` into `Clash.GHC` and provided generic interface in `Clash.Core.Evalautor.Types`. This removes all GHC specific code from the evaluator in clash-lib.+  * Clash no longer disables the monomorphism restriction. See [#1270](https://github.com/clash-lang/clash-compiler/issues/1270), and mentioned issues, as to why. This can cause, among other things, certain eta-reduced descriptions of sequential circuits to no longer type-check. See [#1349](https://github.com/clash-lang/clash-compiler/pull/1349) for code hints on what kind of changes to make to your own code in case it no longer type-checks due to this change.+  * Clash now generates SDC files for each topentity with clock inputs+  * `deepErrorX` is now equal to `undefined#`, which means that instead of the whole BitVector being undefined, its individual bits are. This makes sure bit operations are possible on it. [#1532](https://github.com/clash-lang/clash-compiler/pull/1532)+  * From GHC 9.0.1 onwards the following types: `BiSignalOut`, `Index`, `Signed`, `Unsigned`, `File`, `Ref`, and `SimIO` are all encoded as `data` instead of `newtype` to work around an [issue](https://github.com/clash-lang/clash-compiler/pull/1624#discussion_r558333461) where the Clash compiler can no longer recognize primitives over these types. This means you can no longer use `Data.Coerce.coerce` to coerce between these types and their underlying representation.+  * Signals on different domains used to be coercable because the domain had a type role "phantom". This has been changed to "nominal" to prevent accidental, unsafe coercions. [#1640](https://github.com/clash-lang/clash-compiler/pull/1640)+  * Size parameters on types in Clash.Sized.Internal.* are now nominal to prevent unsafe coercions. [#1640](https://github.com/clash-lang/clash-compiler/pull/1640)+  * `hzToPeriod` now takes a `Ratio Natural` rather than a `Double`. It rounds slightly differently, leading to more intuitive results and satisfying the requested change in [#1253](https://github.com/clash-lang/clash-compiler/issues/1253). Clash expresses clock rate as the clock period in picoseconds. If picosecond precision is required for your design, please use the exact method of specifying a clock period rather than a clock frequency.+  * `periodToHz` now results in a `Ratio Natural`+  * `createDomain` doesn't override existing definitions anymore, fixing [#1674](https://github.com/clash-lang/clash-compiler/issues/1674)+  * Manifest files are now stored as `clash-manifest.json`+  * Manifest files now store hashes of the files Clash generated. This allows Clash to detect user changes on a next run, preventing accidental data loss.+  * Primitives should now be stored in `*.primitives` files. While primitive files very much look like JSON files, they're not actually spec complaint as they use newlines in strings. This has recently been brought to our attention by Aeson fixing an oversight in their parser implementation. We've therefore decided to rename the extension to prevent confusion.+  * Each binder marked with a `Synthesize` or `TestBench` pragma will be put in its own directory under their fully qualified Haskell name. For example, two binders `foo` and `bar` in module `A` will be synthesized in `A.foo` and `A.bar`.+  * Clash will no longer generate vhdl, verilog, or systemverilog subdirectories when using `-fclash-hdldir`.+  * `Data.Kind.Type` is now exported from `Clash.Prelude` [#1700](https://github.com/clash-lang/clash-compiler/issues/1700)+++Added:+  * Support for GHC 9.0.1+  * `Clash.Signal.sameDomain`: Allows user obtain evidence whether two domains are equal.+  * `xToErrorCtx`: makes it easier to track the origin of `XException` where `pack` would hide them [#1461](https://github.com/clash-lang/clash-compiler/pull/1461)+  * Additional field with synthesis attributes added to `InstDecl` in `Clash.Netlist.Types` [#1482](https://github.com/clash-lang/clash-compiler/pull/1482)+  * `Data.Ix.Ix` instances for `Signed`, `Unsigned`, and `Index` [#1481](https://github.com/clash-lang/clash-compiler/pull/1481) [#1631](https://github.com/clash-lang/clash-compiler/pull/1631)+  * Added `nameHint` to allow explicitly naming terms, e.g. `Signal`s.+  * Checked versions of `resize`, `truncateB`, and `fromIntegral`. Depending on the type `resize`, `truncateB`, and `fromIntegral` either yield an `XException` or silently perform wrap-around if its argument does not fit in the resulting type's bounds. The added functions check the bound condition and fail with an error call if the condition is violated. They do not affect HDL generation. [#1491](https://github.com/clash-lang/clash-compiler/pull/1491)+  * `HasBiSignalDefault`: constraint to Clash.Signal.BiSignal, `pullUpMode` gives access to the pull-up mode. [#1498](https://github.com/clash-lang/clash-compiler/pull/1498)+  * Match patterns to bitPattern [#1545](https://github.com/clash-lang/clash-compiler/pull/1545)+  * Non TH `fromList` and `unsafeFromList` for Vec. These functions allow Vectors to be created from a list without needing to use template haskell, which is not always desirable. The unsafe version of the function does not compare the length of the list to the desired length of the vector, either truncating or padding with undefined if the lengths differ.+  * `Clash.Explicit.Reset.resetGlitchFilter`: filters glitchy reset signals. Useful when your reset signal is connected to sensitive actuators.+  * Clash can now generate EDAM for using Edalize. This generates edam.py files in all top entities with the configuration for building that entity. Users still need to edit this file to specify the EDA tool to use, and if necessary the device to target (for Quartus, Vivado etc.). [#1386](https://github.com/clash-lang/clash-compiler/issues/1386)+  * `-fclash-aggressive-x-optimization-blackboxes`: when enabled primitives can detect undefined values and change their behavior accordingly. For example, if `register` is used in combination with an undefined reset value, it will leave out the reset logic entirely. Related issue: [#1506](https://github.com/clash-lang/clash-compiler/issues/1506).+  * Automaton-based interface to simulation, to allow interleaving of cyle-by-cycle simulation and external effects [#1261](https://github.com/clash-lang/clash-compiler/pull/1261)+++New internal features:+  * `constructProduct` and `deconstructProduct` in `Clash.Primitives.DSL`. Like `tuple` and `untuple`, but on arbitrary product types.+  * Support for multi result primitives. Primitives can now assign their results to multiple variables. This can help to work around synthesis tools limits in some cases. See [#1560](https://github.com/clash-lang/clash-compiler/pull/1560).+  * Added a rule for missing `Int` comparisons in `GHC.Classes` in the compile time evaluator. [#1648](https://github.com/clash-lang/clash-compiler/issues/1648)+  * Clash now creates a mapping from domain names to configurations in `LoadModules`. [#1405](https://github.com/clash-lang/clash-compiler/pull/1405)+  * The convenience functions in `Clash.Primitives.DSL` now take a list of HDLs, instead of just one.+  * `Clash.Netlist.Id` overhauls the way identifiers are generated in the Netlist part of Clash.+  * Added `defaultWithAction` to Clash-as-a-library API to work around/fix issues such as [#1686](https://github.com/clash-lang/clash-compiler/issues/1686)+  * Manifest files now list files and components in an reverse topological order. This means it can be used when calling EDA tooling without causing compilation issues.++Deprecated:+  * `Clash.Prelude.DataFlow`: see [#1490](https://github.com/clash-lang/clash-compiler/pull/1490). In time, its functionality will be replaced by [clash-protocols](https://github.com/clash-lang/clash-protocols).++Removed:+  * The deprecated function `freqCalc` has been removed.+ ## 1.2.5 *November 9th 2020* Fixed:   * The normalizeType function now fully normalizes types which require calls to@@ -13,6 +98,9 @@   * Clash now uses correct function names in manifest and sdc files [#1533](https://github.com/clash-lang/clash-compiler/issues/1533)   * Clash no longer produces erroneous HDL in very specific cases [#1536](https://github.com/clash-lang/clash-compiler/issues/1536)   * Usage of `fold` inside other HO primitives (e.g., `map`) no longer fails [#1524](https://github.com/clash-lang/clash-compiler/issues/1524)++Changed:+  * Due to difficulties using `resetSynchronizer` we've decided to make this function always insert a synchronizer. See: [#1528](https://github.com/clash-lang/clash-compiler/issues/1528).  ## 1.2.4 *July 28th 2020* * Changed:

@@ -13,9 +13,11 @@ -- If the macro is defined, we have new cabal-install, -- but for some reason we don't have cabal-doctest in package-db ----- Probably we are running cabal sdist, when otherwise using new-build+-- Probably we are running cabal sdist, when otherwise using v2-build -- workflow-import Warning ()+#warning You are configuring this package without cabal-doctest installed. \+         The doctests test-suite will not work as a result. \+         To fix this, install cabal-doctest before configuring. #endif import Distribution.Simple main :: IO ()

@@ -1,7 +1,7 @@ Cabal-version:        2.2 Name:                 clash-prelude-Version:              1.2.5-Synopsis:             CAES Language for Synchronous Hardware - Prelude library+Version:              1.4.0+Synopsis:             Clash: a functional hardware description language - Prelude library Description:   Clash is a functional hardware description language that borrows both its   syntax and semantics from the functional programming language Haskell. The@@ -69,14 +69,12 @@   description:     Generate instances for classes such as `NFDataX` and `BitPack` for tuples     up to and including 62 elements - the GHC imposed maximum. This greatly-    increases compile times for `clash-prelude` and therefore mostly impacts the-    Clash developers themselves. Hence its default is set to disabled on-    development versions and enabled on releases.+    increases compile times for `clash-prelude`.   -- I have no idea to pass cabal flags to nix, so the comment below,   -- "-- large-tuples", is there to enable a call to 'sed' that replaces   -- True with False. This is done to prevent OOM on CircleCI.   -- large-tuples-  default: True+  default: False   manual: True  flag super-strict@@ -212,11 +210,13 @@                       Clash.Explicit.ROM.File                       Clash.Explicit.Prelude                       Clash.Explicit.Prelude.Safe+                      Clash.Explicit.Reset                       Clash.Explicit.SimIO                       Clash.Explicit.Signal                       Clash.Explicit.Signal.Delayed                       Clash.Explicit.Synchronizer                       Clash.Explicit.Testbench+                      Clash.Explicit.Verification                        Clash.HaskellPrelude @@ -273,7 +273,13 @@                       Clash.Sized.Internal.Signed                       Clash.Sized.Internal.Unsigned +                      Clash.Verification+                      Clash.Verification.DSL+                      Clash.Verification.PrettyPrinters+                      Clash.Verification.Internal+                       Clash.XException+                      Clash.XException.Internal                       Clash.XException.TH                        Clash.Xilinx.ClockGen@@ -306,6 +312,7 @@                       UndecidableInstances    Build-depends:      array                     >= 0.5.1.0 && < 0.6,+                      arrows                    >= 0.4     && < 0.5,                       base                      >= 4.11    && < 5,                       bifunctors                >= 5.4.0   && < 6.0,                       binary                    >= 0.8.5   && < 0.11,@@ -314,32 +321,36 @@                       containers                >= 0.4.0   && < 0.7,                       data-binary-ieee754       >= 0.4.4   && < 0.6,                       data-default-class        >= 0.1.2   && < 0.2,-                      integer-gmp               >= 0.5.1.0 && < 1.1,                       deepseq                   >= 1.4.1.0 && < 1.5,-                      ghc-prim                  >= 0.5.1.0 && < 0.7,-                      ghc-typelits-extra        >= 0.3.3   && < 0.5,+                      ghc-prim                  >= 0.5.1.0 && < 0.8,+                      ghc-typelits-extra        >= 0.4     && < 0.5,                       ghc-typelits-knownnat     >= 0.7.2   && < 0.8,                       ghc-typelits-natnormalise >= 0.7.2   && < 0.8,-                      hashable                  >= 1.2.1.0 && < 1.4,+                      hashable                  >= 1.2.1.0  && < 1.4,                       half                      >= 0.2.2.3 && < 1.0,                       interpolate               >= 0.2     && < 0.3,-                      lens                      >= 4.10    && < 4.20,+                      lens                      >= 4.10    && < 5.1.0,                       recursion-schemes         >= 5.1     && < 5.3,                       QuickCheck                >= 2.7     && < 2.15,                       reflection                >= 2       && < 2.2,                       singletons                >= 1.0     && < 3.0,-                      template-haskell          >= 2.12.0.0 && < 2.17,+                      template-haskell          >= 2.12.0.0 && < 2.18,                       th-abstraction            >= 0.2.10 && < 0.5.0,                       th-lift                   >= 0.7.0    && < 0.9,                       th-orphans                >= 0.13.1   && < 1.0,                       text                      >= 0.11.3.1 && < 1.3,-                      text-show                 >= 3.8     && < 3.10,+                      text-show                 >= 3.7     && < 3.10,                       time                      >= 1.8     && < 1.12,                       transformers              >= 0.5.2.0 && < 0.6,                       type-errors               >= 0.2.0.0 && < 0.3,                       uniplate                  >= 1.6.12  && < 1.7,                       vector                    >= 0.11    && < 1.0 +  if impl(ghc >= 9.0.0)+    Build-Depends:    ghc-bignum                >= 1.0      && < 1.1+  else+    Build-Depends:    integer-gmp               >= 1.0.1.0  && < 2.0+ test-suite doctests   type:             exitcode-stdio-1.0   default-language: Haskell2010@@ -354,7 +365,7 @@   else     build-depends:       base,-      doctest >= 0.9.1 && < 0.18,+      doctest >= 0.9.1 && < 0.19,       clash-prelude   if impl(ghc >= 8.6)     build-depends:@@ -364,7 +375,7 @@   import:           common-options   type:             exitcode-stdio-1.0   main-is:          unittests.hs-  ghc-options:      -Wall -Wcompat+  ghc-options:      -Wall -Wcompat -threaded -with-rtsopts=-N   hs-source-dirs:   tests    if !flag(unittests)@@ -378,12 +389,14 @@       ghc-typelits-extra,        base,-      hedgehog,+      deepseq,+      hedgehog      >= 1.0.3    && < 1.1,       hint          >= 0.7      && < 0.10,       quickcheck-classes-base >= 0.6 && < 1.0,       tasty         >= 1.2      && < 1.5,       tasty-hedgehog,       tasty-hunit,+      tasty-th,       tasty-quickcheck,       template-haskell @@ -394,13 +407,23 @@                  Clash.Tests.DerivingDataRepr                  Clash.Tests.DerivingDataReprTypes                  Clash.Tests.Fixed+                 Clash.Tests.FixedExhaustive                  Clash.Tests.NFDataX+                 Clash.Tests.Reset+                 Clash.Tests.Resize                  Clash.Tests.Signal                  Clash.Tests.Signed                  Clash.Tests.SizedNum                  Clash.Tests.TopEntityGeneration                  Clash.Tests.Unsigned +                 Clash.Tests.Laws.Enum+                 Clash.Tests.Laws.SaturatingNum++                 Hedgehog.Extra++                 Test.Tasty.HUnit.Extra+                 Test.QuickCheck.Extra  benchmark benchmark-clash-prelude   type:             exitcode-stdio-1.0

@@ -159,9 +159,15 @@ bitsNeeded :: Integer -> Int bitsNeeded = integerLog2Ceil +#if MIN_VERSION_template_haskell(2,17,0)+tyVarBndrName :: TyVarBndr f -> Name+tyVarBndrName (PlainTV n _f) = n+tyVarBndrName (KindedTV n _f _k) = n+#else tyVarBndrName :: TyVarBndr -> Name tyVarBndrName (PlainTV n) = n tyVarBndrName (KindedTV n _k) = n+#endif  -- | Replace Vars types given in mapping resolve :: NameMap -> Type -> Type

@@ -3,9 +3,10 @@ License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> -Instruct the clash compiler to look for primitive HDL templates in the-indicated directory. For distribution of new packages with primitive HDL-templates.+Instruct the Clash compiler to look for primitive HDL templates provided inline+or in a specified directory. For distribution of new packages with primitive+HDL templates. Primitive guards can be added to warn on instantiating+primitives. -}  {-# LANGUAGE DeriveAnyClass #-}@@ -22,9 +23,11 @@   , warnNonSynthesizable   , warnAlways   , Primitive(..)-  , PrimitiveGuard(..)   , HDL(..)+  , PrimitiveGuard(..)+  , PrimitiveWarning(..)   , extractPrim+  , extractWarnings   ) where  import           Control.DeepSeq                          (NFData)@@ -134,18 +137,49 @@     nm -} +-- | Marks value as not translatable. Clash will error if it finds a blackbox+-- definition for it, or when it is forced to translate it. You can annotate a+-- variable or function @f@ like:+--+-- @+-- {\-\# ANN f dontTranslate \#-\}+-- @ dontTranslate :: PrimitiveGuard () dontTranslate = DontTranslate +-- | Marks a value as having a blackbox. Clash will error if it hasn't found+-- a blackbox. You can annotate a variable or function @f@ like:+--+-- @+-- {\-\# ANN f hasBlackBox \#-\}+-- @ hasBlackBox :: PrimitiveGuard ()-hasBlackBox = HasBlackBox ()+hasBlackBox = HasBlackBox [] () +-- | Marks value as non-synthesizable. This will trigger a warning if+-- instantiated in a non-testbench context. You can annotate a variable or+-- function @f@ like:+--+-- @+-- {\-\# ANN f (warnNonSynthesizable "Tread carefully, user!") \#-\}+-- @+--+-- Implies `hasBlackBox`. warnNonSynthesizable :: String -> PrimitiveGuard ()-warnNonSynthesizable s = WarnNonSynthesizable s ()+warnNonSynthesizable s = HasBlackBox [WarnNonSynthesizable s] () +-- | Always emit warning upon primitive instantiation. You can annotate a+-- variable or function @f@ like:+--+-- @+-- {\-\# ANN f (warnAlways "Tread carefully, user!") \#-\}+-- @+--+-- Implies `hasBlackBox`. warnAlways :: String -> PrimitiveGuard ()-warnAlways s = WarnAlways s ()+warnAlways s = HasBlackBox [WarnAlways s] () +-- | A compilation target HDL. data HDL   = SystemVerilog   | Verilog@@ -166,7 +200,7 @@ -- You create a package which has a @myfancyip.cabal@ file with the following stanza: -- -- @--- data-files: path\/to\/MyFancyIP.json+-- data-files: path\/to\/MyFancyIP.primitives -- cpp-options: -DCABAL -- @ --@@ -239,44 +273,30 @@   -- ^ Description of a primitive for a given 'HDL's as an inline 'String'   deriving (Show, Read, Data, Generic, NFData, Hashable) --- | Guard primitive functions. This will help Clash generate better error--- messages. You can annotate a function like:------ @--- {\-\# ANN f dontTranslate \#-\}--- @------ or------ @--- {\-\# ANN f hasBlackBox \#-\}--- @------ or------ @--- {\-\# ANN f (warnNonSynthesizable "Tread carefully, user!") \#-\}--- @------ or+-- | Primitive guard to mark a value as either not translatable or as having a+-- blackbox with an optional extra warning. Helps Clash generate better error+-- messages. ----- @--- {\-\# ANN f (warnAlways "Tread carefully, user!") \#-\}--- @+-- For use, see 'dontTranslate', 'hasBlackBox', 'warnNonSynthesizable' and+-- 'warnAlways'. data PrimitiveGuard a   = DontTranslate   -- ^ Marks value as not translatable. Clash will error if it finds a blackbox   -- definition for it, or when it is forced to translate it.-  | HasBlackBox a-  -- ^ Marks a value as having a blackbox. Clash will err if it hasn't found-  -- a blackbox-  | WarnNonSynthesizable String a-  -- ^ Marks value as non-synthesizable. This will trigger a warning if-  -- instantiated in a non-testbench context. Implies @HasBlackBox@.-  | WarnAlways String a-  -- ^ Always emit warning upon instantiation. Implies @HasBlackBox@.+  | HasBlackBox [PrimitiveWarning] a+  -- ^ Marks a value as having a blackbox. Clash will error if it hasn't found+  -- a blackbox.     deriving (Show, Read, Data, Generic, NFData, Hashable, Functor, Foldable, Traversable, Binary) +-- | Warning that will be emitted on instantiating a guarded value.+data PrimitiveWarning+  = WarnNonSynthesizable String+  -- ^ Marks value as non-synthesizable. This will trigger a warning if+  -- instantiated in a non-testbench context.+  | WarnAlways String+  -- ^ Always emit warning upon primitive instantiation.+    deriving (Show, Read, Data, Generic, NFData, Hashable, Binary)+ -- | Extract primitive definition from a PrimitiveGuard. Will yield Nothing -- for guards of value 'DontTranslate'. extractPrim@@ -284,7 +304,15 @@   -> Maybe a extractPrim =   \case-    HasBlackBox a            -> Just a-    WarnNonSynthesizable _ a -> Just a-    WarnAlways _ a           -> Just a-    DontTranslate            -> Nothing+    HasBlackBox _ p -> Just p+    DontTranslate   -> Nothing++-- | Extract primitive warnings from a PrimitiveGuard. Will yield an empty list+-- for guards of value 'DontTranslate'.+extractWarnings+  :: PrimitiveGuard a+  -> [PrimitiveWarning]+extractWarnings =+  \case+    HasBlackBox w _ -> w+    DontTranslate   -> []

@@ -1,16 +1,17 @@ {-|  This module can automatically generate TopEntity definitions from 'Clash.NamedTypes'-annotations. Annotations involving data/type families must be inspected for correctness.+annotations. Annotations involving data\/type families must be inspected for correctness. Not all cases can be handled with automatic generation due to the difficulty of type manipulation-in template Haskell. In particular annotations _inside_ the following is unlikely to work:+in template Haskell. In particular annotations __inside__ the following is unlikely to work: -- Data/type family referencing other data/type families.+- Data\/type family referencing other data\/type families. - Annotations inside recursive data types - Clock constraints other than a single HiddenClockResetEnable. (You can still-  use arbitrary explicit clock/reset/enables!)+  use arbitrary explicit clock\/reset\/enables!) -See "Clash.Tests.TopEntityGeneration" for more examples.+See <https://github.com/clash-lang/clash-compiler/blob/master/clash-prelude/tests/Clash/Tests/TopEntityGeneration.hs Clash.Tests.TopEntityGeneration>+for more examples.  @ import Clash.Annotations.TH@@ -142,7 +143,7 @@ unarrow (ArrowTy x y) = x : unarrow y unarrow _ = [] --- | Collapse a list of 'PortNames' into a single 'PortName'+-- | Collapse a list of 'PortName's into a single 'PortName' collapseNames :: [PortName] -> [PortName] collapseNames [] = [] collapseNames [x] = [x]@@ -179,11 +180,11 @@  -- | Run a 'Name' through the template haskell machinery, getting a -- 'DatatypeInfo' if the 'Name' specified a datatype. The result is processed by--- a given function or a default 'a' is returned in the style of 'maybe'.+-- a given function or a default @a@ is returned in the style of 'maybe'. tryReifyDatatype :: a -> (DatatypeInfo -> a) -> Name -> Tracked Q a tryReifyDatatype a f name = lift (recover (pure a) $ f <$> reifyDatatype name) --- * Type tree folding / unfolding+-- * Type tree folding \/ unfolding  -- | Flag constructors with partially named fields as failing. portsFromTypes@@ -488,19 +489,30 @@           Just name' -> name'          -- user specified name           Nothing    -> nameBase name  -- auto-generated from Haskell name -    [|| Synthesize-        { t_name   = outName-        , t_inputs = ins-        , t_output = out-        } ||]+#if MIN_VERSION_template_haskell(2,17,0)+    (examineCode+#else+    (+#endif+                  [|| Synthesize+                     { t_name   = outName+                     , t_inputs = ins+                     , t_output = out+                     } ||])  -- | Return a typed 'Maybe TopEntity' expression given a 'Name'. -- This will return an 'TExp' of 'Nothing' if 'TopEntity' generation failed. maybeBuildTopEntity :: Maybe String -> Name -> Q (TExp (Maybe TopEntity)) maybeBuildTopEntity topName name = do+#if MIN_VERSION_template_haskell(2,17,0)+  recover (examineCode [|| Nothing ||]) $ do+    let expr = liftCode (getNameBinding name >>= buildTopEntity topName)+    examineCode [|| Just ($$expr) ||]+#else   recover ([|| Nothing ||]) $ do     let expr = getNameBinding name >>= buildTopEntity topName     [|| Just ($$expr) ||]+#endif  -- | Turn the 'Name' of a value to a @('Name', 'Type')@ getNameBinding :: Name -> Q (Name, Type)

@@ -48,8 +48,20 @@ import           Language.Haskell.TH.Lib import           Language.Haskell.TH.Ppr -import           Control.Lens.Internal.TH     (bndrName, conAppsT)+import           Control.Lens.Internal.TH     (conAppsT) +#if MIN_VERSION_base(4,15,0)+-- | Return 'Name' contained in a 'TyVarBndr'.+bndrName :: TyVarBndr a -> Name+bndrName (PlainTV  n _) = n+bndrName (KindedTV n _ _) = n+#else+-- | Return 'Name' contained in a 'TyVarBndr'.+bndrName :: TyVarBndr -> Name+bndrName (PlainTV  n) = n+bndrName (KindedTV n _) = n+#endif+ -- $setup -- >>> import Data.Maybe -- >>> import Clash.Class.BitPack (pack)@@ -70,7 +82,7 @@ --   "potentially uninteresting" part will only be enabled if the constructor --   bits indicate they're interesting. -----   The most important example of this is "Maybe". Consider "Maybe Byte)";+--   The most important example of this is 'Maybe'. Consider @Maybe (Signed 16)@; --   when viewed as bits, a 'Nothing' would look like: -- --     >>> pack @(Maybe (Signed 16)) Nothing@@ -82,14 +94,14 @@ --     1_0000_0000_0000_0011 -- --   In the first case, Nothing, we don't particularly care about updating the---   register holding the "Signed 16" field, as they'll be unknown anyway. We+--   register holding the @Signed 16@ field, as they'll be unknown anyway. We --   can therefore deassert its enable line. -- -- Making Clash lay it out like this increases the chances of synthesis tools -- clock gating the registers, saving energy. -- -- This version of 'autoReg' will split the given data type up recursively. For--- example, given "a :: Maybe (Maybe Int, Maybe Int)", a total of five registers+-- example, given @a :: Maybe (Maybe Int, Maybe Int)@, a total of five registers -- will be rendered. Both the "interesting" and "uninteresting" enable lines of -- the inner Maybe types will be controlled by the outer one, in addition to -- the inner parts controlling their "uninteresting" parts as described in (2).@@ -102,8 +114,11 @@ -- -- If you have a product type you can use 'deriveAutoReg' to derive an instance. ----- "Clash.Prelude" exports an implicit version of this: 'Clash.Prelude.autoReg' class NFDataX a => AutoReg a where+  -- | For documentation see class 'AutoReg'.+  --+  -- This is version with explicit clock/reset/enable,+  -- "Clash.Prelude" exports an implicit version of this: 'Clash.Prelude.autoReg'   autoReg     :: (HasCallStack, KnownDomain dom)     => Clock dom -> Reset dom -> Enable dom@@ -136,7 +151,7 @@ instance AutoReg Word64  instance AutoReg Bit-instance AutoReg (BitVector n)+instance KnownNat n => AutoReg (BitVector n) instance AutoReg (Signed n) instance AutoReg (Unsigned n) instance AutoReg (Index n)@@ -380,9 +395,10 @@   needRecurse :: Type -> Bool   needRecurse (unfoldType -> (cls,tys)) =     case tys of-      [VarT _] -> False-      [ConT _] -> False  -- we can just drop constraints like: "AutoReg Bool => ..."       [AppT _ _] -> True+      [VarT _] -> False  -- gets copied by "filter isOk" above+      [ConT _] -> False  -- we can just drop constraints like: "AutoReg Bool => ..."+      [LitT _] -> False  -- or "KnownNat 4 =>"       [_] -> error ( "Error while deriveAutoReg: don't know how to handle: "                   ++ pprint cls ++ " (" ++ pprint tys ++ ")" )       _ -> False  -- see [NOTE: MultiParamTypeClasses]

@@ -28,6 +28,9 @@   , boolToBit   , bitToBool   , packXWith++  -- * Internals+  , GBitPack(..)   ) where 

@@ -6,6 +6,7 @@  {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} @@ -22,6 +23,7 @@  import           GHC.TypeLits   (KnownNat, Nat, type (^), type (*))+import           GHC.TypeLits.Extra            (Max)  -- | Type class implementing exponentiation with explicitly resizing results. class Exp a where@@ -37,19 +39,19 @@     -- ^ Resized result, guaranteed to not have overflown  instance KnownNat m => Exp (Index m) where-  type ExpResult (Index m) n = Index (m ^ n)+  type ExpResult (Index m) n = Index (Max 2 (m ^ n))    (^) = expIndex#   {-# INLINE (^) #-}  instance KnownNat m => Exp (Signed m) where-  type ExpResult (Signed m) n = Signed (m * n)+  type ExpResult (Signed m) n = Signed (Max 2 (m * n))    (^) = expSigned#   {-# INLINE (^) #-}  instance KnownNat m => Exp (Unsigned m) where-  type ExpResult (Unsigned m) n = Unsigned (m * n)+  type ExpResult (Unsigned m) n = Unsigned (Max 1 (m * n))    (^) = expUnsigned#   {-# INLINE (^) #-}@@ -58,7 +60,7 @@   :: KnownNat m   => Index m   -> SNat n-  -> Index (m ^ n)+  -> Index (Max 2 (m ^ n)) expIndex# b e@SNat =   fromInteger (toInteger b P.^ snatToInteger e) {-# NOINLINE expIndex# #-}@@ -68,7 +70,7 @@   :: KnownNat m   => Signed m   -> SNat n-  -> Signed (m * n)+  -> Signed (Max 2 (m * n)) expSigned# b e@SNat =   fromInteger (toInteger b P.^ snatToInteger e) {-# NOINLINE expSigned# #-}@@ -78,7 +80,7 @@   :: KnownNat m   => Unsigned m   -> SNat n-  -> Unsigned (m * n)+  -> Unsigned (Max 1 (m * n)) expUnsigned# b e@SNat =   fromInteger (toInteger b P.^ snatToInteger e) {-# NOINLINE expUnsigned# #-}

@@ -12,6 +12,9 @@   , (:<<>>:)   , (:$$$:)   , (:++:)++  -- * Internal+  , ToEM   ) where  import           GHC.TypeLits               (Symbol)

@@ -2,6 +2,8 @@ Copyright  :  (C) 2019, Myrtle Software Ltd License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>++Internals for "Clash.Class.HasDomain" -}  {-# LANGUAGE ConstraintKinds #-}@@ -17,6 +19,7 @@ #endif  {-# OPTIONS_GHC -Wno-missing-methods #-}+{-# OPTIONS_HADDOCK not-home #-}  module Clash.Class.HasDomain.HasSingleDomain where 

@@ -2,6 +2,8 @@ Copyright  :  (C) 2019, Myrtle Software Ltd License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>++Internals for "Clash.Class.HasDomain" -}  {-# LANGUAGE ConstraintKinds #-}@@ -18,6 +20,7 @@ #endif  {-# OPTIONS_GHC -Wno-missing-methods #-}+{-# OPTIONS_HADDOCK not-home #-}  module Clash.Class.HasDomain.HasSpecificDomain where @@ -85,7 +88,7 @@   DomEqWorker n n = 'Found   DomEqWorker n m = 'NotFound --- | Check domain for equality. Return 'Found if so, return 'NotFound if not.+-- | Check domain for equality. Return @'Found@ if so, return @'NotFound@ if not. -- The reason d'etre for this type family is that _open_ type families don't -- allow overlapping types. We therefore defer equality checking to a closed -- type family.@@ -111,7 +114,7 @@   ErrOnNotFound dom  'NotFound t = DelayError (NotFoundError dom t)   ErrOnNotFound dom  'Found    t = dom --- | Wrapper that checks for stuckness and returns "NotFound" if so+-- | Wrapper that checks for stuckness and returns @'NotFound@ if so type family HasDomainWrapper (dom :: Domain) (n :: Type) :: HasDomainWrapperResult where   HasDomainWrapper dom n =     IfStuck@@ -132,7 +135,7 @@ -- | Type class that specifies that a certain domain, /dom/, needs to be present -- in some other type, /r/. This is used to disambiguate what hidden clock, -- reset, and enable lines should be exposed in functions such as--- 'withSpecificReset'.+-- 'Clash.Signal.withSpecificReset'. -- -- Functions in need of this class should use 'WithSpecificDomain' though, to -- force Clash to display an error instead of letting it silently pass.

@@ -1,7 +1,8 @@ {-| Copyright  :  (C) 2013-2016, University of Twente+                  2020,      Myrtle Software Ltd License    :  BSD2 (see the file LICENSE)-Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>+Maintainer :  QBayLogic B.V. <devops@qbaylogic.com> -}  {-# LANGUAGE Safe #-}@@ -9,9 +10,18 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} {-# OPTIONS_HADDOCK show-extensions #-} -module Clash.Class.Resize where+module Clash.Class.Resize+ ( Resize(..) + -- * Resize helpers+ , checkedResize+ , checkedFromIntegral+ , checkedTruncateB+ ) where+ import Data.Kind (Type)+import Data.Proxy (Proxy(Proxy))+import GHC.Stack (HasCallStack) import GHC.TypeLits (Nat, KnownNat, type (+))  -- | Coerce a value to be represented by a different number of bits@@ -37,3 +47,66 @@   signExtend = resize   -- | Remove bits from the MSB   truncateB :: KnownNat a => f (a + b) -> f a++-- | Helper function of 'checkedFromIntegral', 'checkedResize' and 'checkedTruncateB'+checkIntegral ::+  forall a b.+  HasCallStack =>+  (Integral a, Integral b, Bounded b) =>+  Proxy b ->+  a -> ()+checkIntegral Proxy v =+  if toInteger v > toInteger (maxBound @b)+  || toInteger v < toInteger (minBound @b) then+    error $ "Given integral " <> show (toInteger v) <> " is out of bounds for" <>+            " target type. Bounds of target type are: [" <>+            show (toInteger (minBound @b)) <> ".." <>+            show (toInteger (maxBound @b)) <> "]."+  else+    ()++-- | Like 'fromIntegral', but errors if /a/ is out of bounds for /b/. Useful when+-- you "know" /a/ can't be out of bounds, but would like to have your assumptions+-- checked.+--+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted+-- into the generated HDL+checkedFromIntegral ::+  forall a b.+  HasCallStack =>+  (Integral a, Integral b, Bounded b) =>+  a -> b+checkedFromIntegral v =+  checkIntegral (Proxy @b) v `seq` fromIntegral v++-- | Like 'resize', but errors if /f a/ is out of bounds for /f b/. Useful when+-- you "know" /f a/ can't be out of bounds, but would like to have your+-- assumptions checked.+--+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted+-- into the generated HDL+checkedResize ::+  forall a b f.+  ( HasCallStack+  , Resize f+  , KnownNat a, Integral (f a)+  , KnownNat b, Integral (f b), Bounded (f b) ) =>+  f a -> f b+checkedResize v =+  checkIntegral (Proxy @(f b)) v `seq` resize v++-- | Like 'truncateB', but errors if /f (a + b)/ is out of bounds for /f a/. Useful+-- when you "know" /f (a + b)/ can't be out of bounds, but would like to have your+-- assumptions checked.+--+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted+-- into the generated HDL+checkedTruncateB ::+  forall a b f.+  ( HasCallStack+  , Resize f+  , KnownNat b, Integral (f (a + b))+  , KnownNat a, Integral (f a), Bounded (f a) ) =>+  f (a + b) -> f a+checkedTruncateB v =+  checkIntegral (Proxy @(f a)) v `seq` truncateB v

@@ -5,6 +5,10 @@ Licence   : Creative Commons 4.0 (CC BY 4.0) (https://creativecommons.org/licenses/by/4.0/) -} +{-# LANGUAGE NoImplicitPrelude #-}++{-# OPTIONS_GHC -Wno-unused-imports #-}+ module Clash.Examples (   -- * Decoders and Encoders   -- $decoders_and_encoders@@ -20,12 +24,17 @@   ) where +import Clash.Prelude+import Control.Lens+import Control.Monad+import Control.Monad.Trans.State+ {- $setup >>> :set -XDataKinds >>> :m -Clash.Explicit.Prelude >>> :m -Clash.Signal.Internal >>> import Clash.Prelude->>> import Test.QuickCheck+>>> import Test.QuickCheck ((===)) >>> import Clash.Examples.Internal -} 

@@ -82,7 +82,7 @@ cpu regbank (memOut,instr) = (regbank',(rdAddr,(,aluOut) '<$>' wrAddrM,fromIntegral ipntr))   where     -- Current instruction pointer-    ipntr = regbank '!!' PC+    ipntr = regbank 'Clash.Sized.Vector.!!' PC      -- Decoder     (MachCode {..}) = case instr of@@ -94,8 +94,8 @@       Nop                  -> nullCode      -- ALU-    regX   = regbank '!!' inputX-    regY   = regbank '!!' inputY+    regX   = regbank 'Clash.Sized.Vector.!!' inputX+    regY   = regbank 'Clash.Sized.Vector.!!' inputY     aluOut = alu aluCode regX regY      -- next instruction@@ -104,10 +104,10 @@                _                    -> ipntr + 1      -- update registers-    regbank' = 'replace' Zero   0-             $ 'replace' PC     nextPC-             $ 'replace' result aluOut-             $ 'replace' ldReg  memOut+    regbank' = 'Clash.Sized.Vector.replace' Zero   0+             $ 'Clash.Sized.Vector.replace' PC     nextPC+             $ 'Clash.Sized.Vector.replace' result aluOut+             $ 'Clash.Sized.Vector.replace' ldReg  memOut              $ regbank  alu Add   x y = x + y@@ -135,9 +135,9 @@   where     dataMemT mem (rd,wrM) = (mem',dout)       where-        dout = mem '!!' rd+        dout = mem 'Clash.Sized.Vector.!!' rd         mem' = case wrM of-                 Just (wr,din) -> 'replace' wr din mem+                 Just (wr,din) -> 'Clash.Sized.Vector.replace' wr din mem                  _ -> mem @ @@ -206,8 +206,9 @@ === Improvement 1: using @asyncRam@  As you can see, it's fairly straightforward to build a memory using registers-and read ('!!') and write ('replace') logic. This might however not result in-the most efficient hardware structure, especially when building an ASIC.+and read ('Clash.Sized.Vector.!!') and write ('Clash.Sized.Vector.replace')+logic. This might however not result in the most efficient hardware structure,+especially when building an ASIC.  Instead it is preferable to use the 'Clash.Prelude.RAM.asyncRam' function which has the potential to be translated to a more efficient structure:@@ -224,15 +225,16 @@ system2 instrs clk rst en = memOut   where     memOut = 'Clash.Explicit.RAM.asyncRam' clk clk en d32 rdAddr dout-    (rdAddr,dout,ipntr) = 'mealyB' clk rst en cpu ('Clash.Sized.Vector.replicate' d7 0) (memOut,instr)+    (rdAddr,dout,ipntr) = 'Clash.Explicit.Prelude.mealyB' clk rst en cpu ('Clash.Sized.Vector.replicate' d7 0) (memOut,instr)     instr  = 'Clash.Prelude.ROM.asyncRom' instrs '<$>' ipntr @  Again, we can simulate our system and see that it works. This time however, we need to disregard the first few output samples, because the initial content of an-'Clash.Prelude.RAM.asyncRam' is 'undefined', and consequently, the first few-output samples are also 'undefined'. We use the utility function 'printX' to conveniently-filter out the undefinedness and replace it with the string "X" in the few leading outputs.+'Clash.Prelude.RAM.asyncRam' is /undefined/, and consequently, the first few+output samples are also /undefined/. We use the utility function+'Clash.XException.printX' to conveniently filter out the undefinedness and+replace it with the string "X" in the few leading outputs.  @ >>> printX $ sampleN 32 $ system2 prog systemClockGen resetGen enableGen@@ -272,7 +274,7 @@ cpu2 (regbank,ldRegD) (memOut,instr) = ((regbank',ldRegD'),(rdAddr,(,aluOut) '<$>' wrAddrM,fromIntegral ipntr))   where     -- Current instruction pointer-    ipntr = regbank '!!' PC+    ipntr = regbank 'Clash.Sized.Vector.!!' PC      -- Decoder     (MachCode {..}) = case instr of@@ -284,8 +286,8 @@       Nop                  -> nullCode      -- ALU-    regX   = regbank '!!' inputX-    regY   = regbank '!!' inputY+    regX   = regbank 'Clash.Sized.Vector.!!' inputX+    regY   = regbank 'Clash.Sized.Vector.!!' inputY     aluOut = alu aluCode regX regY      -- next instruction@@ -295,10 +297,10 @@      -- update registers     ldRegD'  = ldReg -- Delay the ldReg by 1 cycle-    regbank' = 'replace' Zero   0-             $ 'replace' PC     nextPC-             $ 'replace' result aluOut-             $ 'replace' ldRegD memOut+    regbank' = 'Clash.Sized.Vector.replace' Zero   0+             $ 'Clash.Sized.Vector.replace' PC     nextPC+             $ 'Clash.Sized.Vector.replace' result aluOut+             $ 'Clash.Sized.Vector.replace' ldRegD memOut              $ regbank @ @@ -316,7 +318,7 @@ system3 instrs clk rst en = memOut   where     memOut = 'blockRam' clk en (replicate d32 0) rdAddr dout-    (rdAddr,dout,ipntr) = 'mealyB' clk rst en cpu2 (('Clash.Sized.Vector.replicate' d7 0),Zero) (memOut,instr)+    (rdAddr,dout,ipntr) = 'Clash.Explicit.Prelude.mealyB' clk rst en cpu2 (('Clash.Sized.Vector.replicate' d7 0),Zero) (memOut,instr)     instr  = 'Clash.Explicit.Prelude.asyncRom' instrs '<$>' ipntr @ @@ -361,8 +363,8 @@  When we simulate our system we see that it works. This time again, we need to disregard the first sample, because the initial output of a-'blockRam' is 'undefined'. We use the utility function 'printX' to conveniently-filter out the undefinedness and replace it with the string "X".+'blockRam' is /undefined/. We use the utility function 'Clash.XException.printX'+to conveniently filter out the undefinedness and replace it with the string "X".  @ >>> printX $ sampleN 34 $ system3 prog2 systemClockGen resetGen enableGen@@ -375,6 +377,7 @@ -}  {-# LANGUAGE GADTs #-}+{-# LANGUAGE NoImplicitPrelude#-}  {-# LANGUAGE Trustworthy #-} @@ -399,11 +402,12 @@   ) where +import           Clash.HaskellPrelude+ import           Data.Maybe             (isJust) import qualified Data.Sequence          as Seq import           GHC.Stack              (HasCallStack, withFrozenCallStack) import           GHC.TypeLits           (KnownNat, type (^), type (<=))-import           Prelude                hiding (length, replicate)  import           Clash.Annotations.Primitive   (hasBlackBox)@@ -418,7 +422,7 @@ import           Clash.Sized.Vector     (Vec, replicate, toList, iterateI) import qualified Clash.Sized.Vector     as CV import           Clash.XException-  (maybeIsX, seqX, NFDataX, deepErrorX, defaultSeqX, fromJustX)+  (maybeIsX, seqX, NFDataX, deepErrorX, defaultSeqX, fromJustX, undefined)  {- $setup >>> :m -Clash.Prelude@@ -691,7 +695,7 @@ -- | Create a blockRAM with space for @n@ elements -- -- * __NB__: Read value is delayed by 1 cycle--- * __NB__: Initial output value is 'undefined'+-- * __NB__: Initial output value is /undefined/ -- -- @ -- bram40@@ -737,7 +741,7 @@ -- | Create a blockRAM with space for 2^@n@ elements -- -- * __NB__: Read value is delayed by 1 cycle--- * __NB__: Initial output value is 'undefined'+-- * __NB__: Initial output value is /undefined/ -- -- @ -- bram32@@ -842,7 +846,7 @@   wa1 = mux rstBool (fromInteger . toInteger <$> waCounter) (fromEnum <$> wa0)   w1  = mux rstBool (initF <$> waCounter) w0 --- | blockRAM1 primitive+-- | blockRAMU primitive blockRamU#   :: forall n dom a    . ( KnownDomain dom@@ -870,7 +874,7 @@     clk     en     (CV.map-      (\i -> deepErrorX $ "Initial value at index " ++ show i ++ " undefined.")+      (\i -> deepErrorX $ "Initial value at index " <> show i <> " undefined.")       (iterateI @n succ (0 :: Int))) {-# NOINLINE blockRamU# #-} {-# ANN blockRamU# hasBlackBox #-}

@@ -152,7 +152,7 @@   -> Signal dom (BitVector m)   -- ^ Value of the @blockRAM@ at address @r@ from the previous clock cycle blockRamFilePow2 = \clk en file rd wrM -> withFrozenCallStack-  (blockRamFile clk en (pow2SNat (SNat @ n)) file rd wrM)+  (blockRamFile clk en (pow2SNat (SNat @n)) file rd wrM) {-# INLINE blockRamFilePow2 #-}  -- | Create a blockRAM with space for @n@ elements

@@ -180,7 +180,7 @@     -- That is why we drop the first value of the stream.     let (_ :- out) = zipSig xs' ys' in out   where-    xs' = register# clk rst en (error "ddrOut: unreachable error") i0 xs+    xs' = register# clk rst en (errorX "ddrOut: unreachable error") i0 xs     ys' = register# clk rst en (deepErrorX "ddrOut: initial value undefined") i0 ys     zipSig (a :- as) (b :- bs) = a :- b :- zipSig as bs {-# NOINLINE ddrOut# #-}

@@ -72,10 +72,9 @@   , dumpVCD     -- * Exported modules     -- ** Synchronous signals+  , module Clash.Explicit.Reset   , module Clash.Explicit.Signal   , module Clash.Explicit.Signal.Delayed-    -- ** DataFlow interface-  , module Clash.Prelude.DataFlow     -- ** Datatypes     -- *** Bit vectors   , module Clash.Sized.BitVector@@ -139,7 +138,7 @@  import Clash.Annotations.TopEntity import Clash.Class.AutoReg-import Clash.Class.BitPack+import Clash.Class.BitPack hiding (GBitPack(..)) import Clash.Class.Exp import Clash.Class.Num import Clash.Class.Resize@@ -153,12 +152,12 @@ import Clash.Explicit.ROM import Clash.Explicit.ROM.File import Clash.Explicit.Prelude.Safe+import Clash.Explicit.Reset import Clash.Explicit.Signal import Clash.Explicit.Signal.Delayed import Clash.Explicit.Testbench import Clash.Prelude.BitIndex import Clash.Prelude.BitReduction-import Clash.Prelude.DataFlow import Clash.Prelude.ROM.File       (asyncRomFile, asyncRomFilePow2) import Clash.Promoted.Nat import Clash.Promoted.Nat.TH@@ -171,7 +170,7 @@ import Clash.Sized.RTree import Clash.Sized.Signed import Clash.Sized.Unsigned-import Clash.Sized.Vector+import Clash.Sized.Vector hiding (fromList, unsafeFromList) import Clash.XException  {- $setup

@@ -50,8 +50,6 @@     -- ** Synchronous signals   , module Clash.Explicit.Signal   , module Clash.Explicit.Signal.Delayed-    -- ** DataFlow interface-  , module Clash.Prelude.DataFlow     -- ** Datatypes     -- *** Bit vectors   , module Clash.Sized.BitVector@@ -123,7 +121,6 @@   (dualFlipFlopSynchronizer, asyncFIFOSynchronizer) import Clash.Prelude.BitIndex import Clash.Prelude.BitReduction-import Clash.Prelude.DataFlow import Clash.Prelude.ROM             (asyncRom, asyncRomPow2) import Clash.Promoted.Nat import Clash.Promoted.Nat.TH@@ -135,7 +132,7 @@ import Clash.Sized.RTree import Clash.Sized.Signed import Clash.Sized.Unsigned-import Clash.Sized.Vector+import Clash.Sized.Vector hiding (fromList, unsafeFromList) import Clash.XException  {- $setup@@ -249,4 +246,3 @@       then (0,   not i) -- reset state and oscillate output       else (s+1, i)     -- hold current output {-# INLINEABLE oscillate #-}-

@@ -133,7 +133,7 @@   -- ^ Read address @rd@   -> Signal dom (BitVector m)   -- ^ The value of the ROM at address @rd@ from the previous clock cycle-romFilePow2 = \clk en -> romFile clk en (pow2SNat (SNat @ n))+romFilePow2 = \clk en -> romFile clk en (pow2SNat (SNat @n)) {-# INLINE romFilePow2 #-}  -- | A ROM with a synchronous read port, with space for @n@ elements

@@ -0,0 +1,293 @@+{-|+Copyright  :  (C) 2020, QBayLogic B.V.+License    :  BSD2 (see the file LICENSE)+Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>++Utilities to deal with resets.+-}++{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}++{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}++module Clash.Explicit.Reset+  ( -- Defined in this module+    resetSynchronizer+  , resetGlitchFilter+  , holdReset+  , convertReset++    -- Reexports+  , Reset+  , resetGen+  , resetGenN+  , resetKind+  , systemResetGen+  , unsafeToReset+  , unsafeFromReset+  , unsafeToHighPolarity+  , unsafeToLowPolarity+  , unsafeFromHighPolarity+  , unsafeFromLowPolarity+  ) where++import           Data.Bits (testBit, shiftL, (.|.))+import           Data.Type.Equality ((:~:)(Refl))+import           GHC.Generics (Generic)++import           Clash.Class.BitPack (pack)+import           Clash.Class.Resize (resize)+import           Clash.Class.Num (satSucc, SaturationMode(SatBound))+import           Clash.Explicit.Mealy+import           Clash.Explicit.Signal+import           Clash.Promoted.Nat+import           Clash.Signal.Internal+import           Clash.Sized.BitVector (BitVector)+import           Clash.Sized.Index (Index)+import           Clash.XException (NFDataX, ShowX)++import           GHC.TypeLits (type (+), KnownNat)++{- $setup+>>> :m -Clash.Prelude+>>> :m -Clash.Prelude.Safe+>>> import Clash.Explicit.Prelude+-}++-- | The resetSynchronizer will synchronize an incoming reset according to+-- whether the domain is synchronous or asynchronous.+--+-- For asynchronous resets this synchronizer ensures the reset will only+-- be de-asserted synchronously but it can still be asserted asynchronously.+-- The reset assert is immediate, but reset de-assertion is delayed by two+-- cycles.++-- Normally, asynchronous resets can be both asynchronously asserted and+-- de-asserted. Asynchronous de-assertion can induce meta-stability in the+-- component which is being reset. To ensure this doesn't happen,+-- 'resetSynchronizer' ensures that de-assertion of a reset happens+-- synchronously. Assertion of the reset remains asynchronous.+--+-- Note that asynchronous assertion does not induce meta-stability in the+-- component whose reset is asserted. However, when a component \"A\" in another+-- clock or reset domain depends on the value of a component \"B\" being+-- reset, then asynchronous assertion of the reset of component \"B"\ can induce+-- meta-stability in component \"A\". To prevent this from happening you need+-- to use a proper synchronizer, for example one of the synchronizers in+-- "Clash.Explicit.Synchronizer".+--+-- For synchronous resets this function ensures that the reset is asserted and+-- de-asserted synchronously. Both the assertion and de-assertion of the reset+-- are delayed by two cycles.+--+-- === __Example 1__+-- The circuit below detects a rising bit (i.e., a transition from 0 to 1) in a+-- given argument. It takes a reset that is not synchronized to any of the other+-- incoming signals and synchronizes it using 'resetSynchronizer'.+--+-- @+-- topEntity+--   :: Clock  System+--   -> Reset  System+--   -> Enable System+--   -> Signal System Bit+--   -> Signal System (BitVector 8)+-- topEntity clk asyncRst ena key1 =+--   withClockResetEnable clk rst ena leds+--  where+--   rst   = 'resetSynchronizer' clk asyncRst ena+--   key1R = isRising 1 key1+--   leds  = mealy blinkerT (1, False, 0) key1R+-- @+--+-- === __Example 2__+-- Similar to /Example 1/ this circuit detects a rising bit (i.e., a transition+-- from 0 to 1) in a given argument. It takes a clock that is not stable yet and+-- a reset singal that is not synchronized to any other signals. It stabalizes+-- the clock and then synchronizes the reset signal.+--+-- @+-- topEntity+--   :: Clock  System+--   -> Reset  System+--   -> Signal System Bit+--   -> Signal System (BitVector 8)+-- topEntity clk rst ena key1 =+--     let  (pllOut,pllStable) = altpll (SSymbol @"altpll50") clk rst+--          rstSync            = 'resetSynchronizer' pllOut (unsafeToHighPolarity pllStable) ena+--     in   exposeClockResetEnable leds pllOut rstSync enableGen+--   where+--     key1R  = isRising 1 key1+--     leds   = mealy blinkerT (1, False, 0) key1R+-- @+--+-- === __Implementation details__+-- 'resetSynchronizer' implements the following circuit for asynchronous domains:+--+-- @+--                                   rst+--   --------------------------------------++--                       |                 |+--                  +----v----+       +----v----++--     deasserted   |         |       |         |+--   --------------->         +------->         +-------->+--                  |         |       |         |+--              +---|>        |   +---|>        |+--              |   |         |   |   |         |+--              |   +---------+   |   +---------++--      clk     |                 |+--   -----------------------------++-- @+--+-- This corresponds to figure 3d at <https://www.embedded.com/asynchronous-reset-synchronization-and-distribution-challenges-and-solutions/>+--+-- For synchronous domains two sequential dflipflops are used:+--+-- @+--                  +---------+       +---------++--     rst          |         |       |         |+--   --------------->         +------->         +-------->+--                  |         |       |         |+--              +---|>        |   +---|>        |+--              |   |         |   |   |         |+--              |   +---------+   |   +---------++--      clk     |                 |+--   -----------------------------++-- @+--+resetSynchronizer+  :: forall dom+   . KnownDomain dom+  => Clock dom+  -> Reset dom+  -> Enable dom+  -- ^ Warning: this argument will be removed in future versions of Clash.+  -> Reset dom+resetSynchronizer clk rst _ = rstOut+ where+  isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }+  rstOut =+    case (resetKind @dom) of+      SAsynchronous -> unsafeToReset+                         $ register clk rst enableGen isActiveHigh+                         $ register clk rst enableGen isActiveHigh+                         $ pure (not isActiveHigh)+      SSynchronous  -> unsafeToReset+                         $ delay clk enableGen isActiveHigh+                         $ delay clk enableGen isActiveHigh+                         $ unsafeFromReset rst+{-# NOINLINE resetSynchronizer #-} -- Give reset synchronizer its own HDL file++data GlitchFilterState = Idle | InReset+  deriving (Generic, NFDataX, Show, ShowX)++-- | Filter glitches from reset signals by only triggering a reset after it has+-- been asserted for /glitchlessPeriod/ cycles. It will then stay asserted for+-- as long as the given reset was asserted consecutively.+--+-- If synthesized on a domain with initial values, 'resetGlitchFilter' will+-- output an asserted reset for /glitchlessPeriod/ cycles (plus any cycles added+-- by the given reset). If initial values can't be used, it will only output+-- defined reset values after /glitchlessPeriod/ cycles.+--+-- === __Example 1__+-- >>> let sampleResetN n = sampleN n . unsafeToHighPolarity+-- >>> let resetFromList = unsafeFromHighPolarity . fromList+-- >>> let rst = resetFromList [True, True, False, False, True, False, False, True, True, False, True]+-- >>> sampleResetN 12 (resetGlitchFilter d2 systemClockGen rst)+-- [True,True,True,True,False,False,False,False,False,True,True,False]+resetGlitchFilter+  :: forall dom glitchlessPeriod n+   . ( KnownDomain dom+     , glitchlessPeriod ~ (n + 1) )+  => SNat glitchlessPeriod+  -- ^ Consider a reset signal to be properly asserted after having seen the+  -- reset asserted for /glitchlessPeriod/ cycles straight.+  -> Clock dom+  -> Reset dom+  -> Reset dom+resetGlitchFilter SNat clk rst =+  unsafeToReset (mealy clk noReset enableGen go Idle shiftReg)+ where+  shiftReg =+    delay clk enableGen noGlitch (shiftInLsb <$> shiftReg <*> unsafeFromReset rst)++  go gfs sreg+    | sreg == noGlitch = (InReset, asserted)+    | Idle <- gfs = (Idle, not asserted)+    | otherwise = (if msb == asserted then InReset else Idle, msb)+   where+    msb = testBit sreg (natToNum @n)++  noGlitch :: BitVector glitchlessPeriod+  noGlitch = if asserted then maxBound else minBound++  noReset :: Reset dom+  noReset = unsafeToReset (pure (not asserted))++  asserted :: Bool+  asserted =+    case resetPolarity @dom of+      SActiveHigh -> True+      SActiveLow -> False++  shiftInLsb :: forall m. KnownNat m => BitVector (m + 1) -> Bool -> BitVector (m + 1)+  shiftInLsb bv s = shiftL bv 1 .|. resize (pack s)+{-# NOINLINE resetGlitchFilter #-} -- Give reset glitch filter its own HDL file++-- | Hold reset for a number of cycles relative to an incoming reset signal.+--+-- Example:+--+-- >>> let sampleWithReset = sampleN 8 . unsafeToHighPolarity+-- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (resetGenN (SNat @3)))+-- [True,True,True,True,True,False,False,False]+--+-- 'holdReset' holds the reset for an additional 2 clock cycles for a total+-- of 5 clock cycles where the reset is asserted. 'holdReset' also works on+-- intermediate assertions of the reset signal:+--+-- >>> let rst = fromList [True, False, False, False, True, False, False, False]+-- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (unsafeFromHighPolarity rst))+-- [True,True,True,False,True,True,True,False]+--+holdReset+  :: forall dom n+   . KnownDomain dom+  => Clock dom+  -> Enable dom+  -- ^ Global enable+  -> SNat n+  -- ^ Hold for /n/ cycles, counting from the moment the incoming reset+  -- signal becomes deasserted.+  -> Reset dom+  -- ^ Reset to extend+  -> Reset dom+holdReset clk en SNat rst =+  unsafeFromHighPolarity ((/=maxBound) <$> counter)+ where+  counter :: Signal dom (Index (n+1))+  counter = register clk rst en 0 (satSucc SatBound <$> counter)++-- | Convert between different types of reset, adding a synchronizer when+-- the domains are not the same. See 'resetSynchronizer' for further details+-- about reset synchronization.+convertReset+  :: forall domA domB+   . ( KnownDomain domA+     , KnownDomain domB+     )+  => Clock domA+  -> Clock domB+  -> Reset domA+  -> Reset domB+convertReset clkA clkB rstA0 = rstA2+ where+  rstA1 = unsafeToReset (unsafeSynchronizer clkA clkB (unsafeFromReset rstA0))+  rstA2 =+    case (sameDomain @domA @domB) of+      Just Refl -> rstA0+      Nothing   -> resetSynchronizer clkB rstA1 enableGen

@@ -2,6 +2,7 @@ Copyright  :  (C) 2013-2016, University of Twente,                   2016-2019, Myrtle Software,                   2017     , Google Inc.+                  2020     , Ben Gamari License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> @@ -193,7 +194,6 @@   , enableGen     -- * Clock   , Clock-  , freqCalc  -- DEPRECATED   , periodToHz   , hzToPeriod     -- ** Synchronization primitive@@ -207,9 +207,6 @@   , unsafeToLowPolarity   , unsafeFromHighPolarity   , unsafeFromLowPolarity-  , convertReset-  , resetSynchronizer-  , holdReset     -- * Basic circuit functions   , enable   , dflipflop@@ -240,6 +237,8 @@     -- ** lazy versions   , simulate_lazy   , simulateB_lazy+    -- ** Automaton+  , signalAutomaton     -- * List \<-\> Signal conversion (not synthesizable)   , sample   , sampleN@@ -267,10 +266,9 @@ where  import           Data.Maybe                     (isJust)-import           GHC.TypeLits                   (type (+), type (<=))+import           GHC.TypeLits                   (type (<=))  import           Clash.Annotations.Primitive    (hasBlackBox)-import           Clash.Class.Num                (satSucc, SaturationMode(SatBound)) import           Clash.Promoted.Nat             (SNat(..), snatToNum) import           Clash.Signal.Bundle   (Bundle (..), EmptyTuple(..), TaggedEmptyTuple(..), vecBundle#)@@ -278,7 +276,6 @@ import           Clash.Signal.Internal import           Clash.Signal.Internal.Ambiguous   (knownVDomain, clockPeriod, activeEdge, resetKind, initBehavior, resetPolarity)-import           Clash.Sized.Index              (Index) import qualified Clash.Sized.Vector import           Clash.XException               (NFDataX, deepErrorX, fromJustX) @@ -333,7 +330,7 @@ -- | Clock generator for the 'System' clock domain. -- -- __NB__: should only be used for simulation, and __not__ for the /testBench/--- function. For the /testBench/ function, used 'tbSystemClockGen'+-- function. For the /testBench/ function, used 'Clash.Explicit.Testbench.tbSystemClockGen' systemClockGen   :: Clock System systemClockGen = clockGen@@ -360,66 +357,6 @@ systemResetGen ::Reset System systemResetGen = resetGen --- | Normally, asynchronous resets can be both asynchronously asserted and--- de-asserted. Asynchronous de-assertion can induce meta-stability in the--- component which is being reset. To ensure this doesn't happen,--- 'resetSynchronizer' ensures that de-assertion of a reset happens--- synchronously. Assertion of the reset remains asynchronous.------ Note that asynchronous assertion does not induce meta-stability in the--- component whose reset is asserted. However, when a component \"A\" in another--- clock or reset domain depends on the value of a component \"B\" being--- reset, then asynchronous assertion of the reset of component \"B"\ can induce--- meta-stability in component \"A\". To prevent this from happening you need--- to use a proper synchronizer, for example one of the synchronizers in--- "Clash.Explicit.Synchronizer"------ === __Example__------ @--- topEntity---   :: Clock  System---   -> Reset  System---   -> Signal System Bit---   -> Signal System (BitVector 8)--- topEntity clk rst key1 =---     let  (pllOut,pllStable) = altpll (SSymbol @"altpll50") clk rst---          rstSync            = 'resetSynchronizer' pllOut (unsafeToHighPolarity pllStable)---     in   exposeClockResetEnable leds pllOut rstSync---   where---     key1R  = isRising 1 key1---     leds   = mealy blinkerT (1, False, 0) key1R--- @-resetSynchronizer-  :: forall dom-   . KnownDomain dom-  => Clock dom-  -> Reset dom-  -> Enable dom-  -> Reset dom-resetSynchronizer clk rst en =-  case resetKind @dom of-    SAsynchronous ->-      let isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }-          r1 = register clk rst en isActiveHigh (pure (not isActiveHigh))-          r2 = register clk rst en isActiveHigh r1-       in unsafeToReset r2-    SSynchronous ->-      -- Reset is already synchronous, nothing to do!-      rst---- | Calculate the period, in __ps__, given a frequency in __Hz__------ i.e. to calculate the clock period for a circuit to run at 240 MHz we get------ >>> freqCalc 240e6--- 4167------ __NB__: This function is /not/ synthesizable-freqCalc :: Double -> Integer-freqCalc = toInteger . hzToPeriod-{-# DEPRECATED freqCalc "Use 'hzToPeriod' instead." #-}- -- ** Synchronization primitive -- | The 'unsafeSynchronizer' function is a primitive that must be used to -- connect one clock domain to the other, and will be synthesized to a (bundle@@ -531,13 +468,13 @@ -- with values appearing from the "future". veryUnsafeSynchronizer   :: Int-  -- ^ Period of clock belonging to 'dom1'+  -- ^ Period of clock belonging to @dom1@   -> Int-  -- ^ Period of clock belonging to 'dom2'+  -- ^ Period of clock belonging to @dom2@   -> Signal dom1 a   -> Signal dom2 a veryUnsafeSynchronizer t1 t2-  -- this case is just an optimisation for when the periods are the same+  -- this case is just an optimization for when the periods are the same   | t1 == t2 = same    | otherwise = go 0@@ -836,40 +773,6 @@ simulateB_lazy f = simulate_lazy (bundle . f . unbundle)  --- | Hold reset for a number of cycles relative to an incoming reset signal.------ Example:------ >>> let sampleWithReset = sampleN 8 . unsafeToHighPolarity--- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (resetGenN (SNat @3)))--- [True,True,True,True,True,False,False,False]------ 'holdReset' holds the reset for an additional 2 clock cycles for a total--- of 5 clock cycles where the reset is asserted. 'holdReset' also works on--- intermediate assertions of the reset signal:------ >>> let rst = fromList [True, False, False, False, True, False, False, False]--- >>> sampleWithReset (holdReset @System clockGen enableGen (SNat @2) (unsafeFromHighPolarity rst))--- [True,True,True,False,True,True,True,False]----holdReset-  :: forall dom n-   . KnownDomain dom-  => Clock dom-  -> Enable dom-  -- ^ Global enable-  -> SNat n-  -- ^ Hold for /n/ cycles, counting from the moment the incoming reset-  -- signal becomes deasserted.-  -> Reset dom-  -- ^ Reset to extend-  -> Reset dom-holdReset clk en SNat rst =-  unsafeFromHighPolarity ((/=maxBound) <$> counter)- where-  counter :: Signal dom (Index (n+1))-  counter = register clk rst en 0 (satSucc SatBound <$> counter)- -- | Like 'fromList', but resets on reset and has a defined reset value. -- -- >>> let rst = unsafeFromHighPolarity (fromList [True, True, False, False, True, False])@@ -891,30 +794,6 @@   go (r :- rs) _ | r = resetValue :- go rs vals   go (_ :- rs) [] = deepErrorX "fromListWithReset: input ran out" :- go rs []   go (_ :- rs) (a : as) = a :- go rs as---- | Convert between different types of reset, adding a synchronizer in case--- it needs to convert from an asynchronous to a synchronous reset.-convertReset-  :: forall domA domB-   . ( KnownDomain domA-     , KnownDomain domB-     )-  => Clock domA-  -> Clock domB-  -> Reset domA-  -> Reset domB-convertReset clkA clkB (unsafeToHighPolarity -> rstA0) =-  unsafeFromHighPolarity rstA2- where-  rstA1 = unsafeSynchronizer clkA clkB rstA0-  rstA2 =-    case (resetKind @domA, resetKind @domB) of-      (SSynchronous,  SSynchronous)  -> rstA1-      (SAsynchronous, SAsynchronous) -> rstA1-      (SSynchronous,  SAsynchronous) -> rstA1-      (SAsynchronous, SSynchronous) ->-        delay clkB enableGen True $-          delay clkB enableGen True rstA1  -- | Get a list of samples from a 'Signal', while asserting the reset line -- for /n/ clock cycles. 'sampleWithReset' does not return the first /n/ cycles,

@@ -9,6 +9,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -43,15 +44,15 @@   ) where +import Prelude                    ((.), (<$>), (<*>), id, Num(..))+ import Data.Coerce                (coerce) import Data.Kind                  (Type) import Data.Proxy                 (Proxy (..)) import Data.Singletons.Prelude    (Apply, TyFun, type (@@)) import GHC.TypeLits               (KnownNat, Nat, type (+), type (^), type (*))-import Prelude                    hiding (head, length, repeat)  import Clash.Sized.Vector-  (Vec, dtfold, head, length, repeat, shiftInAt0, singleton) import Clash.Signal.Delayed.Internal   (DSignal(..), dfromList, dfromList_lazy, fromSignal, toSignal,    unsafeFromSignal, antiDelay, feedback)@@ -217,6 +218,7 @@ -- [-1,-1,1,2,3,4] -- -- You can also use type application to do the same:+-- -- >>> sampleN 6 (toSignal (delayI @2 (-1) enableGen systemClockGen (dfromList [1..]))) -- [-1,-1,1,2,3,4] delayI

@@ -6,6 +6,7 @@   I\/O actions that are translatable to HDL -} +{-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns, MagicHash, TypeOperators, ScopedTypeVariables, FlexibleContexts #-} {-# LANGUAGE DataKinds, GADTs, TypeApplications #-} @@ -43,7 +44,9 @@ where  import Control.Monad (when)+#if __GLASGOW_HASKELL__ < 900 import Data.Coerce+#endif import Data.IORef import GHC.TypeLits import Prelude hiding (getChar, putChar, getLine)@@ -61,7 +64,11 @@ -- itself is unlikely to be synthesisable to a digital circuit. -- -- See 'mealyIO' as to its use.+#if __GLASGOW_HASKELL__ >= 900+data SimIO a = SimIO {unSimIO :: !(IO a)}+#else newtype SimIO a = SimIO {unSimIO :: IO a}+#endif  instance Functor SimIO where   fmap = fmapSimIO#@@ -87,7 +94,11 @@   (>>=)  = bindSimIO#  bindSimIO# :: SimIO a -> (a -> SimIO b) -> SimIO b+#if __GLASGOW_HASKELL__ >= 900+bindSimIO# (SimIO m) k = SimIO (m >>= (\x -> x `seqX` unSimIO (k x)))+#else bindSimIO# (SimIO m) k = SimIO (m >>= (\x -> x `seqX` coerce k x))+#endif {-# NOINLINE bindSimIO# #-}  -- | Display a string on /stdout/@@ -109,7 +120,11 @@ {-# ANN finish hasBlackBox #-}  -- | Mutable reference+#if __GLASGOW_HASKELL__ >= 900+data Reg a = Reg !(IORef a)+#else newtype Reg a = Reg (IORef a)+#endif  -- | Create a new mutable reference with the given starting value reg@@ -138,7 +153,11 @@ {-# ANN writeReg hasBlackBox #-}  -- | File handle+#if __GLASGOW_HASKELL__ >= 900+data File = File !IO.Handle+#else newtype File = File IO.Handle+#endif  -- | Open a file openFile@@ -154,6 +173,23 @@   -- * "w+": Create for update   -- * "a+": Append, open or create for update at end-of-file   -> SimIO File+#if __GLASGOW_HASKELL__ >= 900+openFile fp "r"   = SimIO $ fmap File (IO.openFile fp IO.ReadMode)+openFile fp "w"   = SimIO $ fmap File (IO.openFile fp IO.WriteMode)+openFile fp "a"   = SimIO $ fmap File (IO.openFile fp IO.AppendMode)+openFile fp "rb"  = SimIO $ fmap File (IO.openBinaryFile fp IO.ReadMode)+openFile fp "wb"  = SimIO $ fmap File (IO.openBinaryFile fp IO.WriteMode)+openFile fp "ab"  = SimIO $ fmap File (IO.openBinaryFile fp IO.AppendMode)+openFile fp "r+"  = SimIO $ fmap File (IO.openFile fp IO.ReadWriteMode)+openFile fp "w+"  = SimIO $ fmap File (IO.openFile fp IO.WriteMode)+openFile fp "a+"  = SimIO $ fmap File (IO.openFile fp IO.AppendMode)+openFile fp "r+b" = SimIO $ fmap File (IO.openBinaryFile fp IO.ReadWriteMode)+openFile fp "w+b" = SimIO $ fmap File (IO.openBinaryFile fp IO.WriteMode)+openFile fp "a+b" = SimIO $ fmap File (IO.openBinaryFile fp IO.AppendMode)+openFile fp "rb+" = SimIO $ fmap File (IO.openBinaryFile fp IO.ReadWriteMode)+openFile fp "wb+" = SimIO $ fmap File (IO.openBinaryFile fp IO.WriteMode)+openFile fp "ab+" = SimIO $ fmap File (IO.openBinaryFile fp IO.AppendMode)+#else openFile fp "r"   = coerce (IO.openFile fp IO.ReadMode) openFile fp "w"   = coerce (IO.openFile fp IO.WriteMode) openFile fp "a"   = coerce (IO.openFile fp IO.AppendMode)@@ -169,6 +205,7 @@ openFile fp "rb+" = coerce (IO.openBinaryFile fp IO.ReadWriteMode) openFile fp "wb+" = coerce (IO.openBinaryFile fp IO.WriteMode) openFile fp "ab+" = coerce (IO.openBinaryFile fp IO.AppendMode)+#endif openFile _  m     = error ("openFile unknown mode: " ++ show m) {-# NOINLINE openFile #-} {-# ANN openFile hasBlackBox #-}@@ -313,7 +350,7 @@ --     rst = resetGen --     ena = enableGen -----     regOut = register clk rst ena (fromEnum 'a') regIn+--     regOut = register clk rst ena (fromEnum \'a\') regIn --     regIn  = 'mealyIO' clk tbMachine tbInit regOut -- @ mealyIO

@@ -48,9 +48,7 @@   (Clock, Reset, System, Signal, clockPeriod, toEnable, fromList, register,   unbundle, unsafeSynchronizer, veryUnsafeSynchronizer) import Clash.Signal.Internal (Clock (..), Reset (..))-import Clash.Signal-  (mux, DomainResetKind, ResetKind(Asynchronous), KnownDomain,-  Enable)+import Clash.Signal          (mux, KnownDomain, Enable) import Clash.Sized.Index     (Index) import Clash.Sized.Internal.BitVector   (BitVector, isLike)@@ -193,7 +191,6 @@   :: forall l a dom    . ( KnownNat l      , KnownDomain dom-     , DomainResetKind dom ~ 'Asynchronous      , Eq a      , ShowX a )   => Clock dom@@ -256,7 +253,6 @@    . ( KnownNat l      , KnownDomain testDom      , KnownDomain circuitDom-     , DomainResetKind testDom ~ 'Asynchronous      , Eq a      , ShowX a )   => Clock testDom@@ -300,7 +296,6 @@    . ( KnownNat l      , KnownNat n      , KnownDomain dom-     , DomainResetKind dom ~ 'Asynchronous      )   => Clock dom   -- ^ Clock to which the input signal is synchronized to@@ -323,7 +318,6 @@      , KnownNat n      , KnownDomain testDom      , KnownDomain circuitDom-     , DomainResetKind testDom ~ 'Asynchronous      )   => Clock testDom   -- ^ Clock to which the input signal is synchronized to@@ -387,7 +381,6 @@   :: forall testDom circuitDom    . ( KnownDomain testDom      , KnownDomain circuitDom-     , DomainResetKind testDom ~ 'Asynchronous      )   => Signal testDom Bool   -> (Clock testDom, Clock circuitDom)@@ -413,10 +406,10 @@ -- import "Clash.Explicit.Testbench" -- -- -- Fast domain: twice as fast as \"Slow\"--- 'createDomain' 'vSystem'{vName=\"Fast\", vPeriod=10}+-- 'Clash.Explicit.Prelude.createDomain' 'Clash.Explicit.Prelude.vSystem'{vName=\"Fast\", vPeriod=10} ----- -- Slow domain: twice as slow as "Fast"--- 'createDomain' 'vSystem'{vName=\"Slow\", vPeriod=20}+-- -- Slow domain: twice as slow as \"Fast\"+-- 'Clash.Explicit.Prelude.createDomain' 'Clash.Explicit.Prelude.vSystem'{vName=\"Slow\", vPeriod=20} -- -- topEntity --   :: 'Clock' \"Fast\"@@ -434,14 +427,14 @@ --   :: 'Signal' \"Slow\" Bool -- testBench = done --   where---     testInput      = 'Clash.Explicit.Testbench.stimuliGenerator' clkA1 rstA1 $('listToVecTH' [1::Unsigned 8,2,3,4,5,6,7,8])---     expectedOutput = 'Clash.Explicit.Testbench.outputVerifier'   clkB2 rstB2 $('listToVecTH' [(0,0) :: (Unsigned 8, Unsigned 8),(1,2),(3,4),(5,6),(7,8)])+--     testInput      = 'Clash.Explicit.Testbench.stimuliGenerator' clkA1 rstA1 $('Clash.Sized.Vector.listToVecTH' [1::Unsigned 8,2,3,4,5,6,7,8])+--     expectedOutput = 'Clash.Explicit.Testbench.outputVerifier'   clkB2 rstB2 $('Clash.Sized.Vector.listToVecTH' [(0,0) :: (Unsigned 8, Unsigned 8),(1,2),(3,4),(5,6),(7,8)]) --     done           = expectedOutput (topEntity clkA1 rstA1 enableGen clkB2 testInput) --     done'          = not \<$\> done --     clkA1          = 'tbClockGen' \@\"Fast\" (unsafeSynchronizer clkB2 clkA1 done') --     clkB2          = 'tbClockGen' \@\"Slow\" done'---     rstA1          = 'resetGen' \@\"Fast\"---     rstB2          = 'resetGen' \@\"Slow\"+--     rstA1          = 'Clash.Signal.resetGen' \@\"Fast\"+--     rstB2          = 'Clash.Signal.resetGen' \@\"Slow\" -- @ tbClockGen   :: KnownDomain testDom

@@ -0,0 +1,266 @@+{-|+Copyright  :  (C) 2019, Myrtle Software Ltd+License    :  BSD2 (see the file LICENSE)+Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>++Verification primitives for Clash. Currently implements PSL (Property+Specification Language) and SVA (SystemVerilog Assertions). For a good overview+of PSL and an introduction to the concepts of property checking, read+<https://standards.ieee.org/standard/62531-2012.html>.++The verification API is currently experimental and subject to change.+-}++{-# LANGUAGE NoImplicitPrelude #-}++module Clash.Explicit.Verification+  ( -- * Types+    Assertion+  , Property+  , AssertionValue+  , RenderAs(..)++    -- * Bootstrapping functions+  , name+  , lit++    -- * Functions to build a PSL/SVA expressions+  , not+  , and+  , or+  , implies+  , next+  , nextN+  , before+  , timplies+  , timpliesOverlapping+  , always+  , never++  -- * Asserts+  , assert+  , cover++  -- * Assertion checking+  , check+  , checkI++  -- * Functions to deal with assertion results+  , hideAssertion+  )+ where++import           Prelude+  (Bool, Word, (.), pure, max, concat)++import           Data.Text  (Text)+import           Data.Maybe (Maybe(Just))++import           Clash.Annotations.Primitive+  (Primitive(InlinePrimitive), HDL(..))+import           Clash.Signal.Internal (KnownDomain, Signal, Clock, Reset)+import           Clash.XException      (errorX, hwSeqX)++import           Clash.Verification.Internal++-- | Convert a signal to a cv expression with a name hint. Clash will try its+-- best to use this name in the rendered assertion, but might run into+-- collisions. You can skip using 'name' altogether. Clash will then try its+-- best to get a readable name from context.+name :: Text -> Signal dom Bool -> Assertion dom+name nm signal = Assertion IsNotTemporal (CvPure (Just nm, signal))+{-# INLINE name #-}++-- | For using a literal (either True or False) in assertions+lit :: Bool -> Assertion dom+lit = Assertion IsNotTemporal . CvLit+{-# INLINE lit #-}++-- | Truth table for 'not':+--+-- @+-- a     | not a+-- ------------+-- True  | False+-- False | True+-- @+not :: AssertionValue dom a => a -> Assertion dom+not (toAssertionValue -> a) = Assertion (isTemporal a) (CvNot (assertion a))+{-# INLINE not #-}++-- | Truth table for 'and':+--+-- @+-- a     | b     | a `and` b+-- --------------|----------+-- False | False | False+-- False | True  | False+-- True  | False | False+-- True  | True  | True+-- @+and :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom+and (toAssertionValue -> a) (toAssertionValue -> b) =+  Assertion+    (max (isTemporal a) (isTemporal b))+    (CvAnd (assertion a) (assertion b))+{-# INLINE and #-}++-- | Truth table for 'or':+--+-- @+-- a     | b     | a `or` b+-- --------------|---------+-- False | False | False+-- False | True  | True+-- True  | False | True+-- True  | True  | True+-- @+or :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom+or (toAssertionValue -> a) (toAssertionValue -> b) =+  Assertion+    (max (isTemporal a) (isTemporal b))+    (CvOr (assertion a) (assertion b))+{-# INLINE or #-}++-- |+-- Truth table for 'implies':+--+-- @+-- a     | b     | a `implies` b+-- --------------|--------------+-- False | False | True+-- False | True  | True+-- True  | False | False+-- True  | True  | True+-- @+implies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom+implies (toAssertionValue -> Assertion aTmp a) (toAssertionValue -> Assertion bTmp b) =+  Assertion (max aTmp bTmp) (CvImplies a b)+{-# INLINE implies #-}++-- | Truth table for 'next':+--+-- @+-- a[n]  | a[n+1] | a `implies` next a+-- ---------------|-------------------+-- False | False  | True+-- False | True   | True+-- True  | False  | False+-- True  | True   | True+-- @+--+-- where a[n] represents the value of @a@ at cycle @n@ and @a[n+1]@ represents+-- the value of @a@ at cycle @n+1@. Cycle n is an arbitrary cycle.+next :: AssertionValue dom a => a -> Assertion dom+next = nextN 1+{-# INLINE next #-}++-- | Truth table for 'nextN':+--+-- @+-- a[n]  | a[n+m] | a `implies` next m a+-- ---------------|---------------------+-- False | False  | True+-- False | True   | True+-- True  | False  | False+-- True  | True   | True+-- @+--+-- where a[n] represents the value of @a@ at cycle @n@ and a[n+m] represents+-- the value of @a@ at cycle @n+m@. Cycle n is an arbitrary cycle.+nextN :: AssertionValue dom a => Word -> a -> Assertion dom+nextN n = Assertion IsTemporal . CvNext n . assertion . toAssertionValue+{-# INLINE nextN #-}++-- | Same as @a && next b@ but with a nice syntax. E.g., @a && next b@ could+-- be written as @a `before` b@. Might be read as "a happens one cycle before b".+before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom+before a0 b0 = Assertion IsTemporal (CvBefore a1 b1)+ where+  a1 = assertion (toAssertionValue a0)+  b1 = assertion (toAssertionValue b0)+{-# INLINE before #-}++-- | Same as @a `implies` next b@ but with a nice syntax. E.g.,+-- @a `implies` next b@ could be written as @a `timplies` b@. Might be read+-- as "a at cycle n implies b at cycle n+1".+timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom+timplies a0 b0 = Assertion IsTemporal (CvTemporalImplies 1 a1 b1)+ where+  a1 = toTemporal (toAssertionValue a0)+  b1 = toTemporal (toAssertionValue b0)+{-# INLINE timplies #-}++-- | Same as 'implies' but strictly temporal.+timpliesOverlapping+  :: (AssertionValue dom a, AssertionValue dom b)+  => a+  -> b+  -> Assertion dom+timpliesOverlapping a0 b0 =+  Assertion IsTemporal (CvTemporalImplies 0 a1 b1)+ where+  a1 = toTemporal (toAssertionValue a0)+  b1 = toTemporal (toAssertionValue b0)+{-# INLINE timpliesOverlapping #-}++-- | Specify assertion should _always_ hold+always :: AssertionValue dom a => a -> Assertion dom+always = Assertion IsTemporal . CvAlways . assertion . toAssertionValue+{-# INLINE always #-}++-- | Specify assertion should _never_ hold+never :: AssertionValue dom a => a -> Assertion dom+never = Assertion IsTemporal . CvNever . assertion . toAssertionValue+{-# INLINE never #-}++-- | Check whether given assertion always holds. Results can be collected with+-- 'check'.+assert :: AssertionValue dom a => a -> Property dom+assert = Property . CvAssert . assertion . toAssertionValue+{-# INLINE assert #-}++-- | Check whether given assertion holds for at least a single cycle. Results+-- can be collected with 'check'.+cover :: AssertionValue dom a => a -> Property dom+cover = Property . CvCover . assertion . toAssertionValue+{-# INLINE cover #-}++-- | Print property as PSL/SVA in HDL. Clash simulation support not yet+-- implemented.+check+  :: KnownDomain dom+  => Clock dom+  -> Reset dom+  -> Text+  -- ^ Property name (used in reports and error messages)+  -> RenderAs+  -- ^ Assertion language to use in HDL+  -> Property dom+  -> Signal dom AssertionResult+check !_clk !_rst !_propName !_renderAs !_prop =+  pure (errorX (concat [+      "Simulation for Clash.Verification not yet implemented. If you need this,"+    , " create an issue at https://github.com/clash-compiler/clash-lang/issues." ]))+{-# NOINLINE check #-}+{-# ANN check (InlinePrimitive [Verilog, SystemVerilog, VHDL] "[ { \"BlackBoxHaskell\" : { \"name\" : \"Clash.Explicit.Verification.check\", \"templateFunction\" : \"Clash.Primitives.Verification.checkBBF\"}} ]") #-}++-- | Same as 'check', but doesn't require a design to explicitly carried to+-- top-level.+checkI+  :: KnownDomain dom+  => Clock dom+  -> Reset dom+  -> Text+  -- ^ Property name (used in reports and error messages)+  -> RenderAs+  -- ^ Assertion language to use in HDL+  -> Property dom+  -> Signal dom a+  -> Signal dom a+checkI clk rst propName renderAs prop =+  hideAssertion (check clk rst propName renderAs prop)++-- | Print assertions in HDL+hideAssertion :: Signal dom AssertionResult -> Signal dom a -> Signal dom a+hideAssertion = hwSeqX

@@ -3,7 +3,17 @@   License     :  BSD2 (see the file LICENSE)   Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com> -Control module instance, and register, names in generated HDL code.+Control naming and deduplication in the generated HDL code. Explicitly nameable+things include:++* Component (VHDL) / module ((System)Verilog) instances++* Registers++* Terms++Refer to "Clash.Annotations.TopEntity" for controlling naming of entities+(VHDL) / modules ((System)Verilog) and their ports. -}  module Clash.Magic@@ -15,14 +25,17 @@   , suffixNameFromNat   , suffixNameFromNatP   , setName+  , nameHint    -- ** Functions to control Clash's (de)duplication mechanisms   , deDup   , noDeDup   ) where -import Clash.NamedTypes ((:::))-import GHC.TypeLits     (Nat,Symbol)+import Clash.NamedTypes            ((:::))+import GHC.TypeLits                (Nat,Symbol)+import Clash.Promoted.Symbol       (SSymbol)+import Clash.Annotations.Primitive (hasBlackBox)  -- | Prefix instance and register names with the given 'Symbol' prefixName@@ -96,6 +109,26 @@   :: forall (name :: Symbol) a . a -> name ::: a setName = id {-# NOINLINE setName #-}++-- | Name a given term, such as one of type 'Clash.Signal.Signal', using the+-- given 'SSymbol'. Results in a declaration with the name used as the+-- identifier in the generated HDL code.+--+-- Example usage:+--+-- @+-- nameHint (SSymbol @"identifier") term+-- @+--+-- __NB__: The given name should be considered a hint as it may be expanded,+-- e.g. if it collides with existing identifiers.+nameHint+  :: SSymbol sym+  -- ^ A hint for a name+  -> a -> a+nameHint = seq+{-# NOINLINE nameHint #-}+{-# ANN nameHint hasBlackBox #-}  -- | Force deduplication, i.e. share a function or operator between multiple -- branches.

@@ -98,8 +98,6 @@     -- ** Synchronous signals   , module Clash.Signal   , module Clash.Signal.Delayed-    -- ** DataFlow interface-  , module Clash.Prelude.DataFlow     -- ** Datatypes     -- *** Bit vectors   , module Clash.Sized.BitVector@@ -132,8 +130,7 @@   , Lift (..)     -- ** Type classes     -- *** Clash-  -- , module Clash.Class.AutoReg-  , autoReg, deriveAutoReg+  , AutoReg, autoReg, deriveAutoReg   , module Clash.Class.BitPack   , module Clash.Class.Exp   , module Clash.Class.Num@@ -143,6 +140,7 @@   , module Control.Applicative   , module Data.Bits   , module Data.Default.Class+  , module Data.Kind     -- ** Exceptions   , module Clash.XException     -- ** Named types@@ -160,6 +158,7 @@ import           Control.Applicative import           Data.Bits import           Data.Default.Class+import           Data.Kind (Type, Constraint) import           GHC.Stack                   (HasCallStack) import           GHC.TypeLits import           GHC.TypeLits.Extra@@ -168,7 +167,7 @@  import           Clash.Annotations.TopEntity import           Clash.Class.AutoReg         (AutoReg, deriveAutoReg)-import           Clash.Class.BitPack+import           Clash.Class.BitPack hiding  (GBitPack(..)) import           Clash.Class.Exp import           Clash.Class.Num import           Clash.Class.Parity@@ -181,7 +180,6 @@ import           Clash.Prelude.BitReduction import           Clash.Prelude.BlockRam import           Clash.Prelude.BlockRam.File-import           Clash.Prelude.DataFlow import           Clash.Prelude.ROM.File import           Clash.Prelude.Safe #ifdef CLASH_MULTIPLE_HIDDEN@@ -197,8 +195,9 @@ import           Clash.Sized.RTree import           Clash.Sized.Signed import           Clash.Sized.Unsigned-import           Clash.Sized.Vector-import           Clash.Signal+import           Clash.Sized.Vector hiding (fromList, unsafeFromList)+import           Clash.Signal hiding+  (HiddenClockName, HiddenResetName, HiddenEnableName) import           Clash.Signal.Delayed import           Clash.Signal.Trace import           Clash.XException

@@ -84,10 +84,10 @@        , (MemAddr, Maybe (MemAddr,Value), InstrAddr)        ) cpu regbank (memOut, instr) =-  (regbank', (rdAddr, (,aluOut) '<$>' wrAddrM, fromIntegral ipntr))+  (regbank', (rdAddr, (,aluOut) 'Prelude.<$>' wrAddrM, fromIntegral ipntr))  where   -- Current instruction pointer-  ipntr = regbank '!!' PC+  ipntr = regbank 'Clash.Sized.Vector.!!' PC    -- Decoder   (MachCode {..}) = case instr of@@ -99,8 +99,8 @@     Nop                  -> nullCode    -- ALU-  regX   = regbank '!!' inputX-  regY   = regbank '!!' inputY+  regX   = regbank 'Clash.Sized.Vector.!!' inputX+  regY   = regbank 'Clash.Sized.Vector.!!' inputY   aluOut = alu aluCode regX regY    -- next instruction@@ -110,10 +110,10 @@       _                    -> ipntr + 1    -- update registers-  regbank' = 'replace' Zero   0-           $ 'replace' PC     nextPC-           $ 'replace' result aluOut-           $ 'replace' ldReg  memOut+  regbank' = 'Clash.Sized.Vector.replace' Zero   0+           $ 'Clash.Sized.Vector.replace' PC     nextPC+           $ 'Clash.Sized.Vector.replace' result aluOut+           $ 'Clash.Sized.Vector.replace' ldReg  memOut            $ regbank  alu Add   x y = x + y@@ -135,14 +135,14 @@   -> Signal dom Value   -- ^ data out dataMem rd wrM =-  'Clash.Prelude.Mealy.mealy' dataMemT ('replicate' d32 0) (bundle (rd,wrM))+  'Clash.Prelude.Mealy.mealy' dataMemT ('Clash.Sized.Vector.replicate' d32 0) (bundle (rd,wrM))  where   dataMemT mem (rd,wrM) = (mem',dout)     where-      dout = mem '!!' rd+      dout = mem 'Clash.Sized.Vector.!!' rd       mem' =         case wrM of-          Just (wr,din) -> 'replace' wr din mem+          Just (wr,din) -> 'Clash.Sized.Vector.replace' wr din mem           _             -> mem @ @@ -158,8 +158,8 @@ system instrs = memOut   where     memOut = dataMem rdAddr dout-    (rdAddr, dout, ipntr) = 'Clash.Prelude.Mealy.mealyB' cpu ('replicate' d7 0) (memOut,instr)-    instr  = 'Clash.Prelude.ROM.asyncRom' instrs '<$>' ipntr+    (rdAddr, dout, ipntr) = 'Clash.Prelude.Mealy.mealyB' cpu ('Clash.Sized.Vector.replicate' d7 0) (memOut,instr)+    instr  = 'Clash.Prelude.ROM.asyncRom' instrs 'Prelude.<$>' ipntr @  Create a simple program that calculates the GCD of 4 and 6:@@ -209,8 +209,9 @@ === Improvement 1: using @asyncRam@  As you can see, it's fairly straightforward to build a memory using registers-and read ('!!') and write ('replace') logic. This might however not result in-the most efficient hardware structure, especially when building an ASIC.+and read ('Clash.Sized.Vector.!!') and write ('Clash.Sized.Vector.replace')+logic. This might however not result in the most efficient hardware structure,+especially when building an ASIC.  Instead it is preferable to use the 'Clash.Prelude.RAM.asyncRam' function which has the potential to be translated to a more efficient structure:@@ -224,15 +225,16 @@ system2 instrs = memOut   where     memOut = 'Clash.Prelude.RAM.asyncRam' d32 rdAddr dout-    (rdAddr,dout,ipntr) = 'mealyB' cpu ('replicate' d7 0) (memOut,instr)-    instr  = 'Clash.Prelude.ROM.asyncRom' instrs '<$>' ipntr+    (rdAddr,dout,ipntr) = 'Clash.Prelude.mealyB' cpu ('Clash.Sized.Vector.replicate' d7 0) (memOut,instr)+    instr  = 'Clash.Prelude.ROM.asyncRom' instrs 'Prelude.<$>' ipntr @  Again, we can simulate our system and see that it works. This time however, we need to disregard the first few output samples, because the initial content of an-'Clash.Prelude.RAM.asyncRam' is 'undefined', and consequently, the first few-output samples are also 'undefined'. We use the utility function 'printX' to conveniently-filter out the undefinedness and replace it with the string "X" in the few leading outputs.+'Clash.Prelude.RAM.asyncRam' is 'Clash.XException.undefined', and consequently, the first few+output samples are also 'Clash.XException.undefined'. We use the utility function+'Clash.XException.printX' to conveniently filter out the undefinedness and+replace it with the string "X" in the few leading outputs.  @ >>> printX $ sampleN @System 32 (system2 prog)@@ -270,10 +272,10 @@      , (MemAddr, Maybe (MemAddr, Value), InstrAddr)      ) cpu2 (regbank,ldRegD) (memOut,instr) =-  ((regbank', ldRegD'), (rdAddr, (,aluOut) '<$>' wrAddrM, fromIntegral ipntr))+  ((regbank', ldRegD'), (rdAddr, (,aluOut) 'Prelude.<$>' wrAddrM, fromIntegral ipntr))  where   -- Current instruction pointer-  ipntr = regbank '!!' PC+  ipntr = regbank 'Clash.Sized.Vector.!!' PC    -- Decoder   (MachCode {..}) = case instr of@@ -285,8 +287,8 @@     Nop                  -> nullCode    -- ALU-  regX   = regbank '!!' inputX-  regY   = regbank '!!' inputY+  regX   = regbank 'Clash.Sized.Vector.!!' inputX+  regY   = regbank 'Clash.Sized.Vector.!!' inputY   aluOut = alu aluCode regX regY    -- next instruction@@ -297,10 +299,10 @@    -- update registers   ldRegD'  = ldReg  -- Delay the ldReg by 1 cycle-  regbank' = 'replace' Zero   0-           $ 'replace' PC     nextPC-           $ 'replace' result aluOut-           $ 'replace' ldRegD memOut+  regbank' = 'Clash.Sized.Vector.replace' Zero   0+           $ 'Clash.Sized.Vector.replace' PC     nextPC+           $ 'Clash.Sized.Vector.replace' result aluOut+           $ 'Clash.Sized.Vector.replace' ldRegD memOut            $ regbank @ @@ -315,8 +317,8 @@ system3 instrs = memOut   where     memOut = 'blockRam' (replicate d32 0) rdAddr dout-    (rdAddr,dout,ipntr) = 'mealyB' cpu2 (('replicate' d7 0),Zero) (memOut,instr)-    instr  = 'Clash.Prelude.ROM.asyncRom' instrs '<$>' ipntr+    (rdAddr,dout,ipntr) = 'Clash.Prelude.mealyB' cpu2 (('Clash.Sized.Vector.replicate' d7 0),Zero) (memOut,instr)+    instr  = 'Clash.Prelude.ROM.asyncRom' instrs 'Prelude.<$>' ipntr @  We are, however, not done. We will also need to update our program. The reason@@ -360,8 +362,8 @@  When we simulate our system we see that it works. This time again, we need to disregard the first sample, because the initial output of a-'blockRam' is 'undefined'. We use the utility function 'printX' to conveniently-filter out the undefinedness and replace it with the string "X".+'blockRam' is 'Clash.XException.undefined'. We use the utility function 'Clash.XException.printX'+to conveniently filter out the undefinedness and replace it with the string "X".  @ >>> printX $ sampleN @System 34 (system3 prog2)@@ -374,6 +376,7 @@ -}  {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE GADTs #-}  {-# LANGUAGE Safe #-}@@ -392,6 +395,8 @@   ) where +import           Prelude                 (Enum, Maybe, Eq)+ import           GHC.TypeLits            (KnownNat, type (^), type (<=)) import           GHC.Stack               (HasCallStack, withFrozenCallStack) @@ -668,7 +673,7 @@ -- | Create a blockRAM with space for @n@ elements. -- -- * __NB__: Read value is delayed by 1 cycle--- * __NB__: Initial output value is 'undefined'+-- * __NB__: Initial output value is 'Clash.XException.undefined' -- -- @ -- bram40@@ -716,9 +721,9 @@      , Enum addr      , 1 <= n )   => E.ResetStrategy r-  -- ^ Whether to clear BRAM on asserted reset ('ClearOnReset') or-  -- not ('NoClearOnReset'). Reset needs to be asserted at least /n/ cycles to-  -- clear the BRAM.+  -- ^ Whether to clear BRAM on asserted reset ('Clash.Explicit.BlockRam.ClearOnReset')+  -- or not ('Clash.Explicit.BlockRam.NoClearOnReset'). Reset needs to be+  -- asserted at least /n/ cycles to clear the BRAM.   -> SNat n   -- ^ Number of elements in BRAM   -> (Index n -> a)@@ -744,9 +749,9 @@      , Enum addr      , 1 <= n )   => E.ResetStrategy r-  -- ^ Whether to clear BRAM on asserted reset ('ClearOnReset') or-  -- not ('NoClearOnReset'). Reset needs to be asserted at least /n/ cycles to-  -- clear the BRAM.+  -- ^ Whether to clear BRAM on asserted reset ('Clash.Explicit.BlockRam.ClearOnReset')+  -- or not ('Clash.Explicit.BlockRam.NoClearOnReset'). Reset needs to be+  -- asserted at least /n/ cycles to clear the BRAM.   -> SNat n   -- ^ Number of elements in BRAM   -> a@@ -765,7 +770,7 @@ -- | Create a blockRAM with space for 2^@n@ elements -- -- * __NB__: Read value is delayed by 1 cycle--- * __NB__: Initial output value is 'undefined'+-- * __NB__: Initial output value is 'Clash.XException.undefined' -- -- @ -- bram32

@@ -18,7 +18,7 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-} {-# OPTIONS_HADDOCK show-extensions #-} -module Clash.Prelude.DataFlow+module Clash.Prelude.DataFlow {-# DEPRECATED "Module will be removed in future versions of clash-prelude in favor of clash-protocols. See: https://github.com/clash-lang/clash-protocols/." #-}   ( -- * Data types     DataFlow (..)     -- * Creating DataFlow circuits@@ -112,7 +112,7 @@           )   } --- | Dataflow circuit synchronized to the 'systemClockGen'.+-- | Dataflow circuit synchronized to the 'Clash.Signal.systemClockGen'. -- type DataFlow iEn oEn i o = DataFlow' systemClockGen iEn oEn i o  -- | Create a 'DataFlow' circuit from a circuit description with the appropriate

@@ -220,7 +220,7 @@   -- ^ Read address @rd@   -> BitVector m   -- ^ The value of the ROM at address @rd@-asyncRomFilePow2 = asyncRomFile (pow2SNat (SNat @ n))+asyncRomFilePow2 = asyncRomFile (pow2SNat (SNat @n)) {-# INLINE asyncRomFilePow2 #-}  -- | asyncROMFile primitive

@@ -66,8 +66,6 @@     -- ** Synchronous signals   , module Clash.Signal   , module Clash.Signal.Delayed-    -- ** DataFlow interface-  , module Clash.Prelude.DataFlow     -- ** Datatypes     -- *** Bit vectors   , module Clash.Sized.BitVector@@ -138,7 +136,6 @@ import           Clash.Prelude.Moore         (moore, mooreB) import           Clash.Prelude.RAM           (asyncRam,asyncRamPow2) import           Clash.Prelude.ROM           (asyncRom,asyncRomPow2,rom,romPow2)-import           Clash.Prelude.DataFlow import           Clash.Promoted.Nat import           Clash.Promoted.Nat.TH import           Clash.Promoted.Nat.Literals@@ -149,7 +146,7 @@ import           Clash.Sized.RTree import           Clash.Sized.Signed import           Clash.Sized.Unsigned-import           Clash.Sized.Vector+import           Clash.Sized.Vector hiding (fromList, unsafeFromList) import           Clash.Signal import           Clash.Signal.Delayed import           Clash.XException

@@ -33,7 +33,7 @@ import qualified Clash.Explicit.Testbench as E import           Clash.Signal   (HiddenClock, HiddenReset, HiddenClockResetEnable, Signal,-  DomainResetKind, ResetKind(Asynchronous), hideClock, hideReset, hideClockResetEnable)+  hideClock, hideReset, hideClockResetEnable) import Clash.Promoted.Nat                 (SNat) import Clash.Sized.BitVector              (BitVector) import Clash.Sized.Vector                 (Vec)@@ -153,7 +153,6 @@   :: ( KnownNat l      , Eq a      , ShowX a-     , DomainResetKind dom ~ 'Asynchronous      , HiddenClock dom      , HiddenReset dom  )   => Vec l a@@ -171,7 +170,6 @@ outputVerifierBitVector'   :: ( KnownNat l      , KnownNat n-     , DomainResetKind dom ~ 'Asynchronous      , HiddenClock dom      , HiddenReset dom  )   => Vec l (BitVector n)

@@ -89,7 +89,7 @@ >>> import Clash.Promoted.Nat.Literals (d789) -} --- | Singleton value for a type-level natural number 'n'+-- | Singleton value for a type-level natural number @n@ -- -- * "Clash.Promoted.Nat.Literals" contains a list of predefined 'SNat' literals -- * "Clash.Promoted.Nat.TH" has functions to easily create large ranges of new@@ -119,7 +119,7 @@   showsPrecX = showsPrecXWith showsPrec  {-# INLINE withSNat #-}--- | Supply a function with a singleton natural 'n' according to the context+-- | Supply a function with a singleton natural @n@ according to the context withSNat :: KnownNat n => (SNat n -> a) -> a withSNat f = f SNat @@ -347,13 +347,13 @@ -- * Append a zero (/0/): -- --      @---      __B0__ :: 'BNat' n -> 'BNat' (2 '*' n)+--      __B0__ :: 'BNat' n -> 'BNat' (2 'GHC.TypeNats.*' n) --      @ -- -- * Append a one (/1/): -- --      @---      __B1__ :: 'BNat' n -> 'BNat' ((2 '*' n) '+' 1)+--      __B1__ :: 'BNat' n -> 'BNat' ((2 'GHC.TypeNats.*' n) 'GHC.TypeNats.+' 1) --      @ data BNat :: Nat -> Type where   BT :: BNat 0@@ -509,7 +509,7 @@ -- @ -- f :: Index (n+1) -> Index (n + 1) -> Bool ----- g :: forall n. (1 '<=' n) => Index n -> Index n -> Bool+-- g :: forall n. (1 'GHC.TypeNats.<=' n) => Index n -> Index n -> Bool -- g a b = 'leToPlus' \@1 \@n (f a b) -- @ --@@ -518,7 +518,7 @@ -- @ -- head :: Vec (n + 1) a -> a ----- head' :: forall n a. (1 '<=' n) => Vec n a -> a+-- head' :: forall n a. (1 'GHC.TypeNats.<=' n) => Vec n a -> a -- head' = 'leToPlus' @1 @n head -- @ leToPlus

@@ -3,7 +3,7 @@ License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> -Predefined 'SNat' singleton literals in the range [0 .. 1024]+Predefined 'Clash.Promoted.Nat.SNat' singleton literals in the range [0 .. 1024]  Defines: @@ -15,7 +15,8 @@ d1024 = SNat :: SNat 1024 @ -You can generate more 'SNat' literals using 'decLiteralsD' from "Clash.Promoted.Nat.TH"+You can generate more 'Clash.Promoted.Nat.SNat' literals using 'decLiteralsD'+from "Clash.Promoted.Nat.TH" -}  {-# LANGUAGE CPP #-}

@@ -30,7 +30,9 @@     where       tt = LitT (StrTyLit (ssymbolToString t)) -#if MIN_VERSION_template_haskell(2,16,0)+#if MIN_VERSION_template_haskell(2,17,0)+  liftTyped = unsafeCodeCoerce . lift+#elif MIN_VERSION_template_haskell(2,16,0)   liftTyped = unsafeTExpCoerce . lift #endif 

@@ -24,16 +24,16 @@ 'DomainConfiguration'   { _name :: 'Domain'   -- ^ Domain name-  , _period :: 'Nat'+  , _period :: 'Clash.Promoted.Nat.Nat'   -- ^ Clock period in /ps/-  , _edge :: 'ActiveEdge'+  , _activeEdge :: 'ActiveEdge'   -- ^ Active edge of the clock-  , _reset :: 'ResetKind'+  , _resetKind :: 'ResetKind'   -- ^ Whether resets are synchronous (edge-sensitive) or asynchronous (level-sensitive)-  , _init :: 'InitBehavior'+  , _initBehavior :: 'InitBehavior'   -- ^ Whether the initial (or "power up") value of memory elements is   -- unknown/undefined, or configurable to a specific value-  , _polarity :: ResetPolarity+  , _resetPolarity :: ResetPolarity   -- ^ Whether resets are active high or active low   } @@@ -49,7 +49,7 @@   knownDomain = SDomainConfiguration SSymbol SNat SRising SAsynchronous SDefined SActiveHigh @ -In words, "System" is a synthesis domain with a clock running with a period+In words, \"System\" is a synthesis domain with a clock running with a period of 10000 /ps/. Memory elements respond to the rising edge of the clock, asynchronously to changes in their resets, and have defined power up values if applicable.@@ -90,6 +90,7 @@   , BiSignalDefault(..)     -- * Domain   , Domain+  , sameDomain   , KnownDomain(..)   , KnownConfiguration   , ActiveEdge(..)@@ -145,6 +146,7 @@   , convertReset #endif   , resetSynchronizer+  , resetGlitchFilter   , holdReset     -- ** Enabling   , Enable@@ -224,6 +226,8 @@     -- ** lazy versions   , simulate_lazy   , simulateB_lazy+    -- ** Automaton+  , signalAutomaton     -- * List \<-\> Signal conversion (not synthesizable)   , sample   , sampleN@@ -247,8 +251,15 @@   , readFromBiSignal   , writeToBiSignal   , mergeBiSignalOuts++    -- * Internals+  , HiddenClockName+  , HiddenResetName+  , HiddenEnableName   ) where++import           Control.Arrow.Transformer.Automaton (Automaton) import           GHC.TypeLits          (type (<=)) import           Data.Proxy            (Proxy(..)) import           Prelude@@ -262,8 +273,9 @@  import           Clash.Class.HasDomain (WithSpecificDomain) import qualified Clash.Explicit.Signal as E-import           Clash.Explicit.Signal-  (resetSynchronizer, systemClockGen, systemResetGen)+import qualified Clash.Explicit.Reset  as E+import           Clash.Explicit.Reset  (resetSynchronizer, resetGlitchFilter)+import           Clash.Explicit.Signal (systemClockGen, systemResetGen) import qualified Clash.Explicit.Signal as S import           Clash.Hidden import           Clash.Promoted.Nat    (SNat (..), snatToNum)@@ -271,7 +283,8 @@   (Bundle (..), EmptyTuple(..), TaggedEmptyTuple(..)) import           Clash.Signal.BiSignal --(BisignalIn, BisignalOut, ) import           Clash.Signal.Internal hiding-  (sample, sample_lazy, sampleN, sampleN_lazy, simulate, simulate_lazy, testFor)+  (sample, sample_lazy, sampleN, sampleN_lazy, simulate, simulate_lazy, testFor,+   signalAutomaton) import           Clash.Signal.Internal.Ambiguous   (knownVDomain, clockPeriod, activeEdge, resetKind, initBehavior, resetPolarity) import           Clash.XException      (NFDataX)@@ -301,7 +314,7 @@  -} --- * Hidden clock and reset arguments+-- * Hidden clock, reset, and enable arguments  {- $hiddenclockandreset #hiddenclockandreset# Clocks and resets are by default implicitly routed to their components. You can@@ -319,7 +332,7 @@ Or it has a hidden reset when it has a:  @-g :: 'HiddenReset' dom polarity => ...+g :: 'HiddenReset' dom => ... @  Constraint.@@ -328,30 +341,30 @@ has a:  @-h :: 'HiddenClockReset' dom  => ..+h :: 'HiddenClockResetEnable' dom  => .. @  Constraint.  Given a component with an explicit clock and reset arguments, you can turn them-into hidden arguments using 'hideClock' and 'hideReset'. So given a:+into hidden arguments using 'hideClock', 'hideReset', and 'hideEnable'. So given a:  @-f :: Clock dom -> Reset dom -> Signal dom a -> ...+f :: Clock dom -> Reset dom -> Enable dom -> Signal dom a -> ... @  You hide the clock and reset arguments by:  @--- g :: 'HiddenClockReset' dom  => Signal dom a -> ...-g = 'hideClockReset' f+-- g :: 'HiddenClockResetEnable' dom  => Signal dom a -> ...+g = 'hideClockResetEnable' f @  Or, alternatively, by:  @--- h :: HiddenClockResetEnable dom  => Signal dom a -> ...-h = f 'hasClock' 'hasReset'+-- h :: 'HiddenClockResetEnable' dom  => Signal dom a -> ...+h = f 'hasClock' 'hasReset' 'hasEnable' @  === Assigning explicit clock and reset arguments to hidden clocks and resets@@ -359,7 +372,7 @@ Given a component:  @-f :: HiddenClockResetEnable dom+f :: 'HiddenClockResetEnable' dom   => Signal dom Int   -> Signal dom Int @@@ -387,29 +400,34 @@  @ topEntity-  :: Clock System-  -> Reset System-  -> Enable System-  -> Signal System Int-  -> Signal System Int-topEntity clk rst =-  let (pllOut,pllStable) = 'Clash.Intel.ClockGen.altpll' (SSymbol \@\"altpll50\") clk rst-      rstSync            = 'resetSynchronizer' pllOut ('unsafeToAsyncReset' pllStable)-  in  'exposeClockResetEnable' f pllOut rstSync+  :: Clock  System+  -> Reset  System+  -> Signal System Bit+  -> Signal System (BitVector 8)+topEntity clk rst ena key1 =+    let  (pllOut,pllStable) = altpll (SSymbol \@\"altpll50\") clk rst+         rstSync            = 'resetSynchronizer' pllOut (unsafeToHighPolarity pllStable) ena+    in   exposeClockResetEnable leds pllOut rstSync enableGen+  where+    key1R  = isRising 1 key1+    leds   = mealy blinkerT (1, False, 0) key1R @  or, using the alternative method:  @-topEntity2-  :: Clock System-  -> Reset System-  -> Signal System Int-  -> Signal System Int-topEntity2 clk rst =-  let (pllOut,pllStable) = 'Clash.Intel.ClockGen.altpll' (SSymbol \@\"altpll50\") clk rst-      rstSync            = 'resetSynchronizer' pllOut ('unsafeToAsyncReset' pllStable)-  in  'withClockReset' pllOut rstSync f+topEntity+  :: Clock  System+  -> Reset  System+  -> Signal System Bit+  -> Signal System (BitVector 8)+topEntity clk rst ena key1 =+    let  (pllOut,pllStable) = altpll (SSymbol \@\"altpll50\") clk rst+         rstSync            = 'resetSynchronizer' pllOut (unsafeToHighPolarity pllStable) ena+    in   'withClockResetEnable' pllOut rstSync enableGen leds+  where+    key1R  = isRising 1 key1+    leds   = mealy blinkerT (1, False, 0) key1R @  -}@@ -1402,7 +1420,7 @@ -- -- countSometimes = s where --   s     = 'regMaybe' 0 (plusM ('pure' '<$>' s) sometimes1)---   plusM = 'liftA2' (liftA2 (+))+--   plusM = 'Control.Applicative.liftA2' (liftA2 (+)) -- @ -- -- We get:@@ -1881,3 +1899,18 @@ convertReset =   E.convertReset hasClock hasClock #endif++-- | Build an 'Automaton' from a function over 'Signal's.+--+-- __NB__: Consumption of continuation of the 'Automaton' must be affine; that+-- is, you can only apply the continuation associated with a particular element+-- at most once.+signalAutomaton+  :: forall dom a b+   . KnownDomain dom+  => (HiddenClockResetEnable dom => Signal dom a -> Signal dom b)+  -> Automaton (->) a b+signalAutomaton f0 =+  let f1 = exposeClockResetEnable @dom f0 clockGen resetGen enableGen in+  E.signalAutomaton f1+{-# NOINLINE signalAutomaton #-}

@@ -9,7 +9,7 @@ /inout/, thereby making this port function as both a source and a drain for the signals flowing over the wire. -Clash has support for 'inout' ports through the implementation of /BiSignal/s.+Clash has support for @inout@ ports through the implementation of /BiSignal/s. To cleanly map to functions (and thus support software simulation using Haskell), a /BiSignal/ comes in two parts; the __in__ part: @@ -32,7 +32,7 @@   * Lastly, /ds/ indicates the default behavior for the BiSignal if nothing is     being written (pull-down, pull-up, or undefined). -'BiSignalIn' is used by Clash to generate the 'inout' ports on a HDL level,+'BiSignalIn' is used by Clash to generate the @inout@ ports on a HDL level, while 'BiSignalOut' is only used for simulation purposes and generally discarded by the compiler. @@ -95,6 +95,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -110,6 +111,8 @@     BiSignalIn()   , BiSignalOut()   , BiSignalDefault(..)+  , SBiSignalDefault(..)+  , HasBiSignalDefault(..)   , mergeBiSignalOuts   , readFromBiSignal   , writeToBiSignal@@ -132,7 +135,7 @@ import           GHC.Stack                  (HasCallStack) import           Data.Reflection            (Given (..)) --- | Used to specify the /default/ behavior of a 'BiSignal', i.e. what value is+-- | Used to specify the /default/ behavior of a \"BiSignal\", i.e. what value is -- read when no value is being written to it. data BiSignalDefault   = PullUp@@ -141,7 +144,7 @@   -- ^ __inout__ port behaves as if connected to a pull-down resistor   | Floating   -- ^ __inout__ port behaves as if is /floating/. Reading a /floating/-  -- 'BiSignal' value in simulation will yield an errorX (undefined value).+  -- \"BiSignal\" value in simulation will yield an errorX (undefined value).   deriving (Show)  -- | Singleton versions of 'BiSignalDefault'@@ -159,20 +162,61 @@ instance Given (SBiSignalDefault 'Floating) where   given = SFloating --- | The /in/ part of an __inout__ port+-- | Type class for 'BiSignalDefault':+--   can be used as a constraint and for obtaining the pull-up mode+class HasBiSignalDefault (ds :: BiSignalDefault) where+  pullUpMode :: BiSignalIn ds dom n -> SBiSignalDefault ds++instance HasBiSignalDefault 'PullUp where+  pullUpMode _ = SPullUp++instance HasBiSignalDefault 'PullDown where+  pullUpMode _ = SPullDown++instance HasBiSignalDefault 'Floating where+  pullUpMode _ = SFloating++type role BiSignalIn nominal nominal nominal++-- | The /in/ part of an __inout__ port.+-- BiSignalIn has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i BiSignalIn+-- type role BiSignalIn nominal nominal nominal+-- ...+--+-- as it is not safe to coerce the default behaviour, synthesis domain or width+-- of the data in the signal. data BiSignalIn (ds :: BiSignalDefault) (dom :: Domain) (n :: Nat)   = BiSignalIn (SBiSignalDefault ds) (Signal dom (Maybe (BitVector n))) +type role BiSignalOut nominal nominal nominal+ -- | The /out/ part of an __inout__ port -- -- Wraps (multiple) writing signals. The semantics are such that only one of -- the signals may write at a single time step.+--+-- BiSignalOut has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i BiSignalOut+-- type role BiSignalOut nominal nominal nominal+-- ...+--+-- as it is not safe to coerce the default behaviour, synthesis domain or width+-- of the data in the signal.+#if MIN_VERSION_base(4,15,0)+data BiSignalOut (ds :: BiSignalDefault) (dom :: Domain) (n :: Nat)+  = BiSignalOut ![Signal dom (Maybe (BitVector n))]+#else newtype BiSignalOut (ds :: BiSignalDefault) (dom :: Domain) (n :: Nat)   = BiSignalOut [Signal dom (Maybe (BitVector n))]+#endif  type instance HasDomain dom1 (BiSignalOut ds dom2 n) = DomEq dom1 dom2 type instance TryDomain t (BiSignalOut ds dom n) = 'Found dom +-- | __NB__ Not synthesizable instance Semigroup (BiSignalOut defaultState dom n) where   (BiSignalOut b1) <> (BiSignalOut b2) = BiSignalOut (b1 ++ b2) @@ -253,7 +297,7 @@     (pack . fromJustX <$> writes) {-# INLINE writeToBiSignal #-} --- | Converts the 'out' part of a BiSignal to an 'in' part. In simulation it+-- | Converts the @out@ part of a BiSignal to an @in@ part. In simulation it -- checks whether multiple components are writing and will error accordingly. -- Make sure this is only called ONCE for every BiSignal. veryUnsafeToBiSignalIn

@@ -78,6 +78,7 @@ -- @ -- -- For custom product types you'll have to write the instance manually:+-- -- @ -- data Pair a b = MkPair { getA :: a, getB :: b } --@@ -171,35 +172,39 @@     getL (l :*: _) = l     getR (_ :*: r) = r --- | See "TaggedEmptyTuple"+-- | See 'TaggedEmptyTuple' data EmptyTuple = EmptyTuple  -- | Helper type to emulate the "old" behavior of Bundle's unit instance. I.e., -- the instance for @Bundle ()@ used to be defined as: -----     class Bundle () where---       bundle   :: () -> Signal domain ()---       unbundle :: Signal domain () -> ()+-- @+-- class Bundle () where+--   bundle   :: () -> Signal dom ()+--   unbundle :: Signal dom () -> ()+-- @ ----- In order to have sensible type inference, the "Bundle" class specifies that+-- In order to have sensible type inference, the 'Bundle' class specifies that -- the argument type of 'bundle' should uniquely identify the result type, and -- vice versa for 'unbundle'. The type signatures in the snippet above don't -- though, as @()@ doesn't uniquely map to a specific domain. In other words,--- 'domain' should occur in both the argument and result of both functions.+-- @domain@ should occur in both the argument and result of both functions. ----- "TaggedEmptyTuple" tackles this by carrying the domain in its type. The+-- 'TaggedEmptyTuple' tackles this by carrying the domain in its type. The -- 'bundle' and 'unbundle' instance now looks like: -----     class Bundle EmptyTuple where---       bundle   :: TaggedEmptyTuple domain -> Signal domain EmptyTuple---       unbundle :: Signal domain EmptyTuple -> TaggedEmptyTuple domain+-- @+-- class Bundle EmptyTuple where+--   bundle   :: TaggedEmptyTuple dom -> Signal dom EmptyTuple+--   unbundle :: Signal dom EmptyTuple -> TaggedEmptyTuple dom+-- @ ----- @domain@ is now mentioned both the argument and result for both 'bundle' and+-- @dom@ is now mentioned both the argument and result for both 'bundle' and -- 'unbundle'. data TaggedEmptyTuple (dom :: Domain) = TaggedEmptyTuple --- | See https://github.com/clash-lang/clash-compiler/pull/539/commits/94b0bff5770aa4961e04ddce2515130df3fc7863--- and documentation for "TaggedEmptyTuple".+-- | See [commit 94b0bff5](https://github.com/clash-lang/clash-compiler/pull/539/commits/94b0bff5770aa4961e04ddce2515130df3fc7863)+-- and documentation for 'TaggedEmptyTuple'. instance Bundle EmptyTuple where   type Unbundled dom EmptyTuple = TaggedEmptyTuple dom 

@@ -48,7 +48,7 @@   (DSignal(..), dfromList, dfromList_lazy, fromSignal, toSignal,    unsafeFromSignal, antiDelay, feedback) import qualified Clash.Explicit.Signal.Delayed as E-import           Clash.Sized.Vector            (Vec)+import           Clash.Sized.Vector import           Clash.Signal   (HiddenClock, HiddenClockResetEnable, HiddenEnable, hideClock,    hideClockResetEnable, hideEnable)@@ -164,6 +164,7 @@ -- [-1,-1,1,2,3,4] -- -- You can also use type application to do the same:+-- -- >>> sampleN @System 6 (toSignal (delayI @2 (-1) (dfromList [1..]))) -- [-1,-1,1,2,3,4] delayI

@@ -78,7 +78,7 @@   -- | Example:   --   -- @-  -- __bundle__ :: ('DSignal' dom d a, 'DSignal' dom d b) -> 'DSignal' clk d (a,b)+  -- __bundle__ :: ('DSignal' dom d a, 'DSignal' dom d b) -> 'DSignal' dom d (a,b)   -- @   --   -- However:@@ -220,11 +220,11 @@   bundle   = sequenceA   unbundle = sequenceA . fmap lazyT --- | Same as "Clash.Signal.Bundle.TaggedEmptyTuple", but adapted for "DSignal".+-- | Same as 'Clash.Signal.Bundle.TaggedEmptyTuple' in "Clash.Signal.Bundle", but adapted for 'DSignal'. data TaggedEmptyTuple (dom :: Domain) (d :: Nat) = TaggedEmptyTuple --- | See https://github.com/clash-lang/clash-compiler/pull/539/commits/94b0bff5770aa4961e04ddce2515130df3fc7863--- and documentation for "TaggedEmptyTuple".+-- | See [commit 94b0bff5](https://github.com/clash-lang/clash-compiler/pull/539/commits/94b0bff5770aa4961e04ddce2515130df3fc7863)+-- and documentation for 'Clash.Signal.Bundle.TaggedEmptyTuple'. instance Bundle B.EmptyTuple where   type Unbundled dom d B.EmptyTuple = TaggedEmptyTuple dom d 

@@ -7,6 +7,7 @@ -} {-# LANGUAGE CPP #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-}@@ -71,9 +72,19 @@  -- | A synchronized signal with samples of type @a@, synchronized to clock -- @clk@, that has accumulated @delay@ amount of samples delay along its path.+--+-- DSignal has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i DSignal+-- type role DSignal nominal nominal representational+-- ...+--+-- as it is safe to coerce the values in the signal, but not safe to coerce the+-- synthesis domain or delay in the signal.+type role DSignal nominal nominal representational newtype DSignal (dom :: Domain) (delay :: Nat) a =     DSignal { toSignal :: Signal dom a-              -- ^ Strip a 'DSignal' from its delay information.+              -- ^ Strip a 'DSignal' of its delay information.             }   deriving ( Show, Default, Functor, Applicative, Num, Fractional            , Foldable, Traversable, Arbitrary, CoArbitrary, Lift )@@ -112,7 +123,7 @@ --     mac' :: 'DSignal' dom 0 Int -> 'DSignal' dom 0 Int -> 'DSignal' dom 0 Int --          -> ('DSignal' dom 0 Int, 'DSignal' dom 1 Int) --     mac' a b acc = let acc' = a * b + acc---                    in  (acc, 'delay' clk rst en ('singleton' 0) acc')+--                    in  (acc, 'Clash.Explicit.Signal.Delayed.delayedI' clk rst en 0 acc') -- @ -- -- >>> sampleN 7 (mac systemClockGen systemResetGen enableGen (dfromList [0..]) (dfromList [0..]))@@ -130,7 +141,7 @@  -- | __EXPERIMENTAL__ ----- __Unsafely__ convert a 'Signal' to /any/ 'DSignal' clk'.+-- __Unsafely__ convert a 'Signal' to a 'DSignal' with an arbitrary @delay@. -- -- __NB__: Should only be used to interface with functions specified in terms of -- 'Signal'.@@ -147,7 +158,7 @@ -- mac clk rst en x y = acc' --   where --     acc' = (x * y) + 'antiDelay' d1 acc---     acc  = 'delay' clk rst en ('singleton' 0) acc'+--     acc  = 'Clash.Explicit.Signal.Delayed.delayedI' clk rst en 0 acc' -- @ antiDelay :: SNat d -> DSignal dom (n + d) a -> DSignal dom n a antiDelay _ = coerce

@@ -12,6 +12,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-}@@ -39,6 +40,7 @@   , tail#     -- * Domains   , Domain+  , sameDomain   , KnownDomain(..)   , KnownConfiguration   , knownDomainByName@@ -58,6 +60,12 @@   , DomainResetKind   , DomainInitBehavior   , DomainResetPolarity++  , DomainConfigurationPeriod+  , DomainConfigurationActiveEdge+  , DomainConfigurationResetKind+  , DomainConfigurationInitBehavior+  , DomainConfigurationResetPolarity     -- ** Default domains   , System   , XilinxSystem@@ -91,6 +99,9 @@     -- * Basic circuits   , delay#   , register#+  , asyncRegister#+  , syncRegister#+  , registerPowerup#   , mux     -- * Simulation and testbench functions   , clockGen@@ -102,6 +113,8 @@   , simulate     -- ** lazy version   , simulate_lazy+    -- ** Automaton+  , signalAutomaton     -- * List \<-\> Signal conversion (not synthesizable)   , sample   , sampleN@@ -131,23 +144,28 @@   ) where +import Data.IORef                 (IORef, atomicModifyIORef, newIORef, readIORef) import Type.Reflection            (Typeable)+import Control.Arrow.Transformer.Automaton import Control.Applicative        (liftA2, liftA3) import Control.DeepSeq            (NFData)-import Clash.Annotations.Primitive (hasBlackBox)+import Clash.Annotations.Primitive (hasBlackBox, dontTranslate) import Data.Binary                (Binary) import Data.Char                  (isAsciiUpper, isAlphaNum, isAscii)-import Data.Coerce                (coerce) import Data.Data                  (Data) import Data.Default.Class         (Default (..)) import Data.Hashable              (Hashable)+import Data.Maybe                 (isJust) import Data.Proxy                 (Proxy(..))+import Data.Ratio                 (Ratio)+import Data.Type.Equality         ((:~:)) import GHC.Generics               (Generic) import GHC.Stack                  (HasCallStack)-import GHC.TypeLits               (KnownSymbol, Nat, Symbol, type (<=))+import GHC.TypeLits               (KnownSymbol, Nat, Symbol, type (<=), sameSymbol) import Language.Haskell.TH.Syntax -- (Lift (..), Q, Dec) import Language.Haskell.TH.Compat import Numeric.Natural            (Natural)+import System.IO.Unsafe           (unsafeInterleaveIO, unsafePerformIO) import Test.QuickCheck            (Arbitrary (..), CoArbitrary(..), Property,                                    property) @@ -185,7 +203,7 @@   -- ^ Elements are sensitive to the rising edge (low-to-high) of the clock.   | Falling   -- ^ Elements are sensitive to the falling edge (high-to-low) of the clock.-  deriving (Show, Eq, Ord, Generic, NFData, Data, Hashable, Binary)+  deriving (Show, Read, Eq, Ord, Generic, NFData, Data, Hashable, Binary)  -- | Singleton version of 'ActiveEdge' data SActiveEdge (edge :: ActiveEdge) where@@ -205,7 +223,7 @@   -- ^ Elements respond /synchronously/ to changes in their reset input. This   -- means that changes in their reset input won't take effect until the next   -- active clock edge. Common on Xilinx FPGA platforms.-  deriving (Show, Eq, Ord, Generic, NFData, Data, Hashable)+  deriving (Show, Read, Eq, Ord, Generic, NFData, Data, Hashable)  -- | Singleton version of 'ResetKind' data SResetKind (resetKind :: ResetKind) where@@ -225,7 +243,7 @@   -- ^ Reset is considered active if underlying signal is 'True'.   | ActiveLow   -- ^ Reset is considered active if underlying signal is 'False'.-  deriving (Eq, Ord, Show, Generic, NFData, Data, Hashable)+  deriving (Eq, Ord, Show, Read, Generic, NFData, Data, Hashable)  -- | Singleton version of 'ResetPolarity' data SResetPolarity (polarity :: ResetPolarity) where@@ -244,8 +262,9 @@   -- ^ Power up value of memory elements is /unknown/.   | Defined   -- ^ If applicable, power up value of a memory element is defined. Applies to-  -- 'register's for example, but not to 'blockRam'.-  deriving (Show, Eq, Ord, Generic, NFData, Data, Hashable)+  -- 'Clash.Signal.register's for example, but not to+  -- 'Clash.Prelude.BlockRam.blockRam'.+  deriving (Show, Read, Eq, Ord, Generic, NFData, Data, Hashable)  data SInitBehavior (init :: InitBehavior) where   SUnknown :: SInitBehavior 'Unknown@@ -323,7 +342,7 @@ -- domain. Example usage: -- -- @--- myFunc :: (KnownDomain dom, DomainResetKind dom ~ 'Asynchronous) => ...+-- myFunc :: (KnownDomain dom, DomainResetKind dom ~ 'Synchronous) => ... -- @ type DomainResetKind (dom :: Domain) =   DomainConfigurationResetKind (KnownConf dom)@@ -465,7 +484,7 @@ -- -- > createDomain (knownVDomain @System){vName="System10", vPeriod=10} ----- This duplicates the settings in the "System" domain, replaces the name and+-- This duplicates the settings in the 'System' domain, replaces the name and -- period, and creates an instance for it. As most users often want to update -- the system domain, a shortcut is available in the form: --@@ -478,14 +497,15 @@   , vPeriod :: Natural   -- ^ Corresponds to '_period' on 'DomainConfiguration'   , vActiveEdge :: ActiveEdge-  -- ^ Corresponds to '_edge' on 'DomainConfiguration'+  -- ^ Corresponds to '_activeEdge' on 'DomainConfiguration'   , vResetKind :: ResetKind-  -- ^ Corresponds to '_reset' on 'DomainConfiguration'+  -- ^ Corresponds to '_resetKind' on 'DomainConfiguration'   , vInitBehavior :: InitBehavior-  -- ^ Corresponds to '_init' on 'DomainConfiguration'+  -- ^ Corresponds to '_initBehavior' on 'DomainConfiguration'   , vResetPolarity :: ResetPolarity-  -- ^ Corresponds to '_polarity' on 'DomainConfiguration'+  -- ^ Corresponds to '_resetPolarity' on 'DomainConfiguration'   }+  deriving (Eq, Show, Read)  -- | Convert 'SDomainConfiguration' to 'VDomainConfiguration'. Should be used in combination with -- 'createDomain' only.@@ -524,6 +544,16 @@ -- -- > vSystem10 = knownVDomain @System10 --+-- It will also make @System10@ an instance of 'KnownDomain'.+--+-- If either identifier is already in scope it will not be generated a second time.+-- Note: This can be useful for example when documenting a new domain:+--+-- > -- | Here is some documentation for CustomDomain+-- > type CustomDomain = ("CustomDomain" :: Domain)+-- >+-- > -- | Here is some documentation for vCustomDomain+-- > createDomain vSystem{vName="CustomDomain"} createDomain :: VDomainConfiguration -> Q [Dec] createDomain (VDomainConfiguration name period edge reset init_ polarity) =   if isValidDomainName name then do@@ -536,16 +566,28 @@         kcImpl = mkTySynInstD ''KnownConf [LitT (StrTyLit name)] kcType         vName' = mkName ('v':name) -    pure  [ -- KnownDomain instance (ex: instance KnownDomain "System" where ...)-            InstanceD Nothing [] kdType [kcImpl, kdImpl]+    tySynExists <- isJust <$> lookupTypeName name+    vHelperExists <- isJust <$> lookupValueName ('v':name) -            -- Type synonym (ex: type System = "System")-          , TySynD (mkName name) [] (LitT (StrTyLit name)  `SigT`  ConT ''Domain)+    pure $ concat+      [+        [ -- Type synonym (ex: type System = "System")+          TySynD (mkName name) [] (LitT (StrTyLit name)  `SigT`  ConT ''Domain)+        | not tySynExists+        ] -            -- vDomain helper (ex: vSystem = vDomain (knownDomain @System))-          , SigD vName' (ConT ''VDomainConfiguration)+      , concat+        [ -- vDomain helper (ex: vSystem = vDomain (knownDomain @System))+          [ SigD vName' (ConT ''VDomainConfiguration)           , FunD vName' [Clause [] (NormalB vNameImpl) []]           ]+        | not vHelperExists+        ]+      , [ -- KnownDomain instance (ex: instance KnownDomain "System" where ...)+          InstanceD Nothing [] kdType [kcImpl, kdImpl]+        ]+      ]+   else     error ("Domain names should be a valid Haskell type name, not: " ++ name)  where@@ -604,6 +646,14 @@  type Domain = Symbol +-- | We either get evidence that this function was instantiated with the same+-- domains, or Nothing.+sameDomain+  :: forall (domA :: Domain) (domB :: Domain)+   . (KnownDomain domA, KnownDomain domB)+  => Maybe (domA :~: domB)+sameDomain = sameSymbol (Proxy @domA) (Proxy @domB)+ infixr 5 :- {- | Clash has synchronous 'Signal's in the form of: @@ -628,9 +678,19 @@ * __NB__: Whether 'System' has good defaults depends on your target platform. Check out 'IntelSystem' and 'XilinxSystem' too! +Signals have the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>++>>> :i Signal+type role Signal nominal representational+...++as it is safe to coerce the underlying value of a signal, but not safe to coerce+a signal between different synthesis domains.+ See the module documentation of "Clash.Signal" for more information about domains. -}+type role Signal nominal representational data Signal (dom :: Domain) a   -- | The constructor, @(':-')@, is __not__ synthesizable.   = a :- Signal dom a@@ -712,7 +772,7 @@ -- | __WARNING: EXTREMELY EXPERIMENTAL__ -- -- The circuit semantics of this operation are unclear and/or non-existent.--- There is a good reason there is no 'Monad' instance for 'Signal''.+-- There is a good reason there is no 'Monad' instance for 'Signal'. -- -- Is currently treated as 'id' by the Clash compiler. joinSignal# :: Signal dom (Signal dom a) -> Signal dom a@@ -762,17 +822,17 @@ -- | A signal of booleans, indicating whether a component is enabled. No special -- meaning is implied, it's up to the component itself to decide how to respond -- to its enable line. It is used throughout Clash as a global enable signal.-newtype Enable dom = Enable (Signal dom Bool)+data Enable dom = Enable (Signal dom Bool)  -- | Convert 'Enable' construct to its underlying representation: a signal of -- bools. fromEnable :: Enable dom -> Signal dom Bool-fromEnable = coerce+fromEnable (Enable x) = x {-# INLINE fromEnable #-}  -- | Convert a signal of bools to an 'Enable' construct toEnable :: Signal dom Bool -> Enable dom-toEnable = coerce+toEnable = Enable {-# INLINE toEnable #-}  -- | Enable generator for some domain. Is simply always True.@@ -792,7 +852,7 @@ clockTag (Clock dom) = dom  -- | Clock generator for simulations. Do __not__ use this clock generator for--- for the /testBench/ function, use 'tbClockGen' instead.+-- for the /testBench/ function, use 'Clash.Explicit.Testbench.tbClockGen' instead. -- -- To be used like: --@@ -818,7 +878,7 @@ -- rstSystem = resetGen @System -- @ ----- See 'tbClockGen' for example usage.+-- See 'Clash.Explicit.Testbench.tbClockGen' for example usage. -- resetGen   :: forall dom@@ -1074,47 +1134,89 @@   -- ^ Reset value   -> Signal dom a   -> Signal dom a-register# (Clock dom) rst (fromEnable -> ena) powerUpVal0 resetVal =+register# clk@(Clock dom) rst ena powerUpVal resetVal =   case knownDomainByName dom of     SDomainConfiguration _name _period _edge SSynchronous _init _polarity ->-      goSync powerUpVal1 (unsafeToHighPolarity rst) ena+      syncRegister# clk rst ena powerUpVal resetVal     SDomainConfiguration _name _period _edge SAsynchronous _init _polarity ->-      goAsync powerUpVal1 (unsafeToHighPolarity rst) ena- where-  powerUpVal1 :: a-  powerUpVal1 =-    case knownDomainByName dom of-      SDomainConfiguration _dom _period _edge _sync SDefined _polarity ->-        powerUpVal0-      SDomainConfiguration _dom _period _edge _sync SUnknown _polarity ->-        deepErrorX ("First value of register undefined on domain " ++ show dom)+      asyncRegister# clk rst ena powerUpVal resetVal+{-# NOINLINE register# #-}+{-# ANN register# hasBlackBox #-} -  goSync-    :: a-    -> Signal dom Bool-    -> Signal dom Bool-    -> Signal dom a-    -> Signal dom a-  goSync o rt@(~(r :- rs)) enas@(~(e :- es)) as@(~(x :- xs)) =-    let oE = if e then x else o-        oR = if r then resetVal else oE-        -- [Note: register strictness annotations]-    in  o `defaultSeqX` o :- (rt `seq` enas `seq` as `seq` goSync oR rs es xs)+-- | Acts like 'id' if given domain allows powerup values, but returns a+-- value constructed with 'deepErrorX' otherwise.+registerPowerup#+  :: forall dom a+   . ( KnownDomain dom+     , NFDataX a+     , HasCallStack )+  => Clock dom+  -> a+  -> a+registerPowerup# (Clock dom) a =+  case knownDomainByName dom of+    SDomainConfiguration _dom _period _edge _sync SDefined _polarity -> a+    SDomainConfiguration _dom _period _edge _sync SUnknown _polarity ->+      deepErrorX ("First value of register undefined on domain " ++ show dom) -  goAsync-    :: a-    -> Signal dom Bool-    -> Signal dom Bool-    -> Signal dom a-    -> Signal dom a-  goAsync o (r :- rs) enas@(~(e :- es)) as@(~(x :- xs)) =+-- | Version of 'register#' that simulates a register on an asynchronous+-- domain. Is synthesizable.+asyncRegister#+  :: forall dom  a+   . ( KnownDomain dom+     , NFDataX a )+  => Clock dom+  -- ^ Clock signal+  -> Reset dom+  -- ^ Reset signal+  -> Enable dom+  -- ^ Enable signal+  -> a+  -- ^ Power up value+  -> a+  -- ^ Reset value+  -> Signal dom a+  -> Signal dom a+asyncRegister# clk (unsafeToHighPolarity -> rst) (fromEnable -> ena) initVal resetVal =+  go (registerPowerup# clk initVal) rst ena+ where+  go o (r :- rs) enas@(~(e :- es)) as@(~(x :- xs)) =     let oR = if r then resetVal else o         oE = if r then resetVal else (if e then x else o)         -- [Note: register strictness annotations]-    in  oR `defaultSeqX` oR :- (as `seq` enas `seq` goAsync oE rs es xs)-{-# NOINLINE register# #-}-{-# ANN register# hasBlackBox #-}+    in  o `defaultSeqX` oR :- (as `seq` enas `seq` go oE rs es xs)+{-# NOINLINE asyncRegister# #-}+{-# ANN asyncRegister# hasBlackBox #-} +-- | Version of 'register#' that simulates a register on a synchronous+-- domain. Not synthesizable.+syncRegister#+  :: forall dom  a+   . ( KnownDomain dom+     , NFDataX a )+  => Clock dom+  -- ^ Clock signal+  -> Reset dom+  -- ^ Reset signal+  -> Enable dom+  -- ^ Enable signal+  -> a+  -- ^ Power up value+  -> a+  -- ^ Reset value+  -> Signal dom a+  -> Signal dom a+syncRegister# clk (unsafeToHighPolarity -> rst) (fromEnable -> ena) initVal resetVal =+  go (registerPowerup# clk initVal) rst ena+ where+  go o rt@(~(r :- rs)) enas@(~(e :- es)) as@(~(x :- xs)) =+    let oE = if e then x else o+        oR = if r then resetVal else oE+        -- [Note: register strictness annotations]+    in  o `defaultSeqX` o :- (rt `seq` enas `seq` as `seq` go oR rs es xs)+{-# NOINLINE syncRegister# #-}+{-# ANN syncRegister# dontTranslate #-}+ -- | The above type is a generalization for: -- -- @@@ -1167,7 +1269,7 @@ -- __(.<=.)__ :: 'Ord' a => 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' a -> 'Clash.Signal.Signal' 'Bool' -- @ ----- It is a version of ('<=') that returns a 'Clash.Signal.Signal' of 'Bool'+-- It is a version of ('GHC.TypeNats.<=') that returns a 'Clash.Signal.Signal' of 'Bool' (.<=.) :: (Ord a, Applicative f) => f a -> f a -> f Bool (.<=.) = liftA2 (<=) @@ -1343,22 +1445,59 @@ -- i.e. to calculate the clock period for a circuit to run at 240 MHz we get -- -- >>> hzToPeriod 240e6--- 4167+-- 4166 -- -- __NB__: This function is /not/ synthesizable--- __NB__: This function is lossy. I.e., hzToPeriod . periodToHz /= id.-hzToPeriod :: HasCallStack => Double -> Natural-hzToPeriod freq | freq <= 0.0 = error "Frequency must be strictly positive"-                | otherwise   = ceiling ((1.0 / freq) / 1.0e-12)+--+-- __NB__: This function is lossy. I.e.,  periodToHz . hzToPeriod /= id.+hzToPeriod :: HasCallStack => Ratio Natural -> Natural+hzToPeriod freq = floor ((1.0 / freq) / 1.0e-12)  -- | Calculate the frequence in __Hz__, given the period in __ps__ -- -- i.e. to calculate the clock frequency of a clock with a period of 5000 ps: -- -- >>> periodToHz 5000--- 2.0e8+-- 200000000 % 1 -- -- __NB__: This function is /not/ synthesizable--- __NB__: This function is lossy. I.e., hzToPeriod . periodToHz /= id.-periodToHz :: Natural -> Double+periodToHz :: Natural -> Ratio Natural periodToHz period = 1.0 / (1.0e-12 * fromIntegral period)++-- | Build an 'Automaton' from a function over 'Signal's.+--+-- __NB__: Consumption of continuation of the 'Automaton' must be affine; that+-- is, you can only apply the continuation associated with a particular element+-- at most once.+signalAutomaton ::+  forall dom a b .+  (Signal dom a -> Signal dom b) -> Automaton (->) a b+signalAutomaton dut = Automaton $ \input0 -> unsafePerformIO $ do+  inputRefs <- infiniteRefList Nothing+  let inputs = input0 :- fmap readInput inputRefs+      readInput ref = unsafePerformIO $ do+        val <- readIORef ref+        case val of+          Nothing -> fail "signalAutomaton: non-affine use of continuation"+          Just x  -> return x++  let go (inRef :- inRefs) (out :- rest) = do+        let next :: Automaton (->) a b+            next = Automaton $ \i -> unsafePerformIO $ do+              old <- atomicModifyIORef inRef (\old -> (Just i,old))+              case old of+                Nothing -> return ()+                Just _  -> fail "signalAutomaton: non-affine use of continuation"+              unsafeInterleaveIO (go inRefs rest)+        return (out, next)++  go inputRefs (dut inputs)+{-# NOINLINE signalAutomaton #-}++infiniteRefList :: a -> IO (Signal dom (IORef a))+infiniteRefList val = go+ where+  go = do+    rest <- unsafeInterleaveIO go+    ref  <- newIORef val+    return (ref :- rest)

@@ -76,6 +76,7 @@   , Value   , Width   , TraceMap+  , TypeRepBS   -- ** Functions   , traceSignal#   , traceVecSignal#@@ -179,7 +180,7 @@           m       , signal)  where-  width = snatToNum (SNat @ (BitSize a))+  width = snatToNum (SNat @(BitSize a)) {-# NOINLINE traceSignal# #-}  -- | Trace a single vector signal: each element in the vector will show up as

@@ -69,6 +69,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NegativeLiterals #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-}@@ -118,15 +119,21 @@ import Data.List                  (find) import Data.Proxy                 (Proxy (..)) import Data.Ratio                 ((%), denominator, numerator)-import Data.Typeable              (Typeable, TypeRep, typeRep)+import Data.Typeable              (Typeable, TypeRep, typeRep, typeOf) import GHC.TypeLits               (KnownNat, Nat, type (+), natVal) import GHC.TypeLits.Extra         (Max)-import Language.Haskell.TH        (Q, TExp, TypeQ, appT, conT, litT, mkName,+import Language.Haskell.TH        (Q, appT, conT, litT, mkName,                                    numTyLit, sigE) import Language.Haskell.TH.Syntax (Lift(..)) #if MIN_VERSION_template_haskell(2,16,0) import Language.Haskell.TH.Compat #endif+#if MIN_VERSION_template_haskell(2,17,0)+import Language.Haskell.TH        (Quote)+import qualified Language.Haskell.TH as TH+#else+import Language.Haskell.TH        (TExp, TypeQ)+#endif import Test.QuickCheck            (Arbitrary, CoArbitrary)  import Clash.Class.BitPack        (BitPack (..))@@ -135,7 +142,7 @@                                    boundedMul) import Clash.Class.Resize         (Resize (..)) import Clash.Promoted.Nat         (SNat, natToNum, natToInteger)-import Clash.Prelude.BitIndex     (msb, split)+import Clash.Prelude.BitIndex     (lsb, msb, split) import Clash.Prelude.BitReduction (reduceAnd, reduceOr) import Clash.Sized.BitVector      (BitVector, (++#)) import Clash.Sized.Signed         (Signed)@@ -162,6 +169,16 @@ -- -- The 'Num' operators for this type saturate to 'maxBound' on overflow and -- 'minBound' on underflow, and use truncation as the rounding method.+--+-- Fixed has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i Fixed+-- type role Fixed representational nominal nominal+-- ...+--+-- as it is safe to coerce between different compatible underlying types, but+-- not necessasrily safe to coerce between different widths of this type.  To+-- change the width, use the functions in the 'Clash.Class.Resize.Resize' class. newtype Fixed (rep :: Nat -> Type) (int :: Nat) (frac :: Nat) =   Fixed { unFixed :: rep (int + frac) } @@ -170,7 +187,6 @@                   , Data (rep (int + frac))) => Data (Fixed rep int frac) deriving instance Eq (rep (int + frac))      => Eq (Fixed rep int frac) deriving instance Ord (rep (int + frac))     => Ord (Fixed rep int frac)-deriving instance Enum (rep (int + frac))    => Enum (Fixed rep int frac) deriving instance Bounded (rep (int + frac)) => Bounded (Fixed rep int frac) deriving instance Default (rep (int + frac)) => Default (Fixed rep int frac) deriving instance Arbitrary (rep (int + frac)) => Arbitrary (Fixed rep int frac)@@ -366,7 +382,7 @@ the 'Num' class for the 'SFixed' datatype.  Although the number of constraints for the @mac@ function defined earlier might-be considered small, here is an \"this way lies madness\" example where you+be considered small, here is a \"this way lies madness\" example where you really want to use constraint kinds:  @@@ -479,11 +495,10 @@     , BitPack (rep ((int + int) + (frac + frac)))     , Bits    (rep ((int + int) + (frac + frac)))     , BitPack (rep (int + frac))-    , Enum    (rep (int + frac))     , Bits    (rep (int + frac))-    , Ord     (rep (int + frac))     , Integral (rep (int + frac))     , Resize  rep+    , Typeable rep     , KnownNat int     , KnownNat frac     )@@ -546,7 +561,11 @@   liftTyped = liftTypedFromUntyped #endif +#if MIN_VERSION_template_haskell(2,17,0)+decFixed :: Quote m => TypeRep -> Integer -> Integer -> m TH.Type+#else decFixed :: TypeRep -> Integer -> Integer -> TypeQ+#endif decFixed r i f = do   foldl appT (conT ''Fixed) [ conT (mkName (show r))                             , litT (numTyLit i)@@ -695,7 +714,11 @@      , Bounded (rep size)      , Integral (rep size) )   => Double+#if MIN_VERSION_template_haskell(2,17,0)+  -> TH.Code Q (Fixed rep int frac)+#else   -> Q (TExp (Fixed rep int frac))+#endif fLit a = [|| Fixed (fromInteger sat) ||]   where     rMax      = toInteger (maxBound :: rep size)@@ -880,6 +903,184 @@     truncated = truncate shifted :: Integer     shifted   = a * (2 ^ (natToInteger @frac)) +-- | These behave similar to 'Prelude.Float', 'Prelude.Double' and+-- 'Prelude.Rational'. 'succ'\/'pred' add\/subtract 1. See the+-- <https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#dx13-131001 Haskell Report>+-- for full details.+--+-- The rules set out there for instances of both 'Enum' and+-- 'Bounded' are also observed. In particular, 'succ' and 'pred' result in a+-- runtime error if the result cannot be represented. See 'satSucc' and+-- 'satPred' for other options.+instance NumFixedC rep int frac => Enum (Fixed rep int frac) where+  succ f =+    let err = error $+             "Enum.succ{" ++ show (typeOf f) ++ "}: tried to take 'succ' of "+          ++ show f ++ ", causing overflow. Use 'satSucc' and specify a "+          ++ "SaturationMode if you need other behavior."+    in case natToInteger @int of+         0 -> err+         _ -> if f > satPred SatBound maxBound then+                err+              else+                satSucc SatWrap f+++  pred f =+    let err = error $+             "Enum.pred{" ++ show (typeOf f) ++ "}: tried to take 'pred' of "+          ++ show f ++ ", causing negative overflow. Use 'satPred' and "+          ++ "specify a SaturationMode if you need other behavior."+    in case natToInteger @int of+         0 -> err+         _ -> if f < satSucc SatBound minBound then+                err+              else+                satPred SatWrap f++  toEnum i =+    if res > rMax || res < rMin then+      error $  "Enum.toEnum{"+            ++ show (typeRep $ Proxy @(Fixed rep int frac)) ++ "}: tag ("+            ++ show i ++ ") is outside of bounds "+            ++ show ( minBound :: Fixed rep int frac+                    , maxBound :: Fixed rep int frac)+    else+      Fixed (fromInteger res)+     where+      sh   = natToNum @frac+      res  = toInteger i `shiftL` sh+      rMax = toInteger (maxBound :: rep (int + frac))+      rMin = toInteger (minBound :: rep (int + frac))++  fromEnum f@(Fixed fRep) =+    if res > rMax || res < rMin then+      error $  "Enum.fromEnum{" ++ show (typeOf f) ++ "}: value ("+            ++ show f ++ ") is outside of Int's bounds "+            ++ show (rMin, rMax)+    else+      fromInteger res+     where+      nF     = natToNum @frac+      frMask = fromInteger $ (1 `shiftL` nF) - 1+      offset = if f < 0 && fRep .&. frMask /= 0 then 1 else 0+      -- res amounts to "truncate f", but without needing all the constraints+      -- for RealFrac.+      res    = toInteger $ (fRep `shiftR` nF) + offset+      rMax   = toInteger (maxBound :: Int)+      rMin   = toInteger (minBound :: Int)++  enumFrom x1 = enumFromTo x1 maxBound+  enumFromThen (Fixed x1Rep) (Fixed x2Rep) =+    map Fixed $ enumFromThen x1Rep x2Rep++  enumFromTo x1@(Fixed x1Rep) y@(Fixed yRep)+    | yPlusHalf < x1 = []+    | closeToMax     = [x1]+    | otherwise      =  map Fixed $ enumFromThenTo+                                      x1Rep+                                      (unFixed $ satSucc SatWrap x1)+                                      (unFixed $ yPlusHalf)+   where+    closeToMax = natToInteger @int == 0 || x1 > satPred SatBound maxBound+    nF = natToNum @frac+    yPlusHalf | nF == 0       = y+              | isSigned yRep = y - (Fixed $ -1 `shiftL` (nF - 1))+              | otherwise     = y + (Fixed $ 1 `shiftL` (nF - 1))++  enumFromThenTo = enumFromThenTo#++-- Inspired by Enum Int from GHC.Enum in base-4.14.1.0+--+-- Note that if x2 /= x1, it is guaranteed that (int + frac) >= 1, because if it+-- were zero there would only be one concrete value. This fact is relied upon in+-- enumFromThenToUp and enumFromThenToDown, which would have undefined behavior+-- for (int + frac) == 0.+enumFromThenTo#+  :: forall f rep int frac+   . ( NumFixedC rep int frac+     , f ~ Fixed rep int frac)+  => f+  -> f+  -> f+  -> [f]+enumFromThenTo# x1 x2 y+  | x2 == x1  = if y < x1 then+                  []+                else+                  repeat x1+  | x2 > x1   = enumFromThenToUp x1 x2 y+  | otherwise = enumFromThenToDown x1 x2 y++enumFromThenToUp+  :: forall f rep int frac+   . ( NumFixedC rep int frac+     , f ~ Fixed rep int frac)+  => f+  -> f+  -> f+  -> [f]+enumFromThenToUp x1 x2 y+  | y < x1 = let y' = satAdd SatWrap y halfDelta  -- Never wraps+             in if y' < x1 || (isMinusHalf && y' <= x1) then+                  []+                else+                  [x1]+  | y < x2 = let x2' = satSub SatWrap x2 halfDelta  -- Never wraps `+             in if y > x2' || (not isMinusHalf && y >= x2') then+                  [x1, x2]+                else+                  [x1]+  | otherwise = let y' = satSub SatWrap y (delta `shiftR` 1) -- Does wrap+                    go_up x+                      | x' < x            = [x]+                      | isHalf && x >= y' = [x]+                      | x > y'            = [x]+                      | otherwise          = x : go_up x'+                     where+                      x' = satAdd SatWrap x delta  -- Does wrap+                in x1 : go_up x2+ where+   delta = satSub SatWrap x2 x1  -- Does wrap!+   halfDelta = satSub SatWrap (x2 `shiftR` 1) (x1 `shiftR` 1)  -- Never wraps+   isHalf = lsb delta == 1+   isMinusHalf = lsb x2 == 0 && lsb x1 == 1++enumFromThenToDown+  :: forall f rep int frac+   . ( NumFixedC rep int frac+     , f ~ Fixed rep int frac)+  => f+  -> f+  -> f+  -> [f]+enumFromThenToDown x1 x2 y+  | y > x1 = let y' = satSub SatWrap y halfDelta  -- Never wraps+             in if y' > x1 || (isMinusHalf && y' >= x1) then+                  []+                else+                  [x1]+  | y > x2 = let x2' = satAdd SatWrap x2 halfDelta  -- Never wraps `+             in if y < x2' || (not isMinusHalf && y <= x2') then+                  [x1, x2]+                else+                  [x1]+  | otherwise = let y' = satAdd SatWrap y (delta `shiftR` 1)  -- Does wrap+                    go_dn x+                      | x' > x            = [x]+                      | isHalf && x <= y' = [x]+                      | x < y'            = [x]+                      | otherwise         = x : go_dn x'+                     where+                      x' = satSub SatWrap x delta  -- Does wrap+                in x1 : go_dn x2+ where+  delta = satSub SatWrap x1 x2  -- Does wrap!+  halfDelta = satSub SatWrap (x1 `shiftR` 1) (x2 `shiftR` 1)  -- Never wraps+  isHalf = lsb delta == 1+  isMinusHalf = lsb x1 == 0 && lsb x2 == 1++ instance NumFixedC rep int frac => SaturatingNum (Fixed rep int frac) where   satAdd w (Fixed a) (Fixed b) = Fixed (satAdd w a b)   satSub  w (Fixed a) (Fixed b) = Fixed (satSub w a b)@@ -896,7 +1097,7 @@         (rL,rR) = split res :: (BitVector int, BitVector (int + frac + frac))     in  case isSigned a of           True  -> let overflow = complement (reduceOr (pack (msb rR) ++# pack rL)) .|.-                                             reduceAnd (pack (msb rR) ++# pack rL)+                                  reduceAnd (pack (msb rR) ++# pack rL)                    in  case overflow of                          1 -> unpack (resize (shiftR rR sh))                          _ -> case msb rL of@@ -912,7 +1113,7 @@         (rL,rR) = split res :: (BitVector int, BitVector (int + frac + frac))     in  case isSigned a of           True  -> let overflow = complement (reduceOr (pack (msb rR) ++# pack rL)) .|.-                                             reduceAnd (pack (msb rR) ++# pack rL)+                                  reduceAnd (pack (msb rR) ++# pack rL)                    in  case overflow of                          1 -> unpack (resize (shiftR rR sh))                          _ -> 0@@ -926,12 +1127,12 @@         (rL,rR) = split res :: (BitVector int, BitVector (int + frac + frac))     in  case isSigned a of           True  -> let overflow = complement (reduceOr (pack (msb rR) ++# pack rL)) .|.-                                             reduceAnd (pack (msb rR) ++# pack rL)+                                  reduceAnd (pack (msb rR) ++# pack rL)                    in  case overflow of                          1 -> unpack (resize (shiftR rR sh))                          _ -> case msb rL of                                 0 -> maxBound-                                _ -> succ minBound+                                _ -> Fixed $ succ minBound           False -> case rL of                      0 -> unpack (resize (shiftR rR sh))                      _ -> maxBound@@ -951,9 +1152,9 @@   satPred satMode f@(Fixed fRep) =     let sh       = natToNum @frac         symBound = if isSigned fRep-                   then Fixed $ succ minBound+                   then Fixed $ minBound + 1                    else minBound-    in case natVal (Proxy @int) of+    in case natToInteger @int of          0 -> case satMode of                 SatWrap      -> f                 SatBound     -> minBound@@ -1019,9 +1220,6 @@ type FracFixedC rep int frac   = ( NumFixedC rep int frac     , DivideC   rep int frac int frac-    , Integral  (rep (int + frac))-    , KnownNat  int-    , KnownNat  frac     )  -- | Constraint for the 'Fractional' instance of 'SFixed'@@ -1062,18 +1260,17 @@       n    = numerator   r `shiftL` (2 * frac)       d    = denominator r `shiftL` frac -instance (NumFixedC rep int frac, Integral (rep (int + frac))) =>-         Real (Fixed rep int frac) where+instance NumFixedC rep int frac => Real (Fixed rep int frac) where   toRational f@(Fixed fRep) = nom % denom    where      nF        = fracShift f      denom     = 1 `shiftL` nF      nom       = toInteger fRep -instance (FracFixedC rep int frac, NumFixedC rep int frac, Integral (rep (int + frac))) =>-         RealFrac (Fixed rep int frac) where+instance FracFixedC rep int frac => RealFrac (Fixed rep int frac) where   properFraction f@(Fixed fRep) = (fromIntegral whole, fract)     where       whole = (fRep `shiftR` fracShift f) + offset       fract = Fixed $ fRep - (whole `shiftL` fracShift f)-      offset = if f < 0 then 1 else 0+      frMask = fromInteger $ (1 `shiftL` fracShift f) - 1+      offset = if f < 0 && fRep .&. frMask /= 0 then 1 else 0

@@ -10,6 +10,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -134,23 +135,42 @@ import GHC.Generics               (Generic) import Data.Maybe                 (fromMaybe) import GHC.Exts-  ((>#), Word#, Word (W#), eqWord#, int2Word#, isTrue#, uncheckedShiftRL#)+  (Word#, Word (W#), eqWord#, int2Word#, isTrue#, uncheckedShiftRL#)+#if MIN_VERSION_base(4,15,0)+import GHC.Exts (minusWord#, gtWord#, word2Int#)+import GHC.Num.BigNat (bigNatShiftR#, bigNatToWord)+import GHC.Num.Integer (integerFromNatural, integerToNatural)+import GHC.Num.Natural+  (Natural (..), naturalFromWord, naturalShiftL, naturalShiftR, naturalToWord)+#else+import GHC.Exts ((>#)) import qualified GHC.Exts import GHC.Integer.GMP.Internals  (Integer (..), bigNatToWord, shiftRBigNat) import GHC.Natural   (Natural (..), naturalFromInteger, wordToNatural)+#endif #if MIN_VERSION_base(4,12,0) import GHC.Natural                (naturalToInteger) #endif import GHC.Prim                   (dataToTag#) import GHC.Stack                  (HasCallStack, withFrozenCallStack)-import GHC.TypeLits               (KnownNat, Nat, type (+), type (-), natVal)+import GHC.TypeLits               (KnownNat, Nat, type (+), type (-))+#if MIN_VERSION_base(4,15,0)+import GHC.TypeNats               (natVal)+#else+import GHC.TypeLits               (natVal)+#endif import GHC.TypeLits.Extra         (Max)-import Language.Haskell.TH        (Q, TExp, TypeQ, appT, conT, litT, numTyLit, sigE, Lit(..), litE, Pat, litP)+import Language.Haskell.TH        (Lit (..), Pat, Q, appT, conT, litE, litP, litT, mkName, numTyLit, sigE, tupE, tupP, varP) import Language.Haskell.TH.Syntax (Lift(..)) #if MIN_VERSION_template_haskell(2,16,0) import Language.Haskell.TH.Compat #endif+#if MIN_VERSION_template_haskell(2,17,0)+import Language.Haskell.TH        (Code, Quote, Type)+#else+import Language.Haskell.TH        (TExp, TypeQ)+#endif import Test.QuickCheck.Arbitrary  (Arbitrary (..), CoArbitrary (..),                                    arbitraryBoundedIntegral,                                    coarbitraryIntegral, shrinkIntegral)@@ -167,7 +187,9 @@  import {-# SOURCE #-} qualified Clash.Sized.Vector         as V import {-# SOURCE #-} qualified Clash.Sized.Internal.Index as I+import                qualified Data.Char                  as C import                qualified Data.List                  as L+import                qualified Data.Map.Strict            as M  #include "MachDeps.h" @@ -177,14 +199,25 @@ >>> import Clash.Sized.Internal.BitVector -} +type role BitVector nominal+ -- * Type definitions  -- | A vector of bits. -- -- * Bit indices are descending -- * 'Num' instance performs /unsigned/ arithmetic.+--+-- BitVector has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i BitVector+-- type role BitVector nominal+-- ...+--+-- as it is not safe to coerce between different size BitVector. To change the+-- size, use the functions in the 'Clash.Class.Resize.Resize' class. data BitVector (n :: Nat) =-    -- | The constructor, 'BV', and  the field, 'unsafeToInteger', are not+    -- | The constructor, 'BV', and  the field, 'unsafeToNatural', are not     -- synthesizable.     BV { unsafeMask      :: !Natural        , unsafeToNatural :: !Natural@@ -350,14 +383,23 @@  -- *** BitPack pack# :: Bit -> BitVector 1+#if MIN_VERSION_base(4,15,0)+pack# (Bit (W# m) (W# b)) = BV (NS m) (NS b)+#else pack# (Bit (W# m) (W# b)) = BV (NatS# m) (NatS# b)+#endif {-# NOINLINE pack# #-}  unpack# :: BitVector 1 -> Bit unpack# (BV m b) = Bit (go m) (go b)  where+#if MIN_VERSION_base(4,15,0)+  go (NS w) = W# w+  go (NB w) = bigNatToWord w+#else   go (NatS# w) = W# w   go (NatJ# w) = W# (bigNatToWord w)+#endif {-# NOINLINE unpack# #-}  -- * Instances@@ -386,8 +428,8 @@ instance KnownNat n => ShowX (BitVector n) where   showsPrecX = showsPrecXWith showsPrec -instance NFDataX (BitVector n) where-  deepErrorX = errorX+instance KnownNat n => NFDataX (BitVector n) where+  deepErrorX _ = undefined#   rnfX = rwhnfX   hasUndefined bv = isLeft (isX bv) || unsafeMask bv /= 0 @@ -414,7 +456,11 @@ -- -- >>> $$(bLit "1.0.") :: BitVector 4 -- 1.0.+#if MIN_VERSION_template_haskell(2,17,0)+bLit :: forall n. KnownNat n => String -> Code Q (BitVector n)+#else bLit :: forall n. KnownNat n => String -> Q (TExp (BitVector n))+#endif bLit s = [|| fromInteger# m i1 ||]   where     bv :: BitVector n@@ -488,7 +534,11 @@  enumFrom# :: forall n. KnownNat n => BitVector n -> [BitVector n] enumFrom# (BV 0 x) = map (BV 0 . (`mod` m)) [x .. unsafeToNatural (maxBound :: BitVector n)]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif enumFrom# bv = undefErrorU "enumFrom" bv {-# NOINLINE enumFrom# #-} @@ -503,7 +553,11 @@  where   bound = if x <= y then maxBound else minBound :: BitVector n   toBvs = map (BV 0 . (`mod` m))+#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif enumFromThen# bv1 bv2 = undefErrorP "enumFromThen" bv1 bv2 {-# NOINLINE enumFromThen# #-} @@ -514,7 +568,11 @@   -> BitVector n   -> [BitVector n] enumFromTo# (BV 0 x) (BV 0 y) = map (BV 0 . (`mod` m)) [x .. y]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif enumFromTo# bv1 bv2 = undefErrorP "enumFromTo" bv1 bv2 {-# NOINLINE enumFromTo# #-} @@ -526,7 +584,11 @@   -> BitVector n   -> [BitVector n] enumFromThenTo# (BV 0 x1) (BV 0 x2) (BV 0 y) = map (BV 0 . (`mod` m)) [x1, x2 .. y]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif enumFromThenTo# bv1 bv2 bv3 = undefErrorP3 "enumFromTo" bv1 bv2 bv3 {-# NOINLINE enumFromThenTo# #-} @@ -559,7 +621,11 @@     go (BV 0 i) (BV 0 j) = BV 0 (addMod m i j)     go bv1 bv2 = undefErrorI "+" bv1 bv2 +#if MIN_VERSION_base(4,15,0)+    m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else     m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE (-#) #-} (-#) = go@@ -567,7 +633,11 @@     go (BV 0 i) (BV 0 j) = BV 0 (subMod m i j)     go bv1 bv2 = undefErrorI "-" bv1 bv2 +#if MIN_VERSION_base(4,15,0)+    m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else     m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE (*#) #-} (*#) = go@@ -575,7 +645,11 @@   go (BV 0 i) (BV 0 j) = BV 0 (mulMod2 m i j)   go bv1 bv2 = undefErrorI "*" bv1 bv2 +#if MIN_VERSION_base(4,15,0)+  m = (1 `naturalShiftL` naturalToWord (natVal (Proxy @n))) - 1+#else   m = (1 `shiftL` fromInteger (natVal (Proxy @n))) - 1+#endif  {-# NOINLINE negate# #-} negate# :: forall n . KnownNat n => BitVector n -> BitVector n@@ -584,15 +658,25 @@   go (BV 0 i) = BV 0 (negateMod m i)   go bv = undefErrorU "negate" bv +#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE fromInteger# #-} fromInteger# :: KnownNat n => Natural -> Integer -> BitVector n fromInteger# m i = sz `seq` mx   where+#if MIN_VERSION_base(4,15,0)+    mx = BV (m `mod` sz)+            (integerToNatural (i `mod` integerFromNatural sz))+    sz  = 1 `naturalShiftL` naturalToWord (natVal mx)+#else     mx = BV (m `mod` naturalFromInteger sz)             (naturalFromInteger (i `mod` sz))     sz  = 1 `shiftL` fromInteger (natVal mx) :: Integer+#endif  instance (KnownNat m, KnownNat n) => ExtendingNum (BitVector m) (BitVector n) where   type AResult (BitVector m) (BitVector n) = BitVector (Max m n + 1)@@ -614,7 +698,11 @@   go (BV 0 a) (BV 0 b) = BV 0 (subMod m a b)   go bv1 bv2 = undefErrorP "sub" bv1 bv2 +#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @(Max m n + 1)))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @(Max m n + 1)))+#endif  {-# NOINLINE times# #-} times# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (m + n)@@ -708,11 +796,19 @@ -- ** Length information {-# NOINLINE size# #-} size# :: KnownNat n => BitVector n -> Int+#if MIN_VERSION_base(4,15,0)+size# bv = fromIntegral (natVal bv)+#else size# bv = fromInteger (natVal bv)+#endif  {-# NOINLINE maxIndex# #-} maxIndex# :: KnownNat n => BitVector n -> Int+#if MIN_VERSION_base(4,15,0)+maxIndex# bv = fromIntegral (natVal bv) - 1+#else maxIndex# bv = fromInteger (natVal bv) - 1+#endif  -- ** Indexing {-# NOINLINE index# #-}@@ -722,7 +818,11 @@                              (W# (int2Word# (dataToTag# (testBit v i))))     | otherwise        = err   where+#if MIN_VERSION_base(4,15,0)+    sz  = fromIntegral (natVal bv)+#else     sz  = fromInteger (natVal bv)+#endif     err = error $ concat [ "(!): "                          , show i                          , " is out of range ["@@ -737,12 +837,23 @@   = Bit (msbN m)         (msbN v)  where+#if MIN_VERSION_base(4,15,0)+  !(NS i#) = natVal (Proxy @n)++  msbN (NS w) =+    if isTrue# (i# `gtWord#` WORD_SIZE_IN_BITS##)+    then W# 0##+    else W# (w `uncheckedShiftRL#` (word2Int# (i# `minusWord#` 1##)))+  msbN (NB bn) = bigNatToWord (bigNatShiftR# bn (i# `minusWord#` 1##))+#else   !(S# i#) = natVal (Proxy @n)+   msbN (NatS# w) =     if isTrue# (i# ># WORD_SIZE_IN_BITS#)     then W# 0##     else W# (w `uncheckedShiftRL#` (i# GHC.Exts.-# 1#))   msbN (NatJ# bn) = W# (bigNatToWord (shiftRBigNat bn (i# GHC.Exts.-# 1#)))+#endif  {-# NOINLINE lsb# #-} -- | LSB@@ -768,19 +879,33 @@ (++#) :: KnownNat m => BitVector n -> BitVector m -> BitVector (n + m) (BV m1 v1) ++# bv2@(BV m2 v2) = BV (m1' .|. m2) (v1' .|. v2)   where+#if MIN_VERSION_base(4,15,0)+    size2 = fromIntegral (natVal bv2)+    v1' = naturalShiftL v1 size2+    m1' = naturalShiftL m1 size2+#else     size2 = fromInteger (natVal bv2)     v1' = shiftL v1 size2     m1' = shiftL m1 size2+#endif  -- * Modifying BitVectors {-# NOINLINE replaceBit# #-} replaceBit# :: KnownNat n => BitVector n -> Int -> Bit -> BitVector n replaceBit# bv@(BV m v) i (Bit mb b)-    | i >= 0 && i < sz = BV (clearBit m i  .|. (wordToNatural mb `shiftL` i))+#if MIN_VERSION_base(4,15,0)+    | i >= 0 && i < sz = BV (clearBit m i .|. (naturalFromWord mb `shiftL` i))+#else+    | i >= 0 && i < sz = BV (clearBit m i .|. (wordToNatural mb `shiftL` i))+#endif                             (if testBit b 0 && mb == 0 then setBit v i else clearBit v i)     | otherwise        = err   where+#if MIN_VERSION_base(4,15,0)+    sz   = fromIntegral (natVal bv)+#else     sz   = fromInteger (natVal bv)+#endif     err  = error $ concat [ "replaceBit: "                           , show i                           , " is out of range ["@@ -816,12 +941,21 @@   => BitVector (m + n)   -> (BitVector m, BitVector n) split# (BV m i) =+#if MIN_VERSION_base(4,15,0)+  let n     = naturalToWord (natVal (Proxy @n))+      mask  = maskMod (natVal (Proxy @n))+      r     = mask i+      rMask = mask m+      l     = i `naturalShiftR` n+      lMask = m `naturalShiftR` n+#else   let n     = fromInteger (natVal (Proxy @n))       mask  = maskMod (natVal (Proxy @n))       r     = mask i       rMask = mask m       l     = i `shiftR` n       lMask = m `shiftR` n+#endif   in  (BV lMask l, BV rMask r)  and#, or#, xor# :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n@@ -865,7 +999,11 @@     else       error ("'shiftL' undefined for negative number: " ++ show i)  where+#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE shiftR# #-} shiftR# (BV m v) i@@ -877,6 +1015,15 @@ rotateL# =   \(BV msk v) b ->     if b >= 0 then+#if MIN_VERSION_base(4,15,0)+      let vl    = naturalShiftL v b'+          vr    = naturalShiftR v b''++          ml    = naturalShiftL msk b'+          mr    = naturalShiftR msk b''++          b'   = fromIntegral b `mod` sz+#else       let vl    = shiftL v b'           vr    = shiftR v b'' @@ -884,30 +1031,49 @@           mr    = shiftR msk b''            b'   = b `mod` sz+#endif           b''  = sz - b'       in  BV ((ml .|. mr) `mod` m) ((vl .|. vr) `mod` m)     else       error "'rotateL' undefined for negative numbers"  where+#if MIN_VERSION_base(4,15,0)+  sz = naturalToWord (natVal (Proxy @n))+  m  = 1 `naturalShiftL` sz+#else   sz = fromInteger (natVal (Proxy @n)) :: Int   m  = 1 `shiftL` sz+#endif  {-# NOINLINE rotateR# #-} rotateR# =   \(BV msk v) b ->     if b >= 0 then+#if MIN_VERSION_base(4,15,0)+      let vl   = naturalShiftR v b'+          vr   = naturalShiftL v b''+          ml   = naturalShiftR msk b'+          mr   = naturalShiftL msk b''+          b'   = fromIntegral b `mod` sz+#else       let vl   = shiftR v b'           vr   = shiftL v b''           ml   = shiftR msk b'           mr   = shiftL msk b''           b'   = b `mod` sz+#endif           b''  = sz - b'       in  BV ((ml .|. mr) `mod` m) ((vl .|. vr) `mod` m)     else       error "'rotateR' undefined for negative numbers"  where+#if MIN_VERSION_base(4,15,0)+  sz = naturalToWord (natVal (Proxy @n))+  m  = 1 `naturalShiftL` sz+#else   sz = fromInteger (natVal (Proxy @n)) :: Int   m  = 1 `shiftL` sz+#endif  popCountBV :: forall n . KnownNat n => BitVector (n+1) -> I.Index (n+2) popCountBV bv =@@ -929,7 +1095,11 @@  truncateB# :: forall a b . KnownNat a => BitVector (a + b) -> BitVector a truncateB# = \(BV msk i) -> BV (msk `mod` m) (i `mod` m)+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @a))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @a))+#endif {-# NOINLINE truncateB# #-}  instance KnownNat n => Lift (BitVector n) where@@ -939,8 +1109,13 @@   liftTyped = liftTypedFromUntyped #endif +#if MIN_VERSION_template_haskell(2,17,0)+decBitVector :: Quote m => Natural -> m Type+decBitVector n = appT (conT ''BitVector) (litT $ numTyLit (integerFromNatural n))+#else decBitVector :: Integer -> TypeQ decBitVector n = appT (conT ''BitVector) (litT $ numTyLit n)+#endif  instance KnownNat n => SaturatingNum (BitVector n) where   satAdd SatWrap a b = a +# b@@ -1051,7 +1226,11 @@ -- | Create a BitVector with all its bits undefined undefined# :: forall n . KnownNat n => BitVector n undefined# =+#if MIN_VERSION_base(4,15,0)+  let m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   let m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif   in  BV (m-1) 0 {-# NOINLINE undefined# #-} @@ -1091,27 +1270,55 @@ -- pattern. The scrutinee can be any type that is an instance of the -- 'Num', 'Bits' and 'Eq' typeclasses. ----- The bit pattern is specified by a string which contains @\'0\'@ or--- @\'1\'@ for matching a bit, or @\'.\'@ for bits which are not matched.+-- The bit pattern is specified by a string which contains: --+--   * @\'0\'@ or @\'1\'@ for matching a bit+--+--   * @\'.\'@ for bits which are not matched (wildcard)+--+--   * @\'_\'@ can be used as a separator similar to the NumericUnderscores+--   language extension+--+--   * lowercase alphabetical characters can be used to bind some bits to variables.+--   For example @"0aab11bb"@ will bind two variables @aa :: BitVector 2@ and+--   @bbb :: BitVector 3@ with their values set by the corresponding bits+-- -- The following example matches a byte against two bit patterns where--- some bits are relevant and others are not:+-- some bits are relevant and others are not while binding two variables @aa@+-- and @bb@: -- -- @ --   decode :: Unsigned 8 -> Maybe Bool---   decode $(bitPattern "00...110") = Just True---   decode $(bitPattern "10..0001") = Just False+--   decode $(bitPattern "00.._.110") = Just True+--   decode $(bitPattern "10.._0001") = Just False+--   decode $(bitPattern "aa.._b0b1") = Just (aa + bb > 1) --   decode _ = Nothing -- @ bitPattern :: String -> Q Pat-bitPattern s = [p| (($mask .&.) -> $target) |]+bitPattern s = [p| ((\_x -> $preprocess) -> $tuple) |]   where-    bs = parse <$> s+    (_, bs, M.toList -> ns) = L.foldr parse (0, [], M.empty) $ filter (/= '_') s +    var c is = varP . mkName $ L.replicate (length is) c+    bitSelect i = [e| if testBit _x $(litE $ IntegerL i) then pack# high else pack# low |]+    varSelect is = L.foldr1 (\a b -> [e| $a ++# $b |]) (bitSelect <$> is)+     mask = litE . IntegerL . fromBits $ maybe 0 (const 1) <$> bs+    maskE = [e| $mask .&. _x |]     target = litP . IntegerL . fromBits $ fromMaybe 0 <$> bs -    parse '.' = Nothing-    parse '0' = Just 0-    parse '1' = Just 1-    parse c = error $ "Invalid bit pattern: " ++ show c+    preprocess = tupE $ maskE : (varSelect . snd <$> ns)+    tuple = tupP $ target : (uncurry var <$> ns)++    parse '.' (i, b, n) = (succ i, Nothing:b, n)+    parse '0' (i, b, n) = (succ i, Just 0:b, n)+    parse '1' (i, b, n) = (succ i, Just 1:b, n)+    parse c (i, b, n)+      | C.isAlpha c && C.isLower c =+        ( succ i+        , Nothing:b+        , M.alter (Just . (i:) . fromMaybe []) c n+        )+      | otherwise = error $+        "Invalid bit pattern: " ++ show c +++        ", expecting one of '0', '1', '.', '_', or a lowercase alphabetic character"

@@ -13,7 +13,7 @@ import GHC.Stack    (HasCallStack) import Data.Kind    (Type) -type role BitVector phantom+type role BitVector nominal data BitVector :: Nat -> Type data Bit 

@@ -9,6 +9,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -72,12 +73,18 @@ import Data.Data                  (Data) import Data.Default.Class         (Default (..)) import Text.Read                  (Read (..), ReadPrec)-import Text.Printf                (PrintfArg (..))-import Language.Haskell.TH        (TypeQ, appT, conT, litT, numTyLit, sigE)+import Text.Printf                (PrintfArg (..), printf)+import Data.Ix                    (Ix(..))+import Language.Haskell.TH        (appT, conT, litT, numTyLit, sigE) import Language.Haskell.TH.Syntax (Lift(..)) #if MIN_VERSION_template_haskell(2,16,0) import Language.Haskell.TH.Compat #endif+#if MIN_VERSION_template_haskell(2,17,0)+import Language.Haskell.TH        (Quote, Type)+#else+import Language.Haskell.TH        (TypeQ)+#endif import GHC.Generics               (Generic) import GHC.Natural                (Natural, naturalFromInteger) #if MIN_VERSION_base(4,12,0)@@ -109,6 +116,8 @@ >>> import Clash.Sized.Internal.Index -} +type role Index nominal+ -- | Arbitrary-bounded unsigned integer represented by @ceil(log_2(n))@ bits. -- -- Given an upper bound @n@, an 'Index' @n@ number has a range of: [0 .. @n@-1]@@ -132,10 +141,26 @@ -- >>> 2 * 4 :: Index 8 -- *** Exception: X: Clash.Sized.Index: result 8 is out of bounds: [0..7] -- ...+--+-- Index has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i Index+-- type role Index nominal+-- ...+--+-- as it is not safe to coerce between different range Index. To change the+-- size, use the functions in the 'Clash.Class.Resize.Resize' class.+#if MIN_VERSION_base(4,15,0)+data Index (n :: Nat) =+    -- | The constructor, 'I', and the field, 'unsafeToInteger', are not+    -- synthesizable.+    I { unsafeToInteger :: !Integer }+#else newtype Index (n :: Nat) =     -- | The constructor, 'I', and the field, 'unsafeToInteger', are not     -- synthesizable.     I { unsafeToInteger :: Integer }+#endif   deriving (Data, Generic)  {-# NOINLINE size# #-}@@ -154,7 +179,7 @@   unpack = unpack#  -- | Safely convert an `SNat` value to an `Index`-fromSNat :: (KnownNat m, n <= m + 1) => SNat n -> Index m+fromSNat :: (KnownNat m, n + 1 <= m) => SNat n -> Index m fromSNat = snatToNum  {-# NOINLINE pack# #-}@@ -322,6 +347,7 @@   satMul SatWrap !a !b =     case natToInteger @n of       1 -> fromInteger# 0+      2 -> case a of {0 -> 0; _ -> b}       _ -> leToPlusKN @1 @n $         case times# a b of           z -> let m = fromInteger# (natToInteger @n)@@ -421,7 +447,11 @@   liftTyped = liftTypedFromUntyped #endif +#if MIN_VERSION_template_haskell(2,17,0)+decIndex :: Quote m => Integer -> m Type+#else decIndex :: Integer -> TypeQ+#endif decIndex n = appT (conT ''Index) (litT $ numTyLit n)  instance Show (Index n) where@@ -456,3 +486,10 @@  instance KnownNat n => CoArbitrary (Index n) where   coarbitrary = coarbitraryIntegral++instance (KnownNat n) => Ix (Index n) where+  range (a, b) = [a..b]+  index ab@(a, b) x+    | inRange ab x = fromIntegral $ x - a+    | otherwise = error $ printf "Index %d out of bounds (%d, %d)" x a b+  inRange (a, b) x = a <= x && x <= b

@@ -13,7 +13,7 @@ import Data.Kind (Type) import GHC.TypeLits (KnownNat, Nat) -type role Index phantom+type role Index nominal data Index :: Nat -> Type  instance KnownNat n => Num (Index n)

@@ -29,8 +29,13 @@  module Clash.Sized.Internal.Mod where +#if MIN_VERSION_base(4,15,0)+import GHC.Exts (eqWord#, leWord#, word2Int#)+#else+import GHC.Exts ((==#))+#endif import GHC.Exts-  ((==#), (<=#), geWord#, isTrue#, minusWord#, plusWord#, uncheckedShiftL#, xor#,+  ((<=#), geWord#, isTrue#, minusWord#, plusWord#, uncheckedShiftL#, xor#,    timesWord2#, quotRemWord2#, and#) #if MIN_VERSION_base(4,12,0) import GHC.Exts (addWordC#)@@ -38,19 +43,175 @@ #if !MIN_VERSION_base(4,12,0) import GHC.Exts (Int#, Word#, plusWord2#, word2Int#) #endif+#if MIN_VERSION_base(4,15,0)+import GHC.Num.BigNat+  (BigNat#, bigNatAdd, bigNatAddWord#, bigNatAnd, bigNatBit#, bigNatCompare,+   bigNatFromWord#, bigNatFromWord2#, bigNatMul, bigNatMulWord#, bigNatRem,+   bigNatSize#, bigNatSubUnsafe, bigNatSubWordUnsafe#, bigNatToWord#, bigNatXor)+import GHC.Num.Natural (Natural (..))+#else import GHC.Natural (Natural (..)) import GHC.Integer.GMP.Internals   (BigNat, Integer (..), bigNatToWord, compareBigNat, minusBigNat, minusBigNatWord,    plusBigNat, plusBigNatWord, sizeofBigNat#, bitBigNat, wordToBigNat2,    remBigNat, timesBigNat, timesBigNatWord, xorBigNat, wordToBigNat, andBigNat)+#endif #if !MIN_VERSION_base(4,12,0) import GHC.Integer.GMP.Internals (wordToInteger) #endif  #include "MachDeps.h" +#if MIN_VERSION_base(4,15,0) -- | modular subtraction subMod :: Natural -> Natural -> Natural -> Natural+subMod (NS m#) (NS x#) (NS y#) =+  if isTrue# (x# `geWord#` y#) then NS z# else NS (z# `plusWord#` m#)+  where+    z# = x# `minusWord#` y#+subMod NS{} _ _ = brokenInvariant+subMod (NB m#) (NS x#) (NS y#) =+  if isTrue# (x# `geWord#` y#)+    then NS (x# `minusWord#` y#)+    else bigNatToNat (m# `bigNatSubWordUnsafe#` (y# `minusWord#` x#))+subMod (NB m#) (NS x#) (NB y#) =+  bigNatToNat ((m# `bigNatSubUnsafe` y#) `bigNatAddWord#` x#)+subMod NB{} (NB x#) (NS y#) =+  bigNatToNat (x# `bigNatSubWordUnsafe#` y#)+subMod (NB m#) (NB x#) (NB y#) = case x# `bigNatCompare` y# of+  LT -> bigNatToNat ((m# `bigNatSubUnsafe` y#) `bigNatAdd` x#)+  EQ -> NS 0##+  GT -> bigNatToNat (x# `bigNatSubUnsafe` y#)++-- | modular addition+addMod :: Natural -> Natural -> Natural -> Natural+addMod (NS m#) (NS x#) (NS y#) =+  if isTrue# c# || isTrue# (z# `geWord#` m#) then NS (z# `minusWord#` m#) else NS z#+  where+    !(# z#, c# #) = x# `addWordC#` y#+addMod NS{} _ _ = brokenInvariant+addMod (NB m#) (NS x#) (NS y#) =+  if isTrue# c# then subIfGe (bigNatFromWord2# 1## z#) m# else NS z#+  where+    !(# z#, c# #) = x# `addWordC#` y#+addMod (NB m#) (NS x#) (NB y#) = subIfGe (y# `bigNatAddWord#` x#) m#+addMod (NB m#) (NB x#) (NS y#) = subIfGe (x# `bigNatAddWord#` y#) m#+addMod (NB m#) (NB x#) (NB y#) = subIfGe (x# `bigNatAdd`     y#) m#++-- | modular multiplication+mulMod :: Natural -> Natural -> Natural -> Natural+mulMod (NS m#) (NS x#) (NS y#) = NS r#+  where+    !(# z1#, z2# #) = timesWord2# x# y#+    !(# _, r# #) = quotRemWord2# z1# z2# m#+mulMod NS{} _ _ = brokenInvariant+mulMod (NB m#) (NS x#) (NS y#) =+  bigNatToNat (bigNatFromWord2# z1# z2# `bigNatRem` m#)+  where+    !(# z1#, z2# #) = timesWord2# x# y#+mulMod (NB m#) (NS x#) (NB y#) =+  bigNatToNat ((y# `bigNatMulWord#` x#) `bigNatRem` m#)+mulMod (NB m#) (NB x#) (NS y#) =+  bigNatToNat ((x# `bigNatMulWord#` y#) `bigNatRem` m#)+mulMod (NB m#) (NB x#) (NB y#) =+  bigNatToNat ((x# `bigNatMul` y#) `bigNatRem` m#)++-- | modular multiplication for powers of 2, takes a mask instead of a+-- wrap-around point+mulMod2 :: Natural -> Natural -> Natural -> Natural+mulMod2 (NS m#) (NS x#) (NS y#) = NS (z2# `and#` m#)+  where+    !(# _, z2# #) = timesWord2# x# y#+mulMod2 NS{} _ _ = brokenInvariant+mulMod2 (NB m#) (NS x#) (NS y#) =+  bigNatToNat (bigNatFromWord2# z1# z2# `bigNatAnd` m#)+  where+    !(# z1#, z2# #) = timesWord2# x# y#+mulMod2 (NB m#) (NS x#) (NB y#) =+  bigNatToNat ((y# `bigNatMulWord#` x#) `bigNatAnd` m#)+mulMod2 (NB m#) (NB x#) (NS y#) =+  bigNatToNat ((x# `bigNatMulWord#` y#) `bigNatAnd` m#)+mulMod2 (NB m#) (NB x#) (NB y#) =+  bigNatToNat ((x# `bigNatMul` y#) `bigNatAnd` m#)++-- | modular negations+negateMod :: Natural -> Natural -> Natural+negateMod _ (NS 0##) = NS 0##+negateMod (NS m#) (NS x#) = NS (m# `minusWord#` x#)+negateMod NS{} _ = brokenInvariant+negateMod (NB m#) (NS x#) = bigNatToNat (m# `bigNatSubWordUnsafe#` x#)+negateMod (NB m#) (NB x#) = bigNatToNat (m# `bigNatSubUnsafe`      x#)++-- | Given a size in bits, return a function that complements the bits in a+-- 'Natural' up to that size.+complementMod+  :: Natural+  -> (Natural -> Natural)+complementMod (NS sz#) =+  if isTrue# (sz# `leWord#` WORD_SIZE_IN_BITS##) then+    let m# = if isTrue# (sz# `eqWord#` WORD_SIZE_IN_BITS##) then+#if WORD_SIZE_IN_BITS == 64+                0xFFFFFFFFFFFFFFFF##+#elif WORD_SIZE_IN_BITS == 32+                0xFFFFFFFF##+#else+#error Unhandled value for WORD_SIZE_IN_BITS+#endif+             else+               (1## `uncheckedShiftL#` (word2Int# sz#)) `minusWord#` 1##+        go (NS x#) = NS (x# `xor#` m#)+        go (NB r#) = NS (bigNatToWord# r# `xor#` m#)+    in  go+  else+    let m# = bigNatBit# sz# `bigNatSubWordUnsafe#` 1##++        go (NS x#) = bigNatToNat (bigNatXor (bigNatFromWord# x#) m#)+        go (NB x#) = bigNatToNat (bigNatXor x# m#)+    in  go+complementMod _ = error "size too large"++-- | Keep all the bits up to a certain size+maskMod+  :: Natural+  -> (Natural -> Natural)+maskMod (NS sz#) =+  if isTrue# (sz# `leWord#` WORD_SIZE_IN_BITS##) then+    if isTrue# (sz# `eqWord#` WORD_SIZE_IN_BITS##) then+       -- Mask equal to the word size+       let go (NB x#) = NS (bigNatToWord# x#)+           go n          = n+       in  go+    else+       let m# = (1## `uncheckedShiftL#` (word2Int# sz#)) `minusWord#` 1##++           go (NS x#) = NS (x# `and#` m#)+           go (NB x#) = NS (bigNatToWord# x# `and#` m#)+       in  go+  else+    let m# = bigNatBit# sz#++        -- faster than `bigNatAnd (m# `minuxBigNatWord` 1##)`+        go (NB x#) = bigNatToNat (bigNatRem x# m#)+        -- The mask is larger than the word size, so we can keep all the bits+        go x = x+    in  go+maskMod _ = error "size too large"++bigNatToNat :: BigNat# -> Natural+bigNatToNat r# =+  if isTrue# (bigNatSize# r# <=# 1#) then+    NS (bigNatToWord# r#)+  else+    NB r#++subIfGe :: BigNat# -> BigNat# -> Natural+subIfGe z# m# = case z# `bigNatCompare` m# of+  LT -> NB z#+  EQ -> NS 0##+  GT -> bigNatToNat (z# `bigNatSubUnsafe` m#)+#else+-- | modular subtraction+subMod :: Natural -> Natural -> Natural -> Natural subMod (NatS# m#) (NatS# x#) (NatS# y#) =   if isTrue# (x# `geWord#` y#) then NatS# z# else NatS# (z# `plusWord#` m#)   where@@ -205,6 +366,7 @@ naturalToInteger :: Natural -> Integer naturalToInteger (NatS# w)  = wordToInteger w naturalToInteger (NatJ# bn) = Jp# bn+#endif #endif  brokenInvariant :: a

@@ -8,6 +8,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -87,7 +88,7 @@ import Data.Default.Class             (Default (..)) import Data.Proxy                     (Proxy (..)) import Text.Read                      (Read (..), ReadPrec)-import Text.Printf                    (PrintfArg (..))+import Text.Printf                    (PrintfArg (..), printf) import GHC.Generics                   (Generic) import GHC.Natural                    (naturalFromInteger) #if MIN_VERSION_base(4,12,0)@@ -98,11 +99,17 @@  import GHC.TypeLits                   (KnownNat, Nat, type (+), natVal) import GHC.TypeLits.Extra             (Max)-import Language.Haskell.TH            (TypeQ, appT, conT, litT, numTyLit, sigE)+import Data.Ix                        (Ix(..))+import Language.Haskell.TH            (appT, conT, litT, numTyLit, sigE) import Language.Haskell.TH.Syntax     (Lift(..)) #if MIN_VERSION_template_haskell(2,16,0) import Language.Haskell.TH.Compat #endif+#if MIN_VERSION_template_haskell(2,17,0)+import Language.Haskell.TH            (Quote, Type)+#else+import Language.Haskell.TH            (TypeQ)+#endif import Test.QuickCheck.Arbitrary      (Arbitrary (..), CoArbitrary (..),                                        arbitraryBoundedIntegral,                                        coarbitraryIntegral, shrinkIntegral)@@ -120,6 +127,8 @@ import Clash.XException   (ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX) +type role Signed nominal+ -- | Arbitrary-width signed integer represented by @n@ bits, including the sign -- bit. --@@ -156,10 +165,26 @@ -- 3 -- >>> satAdd SatSymmetric (-2) (-3) :: Signed 3 -- -3+--+-- Signed has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i Signed+-- type role Signed nominal+-- ...+--+-- as it is not safe to coerce between different width Signed. To change the+-- width, use the functions in the 'Clash.Class.Resize.Resize' class.+#if MIN_VERSION_base(4,15,0)+data Signed (n :: Nat) =+    -- | The constructor, 'S', and the field, 'unsafeToInteger', are not+    -- synthesizable.+    S { unsafeToInteger :: !Integer}+#else newtype Signed (n :: Nat) =     -- | The constructor, 'S', and the field, 'unsafeToInteger', are not     -- synthesizable.     S { unsafeToInteger :: Integer}+#endif   deriving (Data, Generic)  instance NFDataX (Signed n) where@@ -194,13 +219,13 @@  {-# NOINLINE pack# #-} pack# :: forall n . KnownNat n => Signed n -> BitVector n-pack# (S i) = let m = 1 `shiftL` fromInteger (natVal (Proxy @n))+pack# (S i) = let m = 1 `shiftL0` fromInteger (natVal (Proxy @n))               in  if i < 0 then BV 0 (naturalFromInteger (m + i)) else BV 0 (naturalFromInteger i)  {-# NOINLINE unpack# #-} unpack# :: forall n . KnownNat n => BitVector n -> Signed n unpack# (BV 0 i) =-  let m = 1 `shiftL` fromInteger (natVal (Proxy @n) - 1)+  let m = 1 `shiftL0` fromInteger (natVal (Proxy @n) - 1)       n = naturalToInteger i   in  if n >= m then S (n-2*m) else S n unpack# bv = undefError "Signed.unpack" [bv]@@ -236,8 +261,22 @@ -- | The functions: 'enumFrom', 'enumFromThen', 'enumFromTo', and -- 'enumFromThenTo', are not synthesizable. instance KnownNat n => Enum (Signed n) where-  succ           = (+# fromInteger# 1)-  pred           = (-# fromInteger# 1)+  succ n+    | n == maxBound =+        error $ "'succ' was called on (" <> show @(Signed n) maxBound <> " :: "+             <> "Signed " <> show (natToNatural @n) <> ") and caused an "+             <> "overflow. Use 'satSucc' and specify a SaturationMode if you "+             <> "need other behavior."+    | otherwise = n +# fromInteger# 1++  pred n+    | n == minBound =+        error $ "'pred' was called on (" <> show @(Signed n) maxBound <> " :: "+             <> "Signed " <> show (natToNatural @n) <> ") and caused an "+             <> "underflow. Use 'satPred' and specify a SaturationMode if you "+             <> "need other behavior."+    | otherwise = n -# fromInteger# 1+   toEnum         = fromInteger# . toInteger   fromEnum       = fromEnum . toInteger#   enumFrom       = enumFrom#@@ -320,7 +359,7 @@         else           S z  where-  m = 1 `shiftL` fromInteger (natVal (Proxy @n) -1)+  m = 1 `shiftL0` fromInteger (natVal (Proxy @n) -1)  {-# NOINLINE (-#) #-} (-#) =@@ -333,7 +372,7 @@         else           S z  where-  m  = 1 `shiftL` fromInteger (natVal (Proxy @n) -1)+  m  = 1 `shiftL0` fromInteger (natVal (Proxy @n) -1)  {-# NOINLINE (*#) #-} (*#) = \(S a) (S b) -> fromInteger_INLINE sz mB mask (a * b)@@ -348,7 +387,7 @@     let z = negate n     in  if z == m then S n else S z  where-  m = 1 `shiftL` fromInteger (natVal (Proxy @n) -1)+  m = 1 `shiftL0` fromInteger (natVal (Proxy @n) -1)  {-# NOINLINE abs# #-} abs# =@@ -356,7 +395,7 @@     let z = abs n     in  if z == m then S n else S z  where-  m = 1 `shiftL` fromInteger (natVal (Proxy @n) -1)+  m = 1 `shiftL0` fromInteger (natVal (Proxy @n) -1)  {-# NOINLINE fromInteger# #-} fromInteger# :: forall n . KnownNat n => Integer -> Signed (n :: Nat)@@ -372,7 +411,7 @@             i2 = case i `shiftR` sz of                    q | q .&. 1 == 0 -> i1                      | otherwise    -> i1 - mb-        in  if mb == 0 then S 0 else S i2+        in  if sz < 0 then S 0 else S i2  instance ExtendingNum (Signed m) (Signed n) where   type AResult (Signed m) (Signed n) = Signed (Max m n + 1)@@ -548,8 +587,10 @@  {-# NOINLINE resize# #-} resize# :: forall m n . (KnownNat n, KnownNat m) => Signed n -> Signed m-resize# s@(S i) | n' <= m'  = extended-                | otherwise = truncated+resize# s@(S i)+  | natToNatural @m == 0 = S 0+  | n' <= m'  = extended+  | otherwise = truncated   where     n  = fromInteger (natVal s)     n' = shiftL 1 n@@ -579,7 +620,11 @@   liftTyped = liftTypedFromUntyped #endif +#if MIN_VERSION_template_haskell(2,17,0)+decSigned :: Quote m => Integer -> m Type+#else decSigned :: Integer -> TypeQ+#endif decSigned n = appT (conT ''Signed) (litT $ numTyLit n)  instance KnownNat n => SaturatingNum (Signed n) where@@ -636,7 +681,7 @@     let r        = times# a b         (rL,rR)  = split r         overflow = complement (reduceOr (BV.pack# (msb rR) ++# pack rL)) .|.-                              reduceAnd (BV.pack# (msb rR) ++# pack rL)+                   reduceAnd (BV.pack# (msb rR) ++# pack rL)     in  case overflow of           1 -> unpack# rR           _ -> case msb rL of@@ -646,7 +691,7 @@     let r        = times# a b         (rL,rR)  = split r         overflow = complement (reduceOr (BV.pack# (msb rR) ++# pack rL)) .|.-                              reduceAnd (BV.pack# (msb rR) ++# pack rL)+                   reduceAnd (BV.pack# (msb rR) ++# pack rL)     in  case overflow of           1 -> unpack# rR           _ -> fromInteger# 0@@ -654,7 +699,7 @@     let r        = times# a b         (rL,rR)  = split r         overflow = complement (reduceOr (BV.pack# (msb rR) ++# pack rL)) .|.-                              reduceAnd (BV.pack# (msb rR) ++# pack rL)+                   reduceAnd (BV.pack# (msb rR) ++# pack rL)     in  case overflow of           1 -> unpack# rR           _ -> case msb rL of@@ -692,3 +737,19 @@ instance KnownNat n => Ixed (Signed n) where   ix i f s = unpack# <$> BV.replaceBit# (pack# s) i                      <$> f (BV.index# (pack# s) i)++instance (KnownNat n) => Ix (Signed n) where+  range (a, b) = [a..b]+  index ab@(a, b) x+    | inRange ab x = fromIntegral $ x - a+    | otherwise = error $ printf "Index %d out of bounds (%d, %d) ab" x a b+  inRange (a, b) x = a <= x && x <= b++-- | Shift left that ties to zero on negative shifts+shiftL0 :: Integer -> Int -> Integer+#if MIN_VERSION_base(4,15,0)+shiftL0 = \a sh -> if sh >= 0 then shiftL a sh else 0+#else+shiftL0 = shiftL -- True for use with this module+#endif+{-# INLINE shiftL0 #-}

@@ -8,6 +8,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -85,22 +86,41 @@ import Data.Default.Class             (Default (..)) import Data.Proxy                     (Proxy (..)) import Text.Read                      (Read (..), ReadPrec)-import Text.Printf                    (PrintfArg (..))+import Text.Printf                    (PrintfArg (..), printf) import GHC.Exts                       (narrow8Word#, narrow16Word#, narrow32Word#) import GHC.Generics                   (Generic)+#if MIN_VERSION_base(4,15,0)+import GHC.Num.BigNat                 (bigNatToWord, bigNatToWord#)+import GHC.Num.Integer+  (integerFromNatural, integerShiftL, integerToNatural)+import GHC.Num.Natural+  (Natural (..), naturalShiftL, naturalShiftR, naturalToWord)+#else import GHC.Integer.GMP.Internals      (bigNatToWord) import GHC.Natural                    (Natural (..), naturalFromInteger)+#endif #if MIN_VERSION_base(4,12,0) import GHC.Natural                    (naturalToInteger) #endif-import GHC.TypeLits                   (KnownNat, Nat, type (+), natVal)+import GHC.TypeLits                   (KnownNat, Nat, type (+))+#if MIN_VERSION_base(4,15,0)+import GHC.TypeNats                   (natVal)+#else+import GHC.TypeLits                   (natVal)+#endif import GHC.TypeLits.Extra             (Max) import GHC.Word                       (Word (..), Word8 (..), Word16 (..), Word32 (..))-import Language.Haskell.TH            (TypeQ, appT, conT, litT, numTyLit, sigE)+import Data.Ix                        (Ix(..))+import Language.Haskell.TH            (appT, conT, litT, numTyLit, sigE) import Language.Haskell.TH.Syntax     (Lift(..)) #if MIN_VERSION_template_haskell(2,16,0) import Language.Haskell.TH.Compat #endif+#if MIN_VERSION_template_haskell(2,17,0)+import Language.Haskell.TH            (Quote, Type)+#else+import Language.Haskell.TH            (TypeQ)+#endif import Test.QuickCheck.Arbitrary      (Arbitrary (..), CoArbitrary (..),                                        arbitraryBoundedIntegral,                                        coarbitraryIntegral)@@ -112,7 +132,7 @@ import Clash.Class.Resize             (Resize (..)) import Clash.Prelude.BitIndex         ((!), msb, replaceBit, split) import Clash.Prelude.BitReduction     (reduceOr)-import Clash.Promoted.Nat             (natToNum)+import Clash.Promoted.Nat             (natToNum, natToNatural) import Clash.Sized.Internal.BitVector (BitVector (BV), Bit, high, low, undefError) import qualified Clash.Sized.Internal.BitVector as BV import Clash.Sized.Internal.Mod@@ -121,6 +141,8 @@  #include "MachDeps.h" +type role Unsigned nominal+ -- | Arbitrary-width unsigned integer represented by @n@ bits -- -- Given @n@ bits, an 'Unsigned' @n@ number has a range of: [0 .. 2^@n@-1]@@ -152,15 +174,35 @@ -- 7 -- >>> satSub SatSymmetric 2 3 :: Unsigned 3 -- 0-newtype Unsigned (n :: Nat) =+--+-- Unsigned has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>+--+-- >>> :i Unsigned+-- type role Unsigned nominal+-- ...+--+-- as it is not safe to coerce between different width Unsigned. To change the+-- width, use the functions in the 'Clash.Class.Resize.Resize' class.+#if MIN_VERSION_base(4,15,0)+data Unsigned (n :: Nat) =     -- | The constructor, 'U', and the field, 'unsafeToInteger', are not     -- synthesizable.+    U { unsafeToNatural :: !Natural }+#else+newtype Unsigned (n :: Nat) =+    -- | The constructor, 'U', and the field, 'unsafeToNatural', are not+    -- synthesizable.     U { unsafeToNatural :: Natural }+#endif   deriving (Data, Generic)  {-# NOINLINE size# #-} size# :: KnownNat n => Unsigned n -> Int+#if MIN_VERSION_base(4,15,0)+size# u = fromIntegral (natVal u)+#else size# u = fromInteger (natVal u)+#endif  instance NFData (Unsigned n) where   rnf (U i) = rnf i `seq` ()@@ -228,8 +270,22 @@ -- | The functions: 'enumFrom', 'enumFromThen', 'enumFromTo', and -- 'enumFromThenTo', are not synthesizable. instance KnownNat n => Enum (Unsigned n) where-  succ           = (+# fromInteger# 1)-  pred           = (-# fromInteger# 1)+  succ n+    | n == maxBound =+        error $ "'succ' was called on (" <> show @(Unsigned n) maxBound <> " :: "+             <> "Unsigned " <> show (natToNatural @n) <> ") and caused an "+             <> "overflow. Use 'satSucc' and specify a SaturationMode if you "+             <> "need other behavior."+    | otherwise = n +# fromInteger# 1++  pred n+    | n == minBound =+        error $ "'pred' was called on (" <> show @(Unsigned n) maxBound <> " :: "+             <> "Unsigned " <> show (natToNatural @n) <> ") and caused an "+             <> "underflow. Use 'satPred' and specify a SaturationMode if you "+             <> "need other behavior."+    | otherwise = n -# fromInteger# 1+   toEnum         = fromInteger# . toInteger   fromEnum       = fromEnum . toInteger#   enumFrom       = enumFrom#@@ -239,7 +295,11 @@  enumFrom# :: forall n. KnownNat n => Unsigned n -> [Unsigned n] enumFrom# = \x -> map (U . (`mod` m)) [unsafeToNatural x .. unsafeToNatural (maxBound :: Unsigned n)]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif {-# NOINLINE enumFrom# #-}  enumFromThen# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> [Unsigned n]@@ -247,17 +307,29 @@  where   toUnsigneds = map (U . (`mod` m))   bound x y = unsafeToNatural (if x <= y then maxBound else minBound :: Unsigned n)+#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif {-# NOINLINE enumFromThen# #-}  enumFromTo# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> [Unsigned n] enumFromTo# = \x y -> map (U . (`mod` m)) [unsafeToNatural x .. unsafeToNatural y]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif {-# NOINLINE enumFromTo# #-}  enumFromThenTo# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n] enumFromThenTo# = \x1 x2 y -> map (U . (`mod` m)) [unsafeToNatural x1, unsafeToNatural x2 .. unsafeToNatural y]+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif {-# NOINLINE enumFromThenTo# #-}  instance KnownNat n => Bounded (Unsigned n) where@@ -284,26 +356,48 @@ (+#),(-#),(*#) :: forall n . KnownNat n => Unsigned n -> Unsigned n -> Unsigned n {-# NOINLINE (+#) #-} (+#) = \(U i) (U j) -> U (addMod m i j)+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE (-#) #-} (-#) = \(U i) (U j) -> U (subMod m i j)+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE (*#) #-} (*#) = \(U i) (U j) -> U (mulMod2 m i j)+#if MIN_VERSION_base(4,15,0)+  where m = (1 `naturalShiftL` naturalToWord (natVal (Proxy @n))) - 1+#else   where m = (1 `shiftL` fromInteger (natVal (Proxy @n))) - 1+#endif  {-# NOINLINE negate# #-} negate# :: forall n . KnownNat n => Unsigned n -> Unsigned n negate# = \(U i) -> U (negateMod m i)+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE fromInteger# #-} fromInteger# :: forall n . KnownNat n => Integer -> Unsigned n+#if MIN_VERSION_base(4,15,0)+fromInteger# = \x -> U (integerToNatural (x `mod` m))+ where+  m = 1 `integerShiftL` naturalToWord (natVal (Proxy @n))+#else fromInteger# = \x -> U (naturalFromInteger (x `mod` m))  where   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  instance (KnownNat m, KnownNat n) => ExtendingNum (Unsigned m) (Unsigned n) where   type AResult (Unsigned m) (Unsigned n) = Unsigned (Max m n + 1)@@ -321,8 +415,13 @@                                                 -> Unsigned (Max m n + 1) minus# = \(U a) (U b) -> U (subMod mask a b)  where+#if MIN_VERSION_base(4,15,0)+  sz   = naturalToWord (natVal (Proxy @(Max m n + 1)))+  mask = 1 `naturalShiftL` sz+#else   sz   = fromInteger (natVal (Proxy @(Max m n + 1)))   mask = 1 `shiftL` sz+#endif  {-# NOINLINE times# #-} times# :: Unsigned m -> Unsigned n -> Unsigned (m + n)@@ -399,11 +498,19 @@ shiftL# =   \(U v) i ->     if i >= 0 then+#if MIN_VERSION_base+      U ((naturalShiftL v i) `mod` m)+#else       U ((shiftL v i) `mod` m)+#endif     else       error ("'shiftL undefined for negative number: " ++ show i)  where+#if MIN_VERSION_base(4,15,0)+  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))+#else   m = 1 `shiftL` fromInteger (natVal (Proxy @n))+#endif  {-# NOINLINE shiftR# #-} -- shiftR# doesn't need the KnownNat constraint@@ -418,32 +525,55 @@ rotateL# =   \(U n) b ->     if b >= 0 then+#if MIN_VERSION_base(4,15,0)+      let l   = naturalShiftL n b'+          r   = naturalShiftR n b''+          b'  = fromIntegral b `mod` sz+#else       let l   = shiftL n b'           r   = shiftR n b''           b'  = b `mod` sz+#endif           b'' = sz - b'       in  U ((l .|. r) `mod` m)     else       error "'rotateL undefined for negative numbers"   where+#if MIN_VERSION_base(4,15,0)+    sz = naturalToWord (natVal (Proxy @n))+    m  = 1 `naturalShiftL` sz+#else     sz = fromInteger (natVal (Proxy @n)) :: Int     m  = 1 `shiftL` sz+#endif  {-# NOINLINE rotateR# #-} rotateR# =   \(U n) b ->     if b >= 0 then+#if MIN_VERSION_base(4,15,0)+      let l   = naturalShiftR n b'+          r   = naturalShiftL n b''+          b'  = fromIntegral b `mod` sz+#else       let l   = shiftR n b'           r   = shiftL n b''           b'  = b `mod` sz+#endif           b'' = sz - b'       in  U ((l .|. r) `mod` m)     else       error "'rotateR undefined for negative numbers"   where+#if MIN_VERSION_base(4,15,0)+    sz = naturalToWord (natVal (Proxy @n))+    m  = 1 `naturalShiftL` sz+#else     sz = fromInteger (natVal (Proxy @n)) :: Int     m  = 1 `shiftL` sz+#endif + instance KnownNat n => FiniteBits (Unsigned n) where   finiteBitSize        = size#   countLeadingZeros  u = countLeadingZeros  (pack# u)@@ -457,7 +587,11 @@ {-# NOINLINE resize# #-} resize# :: forall n m . KnownNat m => Unsigned n -> Unsigned m resize# = \(U i) -> if i >= m then U (i `mod` m) else U i+#if MIN_VERSION_base(4,15,0)+  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @m))+#else   where m = 1 `shiftL` fromInteger (natVal (Proxy @m))+#endif  instance Default (Unsigned n) where   def = minBound#@@ -469,8 +603,13 @@   liftTyped = liftTypedFromUntyped #endif +#if MIN_VERSION_template_haskell(2,17,0)+decUnsigned :: Quote m => Natural -> m Type+decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit (integerFromNatural n))+#else decUnsigned :: Integer -> TypeQ decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit n)+#endif  instance KnownNat n => SaturatingNum (Unsigned n) where   satAdd SatWrap a b = a +# b@@ -519,24 +658,51 @@   ix i f s = unpack# <$> BV.replaceBit# (pack# s) i                      <$> f (BV.index# (pack# s) i) +instance (KnownNat n) => Ix (Unsigned n) where+  range (a, b) = [a..b]+  index ab@(a, b) x+    | inRange ab x = fromIntegral $ x - a+    | otherwise = error $ printf "Index %d out of bounds (%d, %d) ab" x a b+  inRange (a, b) x = a <= x && x <= b+ unsignedToWord :: Unsigned WORD_SIZE_IN_BITS -> Word+#if MIN_VERSION_base(4,15,0)+unsignedToWord (U (NS u#)) = W# u#+unsignedToWord (U (NB u#)) = bigNatToWord u#+#else unsignedToWord (U (NatS# u#)) = W# u# unsignedToWord (U (NatJ# u#)) = W# (bigNatToWord u#)+#endif {-# NOINLINE unsignedToWord #-}  unsigned8toWord8 :: Unsigned 8 -> Word8+#if MIN_VERSION_base(4,15,0)+unsigned8toWord8 (U (NS u#)) = W8# (narrow8Word# u#)+unsigned8toWord8 (U (NB u#)) = W8# (narrow8Word# (bigNatToWord# u#))+#else unsigned8toWord8 (U (NatS# u#)) = W8# (narrow8Word# u#) unsigned8toWord8 (U (NatJ# u#)) = W8# (narrow8Word# (bigNatToWord u#))+#endif {-# NOINLINE unsigned8toWord8 #-}  unsigned16toWord16 :: Unsigned 16 -> Word16+#if MIN_VERSION_base(4,15,0)+unsigned16toWord16 (U (NS u#)) = W16# (narrow16Word# u#)+unsigned16toWord16 (U (NB u#)) = W16# (narrow16Word# (bigNatToWord# u#))+#else unsigned16toWord16 (U (NatS# u#)) = W16# (narrow16Word# u#) unsigned16toWord16 (U (NatJ# u#)) = W16# (narrow16Word# (bigNatToWord u#))+#endif {-# NOINLINE unsigned16toWord16 #-}  unsigned32toWord32 :: Unsigned 32 -> Word32+#if MIN_VERSION_base(4,15,0)+unsigned32toWord32 (U (NS u#)) = W32# (narrow32Word# u#)+unsigned32toWord32 (U (NB u#)) = W32# (narrow32Word# (bigNatToWord# u#))+#else unsigned32toWord32 (U (NatS# u#)) = W32# (narrow32Word# u#) unsigned32toWord32 (U (NatJ# u#)) = W32# (narrow32Word# (bigNatToWord u#))+#endif {-# NOINLINE unsigned32toWord32 #-}  {-# RULES

@@ -242,93 +242,118 @@   ensureSpine = fmap ensureSpine . lazyT  --- | A /dependently/ typed fold over trees.------ As an example of when you might want to use 'dtfold' we will build a--- population counter: a circuit that counts the number of bits set to '1' in--- a 'BitVector'. Given a vector of /n/ bits, we only need we need a data type--- that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@ has a range--- of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.--- As an initial attempt we will use 'tfold', because it gives a nice (@log2(n)@)--- tree-structure of adders:------ @--- populationCount :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))---                 => BitVector (2^d) -> Index (2^d+1)--- populationCount = tfold fromIntegral (+) . v2t . bv2v--- @------ The \"problem\" with this description is that all adders have the same--- bit-width, i.e. all adders are of the type:------ @--- (+) :: 'Index' (2^d+1) -> 'Index' (2^d+1) -> 'Index' (2^d+1).--- @------ This is a \"problem\" because we could have a more efficient structure:--- one where each layer of adders is /precisely/ wide enough to count the number--- of bits at that layer. That is, at height /d/ we want the adder to be of--- type:------ @--- 'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)--- @------ We have such an adder in the form of the 'Clash.Class.Num.add' function, as--- defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.--- However, we cannot simply use 'fold' to create a tree-structure of--- 'Clash.Class.Num.add'es:------ >>> :{--- let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))---                      => BitVector (2^d) -> Index (2^d+1)---     populationCount' = tfold fromIntegral add . v2t . bv2v--- :}--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘(((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1’---                      with ‘(2 ^ d) + 1’---       Expected type: Index ((2 ^ d) + 1)---                      -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1)---         Actual type: Index ((2 ^ d) + 1)---                      -> Index ((2 ^ d) + 1)---                      -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1))---     • In the second argument of ‘tfold’, namely ‘add’---       In the first argument of ‘(.)’, namely ‘tfold fromIntegral add’---       In the expression: tfold fromIntegral add . v2t . bv2v---     • Relevant bindings include---         populationCount' :: BitVector (2 ^ d) -> Index ((2 ^ d) + 1)---           (bound at ...)------ because 'tfold' expects a function of type \"@b -> b -> b@\", i.e. a function--- where the arguments and result all have exactly the same type.------ In order to accommodate the type of our 'Clash.Class.Num.add', where the--- result is larger than the arguments, we must use a dependently typed fold in--- the form of 'dtfold':------ @--- {\-\# LANGUAGE UndecidableInstances \#-\}--- import Data.Singletons.Prelude--- import Data.Proxy------ data IIndex (f :: 'TyFun' Nat *) :: *--- type instance 'Apply' IIndex l = 'Index' ((2^l)+1)------ populationCount' :: (KnownNat k, KnownNat (2^k))---                  => BitVector (2^k) -> Index ((2^k)+1)--- populationCount' bv = 'tdfold' (Proxy @IIndex)---                              fromIntegral---                              (\\_ x y -> 'Clash.Class.Num.add' x y)---                              ('v2t' ('Clash.Sized.Vector.bv2v' bv))--- @------ And we can test that it works:------ >>> :t populationCount' (7 :: BitVector 16)--- populationCount' (7 :: BitVector 16) :: Index 17--- >>> populationCount' (7 :: BitVector 16)--- 3+{- | A /dependently/ typed fold over trees.++As an example of when you might want to use 'dtfold' we will build a+population counter: a circuit that counts the number of bits set to '1' in+a 'Clash.Sized.BitVector.BitVector'. Given a vector of /n/ bits, we only need we+need a data type that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@+has a range of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.+As an initial attempt we will use 'tfold', because it gives a nice (@log2(n)@)+tree-structure of adders:++@+populationCount :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))+                => BitVector (2^d) -> Index (2^d+1)+populationCount = tfold fromIntegral (+) . v2t . bv2v+@++The \"problem\" with this description is that all adders have the same+bit-width, i.e. all adders are of the type:++@+(+) :: 'Index' (2^d+1) -> 'Index' (2^d+1) -> 'Index' (2^d+1).+@++This is a \"problem\" because we could have a more efficient structure:+one where each layer of adders is /precisely/ wide enough to count the number+of bits at that layer. That is, at height /d/ we want the adder to be of+type:++@+'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)+@++We have such an adder in the form of the 'Clash.Class.Num.add' function, as+defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.+However, we cannot simply use 'Clash.Sized.Vector.fold' to create a tree-structure of+'Clash.Class.Num.add'es:+#if __GLASGOW_HASKELL__ >= 900+>>> :{+let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))+                     => BitVector (2^d) -> Index (2^d+1)+    populationCount' = tfold fromIntegral add . v2t . bv2v+:}+<BLANKLINE>+<interactive>:...+    • Couldn't match type: (((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1+                     with: (2 ^ d) + 1+      Expected: Index ((2 ^ d) + 1)+                -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1)+        Actual: Index ((2 ^ d) + 1)+                -> Index ((2 ^ d) + 1)+                -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1))+    • In the second argument of ‘tfold’, namely ‘add’+      In the first argument of ‘(.)’, namely ‘tfold fromIntegral add’+      In the expression: tfold fromIntegral add . v2t . bv2v+    • Relevant bindings include+        populationCount' :: BitVector (2 ^ d) -> Index ((2 ^ d) + 1)+          (bound at ...)++#else+>>> :{+let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))+                     => BitVector (2^d) -> Index (2^d+1)+    populationCount' = tfold fromIntegral add . v2t . bv2v+:}+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘(((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1’+                     with ‘(2 ^ d) + 1’+      Expected type: Index ((2 ^ d) + 1)+                     -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1)+        Actual type: Index ((2 ^ d) + 1)+                     -> Index ((2 ^ d) + 1)+                     -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1))+    • In the second argument of ‘tfold’, namely ‘add’+      In the first argument of ‘(.)’, namely ‘tfold fromIntegral add’+      In the expression: tfold fromIntegral add . v2t . bv2v+    • Relevant bindings include+        populationCount' :: BitVector (2 ^ d) -> Index ((2 ^ d) + 1)+          (bound at ...)++#endif++because 'tfold' expects a function of type \"@b -> b -> b@\", i.e. a function+where the arguments and result all have exactly the same type.++In order to accommodate the type of our 'Clash.Class.Num.add', where the+result is larger than the arguments, we must use a dependently typed fold in+the form of 'dtfold':++@+{\-\# LANGUAGE UndecidableInstances \#-\}+import Data.Singletons.Prelude+import Data.Proxy++data IIndex (f :: 'TyFun' Nat *) :: *+type instance 'Apply' IIndex l = 'Index' ((2^l)+1)++populationCount' :: (KnownNat k, KnownNat (2^k))+                 => BitVector (2^k) -> Index ((2^k)+1)+populationCount' bv = 'tdfold' (Proxy @IIndex)+                             fromIntegral+                             (\\_ x y -> 'Clash.Class.Num.add' x y)+                             ('v2t' ('Clash.Sized.Vector.bv2v' bv))+@++And we can test that it works:++>>> :t populationCount' (7 :: BitVector 16)+populationCount' (7 :: BitVector 16) :: Index 17+>>> populationCount' (7 :: BitVector 16)+3+-} tdfold :: forall p k a . KnownNat k        => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/        -> (a -> (p @@ 0)) -- ^ Function to apply to the elements on the leafs@@ -498,7 +523,7 @@      br _ (l1,r1) (l2,r2) = (BR l1 l2, BR r1 r2) --- | Given a function 'f' that is strict in its /n/th 'RTree' argument, make it+-- | Given a function @f@ that is strict in its /n/th 'RTree' argument, make it -- lazy by applying 'lazyT' to this argument: -- -- > f x0 x1 .. (lazyT xn) .. xn_plus_k

@@ -13,6 +13,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE QuasiQuotes #-}  {-# LANGUAGE Trustworthy #-} @@ -81,6 +82,8 @@   , windows1d, windows2d     -- * Conversions   , toList+  , fromList+  , unsafeFromList   , bv2v   , v2bv     -- * Misc@@ -124,15 +127,17 @@                                           repeat, replicate, reverse, scanl,                                           scanr, splitAt, tail, take, unzip,                                           unzip3, zip, zip3, zipWith, zipWith3)+import qualified Data.String.Interpolate as I import qualified Prelude          as P-import Test.QuickCheck            (Arbitrary (..), CoArbitrary (..))+import Test.QuickCheck+  (Arbitrary(arbitrary, shrink), CoArbitrary(coarbitrary)) import Unsafe.Coerce              (unsafeCoerce)  import Clash.Annotations.Primitive-  (Primitive(InlinePrimitive), HDL(..))+  (Primitive(InlinePrimitive), HDL(..), dontTranslate) import Clash.Promoted.Nat   (SNat (..), SNatLE (..), UNat (..), compareSNat, leToPlus, pow2SNat,-   snatProxy, snatToInteger, subSNat, withSNat, toUNat)+   snatProxy, snatToInteger, subSNat, withSNat, toUNat, natToInteger) import Clash.Promoted.Nat.Literals (d1) import Clash.Sized.Internal.BitVector (Bit, BitVector (..), split#) import Clash.Sized.Index          (Index)@@ -152,6 +157,7 @@ >>> import Clash.Prelude >>> import Data.Kind >>> import Data.Proxy+>>> import qualified Clash.Sized.Vector as Vec >>> let compareSwapL a b = if a < b then (a,b) else (b,a) >>> :{ let sortV xs = map fst sorted :< (snd (last sorted))@@ -396,71 +402,135 @@ singleton = (`Cons` Nil)  {-# NOINLINE head #-}--- | Extract the first element of a vector------ >>> head (1:>2:>3:>Nil)--- 1--- >>> head Nil--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘1’ with ‘0’---       Expected type: Vec (0 + 1) a---         Actual type: Vec 0 a---     • In the first argument of ‘head’, namely ‘Nil’---       In the expression: head Nil---       In an equation for ‘it’: it = head Nil+{- | Extract the first element of a vector++>>> head (1:>2:>3:>Nil)+1++#if __GLASGOW_HASKELL__ >= 900+>>> head Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected: Vec (0 + 1) a+        Actual: Vec 0 a+    • In the first argument of ‘head’, namely ‘Nil’+      In the expression: head Nil+      In an equation for ‘it’: it = head Nil++#else+>>> head Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected type: Vec (0 + 1) a+        Actual type: Vec 0 a+    • In the first argument of ‘head’, namely ‘Nil’+      In the expression: head Nil+      In an equation for ‘it’: it = head Nil++#endif+-} head :: Vec (n + 1) a -> a head (x `Cons` _) = x  {-# NOINLINE tail #-}--- | Extract the elements after the head of a vector------ >>> tail (1:>2:>3:>Nil)--- <2,3>--- >>> tail Nil--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘1’ with ‘0’---       Expected type: Vec (0 + 1) a---         Actual type: Vec 0 a---     • In the first argument of ‘tail’, namely ‘Nil’---       In the expression: tail Nil---       In an equation for ‘it’: it = tail Nil+{- | Extract the elements after the head of a vector++>>> tail (1:>2:>3:>Nil)+<2,3>++#if __GLASGOW_HASKELL__ >= 900+>>> tail Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected: Vec (0 + 1) a+        Actual: Vec 0 a+    • In the first argument of ‘tail’, namely ‘Nil’+      In the expression: tail Nil+      In an equation for ‘it’: it = tail Nil++#else+>>> tail Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected type: Vec (0 + 1) a+        Actual type: Vec 0 a+    • In the first argument of ‘tail’, namely ‘Nil’+      In the expression: tail Nil+      In an equation for ‘it’: it = tail Nil++#endif+-} tail :: Vec (n + 1) a -> Vec n a tail (_ `Cons` xs) = xs  {-# NOINLINE last #-}--- | Extract the last element of a vector------ >>> last (1:>2:>3:>Nil)--- 3--- >>> last Nil--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘1’ with ‘0’---       Expected type: Vec (0 + 1) a---         Actual type: Vec 0 a---     • In the first argument of ‘last’, namely ‘Nil’---       In the expression: last Nil---       In an equation for ‘it’: it = last Nil+{- | Extract the last element of a vector++>>> last (1:>2:>3:>Nil)+3++#if __GLASGOW_HASKELL__ >= 900+>>> last Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected: Vec (0 + 1) a+        Actual: Vec 0 a+    • In the first argument of ‘last’, namely ‘Nil’+      In the expression: last Nil+      In an equation for ‘it’: it = last Nil++#else+>>> last Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected type: Vec (0 + 1) a+        Actual type: Vec 0 a+    • In the first argument of ‘last’, namely ‘Nil’+      In the expression: last Nil+      In an equation for ‘it’: it = last Nil++#endif+-} last :: Vec (n + 1) a -> a last (x `Cons` Nil)         = x last (_ `Cons` y `Cons` ys) = last (y `Cons` ys)  {-# NOINLINE init #-}--- | Extract all the elements of a vector except the last element------ >>> init (1:>2:>3:>Nil)--- <1,2>--- >>> init Nil--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘1’ with ‘0’---       Expected type: Vec (0 + 1) a---         Actual type: Vec 0 a---     • In the first argument of ‘init’, namely ‘Nil’---       In the expression: init Nil---       In an equation for ‘it’: it = init Nil+{- | Extract all the elements of a vector except the last element++>>> init (1:>2:>3:>Nil)+<1,2>++#if __GLASGOW_HASKELL__ >= 900+>>> init Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected: Vec (0 + 1) a+        Actual: Vec 0 a+    • In the first argument of ‘init’, namely ‘Nil’+      In the expression: init Nil+      In an equation for ‘it’: it = init Nil++#else+>>> init Nil+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘1’ with ‘0’+      Expected type: Vec (0 + 1) a+        Actual type: Vec 0 a+    • In the first argument of ‘init’, namely ‘Nil’+      In the expression: init Nil+      In an equation for ‘it’: it = init Nil++#endif+-} init :: Vec (n + 1) a -> Vec n a init (_ `Cons` Nil)         = Nil init (x `Cons` y `Cons` ys) = x `Cons` init (y `Cons` ys)@@ -715,21 +785,28 @@     go n (x `Cons` xs) = f n x `Cons` go (n+1) xs {-# NOINLINE imap #-} --- | Zip two vectors with a functions that also takes the elements' indices.------ >>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)--- <*** Exception: X: Clash.Sized.Index: result 3 is out of bounds: [0..1]--- ...--- >>> izipWith (\i a b -> fromIntegral i + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)--- <5,6>------ \"'imap' @f xs@\" corresponds to the following circuit layout:------ <<doc/izipWith.svg>>------ __NB:__ 'izipWith' is /strict/ in its second argument, and /lazy/ in its--- third. This matters when 'izipWith' is used in a recursive setting. See--- 'lazyV' for more information.+{- | Zip two vectors with a functions that also takes the elements' indices.++#if __GLASGOW_HASKELL__ >= 900+>>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)+<*** Exception: X: Clash.Sized.Index: result 2 is out of bounds: [0..1]+...+#else+>>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)+<*** Exception: X: Clash.Sized.Index: result 3 is out of bounds: [0..1]+...+#endif+>>> izipWith (\i a b -> fromIntegral i + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)+<5,6>++\"'imap' @f xs@\" corresponds to the following circuit layout:++<<doc/izipWith.svg>>++__NB:__ 'izipWith' is /strict/ in its second argument, and /lazy/ in its+third. This matters when 'izipWith' is used in a recursive setting. See+'lazyV' for more information.+-} izipWith :: KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b          -> Vec n c izipWith f xs ys = imap (\i -> uncurry (f i)) (zip xs ys)@@ -1021,7 +1098,7 @@ -- \"'fold' @f xs@\" corresponds to the following circuit layout: -- -- <<doc/fold.svg>>-fold :: (a -> a -> a) -> Vec (n + 1) a -> a+fold :: forall n a . (a -> a -> a) -> Vec (n + 1) a -> a fold f vs = fold' (toList vs)   where     fold' [x] = x@@ -1345,24 +1422,41 @@ replace i y xs = replace_int xs (fromEnum i) y {-# INLINE replace #-} --- | \"'take' @n xs@\" returns the /n/-length prefix of /xs/.------ >>> take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)--- <1,2,3>--- >>> take d3               (1:>2:>3:>4:>5:>Nil)--- <1,2,3>--- >>> take d0               (1:>2:>Nil)--- <>--- >>> take d4               (1:>2:>Nil)--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘4 + n0’ with ‘2’---       Expected type: Vec (4 + n0) a---         Actual type: Vec (1 + 1) a---       The type variable ‘n0’ is ambiguous---     • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’---       In the expression: take d4 (1 :> 2 :> Nil)---       In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)+{- | \"'take' @n xs@\" returns the /n/-length prefix of /xs/.++>>> take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)+<1,2,3>+>>> take d3               (1:>2:>3:>4:>5:>Nil)+<1,2,3>+>>> take d0               (1:>2:>Nil)+<>++#if __GLASGOW_HASKELL__ >= 900+>>> take d4               (1:>2:>Nil)+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘4 + n0’ with ‘2’+      Expected: Vec (4 + n0) a+        Actual: Vec (1 + 1) a+      The type variable ‘n0’ is ambiguous+    • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’+      In the expression: take d4 (1 :> 2 :> Nil)+      In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)++#else+>>> take d4               (1:>2:>Nil)+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘4 + n0’ with ‘2’+      Expected type: Vec (4 + n0) a+        Actual type: Vec (1 + 1) a+      The type variable ‘n0’ is ambiguous+    • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’+      In the expression: take d4 (1 :> 2 :> Nil)+      In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)++#endif+-} take :: SNat m -> Vec (m + n) a -> Vec m a take n = fst . splitAt n {-# INLINE take #-}@@ -1504,7 +1598,12 @@   where     xs = init (a `Cons` ws)     ws = map f (lazyV xs)-{-# INLINE iterateI #-}+{-# NOINLINE iterateI #-}+{-# ANN iterateI (InlinePrimitive [VHDL,Verilog,SystemVerilog] [I.i| [{+    "BlackBoxHaskell": {+        "name": "Clash.Sized.Vector.iterateI"+      , "templateFunction": "Clash.Primitives.Sized.Vector.iterateBBF"+    }}] |]) #-}  -- | \"'unfoldr @n f s@\" builds a vector of length @n@ from a seed value @s@, -- where every element @a@ is created by successive calls of @f@ on @s@. Unlike@@ -1844,6 +1943,60 @@ toList = foldr (:) [] {-# INLINE toList #-} +-- | Convert a list to a vector. This function returns Nothing if the size of+-- the list is not equal to the size of the resulting vector.+--+-- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 5 Int)+-- Just <1,2,3,4,5>+--+-- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 3 Int)+-- Nothing+--+-- >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 10 Int)+-- Nothing+--+-- __NB:__ use `listToVecTH` if you want to make a /statically known/ vector+-- __NB:__ this function is not synthesizable+--+fromList :: forall n a. (KnownNat n) => [a] -> Maybe (Vec n a)+fromList xs+  | exactLength (natToInteger @n) xs = Just (unsafeFromList xs)+  | otherwise = Nothing+ where+  exactLength 0 acc = null acc+  exactLength _ []  = False+  exactLength i (_:ys) = exactLength (i - 1) ys+{-# NOINLINE fromList #-}+{-# ANN fromList dontTranslate #-}++-- | Convert a list to a vector. This function always returns a vector of the+-- desired length, by either truncating the list or padding the vector with+-- undefined elements.+--+-- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 5 Int+-- <1,2,3,4,5>+--+-- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 3 Int+-- <1,2,3>+--+-- >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 10 Int+-- <1,2,3,4,5,*** Exception: Clash.Sized.Vector.unsafeFromList: vector larger than list+-- ...+--+-- __NB:__ use `listToVecTH` if you want to make a /statically known/ vector+-- __NB:__ this function is not synthesizable+--+unsafeFromList :: forall n a. (KnownNat n) => [a] -> Vec n a+unsafeFromList = unfoldr SNat go+ where+  go :: [a] -> (a, [a])+  go (x:xs) = (x, xs)+  go [] =+    let item = error "Clash.Sized.Vector.unsafeFromList: vector larger than list"+     in (item, [])+{-# NOINLINE unsafeFromList #-}+{-# ANN unsafeFromList dontTranslate #-}+ -- | Create a vector literal from a list literal. -- -- > $(listToVecTH [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)@@ -2017,104 +2170,128 @@       in  f s' y (go s' ys) {-# NOINLINE dfold #-} --- | A combination of 'dfold' and 'fold': a /dependently/ typed fold that--- reduces a vector in a tree-like structure.------ As an example of when you might want to use 'dtfold' we will build a--- population counter: a circuit that counts the number of bits set to '1' in--- a 'BitVector'. Given a vector of /n/ bits, we only need we need a data type--- that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@ has a range--- of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.--- As an initial attempt we will use 'sum', because it gives a nice (@log2(n)@)--- tree-structure of adders:------ @--- populationCount :: (KnownNat (n+1), KnownNat (n+2))---                 => 'BitVector' (n+1) -> 'Index' (n+2)--- populationCount = sum . map fromIntegral . 'bv2v'--- @------ The \"problem\" with this description is that all adders have the same--- bit-width, i.e. all adders are of the type:------ @--- (+) :: 'Index' (n+2) -> 'Index' (n+2) -> 'Index' (n+2).--- @------ This is a \"problem\" because we could have a more efficient structure:--- one where each layer of adders is /precisely/ wide enough to count the number--- of bits at that layer. That is, at height /d/ we want the adder to be of--- type:------ @--- 'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)--- @------ We have such an adder in the form of the 'Clash.Class.Num.add' function, as--- defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.--- However, we cannot simply use 'fold' to create a tree-structure of--- 'Clash.Class.Num.add'es:------ >>> :{--- let populationCount' :: (KnownNat (n+1), KnownNat (n+2))---                      => BitVector (n+1) -> Index (n+2)---     populationCount' = fold add . map fromIntegral . bv2v--- :}--- <BLANKLINE>--- <interactive>:...---     • Couldn't match type ‘((n + 2) + (n + 2)) - 1’ with ‘n + 2’---       Expected type: Index (n + 2) -> Index (n + 2) -> Index (n + 2)---         Actual type: Index (n + 2)---                      -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))---     • In the first argument of ‘fold’, namely ‘add’---       In the first argument of ‘(.)’, namely ‘fold add’---       In the expression: fold add . map fromIntegral . bv2v---     • Relevant bindings include---         populationCount' :: BitVector (n + 1) -> Index (n + 2)---           (bound at ...)------ because 'fold' expects a function of type \"@a -> a -> a@\", i.e. a function--- where the arguments and result all have exactly the same type.------ In order to accommodate the type of our 'Clash.Class.Num.add', where the--- result is larger than the arguments, we must use a dependently typed fold in--- the form of 'dtfold':------ @--- {\-\# LANGUAGE UndecidableInstances \#-\}--- import Data.Singletons.Prelude--- import Data.Proxy------ data IIndex (f :: 'TyFun' Nat *) :: *--- type instance 'Apply' IIndex l = 'Index' ((2^l)+1)------ populationCount' :: (KnownNat k, KnownNat (2^k))---                  => BitVector (2^k) -> Index ((2^k)+1)--- populationCount' bv = 'dtfold' (Proxy @IIndex)---                              fromIntegral---                              (\\_ x y -> 'Clash.Class.Num.add' x y)---                              ('bv2v' bv)--- @------ And we can test that it works:------ >>> :t populationCount' (7 :: BitVector 16)--- populationCount' (7 :: BitVector 16) :: Index 17--- >>> populationCount' (7 :: BitVector 16)--- 3------ Some final remarks:------   * By using 'dtfold' instead of 'fold', we had to restrict our 'BitVector'---     argument to have bit-width that is a power of 2.---   * Even though our original /populationCount/ function specified a structure---     where all adders had the same width. Most VHDL/(System)Verilog synthesis---     tools will create a more efficient circuit, i.e. one where the adders---     have an increasing bit-width for every layer, from the---     VHDL/(System)Verilog produced by the Clash compiler.------ __NB__: The depth, or delay, of the structure produced by--- \"@'dtfold' m f g xs@\" is O(log_2(@'length' xs@)).+{- | A combination of 'dfold' and 'fold': a /dependently/ typed fold that+reduces a vector in a tree-like structure.++As an example of when you might want to use 'dtfold' we will build a+population counter: a circuit that counts the number of bits set to '1' in+a 'BitVector'. Given a vector of /n/ bits, we only need we need a data type+that can represent the number /n/: 'Index' @(n+1)@. 'Index' @k@ has a range+of @[0 .. k-1]@ (using @ceil(log2(k))@ bits), hence we need 'Index' @n+1@.+As an initial attempt we will use 'sum', because it gives a nice (@log2(n)@)+tree-structure of adders:++@+populationCount :: (KnownNat (n+1), KnownNat (n+2))+                => 'BitVector' (n+1) -> 'Index' (n+2)+populationCount = sum . map fromIntegral . 'bv2v'+@++The \"problem\" with this description is that all adders have the same+bit-width, i.e. all adders are of the type:++@+(+) :: 'Index' (n+2) -> 'Index' (n+2) -> 'Index' (n+2).+@++This is a \"problem\" because we could have a more efficient structure:+one where each layer of adders is /precisely/ wide enough to count the number+of bits at that layer. That is, at height /d/ we want the adder to be of+type:++@+'Index' ((2^d)+1) -> 'Index' ((2^d)+1) -> 'Index' ((2^(d+1))+1)+@++We have such an adder in the form of the 'Clash.Class.Num.add' function, as+defined in the instance 'Clash.Class.Num.ExtendingNum' instance of 'Index'.+However, we cannot simply use 'fold' to create a tree-structure of+'Clash.Class.Num.add'es:++#if __GLASGOW_HASKELL__ >= 900+>>> :{+let populationCount' :: (KnownNat (n+1), KnownNat (n+2))+                     => BitVector (n+1) -> Index (n+2)+    populationCount' = fold add . map fromIntegral . bv2v+:}+<BLANKLINE>+<interactive>:...+    • Couldn't match type: ((n + 2) + (n + 2)) - 1+                     with: n + 2+      Expected: Index (n + 2) -> Index (n + 2) -> Index (n + 2)+        Actual: Index (n + 2)+                -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))+    • In the first argument of ‘fold’, namely ‘add’+      In the first argument of ‘(.)’, namely ‘fold add’+      In the expression: fold add . map fromIntegral . bv2v+    • Relevant bindings include+        populationCount' :: BitVector (n + 1) -> Index (n + 2)+          (bound at ...)++#else+>>> :{+let populationCount' :: (KnownNat (n+1), KnownNat (n+2))+                     => BitVector (n+1) -> Index (n+2)+    populationCount' = fold add . map fromIntegral . bv2v+:}+<BLANKLINE>+<interactive>:...+    • Couldn't match type ‘((n + 2) + (n + 2)) - 1’ with ‘n + 2’+      Expected type: Index (n + 2) -> Index (n + 2) -> Index (n + 2)+        Actual type: Index (n + 2)+                     -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))+    • In the first argument of ‘fold’, namely ‘add’+      In the first argument of ‘(.)’, namely ‘fold add’+      In the expression: fold add . map fromIntegral . bv2v+    • Relevant bindings include+        populationCount' :: BitVector (n + 1) -> Index (n + 2)+          (bound at ...)++#endif++because 'fold' expects a function of type \"@a -> a -> a@\", i.e. a function+where the arguments and result all have exactly the same type.++In order to accommodate the type of our 'Clash.Class.Num.add', where the+result is larger than the arguments, we must use a dependently typed fold in+the form of 'dtfold':++@+{\-\# LANGUAGE UndecidableInstances \#-\}+import Data.Singletons.Prelude+import Data.Proxy++data IIndex (f :: 'TyFun' Nat *) :: *+type instance 'Apply' IIndex l = 'Index' ((2^l)+1)++populationCount' :: (KnownNat k, KnownNat (2^k))+                 => BitVector (2^k) -> Index ((2^k)+1)+populationCount' bv = 'dtfold' (Proxy @IIndex)+                             fromIntegral+                             (\\_ x y -> 'Clash.Class.Num.add' x y)+                             ('bv2v' bv)+@++And we can test that it works:++>>> :t populationCount' (7 :: BitVector 16)+populationCount' (7 :: BitVector 16) :: Index 17+>>> populationCount' (7 :: BitVector 16)+3++Some final remarks:++  * By using 'dtfold' instead of 'fold', we had to restrict our 'BitVector'+    argument to have bit-width that is a power of 2.+  * Even though our original /populationCount/ function specified a structure+    where all adders had the same width. Most VHDL/(System)Verilog synthesis+    tools will create a more efficient circuit, i.e. one where the adders+    have an increasing bit-width for every layer, from the+    VHDL/(System)Verilog produced by the Clash compiler.++__NB__: The depth, or delay, of the structure produced by+\"@'dtfold' m f g xs@\" is O(log_2(@'length' xs@)).+-} dtfold :: forall p k a . KnownNat k        => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/        -> (a -> (p @@ 0)) -- ^ Function to apply to every element@@ -2216,7 +2393,7 @@    . (KnownNat n, KnownNat m)   => BitVector (n * m)   -> Vec n (BitVector m)-unconcatBitVector# orig = snd (go (toUNat (SNat @ n)))+unconcatBitVector# orig = snd (go (toUNat (SNat @n)))   where     go :: forall p . (p <= n) => UNat p -> (BitVector ((n-p)*m), Vec p (BitVector m))     go UZero = (orig,Nil)@@ -2268,7 +2445,7 @@ {-# INLINE forceV #-}  -- | Evaluate all elements of a vector to WHNF, returning the second argument.--- Does not propagate 'XException's.+-- Does not propagate 'Clash.XException.XException's. seqVX   :: KnownNat n   => Vec n a@@ -2280,7 +2457,8 @@ {-# NOINLINE seqVX #-} infixr 0 `seqVX` --- | Evaluate all elements of a vector to WHNF. Does not propagate 'XException's.+-- | Evaluate all elements of a vector to WHNF. Does not propagate+-- 'Clash.XException.XException's. forceVX   :: KnownNat n   => Vec n a