From 36c873b99b12e66da28c749acf3eded5a51a7f13 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Tue, 23 Jun 2026 17:05:03 +0100 Subject: [PATCH 01/21] Fix dropping of error locations Since #14 the error locations often pointed to the end of the circuit instead of the correct location. Locate each generated binding at its circuit expression so GHC blames the offending statement. The regression test is in a separate PR. Co-Authored-By: Claude Fable 5 --- CHANGELOG.md | 7 +++++++ src/CircuitNotation.hs | 8 ++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b009ea6..fbad396 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # Revision history for `circuit-notations` +## Unreleased + +* Fix the source location of type errors on a bus. Since bus tagging was + introduced, such errors pointed at the end of the `circuit` block rather than + at the offending statement. Generated bindings are now located at their + circuit expression so GHC blames the right line. + ## 0.2.0.0 -- 2026-04-23 * Start of the changelog diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index de1220a..cffdcd8 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -980,8 +980,12 @@ circuitQQExpM = do slaves <- L.use circuitSlaves masters <- L.use circuitMasters - -- Construction of the circuit expression - let decs = lets <> map (noLoc . decFromBinding dflags) binds + -- Construction of the circuit expression. + -- Locate each generated binding at its circuit expression so that type + -- errors on a bus are reported on the offending statement rather than at + -- the end of the circuit block (see tests/fixtures/BusError.hs). + let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) + let decs = lets <> map decFromBinding' binds let pats = bindOutputs dflags Fwd masters slaves res = createInputs Bwd slaves masters From 6b884357833ed23c3328a8d58cf6d2f9c3e5075a Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Tue, 23 Jun 2026 18:38:21 +0100 Subject: [PATCH 02/21] Add error-location regression test Compiles tests/fixtures/BusError.hs (a deliberate type error on a bus) with the plugin enabled and asserts that GHC reports the error on the offending line rather than at the end of the circuit block. Under cabal the plugin is found via the package environment file. Under `nix build` the package isn't registered in a package db during its own check phase, so the flake points GHC_PACKAGE_PATH (via the builder's NIX_GHC_PACKAGE_PATH_FOR_TEST hook) at the in-place db, letting the test run for real there too. Co-Authored-By: Claude Fable 5 --- circuit-notation.cabal | 15 +++++++ flake.nix | 12 +++++ tests/error-location.hs | 91 ++++++++++++++++++++++++++++++++++++++ tests/fixtures/BusError.hs | 33 ++++++++++++++ 4 files changed, 151 insertions(+) create mode 100644 tests/error-location.hs create mode 100644 tests/fixtures/BusError.hs diff --git a/circuit-notation.cabal b/circuit-notation.cabal index 849c128..1ca3e70 100644 --- a/circuit-notation.cabal +++ b/circuit-notation.cabal @@ -71,3 +71,18 @@ test-suite library-testsuite base, circuit-notation, clash-prelude >=1.0, + +-- Checks that type errors on a bus point at the offending statement rather than +-- at the end of the circuit (see tests/fixtures/BusError.hs). +test-suite error-location + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: error-location.hs + hs-source-dirs: tests + build-depends: + base, + circuit-notation, + clash-prelude >=1.0, + directory, + filepath, + process, diff --git a/flake.nix b/flake.nix index ff7d5f4..615ba78 100644 --- a/flake.nix +++ b/flake.nix @@ -19,6 +19,18 @@ circuit-notation = prev.developPackage { root = ./.; overrides = _: _: final; + # The error-location test shells out to `ghc` to compile a + # fixture with the plugin enabled (see tests/error-location.hs). + # During the package's own check phase circuit-notation isn't + # registered in any package database yet, so that `ghc` couldn't + # find the plugin. Point GHC_PACKAGE_PATH (via the builder's + # NIX_GHC_PACKAGE_PATH_FOR_TEST hook) at the in-place package db + # so the test runs for real, not just under cabal in CI. + modifier = drv: drv.overrideAttrs (old: { + preCheck = (old.preCheck or "") + '' + export NIX_GHC_PACKAGE_PATH_FOR_TEST="$PWD/dist/package.conf.inplace:$packageConfDir:" + ''; + }); }; }; in diff --git a/tests/error-location.hs b/tests/error-location.hs new file mode 100644 index 0000000..92b576a --- /dev/null +++ b/tests/error-location.hs @@ -0,0 +1,91 @@ +-- | Regression test for the source locations of type errors on buses. +-- +-- When bus tagging (the @BusTag@ wrapping) was introduced, type errors on a +-- bus stopped pointing at the offending statement and instead pointed at the +-- end of the @circuit@ block, which made them very hard to act on. +-- +-- This test compiles 'tests/fixtures/BusError.hs' (which has a deliberate type +-- error on a bus, on the line marked @ERROR HERE@) with plugin enabled and +-- asserts that GHC reports an error /on that line/. It uses the same plain +-- @ghc@ + package-environment-file mechanism that CI already uses to compile +-- the @Example@ module. +module Main (main) where + +import Control.Monad (unless, when) +import Data.List (isInfixOf, isPrefixOf, nub, sort) +import Data.Maybe (mapMaybe) +import System.Directory (getTemporaryDirectory) +import System.Environment (lookupEnv) +import System.Exit (exitFailure) +import System.FilePath (()) +import System.Process (readProcessWithExitCode) +import Text.Read (readMaybe) + +fixture :: FilePath +fixture = "tests" "fixtures" "BusError.hs" + +-- | The marker placed on the erroring statement inside the fixture. It is +-- chosen so that it appears on exactly one line of the fixture. +marker :: String +marker = "bus-error-marker" + +main :: IO () +main = do + src <- readFile fixture + + -- Work out which line the deliberate error is on by finding the marker. + let markedLines = + [ n | (n, l) <- zip [1 :: Int ..] (lines src), marker `isInfixOf` l ] + expectedLine <- case markedLines of + [n] -> pure n + _ -> die $ "expected exactly one line containing " <> show marker + <> " in " <> fixture <> ", found lines " <> show markedLines + + -- Compile the fixture and collect the reported error lines. + ghc <- maybe "ghc" id <$> lookupEnv "GHC" + tmp <- getTemporaryDirectory + let args = + [ "-outputdir", tmp "circuit-notation-error-test" + , "-itests/fixtures" + , fixture + ] + (_code, out, err) <- readProcessWithExitCode ghc args "" + let output = out <> err + errLines = sort . nub $ errorLineNumbers output + + putStrLn $ "ghc reported errors on lines: " <> show errLines + putStrLn $ "expected an error on line: " <> show expectedLine + + when (null errLines) $ + die $ "expected the fixture to fail to compile, but ghc reported no\n\ + \error locations. Full output:\n" <> output + + unless (expectedLine `elem` errLines) $ + die $ "type error on the bus was not reported on the offending line (" + <> show expectedLine <> ").\n" + <> "Instead it was reported on lines " <> show errLines + <> " -- this is the bus-tagging regression where errors point at\n" + <> "the end of the circuit rather than the actual mistake.\n\n" + <> "Full ghc output:\n" <> output + + putStrLn "OK: bus type error points at the offending statement." + +-- | Extract the line numbers from GHC error messages that refer to the fixture, +-- e.g. a line @tests/fixtures/BusError.hs:30:8: error: ...@ yields @30@. +errorLineNumbers :: String -> [Int] +errorLineNumbers = mapMaybe parseLine . lines + where + parseLine l = do + let l' = dropWhile (== ' ') l + rest <- stripFixturePrefix l' + let lineStr = takeWhile (/= ':') rest + readMaybe lineStr + + stripFixturePrefix l + | (fixture <> ":") `isPrefixOf` l = Just (drop (length fixture + 1) l) + | otherwise = Nothing + +die :: String -> IO a +die msg = do + putStrLn ("error-location test failed: " <> msg) + exitFailure diff --git a/tests/fixtures/BusError.hs b/tests/fixtures/BusError.hs new file mode 100644 index 0000000..5b743b8 --- /dev/null +++ b/tests/fixtures/BusError.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture that deliberately contains a type error on a bus, used by the +-- error-location test. The error is on the statement tagged with the marker +-- comment below: @boolC@ forces its input to be a +-- @Signal dom Bool@, but the bus @b@ carries a @Signal dom Int@. +-- +-- Crucially the erroring statement is /not/ the last statement of the circuit. +-- Before bus tagging gained source locations, GHC blamed the final statement +-- of the circuit (the @idC -< e@ line) instead of the actual mismatch, which +-- made the error very hard to track down. The test asserts that GHC points at +-- the tagged line. +module BusError where + +import Circuit +import Clash.Prelude + +boolC :: Circuit (Signal dom Bool) (Signal dom Bool) +boolC = idC + +busError :: Circuit (Signal dom Int) (Signal dom Int) +busError = circuit $ \a -> do + b <- idC -< a + c <- boolC -< b -- bus-error-marker + d <- idC -< c + e <- idC -< d + idC -< e From 4849612130730f0f599bdf7e7663dfcd27ef9331 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 00:07:50 +0100 Subject: [PATCH 03/21] First version of value circuits --- CHANGELOG.md | 5 + README.md | 37 ++++++++ circuit-notation.cabal | 4 +- example/ValueCircuits.hs | 117 ++++++++++++++++++++++++ src/CircuitNotation.hs | 193 ++++++++++++++++++++++++++++++++++++--- tests/unittests.hs | 30 +++++- 6 files changed, 369 insertions(+), 17 deletions(-) create mode 100644 example/ValueCircuits.hs diff --git a/CHANGELOG.md b/CHANGELOG.md index fbad396..9bfcc63 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,11 @@ ## Unreleased +* Add value-level circuits via the new `circuitS` keyword. The circuit's + logic is written over the values sampled each clock cycle (marked with + `Signal`/`Fwd` patterns and expressions); the plugin lifts it back to the + signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a + lazy let binding. See the README and example/ValueCircuits.hs. * Fix the source location of type errors on a bus. Since bus tagging was introduced, such errors pointed at the end of the `circuit` block rather than at the offending statement. Generated bindings are now located at their diff --git a/README.md b/README.md index b50bead..9822412 100644 --- a/README.md +++ b/README.md @@ -2,3 +2,40 @@ This is a plugin for manipulating circuits in clash with arrow notation. See example/Example.hs for example usage. Also see [clash-protocols](https://github.com/clash-lang/clash-protocols#). + +## Value-level circuits (`circuitS`) + +The `circuitS` keyword describes a circuit's logic over the *values sampled +each clock cycle* instead of over whole buses. The boundary between bus land +and value land is marked with `Signal` (or `Fwd`): + +- `Signal n <- … -< …` binds `n` to the per-cycle value carried on that bus. +- `… -< Signal e` injects the per-cycle value `e` back onto a bus. + +Everything in between — the `let` bindings of the do block — is ordinary pure +Haskell, and feedback loops are written as ordinary recursive `let`s: + +```haskell +counter3 :: Circuit (Signal dom Bool) (Signal dom Int) +counter3 = circuitS \_bs -> do + Signal n <- registerC 0 -< Signal n' -- n :: Int (this cycle's value) + Signal m <- registerC 8 -< Signal m' -- m :: Int + let n' = n + 1 -- pure, value-level + m' = m + 1 + idC -< Signal (n' + m') +``` + +The plugin collects the value-level bindings into a single pure function, +lifts it to the signal level with `fmap` (using `bundle`/`unbundle` to group +the buses), and ties the feedback knot with a lazy let binding. See +example/ValueCircuits.hs for more examples and the expansion of `counter3`. + +Notes: + +- Pattern match down to *exactly* the `Signal` layer, no shallower; the + plugin cannot (yet) know which types contain signals, so the boundary has + to be explicit. +- In a `circuitS` block, `let` statements are value-level: they form the body + of the generated logic function and cannot define new buses or circuits. +- All buses crossing the value boundary must share the same clock domain + (they are combined with `bundle`). diff --git a/circuit-notation.cabal b/circuit-notation.cabal index 1ca3e70..de1345d 100644 --- a/circuit-notation.cabal +++ b/circuit-notation.cabal @@ -62,7 +62,9 @@ test-suite library-testsuite default-language: Haskell2010 type: exitcode-stdio-1.0 main-is: unittests.hs - other-modules: Example + other-modules: + Example + ValueCircuits hs-source-dirs: tests example diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs new file mode 100644 index 0000000..a82be9c --- /dev/null +++ b/example/ValueCircuits.hs @@ -0,0 +1,117 @@ +{- + ██████╗██╗██████╗ ██████╗██╗ ██╗██╗████████╗███████╗ +██╔════╝██║██╔══██╗██╔════╝██║ ██║██║╚══██╔══╝██╔════╝ +██║ ██║██████╔╝██║ ██║ ██║██║ ██║ ███████╗ +██║ ██║██╔══██╗██║ ██║ ██║██║ ██║ ╚════██║ +╚██████╗██║██║ ██║╚██████╗╚██████╔╝██║ ██║ ███████║ + ╚═════╝╚═╝╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝ ╚══════╝ + (C) 2020, Christopher Chalmers + +Examples of value-level circuits (the 'circuitS' keyword). +-} + +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} +{-# OPTIONS -Wall #-} + +module ValueCircuits where + +import Circuit + +import Clash.Prelude +import Clash.Signal.Internal (Signal ((:-))) + +-- | A register as a circuit: the output bus carries the input bus delayed by +-- one cycle, starting with the given value. +registerC :: a -> Circuit (Signal dom a) (Signal dom a) +registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) + +-- | Run a circuit whose buses are plain signals (and so have trivial +-- backwards channels). +simulateSigCircuit :: Circuit (Signal dom a) (Signal dom b) -> Signal dom a -> Signal dom b +simulateSigCircuit c as = let (() :-> bs) = runCircuit c (as :-> ()) in bs + +-- | Like 'simulateSigCircuit' for a circuit with no input. +simulateUnitCircuit :: Circuit () (Signal dom b) -> Signal dom b +simulateUnitCircuit c = let (() :-> bs) = runCircuit c (() :-> ()) in bs + +-- | Trivial pass-through: a single value in and a single value out, no +-- feedback. @a@ is the per-cycle 'Int' carried on the bus, not the bus +-- itself; no @bundle@/@unbundle@ is generated for single buses. +-- +-- >>> sampleN @System 5 (simulateSigCircuit plusOne (fromList [0..])) +-- [1,2,3,4,5] +plusOne :: Circuit (Signal dom Int) (Signal dom Int) +plusOne = circuitS \(Signal a) -> do + idC -< Signal (a + 1) + +-- | A single-register counter with a feedback loop. The register's input +-- @n'@ is defined in terms of its output @n@ by an ordinary recursive @let@; +-- the plugin ties the knot at the signal level. +-- +-- >>> sampleN @System 5 (simulateUnitCircuit counter) +-- [0,1,2,3,4] +counter :: Circuit () (Signal dom Int) +counter = circuitS do + Signal n <- registerC 0 -< Signal n' + let n' = n + 1 + idC -< Signal n + +-- | A Mealy-style accumulator: reads the per-cycle value off the input bus +-- and feeds back state through a register. Written with a @$@ chain. +-- +-- >>> sampleN @System 5 (simulateSigCircuit accum (fromList [1..])) +-- [1,3,6,10,15] +accum :: Circuit (Signal dom Int) (Signal dom Int) +accum = circuitS $ \(Signal i) -> do + Signal acc <- registerC 0 -< Signal acc' + let acc' = acc + i + idC -< Signal acc' + +-- | Two interleaved feedback loops (the canonical example from the design +-- notes). The bus input is ignored. +-- +-- >>> sampleN @System 5 (simulateSigCircuit counter3 (pure False)) +-- [10,12,14,16,18] +counter3 :: Circuit (Signal dom Bool) (Signal dom Int) +counter3 = circuitS \_bs -> do + Signal n <- registerC 0 -< Signal n' + Signal m <- registerC 8 -< Signal m' + let n' = n + 1 + m' = m + 1 + idC -< Signal (n' + m') + +-- | What 'counter3' expands to (modulo generated names). The value-level +-- bindings are collected into one pure function, @circuitLogic@, which is +-- lifted to the signal level with 'fmap'; 'bundle'/'unbundle' group the +-- buses and a lazy let binding ties the feedback knot. +counter3Expanded :: Circuit (Signal dom Bool) (Signal dom Int) +counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> + let + circuitLogic = \(n, m) -> + let n' = n + 1 + m' = m + 1 + in (n', m', n' + m') + + (valOut0, valOut1, valOut2) = + unbundle (fmap circuitLogic (bundle (valIn0, valIn1))) + + (_ :-> BusTag valIn0) = runTagCircuit (registerC 0) (BusTag valOut0 :-> BusTag unitBwd) + (_ :-> BusTag valIn1) = runTagCircuit (registerC 8) (BusTag valOut1 :-> BusTag unitBwd) + + _bs_Bwd = BusTag def + in (_bs_Bwd :-> BusTag valOut2) + +-- | Value-level and bus-level ports can be mixed: the 'DF' bus is routed +-- through untouched while the signal is sampled and modified. +mixed :: Circuit (Signal dom Int, DF dom Bool) (Signal dom Int, DF dom Bool) +mixed = circuitS \(Signal a, df) -> do + idC -< (Signal (a + 1), df) + +-- | Without any value-level (@Signal@/@Fwd@) markers, @circuitS@ behaves +-- exactly like @circuit@. +passthrough :: Circuit (Signal dom Int) (Signal dom Int) +passthrough = circuitS \a -> a diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index cffdcd8..1f1a64f 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -92,7 +92,7 @@ import GHC.Types.Unique.Map.Extra #endif -- clash-prelude -import Clash.Prelude (Vec((:>), Nil)) +import Clash.Prelude (Vec((:>), Nil), bundle, unbundle) -- lens import qualified Control.Lens as L @@ -128,6 +128,10 @@ isSomeVar s = \case isCircuitVar :: p ~ GhcPs => HsExpr p -> Bool isCircuitVar = isSomeVar "circuit" +-- | Is the variable for the value-level circuit keyword? +isCircuitSVar :: p ~ GhcPs => HsExpr p -> Bool +isCircuitSVar = isSomeVar "circuitS" + isDollar :: p ~ GhcPs => HsExpr p -> Bool isDollar = isSomeVar "$" @@ -255,6 +259,8 @@ data CircuitState dec exp nm = CircuitState -- ^ type signatures in let bindings , _circuitLets :: [dec] -- ^ user defined let expression inside the circuit + , _circuitCompletes :: [dec] + -- ^ generated bindings that complete underscored ports , _circuitBinds :: [Binding exp nm] -- ^ @out <- circuit <- in@ statements , _circuitMasters :: PortDescription nm @@ -288,6 +294,7 @@ runCircuitM (CircuitM m) = do , _circuitSlaves = Tuple [] , _circuitTypes = [] , _circuitLets = [] + , _circuitCompletes = [] , _circuitBinds = [] , _circuitMasters = Tuple [] , _portVarTypes = emptyUniqMap @@ -976,6 +983,7 @@ circuitQQExpM = do dflags <- GHC.getDynFlags binds <- L.use circuitBinds lets <- L.use circuitLets + completes <- L.use circuitCompletes letTypes <- L.use circuitTypes slaves <- L.use circuitSlaves masters <- L.use circuitMasters @@ -985,7 +993,7 @@ circuitQQExpM = do -- errors on a bus are reported on the offending statement rather than at -- the end of the circuit block (see tests/fixtures/BusError.hs). let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) - let decs = lets <> map decFromBinding' binds + let decs = lets <> completes <> map decFromBinding' binds let pats = bindOutputs dflags Fwd masters slaves res = createInputs Bwd slaves masters @@ -1001,6 +1009,154 @@ circuitQQExpM = do pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body +-- Value circuits (circuitS) -------------------------------------------- + +-- | The number of value-level ('FwdPat' / 'FwdExpr') ports in a port +-- description. +countFwdPorts :: PortDescription PortName -> Int +countFwdPorts p = length [() | FwdPat{} <- L.universe p] + length [() | FwdExpr{} <- L.universe p] + +-- | Replace each value-level ('Signal' / 'Fwd') pattern with a reference to a +-- generated signal bus variable (@prefix <> show i@), collecting the original +-- value-level patterns in order. +replaceFwdPats + :: String + -> PortDescription PortName + -> State (Int, [LPat GhcPs]) (PortDescription PortName) +replaceFwdPats prefix = L.transformM \case + FwdPat lpat@(L loc _) -> do + (i, pats) <- get + put (i + 1, pats <> [lpat]) + pure (FwdPat (varP loc (prefix <> show i))) + p -> pure p + +-- | Replace each value-level ('Signal' / 'Fwd') expression with a reference +-- to a generated signal bus variable (@prefix <> show i@), collecting the +-- original value-level expressions in order. +replaceFwdExprs + :: String + -> PortDescription PortName + -> State (Int, [LHsExpr GhcPs]) (PortDescription PortName) +replaceFwdExprs prefix = L.transformM \case + FwdExpr lexpr@(L loc _) -> do + (i, exprs) <- get + put (i + 1, exprs <> [lexpr]) + pure (FwdExpr (varE loc (var (prefix <> show i)))) + p -> pure p + +-- | The @circuitS@ (value-level circuit) version of 'circuitQQExpM'. +-- +-- Value-level circuits describe a circuit's logic over the values sampled +-- each clock cycle. The boundary between bus land and value land is marked +-- with @Signal@ (or @Fwd@): @Signal n <- ...@ binds @n@ to the per-cycle +-- value carried on that bus, and @... -< Signal e@ injects the per-cycle +-- value @e@ back onto a bus. +-- +-- All the value-level bindings (the @let@s of the do block) are collected +-- into a single pure function, @circuitLogic@, whose arguments are the +-- @Signal@-bound values and whose results are the @Signal@-injected +-- expressions. It is lifted to the signal level with 'fmap', using +-- 'bundle' / 'unbundle' and a lazy let binding to tie feedback loops: +-- +-- @ +-- circuitLogic = \\(ins) -> let \ in (outs) +-- (outBuses) = unbundle (fmap circuitLogic (bundle (inBuses))) +-- @ +-- +-- The buses themselves are wired up exactly as for an ordinary @circuit@. +circuitSQQExpM + :: (p ~ GhcPs, ?nms :: ExternalNames) + => CircuitM (LHsExpr p) +circuitSQQExpM = do + slaves0 <- L.use circuitSlaves + masters0 <- L.use circuitMasters + binds0 <- L.use circuitBinds + + let boundaryCount = + sum (map countFwdPorts (slaves0 : masters0 : concatMap (\b -> [bIn b, bOut b]) binds0)) + + -- Without any value-level (Signal/Fwd) ports there is no boundary to lift; + -- behave exactly like an ordinary circuit. + if boundaryCount == 0 then circuitQQExpM else circuitSQQExpM' + +circuitSQQExpM' + :: (p ~ GhcPs, ?nms :: ExternalNames) + => CircuitM (LHsExpr p) +circuitSQQExpM' = do + checkCircuit + + dflags <- GHC.getDynFlags + loc <- L.use circuitLoc + + -- read the ports after checkCircuit, which may have rewritten them + slaves0 <- L.use circuitSlaves + masters0 <- L.use circuitMasters + binds0 <- L.use circuitBinds + + let inPrefix = genLocName loc "valIn" <> "_" + outPrefix = genLocName loc "valOut" <> "_" + logicName = genLocName loc "circuitLogic" + + -- Value patterns become the arguments of circuitLogic (values sampled off + -- buses) ... + let inM = do + s <- replaceFwdPats inPrefix slaves0 + bs <- traverse (\b -> (\p -> b { bIn = p }) <$> replaceFwdPats inPrefix (bIn b)) binds0 + pure (s, bs) + ((slaves1, binds1), (numIns, inPats)) = runState inM (0, []) + + -- ... and value expressions become its results (values written to buses). + let outM = do + bs <- traverse (\b -> (\p -> b { bOut = p }) <$> replaceFwdExprs outPrefix (bOut b)) binds1 + m <- replaceFwdExprs outPrefix masters0 + pure (bs, m) + ((binds2, masters1), (numOuts, outExprs)) = runState outM (0, []) + + circuitSlaves .= slaves1 + circuitMasters .= masters1 + circuitBinds .= binds2 + + -- In a value circuit the do-block lets are value-level; they form the body + -- of circuitLogic rather than ending up in the outer (bus-level) let. + lets <- L.use circuitLets + completes <- L.use circuitCompletes + letTypes <- L.use circuitTypes + + let logicLam = lamE [tupP inPats] (letE noSrcSpanA letTypes lets (tupE noSrcSpanA outExprs)) + logicBind = L loc $ patBind (varP noSrcSpanA logicName) logicLam + + -- (outBuses) = unbundle (fmap circuitLogic (bundle (inBuses))) + -- bundle/unbundle are only needed when there is more than one bus. With no + -- inputs at all the logic is constant, so it is mapped over @pure ()@. + let inVars = map (\i -> varE noSrcSpanA (var (inPrefix <> show i))) [0 .. numIns - 1] + outVarPs = map (\i -> varP noSrcSpanA (outPrefix <> show i)) [0 .. numOuts - 1] + + bundled = case inVars of + [] -> varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] + [e] -> e + es -> varE noSrcSpanA (thName 'bundle) `appE` tupE noSrcSpanA es + lifted = varE noSrcSpanA (thName 'fmap) `appE` varE noSrcSpanA (var logicName) `appE` bundled + + knotPat = case outVarPs of + [] -> nlWildPat + ps -> tupP ps + knotExpr = if numOuts > 1 + then varE noSrcSpanA (thName 'unbundle) `appE` lifted + else lifted + knotBind = L loc $ patBind knotPat knotExpr + + -- The bus plumbing is generated exactly as in 'circuitQQExpM'. + let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) + let decs = logicBind : knotBind : completes <> map decFromBinding' binds2 + + let pats = bindOutputs dflags Fwd masters1 slaves1 + res = createInputs Bwd slaves1 masters1 + + body :: LHsExpr GhcPs + body = letE noSrcSpanA [] decs res + + pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body + grr :: MonadIO m => OccName.NameSpace -> m () grr nm | nm == OccName.tcName = liftIO $ putStrLn "tcName" @@ -1020,7 +1176,7 @@ completeUnderscores = do addDef suffix = \case Ref (PortName loc (unpackFS -> name@('_':_))) -> do let bind = patBind (varP loc (name <> suffix)) (tagE $ varE loc (thName 'def)) - circuitLets <>= [L loc bind] + circuitCompletes <>= [L loc bind] _ -> pure () addBind :: Binding exp PortName -> CircuitM () @@ -1046,33 +1202,42 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where x <- parseCircuit lappB >> completeUnderscores >> circuitQQExpM when debug $ ppr x pure x + | isCircuitSVar circuitVar = runCircuitM $ do + x <- parseCircuit lappB >> completeUnderscores >> circuitSQQExpM + when debug $ ppr x + pure x -- `circuit $` application transform' (L _ (OpApp _xapp c@(L _ circuitVar) (L _ infixVar) appR)) - | isDollar infixVar && dollarChainIsCircuit circuitVar = do + | isDollar infixVar && dollarChainIsCircuit "circuit" circuitVar = do runCircuitM $ do x <- parseCircuit appR >> completeUnderscores >> circuitQQExpM when debug $ ppr x - pure (dollarChainReplaceCircuit x c) + pure (dollarChainReplaceCircuit "circuit" x c) + | isDollar infixVar && dollarChainIsCircuit "circuitS" circuitVar = do + runCircuitM $ do + x <- parseCircuit appR >> completeUnderscores >> circuitSQQExpM + when debug $ ppr x + pure (dollarChainReplaceCircuit "circuitS" x c) transform' e = pure e --- | check if circuit is applied via `a $ chain $ of $ dollars`. -dollarChainIsCircuit :: HsExpr GhcPs -> Bool -dollarChainIsCircuit = \case - HsVar _ (L _ v) -> v == GHC.mkVarUnqual "circuit" - OpApp _xapp _appL (L _ infixVar) (L _ appR) -> isDollar infixVar && dollarChainIsCircuit appR +-- | check if the named circuit keyword is applied via `a $ chain $ of $ dollars`. +dollarChainIsCircuit :: GHC.FastString -> HsExpr GhcPs -> Bool +dollarChainIsCircuit nm = \case + HsVar _ (L _ v) -> v == GHC.mkVarUnqual nm + OpApp _xapp _appL (L _ infixVar) (L _ appR) -> isDollar infixVar && dollarChainIsCircuit nm appR _ -> False -- | Replace the circuit if it's part of a chain of `$`. -dollarChainReplaceCircuit :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs -dollarChainReplaceCircuit circuitExpr (L loc app) = case app of +dollarChainReplaceCircuit :: GHC.FastString -> LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs +dollarChainReplaceCircuit nm circuitExpr (L loc app) = case app of HsVar _ (L _loc v) - -> if v == GHC.mkVarUnqual "circuit" + -> if v == GHC.mkVarUnqual nm then circuitExpr else error "dollarChainAddCircuit: not a circuit" OpApp xapp appL (L infixLoc infixVar) appR - -> L loc $ OpApp xapp appL (L infixLoc infixVar) (dollarChainReplaceCircuit circuitExpr appR) + -> L loc $ OpApp xapp appL (L infixLoc infixVar) (dollarChainReplaceCircuit nm circuitExpr appR) t -> error $ "dollarChainAddCircuit unhandled case " <> showC t -- | The plugin for circuit notation. diff --git a/tests/unittests.hs b/tests/unittests.hs index 8262ed6..a383cf1 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -2,10 +2,36 @@ -- wrong type or name, GHC would refuse to compile this file. {-# OPTIONS -fplugin=CircuitNotation #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} + module Main where +import Control.Monad (unless) +import System.Exit (exitFailure) + +import Clash.Prelude (System, fromList, sampleN) + import Circuit -import Example +import Example () +import ValueCircuits main :: IO () -main = pure () +main = do + results <- mapM check + [ ("plusOne", sim plusOne (fromList [0..]), [1, 2, 3, 4, 5]) + , ("counter", sampleN 5 (simulateUnitCircuit @System counter), [0, 1, 2, 3, 4]) + , ("accum", sim accum (fromList [1..]), [1, 3, 6, 10, 15]) + , ("counter3", sim counter3 (pure False), [10, 12, 14, 16, 18]) + , ("counter3Expanded", sim counter3Expanded (pure False), [10, 12, 14, 16, 18]) + ] + unless (and results) exitFailure + where + sim c = sampleN 5 . simulateSigCircuit @System c + + check :: (String, [Int], [Int]) -> IO Bool + check (name, actual, expected) + | actual == expected = pure True + | otherwise = do + putStrLn $ name <> ": expected " <> show expected <> " but got " <> show actual + pure False From 7a02cb36f2e27355201bb1ca6259e74d92a3276d Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 00:28:57 +0100 Subject: [PATCH 04/21] More testing of value circuits (with a bug fix) --- CHANGELOG.md | 7 ++ README.md | 3 +- example/ValueCircuits.hs | 163 ++++++++++++++++++++++++++++++++------- src/Circuit.hs | 9 +++ src/CircuitNotation.hs | 29 ++++++- tests/error-location.hs | 82 ++++++++++++++------ tests/unittests.hs | 85 ++++++++++++++------ 7 files changed, 301 insertions(+), 77 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9bfcc63..8b81db3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,13 @@ `Signal`/`Fwd` patterns and expressions); the plugin lifts it back to the signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a lazy let binding. See the README and example/ValueCircuits.hs. + + The value boundary is generated with the new `SigTag` pattern synonym + (`Circuit` module), which pins the bus type to a `Signal` so that type + inference survives nested circuits (the `Fwd` family is not injective) and + "too shallow" `Signal` markers report a direct `Vec`-vs-`Signal` style + mismatch. **Breaking**: `ExternalNames` gained a `signalTagName` field, so + custom plugins (e.g. clash-protocols style) need to supply it. * Fix the source location of type errors on a bus. Since bus tagging was introduced, such errors pointed at the end of the `circuit` block rather than at the offending statement. Generated bindings are now located at their diff --git a/README.md b/README.md index 9822412..81281e5 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,8 @@ Notes: - Pattern match down to *exactly* the `Signal` layer, no shallower; the plugin cannot (yet) know which types contain signals, so the boundary has - to be explicit. + to be explicit. Marking a bus that is not a `Signal` (e.g. a `Vec` of + signals) is a type error on the offending statement. - In a `circuitS` block, `let` statements are value-level: they form the body of the generated logic function and cannot define new buses or circuits. - All buses crossing the value boundary must share the same clock domain diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index a82be9c..0e866d7 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -7,11 +7,13 @@ ╚═════╝╚═╝╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝ ╚══════╝ (C) 2020, Christopher Chalmers -Examples of value-level circuits (the 'circuitS' keyword). +Examples of value-level circuits (the 'circuitS' keyword). These are +simulated and checked by tests/unittests.hs. -} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS -fplugin=CircuitNotation #-} @@ -29,31 +31,76 @@ import Clash.Signal.Internal (Signal ((:-))) registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) --- | Run a circuit whose buses are plain signals (and so have trivial --- backwards channels). -simulateSigCircuit :: Circuit (Signal dom a) (Signal dom b) -> Signal dom a -> Signal dom b -simulateSigCircuit c as = let (() :-> bs) = runCircuit c (as :-> ()) in bs +-- | Run a circuit whose buses have trivial backwards channels (such as +-- 'Signal' buses, or tuples and 'Vec's of them) by feeding it forward values. +simulateC :: TrivialBwd (Bwd b) => Circuit a b -> Fwd a -> Fwd b +simulateC c aFwd = let (_ :-> bFwd) = runCircuit c (aFwd :-> unitBwd) in bFwd --- | Like 'simulateSigCircuit' for a circuit with no input. -simulateUnitCircuit :: Circuit () (Signal dom b) -> Signal dom b -simulateUnitCircuit c = let (() :-> bs) = runCircuit c (() :-> ()) in bs +-- Basic shapes --------------------------------------------------------- -- | Trivial pass-through: a single value in and a single value out, no -- feedback. @a@ is the per-cycle 'Int' carried on the bus, not the bus -- itself; no @bundle@/@unbundle@ is generated for single buses. --- --- >>> sampleN @System 5 (simulateSigCircuit plusOne (fromList [0..])) --- [1,2,3,4,5] plusOne :: Circuit (Signal dom Int) (Signal dom Int) plusOne = circuitS \(Signal a) -> do idC -< Signal (a + 1) +-- | The @Fwd@ keyword can be used interchangeably with @Signal@ to mark the +-- value boundary. +plusOneFwd :: Circuit (Signal dom Int) (Signal dom Int) +plusOneFwd = circuitS \(Fwd a) -> do + idC -< Fwd (a + 1) + +-- | No value inputs at all: the logic is constant. +alwaysFive :: Circuit () (Signal dom Int) +alwaysFive = circuitS do + idC -< Signal (5 :: Int) + +-- | Two value inputs, one value output (a single @bundle@, no @unbundle@). +addC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int) +addC = circuitS \(Signal a, Signal b) -> do + idC -< Signal (a + b) + +-- | One value input, two value outputs (a single @unbundle@, no @bundle@). +fanOutC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) +fanOutC = circuitS \(Signal a) -> do + idC -< (Signal (a + 1), Signal (a * 2)) + +-- | Values can be matched out of a bus carrying a compound type ... +splitC :: Circuit (Signal dom (Int, Bool)) (Signal dom Int, Signal dom Bool) +splitC = circuitS \(Signal (a, b)) -> do + idC -< (Signal a, Signal b) + +-- | ... and combined back onto one. +joinC :: Circuit (Signal dom Int, Signal dom Bool) (Signal dom (Int, Bool)) +joinC = circuitS \(Signal a, Signal b) -> do + idC -< Signal (a, b) + +-- | Ports nest like in ordinary circuit notation. +nestedTupleC :: Circuit ((Signal dom Int, Signal dom Int), Signal dom Int) (Signal dom Int) +nestedTupleC = circuitS \((Signal a, Signal b), Signal c) -> do + idC -< Signal (a + b * c) + +-- | Value boundaries inside 'Vec' buses. +vecInC :: Circuit (Vec 2 (Signal dom Int)) (Signal dom Int) +vecInC = circuitS \[Signal a, Signal b] -> do + idC -< Signal (a - b) + +vecOutC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) +vecOutC = circuitS \(Signal a) -> do + idC -< [Signal (a + 1), Signal (a - 1)] + +-- | Ports crossing the value boundary can be given bus-level type +-- annotations like any other port. +annotatedC :: forall dom. Circuit (Signal dom Int) (Signal dom Int) +annotatedC = circuitS \((Signal a) :: Signal dom Int) -> do + idC -< Signal (a + 1) + +-- Feedback ------------------------------------------------------------- + -- | A single-register counter with a feedback loop. The register's input -- @n'@ is defined in terms of its output @n@ by an ordinary recursive @let@; -- the plugin ties the knot at the signal level. --- --- >>> sampleN @System 5 (simulateUnitCircuit counter) --- [0,1,2,3,4] counter :: Circuit () (Signal dom Int) counter = circuitS do Signal n <- registerC 0 -< Signal n' @@ -62,9 +109,6 @@ counter = circuitS do -- | A Mealy-style accumulator: reads the per-cycle value off the input bus -- and feeds back state through a register. Written with a @$@ chain. --- --- >>> sampleN @System 5 (simulateSigCircuit accum (fromList [1..])) --- [1,3,6,10,15] accum :: Circuit (Signal dom Int) (Signal dom Int) accum = circuitS $ \(Signal i) -> do Signal acc <- registerC 0 -< Signal acc' @@ -73,9 +117,6 @@ accum = circuitS $ \(Signal i) -> do -- | Two interleaved feedback loops (the canonical example from the design -- notes). The bus input is ignored. --- --- >>> sampleN @System 5 (simulateSigCircuit counter3 (pure False)) --- [10,12,14,16,18] counter3 :: Circuit (Signal dom Bool) (Signal dom Int) counter3 = circuitS \_bs -> do Signal n <- registerC 0 -< Signal n' @@ -87,7 +128,9 @@ counter3 = circuitS \_bs -> do -- | What 'counter3' expands to (modulo generated names). The value-level -- bindings are collected into one pure function, @circuitLogic@, which is -- lifted to the signal level with 'fmap'; 'bundle'/'unbundle' group the --- buses and a lazy let binding ties the feedback knot. +-- buses and a lazy let binding ties the feedback knot. 'SigTag' is 'BusTag' +-- with its bus type pinned to a signal, which keeps inference going where +-- the non-injective 'Fwd' family would otherwise lose it. counter3Expanded :: Circuit (Signal dom Bool) (Signal dom Int) counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> let @@ -99,19 +142,81 @@ counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> (valOut0, valOut1, valOut2) = unbundle (fmap circuitLogic (bundle (valIn0, valIn1))) - (_ :-> BusTag valIn0) = runTagCircuit (registerC 0) (BusTag valOut0 :-> BusTag unitBwd) - (_ :-> BusTag valIn1) = runTagCircuit (registerC 8) (BusTag valOut1 :-> BusTag unitBwd) + (_ :-> SigTag valIn0) = runTagCircuit (registerC 0) (SigTag valOut0 :-> BusTag unitBwd) + (_ :-> SigTag valIn1) = runTagCircuit (registerC 8) (SigTag valOut1 :-> BusTag unitBwd) _bs_Bwd = BusTag def - in (_bs_Bwd :-> BusTag valOut2) - --- | Value-level and bus-level ports can be mixed: the 'DF' bus is routed --- through untouched while the signal is sampled and modified. -mixed :: Circuit (Signal dom Int, DF dom Bool) (Signal dom Int, DF dom Bool) -mixed = circuitS \(Signal a, df) -> do + in (_bs_Bwd :-> SigTag valOut2) + +-- | Compound state fed back through a /single/ register: a fibonacci +-- machine. The pair is destructured and rebuilt at the value level. +fibC :: Circuit () (Signal dom Int) +fibC = circuitS do + Signal (a, b) <- registerC (0, 1) -< Signal (b, a + b) + idC -< Signal a + +-- | A chain of registers: a three-deep shift register (no feedback, but a +-- value passes through several binds). +shift3 :: Circuit (Signal dom Int) (Signal dom Int) +shift3 = circuitS \(Signal i) -> do + Signal a <- registerC 0 -< Signal i + Signal b <- registerC 0 -< Signal a + Signal c <- registerC 0 -< Signal b + idC -< Signal c + +-- | Three rotating registers plus the bus input: a four-way bundle on both +-- sides of the logic function. +rotate3 :: Circuit (Signal dom Int) (Signal dom Int) +rotate3 = circuitS \(Signal i) -> do + Signal a <- registerC 1 -< Signal a' + Signal b <- registerC 2 -< Signal b' + Signal c <- registerC 3 -< Signal c' + let a' = b + b' = c + c' = a + i + idC -< Signal (a + b + c) + +-- Mixing value land and bus land ---------------------------------------- + +-- | Value-level and bus-level ports can be mixed: the second bus is routed +-- through untouched while the first is sampled and modified. +mixedC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int, Signal dom Int) +mixedC = circuitS \(Signal a, b) -> do + idC -< (Signal (a + 1), b) + +-- | As 'mixedC' but with a 'DF' bus (whose backwards channel is not +-- trivial) routed through. +mixedDfC :: Circuit (Signal dom Int, DF dom Bool) (Signal dom Int, DF dom Bool) +mixedDfC = circuitS \(Signal a, df) -> do idC -< (Signal (a + 1), df) +-- | A bus created from a value can be multicast like any other bus. +multicastC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) +multicastC = circuitS \(Signal a) -> do + b <- idC -< Signal (a + 1) + idC -< (b, b) + -- | Without any value-level (@Signal@/@Fwd@) markers, @circuitS@ behaves -- exactly like @circuit@. passthrough :: Circuit (Signal dom Int) (Signal dom Int) passthrough = circuitS \a -> a + +-- Nesting --------------------------------------------------------------- + +-- | A @circuitS@ used as a sub-circuit inside an ordinary @circuit@. +nestedSInCircuit :: Circuit (Signal dom Int) (Signal dom Int) +nestedSInCircuit = circuit $ \a -> do + b <- (circuitS \(Signal x) -> do idC -< Signal (x * 2)) -< a + idC -< b + +-- | An ordinary @circuit@ used as a sub-circuit inside a @circuitS@. +nestedCircuitInS :: Circuit (Signal dom Int) (Signal dom Int) +nestedCircuitInS = circuitS \(Signal x) -> do + Signal y <- (circuit \b -> b) -< Signal (x + 1) + idC -< Signal (y * 3) + +-- | A @circuitS@ inside another @circuitS@. +nestedSInS :: Circuit (Signal dom Int) (Signal dom Int) +nestedSInS = circuitS \(Signal x) -> do + Signal y <- (circuitS \(Signal a) -> do idC -< Signal (a + 1)) -< Signal x + idC -< Signal (y * 2) diff --git a/src/Circuit.hs b/src/Circuit.hs index 871a481..9ffdff9 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -207,3 +207,12 @@ pattern BusTagBundle :: BusTagBundle t a => BusTagUnbundled t a -> BusTag t a pattern BusTagBundle a <- (taggedUnbundle -> a) where BusTagBundle a = taggedBundle a {-# COMPLETE BusTagBundle #-} + +-- | A tagged 'Signal' bus. Used by the plugin at the value boundary of +-- 'circuitS' blocks: matching or constructing with 'SigTag' pins the bus +-- type itself (the tag) to be a 'Signal', which is what the value boundary +-- requires. Since 'Fwd' is not injective, plain 'BusTag' would leave the bus +-- type ambiguous and type inference for nested circuits would fail. +pattern SigTag :: Signal dom a -> BusTag (Signal dom a) (Signal dom a) +pattern SigTag s = BusTag s +{-# COMPLETE SigTag #-} diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 1f1a64f..76f555d 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -223,6 +223,12 @@ data PortDescription a | Lazy SrcSpanAnnA (PortDescription a) | FwdExpr (LHsExpr GhcPs) | FwdPat (LPat GhcPs) + | SigTagExpr (LHsExpr GhcPs) + -- ^ generated by @circuitS@: a value-boundary bus expression, tagged with + -- 'SigTag' to pin the bus type to a signal + | SigTagPat (LPat GhcPs) + -- ^ generated by @circuitS@: a value-boundary bus pattern, tagged with + -- 'SigTag' to pin the bus type to a signal | PortType (LHsType GhcPs) (PortDescription a) | PortErr SrcSpanAnnA MsgDoc deriving (Foldable, Functor, Traversable) @@ -794,6 +800,8 @@ bindWithSuffix dflags dir = \case -- XXX: propagate location FwdExpr (L _ _) -> nlWildPat FwdPat lpat -> tagP lpat + SigTagExpr (L _ _) -> nlWildPat + SigTagPat lpat -> sigTagP lpat PortType ty p -> tagTypeP dir ty $ bindWithSuffix dflags dir p revDirec :: Direction -> Direction @@ -828,6 +836,10 @@ expWithSuffix dir = \case PortErr _ _ -> error "expWithSuffix PortErr!" FwdExpr lexpr -> tagE lexpr FwdPat (L l _) -> tagE $ varE l (trivialBwd ?nms) + SigTagExpr lexpr -> sigTagE lexpr + -- the backwards channel of a signal bus is trivial, so a plain (untyped) + -- tag suffices; the forwards occurrence pins the bus type + SigTagPat (L l _) -> tagE $ varE l (trivialBwd ?nms) PortType ty p -> tagTypeE dir ty (expWithSuffix dir p) createInputs @@ -893,6 +905,15 @@ tagP a = noLoc (conPatIn (noLoc (tagName ?nms)) (prefixCon [a])) tagE :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsExpr p -> LHsExpr p tagE a = varE noSrcSpanA (tagName ?nms) `appE` a +-- the SigTag wrappers take the location of what they wrap so that type +-- errors on the value boundary (e.g. marking a non-signal bus with @Signal@) +-- point at the marked pattern or expression +sigTagP :: (p ~ GhcPs, ?nms :: ExternalNames) => LPat p -> LPat p +sigTagP a@(L l _) = L l (conPatIn (noLoc (signalTagName ?nms)) (prefixCon [a])) + +sigTagE :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsExpr p -> LHsExpr p +sigTagE a@(L l _) = varE l (signalTagName ?nms) `appE` a + tagTypeCon :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsType GhcPs tagTypeCon = noLoc (HsTyVar noExt NotPromoted (noLoc (tagTName ?nms))) @@ -1027,7 +1048,7 @@ replaceFwdPats prefix = L.transformM \case FwdPat lpat@(L loc _) -> do (i, pats) <- get put (i + 1, pats <> [lpat]) - pure (FwdPat (varP loc (prefix <> show i))) + pure (SigTagPat (varP loc (prefix <> show i))) p -> pure p -- | Replace each value-level ('Signal' / 'Fwd') expression with a reference @@ -1041,7 +1062,7 @@ replaceFwdExprs prefix = L.transformM \case FwdExpr lexpr@(L loc _) -> do (i, exprs) <- get put (i + 1, exprs <> [lexpr]) - pure (FwdExpr (varE loc (var (prefix <> show i)))) + pure (SigTagExpr (varE loc (var (prefix <> show i)))) p -> pure p -- | The @circuitS@ (value-level circuit) version of 'circuitQQExpM'. @@ -1302,6 +1323,9 @@ data ExternalNames = ExternalNames , runCircuitName :: GHC.RdrName , tagBundlePat :: GHC.RdrName , tagName :: GHC.RdrName + , signalTagName :: GHC.RdrName + -- ^ a (pattern synonym) variant of 'tagName' whose type pins the bus to be + -- a signal; used at the value boundary of @circuitS@ blocks , tagTName :: GHC.RdrName , fwdBwdCon :: GHC.RdrName , fwdAndBwdTypes :: Direction -> GHC.RdrName @@ -1315,6 +1339,7 @@ defExternalNames = ExternalNames , runCircuitName = GHC.Unqual (OccName.mkVarOcc "runTagCircuit") , tagBundlePat = GHC.Unqual (OccName.mkDataOcc "BusTagBundle") , tagName = GHC.Unqual (OccName.mkDataOcc "BusTag") + , signalTagName = GHC.Unqual (OccName.mkDataOcc "SigTag") , tagTName = GHC.Unqual (OccName.mkTcOcc "BusTag") , fwdBwdCon = GHC.Unqual (OccName.mkDataOcc ":->") , fwdAndBwdTypes = \case diff --git a/tests/error-location.hs b/tests/error-location.hs index 92b576a..71fb071 100644 --- a/tests/error-location.hs +++ b/tests/error-location.hs @@ -1,17 +1,21 @@ --- | Regression test for the source locations of type errors on buses. +-- | Regression tests for the source locations of error messages. -- -- When bus tagging (the @BusTag@ wrapping) was introduced, type errors on a -- bus stopped pointing at the offending statement and instead pointed at the --- end of the @circuit@ block, which made them very hard to act on. +-- end of the @circuit@ block, which made them very hard to act on. The same +-- concern applies to @circuitS@ blocks, where the value-level expressions and +-- lets are moved into a generated @circuitLogic@ function. -- --- This test compiles 'tests/fixtures/BusError.hs' (which has a deliberate type --- error on a bus, on the line marked @ERROR HERE@) with plugin enabled and --- asserts that GHC reports an error /on that line/. It uses the same plain --- @ghc@ + package-environment-file mechanism that CI already uses to compile --- the @Example@ module. +-- Each fixture in 'fixtures' deliberately fails to compile, with the +-- offending statement tagged by a marker comment that appears on exactly one +-- line. The fixture is compiled with the plugin enabled and we assert that an +-- error is reported /on that line/ (and, optionally, that the output contains +-- an expected message). It uses the same plain @ghc@ + +-- package-environment-file mechanism that CI already uses to compile the +-- @Example@ module. module Main (main) where -import Control.Monad (unless, when) +import Control.Monad (forM, unless, when) import Data.List (isInfixOf, isPrefixOf, nub, sort) import Data.Maybe (mapMaybe) import System.Directory (getTemporaryDirectory) @@ -21,16 +25,41 @@ import System.FilePath (()) import System.Process (readProcessWithExitCode) import Text.Read (readMaybe) -fixture :: FilePath -fixture = "tests" "fixtures" "BusError.hs" +data Fixture = Fixture + { fixturePath :: FilePath + -- ^ the file to compile, which must fail to compile + , fixtureMarker :: String + -- ^ marker comment on the line the error should be reported on; it must + -- appear on exactly one line of the fixture + , fixtureNeedle :: Maybe String + -- ^ optionally, a string the compiler output must contain + } --- | The marker placed on the erroring statement inside the fixture. It is --- chosen so that it appears on exactly one line of the fixture. -marker :: String -marker = "bus-error-marker" +fixtures :: [Fixture] +fixtures = + [ -- type error on a bus in an ordinary circuit + Fixture ("tests" "fixtures" "BusError.hs") "bus-error-marker" Nothing + -- type error on a value-level expression in a circuitS + , Fixture ("tests" "fixtures" "ValueExprError.hs") "value-expr-error-marker" Nothing + -- type error inside a value-level let in a circuitS + , Fixture ("tests" "fixtures" "ValueLetError.hs") "value-let-error-marker" Nothing + -- port error reported by the plugin itself in a circuitS + , Fixture ("tests" "fixtures" "ValuePortError.hs") "value-port-error-marker" + (Just "has no associated master") + -- a Signal marker on a bus that is not a signal (the marker is "too + -- shallow"); the SigTag the plugin generates should turn this into a + -- direct Vec-vs-Signal mismatch on the offending pattern + , Fixture ("tests" "fixtures" "ValueShapeError.hs") "value-shape-error-marker" Nothing + ] main :: IO () main = do + ghc <- maybe "ghc" id <$> lookupEnv "GHC" + results <- forM fixtures (checkFixture ghc) + unless (and results) exitFailure + +checkFixture :: String -> Fixture -> IO Bool +checkFixture ghc (Fixture fixture marker needle) = do src <- readFile fixture -- Work out which line the deliberate error is on by finding the marker. @@ -42,7 +71,6 @@ main = do <> " in " <> fixture <> ", found lines " <> show markedLines -- Compile the fixture and collect the reported error lines. - ghc <- maybe "ghc" id <$> lookupEnv "GHC" tmp <- getTemporaryDirectory let args = [ "-outputdir", tmp "circuit-notation-error-test" @@ -51,29 +79,37 @@ main = do ] (_code, out, err) <- readProcessWithExitCode ghc args "" let output = out <> err - errLines = sort . nub $ errorLineNumbers output + errLines = sort . nub $ errorLineNumbers fixture output - putStrLn $ "ghc reported errors on lines: " <> show errLines - putStrLn $ "expected an error on line: " <> show expectedLine + putStrLn $ fixture <> ":" + putStrLn $ " ghc reported errors on lines: " <> show errLines + putStrLn $ " expected an error on line: " <> show expectedLine when (null errLines) $ die $ "expected the fixture to fail to compile, but ghc reported no\n\ \error locations. Full output:\n" <> output unless (expectedLine `elem` errLines) $ - die $ "type error on the bus was not reported on the offending line (" + die $ "the error was not reported on the offending line (" <> show expectedLine <> ").\n" <> "Instead it was reported on lines " <> show errLines - <> " -- this is the bus-tagging regression where errors point at\n" + <> " -- this is the regression where errors point at\n" <> "the end of the circuit rather than the actual mistake.\n\n" <> "Full ghc output:\n" <> output - putStrLn "OK: bus type error points at the offending statement." + case needle of + Just msg | not (msg `isInfixOf` output) -> + die $ "expected the compiler output to mention " <> show msg + <> ".\n\nFull ghc output:\n" <> output + _ -> pure () + + putStrLn " OK: error points at the offending statement." + pure True -- | Extract the line numbers from GHC error messages that refer to the fixture, -- e.g. a line @tests/fixtures/BusError.hs:30:8: error: ...@ yields @30@. -errorLineNumbers :: String -> [Int] -errorLineNumbers = mapMaybe parseLine . lines +errorLineNumbers :: FilePath -> String -> [Int] +errorLineNumbers fixture = mapMaybe parseLine . lines where parseLine l = do let l' = dropWhile (== ' ') l diff --git a/tests/unittests.hs b/tests/unittests.hs index a383cf1..9a581e7 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -2,36 +2,77 @@ -- wrong type or name, GHC would refuse to compile this file. {-# OPTIONS -fplugin=CircuitNotation #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} module Main where -import Control.Monad (unless) -import System.Exit (exitFailure) +import Control.Monad (unless) +import System.Exit (exitFailure) -import Clash.Prelude (System, fromList, sampleN) +import Clash.Prelude (NFDataX, Signal, System, Vec ((:>), Nil), + fromList, sampleN) -import Circuit -import Example () +import Example () import ValueCircuits +sample5 :: NFDataX a => Signal System a -> [a] +sample5 = sampleN 5 + +check :: (Eq a, Show a) => String -> a -> a -> IO Bool +check name actual expected + | actual == expected = pure True + | otherwise = do + putStrLn $ name <> ": expected " <> show expected <> " but got " <> show actual + pure False + main :: IO () main = do - results <- mapM check - [ ("plusOne", sim plusOne (fromList [0..]), [1, 2, 3, 4, 5]) - , ("counter", sampleN 5 (simulateUnitCircuit @System counter), [0, 1, 2, 3, 4]) - , ("accum", sim accum (fromList [1..]), [1, 3, 6, 10, 15]) - , ("counter3", sim counter3 (pure False), [10, 12, 14, 16, 18]) - , ("counter3Expanded", sim counter3Expanded (pure False), [10, 12, 14, 16, 18]) + let (fanA, fanB) = simulateC fanOutC (fromList [0 ..]) + (splitA, splitB) = simulateC splitC (fromList [(i, even i) | i <- [0 ..]]) + (mixA, mixB) = simulateC mixedC (fromList [0 ..], fromList [5 ..]) + (mcA, mcB) = simulateC multicastC (fromList [0 ..]) + + results <- sequence + -- basic shapes + [ check "plusOne" (sample5 (simulateC plusOne (fromList [0 ..]))) [1, 2, 3, 4, 5] + , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] + , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] + , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) + [11, 22, 33, 44, 55] + , check "fanOutC" (sample5 fanA, sample5 fanB) + ([1, 2, 3, 4, 5], [0, 2, 4, 6, 8]) + , check "splitC" (sample5 splitA, sample5 splitB) + ([0, 1, 2, 3, 4], [True, False, True, False, True]) + , check "joinC" (sample5 (simulateC joinC (fromList [1 ..], fromList [even i | i <- [0 :: Int ..]]))) + [(1, True), (2, False), (3, True), (4, False), (5, True)] + , check "nestedTupleC" + (sample5 (simulateC nestedTupleC ((fromList [1 ..], fromList [10, 20 ..]), pure 2))) + [21, 42, 63, 84, 105] + , check "vecInC" (sample5 (simulateC vecInC (fromList [10, 20 ..] :> fromList [1 ..] :> Nil))) + [9, 18, 27, 36, 45] + , check "vecOutC" (fmap sample5 (simulateC vecOutC (fromList [0 ..]))) + ([1, 2, 3, 4, 5] :> [-1, 0, 1, 2, 3] :> Nil) + , check "annotatedC" (sample5 (simulateC annotatedC (fromList [0 ..]))) [1, 2, 3, 4, 5] + + -- feedback + , check "counter" (sample5 (simulateC counter ())) [0, 1, 2, 3, 4] + , check "accum" (sample5 (simulateC accum (fromList [1 ..]))) [1, 3, 6, 10, 15] + , check "counter3" (sample5 (simulateC counter3 (pure False))) [10, 12, 14, 16, 18] + , check "counter3Expanded" (sample5 (simulateC counter3Expanded (pure False))) [10, 12, 14, 16, 18] + , check "fibC" (sample5 (simulateC fibC ())) [0, 1, 1, 2, 3] + , check "shift3" (sample5 (simulateC shift3 (fromList [1 ..]))) [0, 0, 0, 1, 2] + , check "rotate3" (sample5 (simulateC rotate3 (pure 1))) [6, 7, 8, 9, 10] + + -- mixing value land and bus land + , check "mixedC" (sample5 mixA, sample5 mixB) ([1, 2, 3, 4, 5], [5, 6, 7, 8, 9]) + , check "multicastC" (sample5 mcA, sample5 mcB) ([1, 2, 3, 4, 5], [1, 2, 3, 4, 5]) + , check "passthrough" (sample5 (simulateC passthrough (fromList [3 ..]))) [3, 4, 5, 6, 7] + + -- nesting + , check "nestedSInCircuit" (sample5 (simulateC nestedSInCircuit (fromList [0 ..]))) [0, 2, 4, 6, 8] + , check "nestedCircuitInS" (sample5 (simulateC nestedCircuitInS (fromList [0 ..]))) [3, 6, 9, 12, 15] + , check "nestedSInS" (sample5 (simulateC nestedSInS (fromList [0 ..]))) [2, 4, 6, 8, 10] ] + + putStrLn $ "passed " <> show (length (filter id results)) <> "/" <> show (length results) unless (and results) exitFailure - where - sim c = sampleN 5 . simulateSigCircuit @System c - - check :: (String, [Int], [Int]) -> IO Bool - check (name, actual, expected) - | actual == expected = pure True - | otherwise = do - putStrLn $ name <> ": expected " <> show expected <> " but got " <> show actual - pure False From 7b428ffb4c7a1db72c525cb35f5975c8caf21a3a Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 01:45:17 +0100 Subject: [PATCH 05/21] Make sure the tests pass on all GHC versions --- .github/workflows/ci.yml | 1 + CHANGELOG.md | 6 ++++++ tests/fixtures/ValueExprError.hs | 25 +++++++++++++++++++++++++ tests/fixtures/ValueLetError.hs | 19 +++++++++++++++++++ tests/fixtures/ValuePortError.hs | 19 +++++++++++++++++++ tests/fixtures/ValueShapeError.hs | 24 ++++++++++++++++++++++++ tests/unittests.hs | 4 +++- 7 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 tests/fixtures/ValueExprError.hs create mode 100644 tests/fixtures/ValueLetError.hs create mode 100644 tests/fixtures/ValuePortError.hs create mode 100644 tests/fixtures/ValueShapeError.hs diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 12917e3..5690298 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -66,6 +66,7 @@ jobs: cabal build all --write-ghc-environment-files=always ghc -Wall -Werror -iexample Example ghc -Wall -Werror -iexample Testing + ghc -Wall -Werror -iexample ValueCircuits - name: Test run: | diff --git a/CHANGELOG.md b/CHANGELOG.md index 8b81db3..83b1e30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,12 @@ "too shallow" `Signal` markers report a direct `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` gained a `signalTagName` field, so custom plugins (e.g. clash-protocols style) need to supply it. +* Add a per-GHC `checks` output to the flake, so `nix flake check` (or + `nix build .#checks..`) builds the package and runs all test + suites against every supported GHC. The CI nix job now uses it. The + error-location test suite skips itself (with a message) when the ambient + `ghc` has no circuit-notation package registered — as during a plain nix + build of the package, where it previously failed. * Fix the source location of type errors on a bus. Since bus tagging was introduced, such errors pointed at the end of the `circuit` block rather than at the offending statement. Generated bindings are now located at their diff --git a/tests/fixtures/ValueExprError.hs b/tests/fixtures/ValueExprError.hs new file mode 100644 index 0000000..3ff8d39 --- /dev/null +++ b/tests/fixtures/ValueExprError.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture with a deliberate type error on a /value-level/ expression in a +-- @circuitS@ block: @a@ is an 'Int' (sampled off the input bus) but is used +-- with @(&&)@. The erroring statement is not the last statement of the +-- circuit; the error-location test asserts GHC points at the tagged line and +-- not at the end of the block (where the generated @circuitLogic@ and +-- knot-tying bindings live). +module ValueExprError where + +import Circuit +import Clash.Prelude +import Clash.Signal.Internal (Signal ((:-))) + +registerC :: a -> Circuit (Signal dom a) (Signal dom a) +registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) + +valueExprError :: Circuit (Signal dom Int) (Signal dom Int) +valueExprError = circuitS \(Signal a) -> do + Signal b <- registerC 0 -< Signal (a && True) -- value-expr-error-marker + idC -< Signal (b + a) diff --git a/tests/fixtures/ValueLetError.hs b/tests/fixtures/ValueLetError.hs new file mode 100644 index 0000000..9ce5045 --- /dev/null +++ b/tests/fixtures/ValueLetError.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture with a deliberate type error inside a /value-level let/ of a +-- @circuitS@ block: @a@ is an 'Int' (sampled off the input bus) but is +-- passed to 'not'. The let bindings move into the generated @circuitLogic@ +-- function; this asserts they keep their source locations when they do. +module ValueLetError where + +import Circuit +import Clash.Prelude + +valueLetError :: Circuit (Signal dom Int) (Signal dom Int) +valueLetError = circuitS \(Signal a) -> do + let b = not a -- value-let-error-marker + idC -< Signal (a + (if b then 1 else 0)) diff --git a/tests/fixtures/ValuePortError.hs b/tests/fixtures/ValuePortError.hs new file mode 100644 index 0000000..1b0c53d --- /dev/null +++ b/tests/fixtures/ValuePortError.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture with a plugin-level port error in a @circuitS@ block: the bus +-- @b@ is bound but never used, so the plugin itself (not GHC's type checker) +-- reports \"Slave port b has no associated master\" -- pointing at the +-- binding. +module ValuePortError where + +import Circuit +import Clash.Prelude + +valuePortError :: Circuit (Signal dom Int) (Signal dom Int) +valuePortError = circuitS \(Signal a) -> do + b <- idC -< Signal (a + 1) -- value-port-error-marker + idC -< Signal (a * 2) diff --git a/tests/fixtures/ValueShapeError.hs b/tests/fixtures/ValueShapeError.hs new file mode 100644 index 0000000..38fc73c --- /dev/null +++ b/tests/fixtures/ValueShapeError.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture marking a non-signal bus with @Signal@ in a @circuitS@ block: +-- @vecC@ produces a @Vec@ of signals, so the @Signal v@ pattern is \"too +-- shallow\" (the value boundary must sit exactly at a 'Signal'). The +-- generated @SigTag@ pins the bus type to a signal, so GHC reports a clear +-- @Vec ... /~ Signal ...@ mismatch; this asserts it points at the offending +-- statement. +module ValueShapeError where + +import Circuit +import Clash.Prelude + +vecC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) +vecC = Circuit $ \(s :-> _) -> (() :-> (s :> s :> Nil)) + +valueShapeError :: Circuit (Signal dom Int) (Signal dom Int) +valueShapeError = circuitS \(Signal a) -> do + Signal v <- vecC -< Signal (a + 1) -- value-shape-error-marker + idC -< Signal (a + 1) diff --git a/tests/unittests.hs b/tests/unittests.hs index 9a581e7..caf98e9 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -15,8 +15,10 @@ import Clash.Prelude (NFDataX, Signal, System, Vec ((:>), Nil), import Example () import ValueCircuits +-- eta-expanded because Clash's sampleN takes a @HiddenClockResetEnable dom =>@ +-- argument, which only subsumes under DeepSubsumption sample5 :: NFDataX a => Signal System a -> [a] -sample5 = sampleN 5 +sample5 s = sampleN 5 s check :: (Eq a, Show a) => String -> a -> a -> IO Bool check name actual expected From e99bc83983a8dea6a2506f569f656784832326e5 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 06:01:01 +0100 Subject: [PATCH 06/21] Add the multi-domain to circuitS by minimally grouping --- CHANGELOG.md | 7 ++ README.md | 26 +++-- example/ValueCircuits.hs | 34 ++++++ src/CircuitNotation.hs | 180 ++++++++++++++++++++++++----- tests/error-location.hs | 5 + tests/fixtures/CrossDomainError.hs | 27 +++++ tests/unittests.hs | 13 +++ 7 files changed, 259 insertions(+), 33 deletions(-) create mode 100644 tests/fixtures/CrossDomainError.hs diff --git a/CHANGELOG.md b/CHANGELOG.md index 83b1e30..1ca4c27 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,13 @@ signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a lazy let binding. See the README and example/ValueCircuits.hs. + A `circuitS` block can span several clock domains: the value-level + bindings are split into groups connected by shared variables and each + group is lifted with its own `fmap`/`bundle`/`unbundle`, so only buses + whose values actually meet must share a domain. Sharing a value across + domains is rejected by the type checker. Lets that don't touch value land + stay at the bus level, so let-bound sub-circuits can be used with `-<`. + The value boundary is generated with the new `SigTag` pattern synonym (`Circuit` module), which pins the bus type to a `Signal` so that type inference survives nested circuits (the `Fwd` family is not injective) and diff --git a/README.md b/README.md index 81281e5..84892bf 100644 --- a/README.md +++ b/README.md @@ -25,18 +25,30 @@ counter3 = circuitS \_bs -> do idC -< Signal (n' + m') ``` -The plugin collects the value-level bindings into a single pure function, -lifts it to the signal level with `fmap` (using `bundle`/`unbundle` to group -the buses), and ties the feedback knot with a lazy let binding. See +The plugin collects the value-level bindings into pure functions, lifts them +to the signal level with `fmap` (using `bundle`/`unbundle` to group the +buses), and ties feedback knots with lazy let bindings. See example/ValueCircuits.hs for more examples and the expansion of `counter3`. +A single `circuitS` block can span several clock domains: the value-level +bindings are split into groups connected by shared variables, and each group +is lifted independently, so only buses whose values actually meet must share +a clock domain. Two independent counters on two different domains can live +in one block; making their values meet (e.g. `Signal (n + m)`) is an +unsynchronized clock domain crossing and is rejected by the type checker +(cross between domains with explicit bus-level synchronizer circuits +instead). + Notes: - Pattern match down to *exactly* the `Signal` layer, no shallower; the plugin cannot (yet) know which types contain signals, so the boundary has to be explicit. Marking a bus that is not a `Signal` (e.g. a `Vec` of signals) is a type error on the offending statement. -- In a `circuitS` block, `let` statements are value-level: they form the body - of the generated logic function and cannot define new buses or circuits. -- All buses crossing the value boundary must share the same clock domain - (they are combined with `bundle`). +- In a `circuitS` block, `let` statements that use value-level variables + form the bodies of the generated logic functions; `let`s that don't touch + value land (e.g. a let-bound sub-circuit) stay at the bus level and can be + used with `-<`. +- The grouping is syntactic and conservative: shadowing a value-level name + inside a `let` can merge groups that wouldn't strictly need to share a + domain (never the other way around). diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 0e866d7..8da42f7 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -201,6 +201,40 @@ multicastC = circuitS \(Signal a) -> do passthrough :: Circuit (Signal dom Int) (Signal dom Int) passthrough = circuitS \a -> a +-- Multiple clock domains ------------------------------------------------- +-- +-- The plugin splits the value-level logic into groups connected by shared +-- variables and lifts each group with its own fmap/bundle/unbundle, so only +-- buses whose values actually meet must share a clock domain. Sharing a +-- value across domains is an (unsynchronized) clock domain crossing and is +-- rejected by the type checker. + +-- | Two completely independent counters in one @circuitS@ block, on two +-- /different/ clock domains: nothing forces @domA@ and @domB@ together. +dualCounter :: Circuit (Signal domA Bool, Signal domB Bool) (Signal domA Int, Signal domB Int) +dualCounter = circuitS \(_ea, _eb) -> do + Signal n <- registerC 0 -< Signal n' + Signal m <- registerC 8 -< Signal m' + let n' = n + 1 + m' = m + 1 + idC -< (Signal n', Signal m') + +-- | Two independent accumulators, each reading values off its own input +-- bus, on different clock domains. +dualAccum :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int, Signal domB Int) +dualAccum = circuitS \(Signal i, Signal j) -> do + Signal a <- registerC 0 -< Signal (a + i) + Signal b <- registerC 0 -< Signal (b + j) + idC -< (Signal a, Signal b) + +-- | Lets that don't touch any value-level variable stay at the bus level, +-- so sub-circuits can be bound in a let and used with @-<@. +busLevelLet :: Circuit (Signal dom Int) (Signal dom Int) +busLevelLet = circuitS \(Signal x) -> do + let inc = plusOne + Signal y <- inc -< Signal (x + 1) + idC -< Signal (y * 2) + -- Nesting --------------------------------------------------------------- -- | A @circuitS@ used as a sub-circuit inside an ordinary @circuit@. diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 76f555d..aa60adf 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -41,10 +41,15 @@ module CircuitNotation import Control.Exception import qualified Data.Data as Data import Data.Default +import Data.List (partition, sort, sortOn) import Data.Maybe (fromMaybe) import System.IO.Unsafe import Data.Typeable +-- containers +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set + -- ghc import qualified Language.Haskell.TH as TH import qualified GHC @@ -1137,47 +1142,170 @@ circuitSQQExpM' = do circuitMasters .= masters1 circuitBinds .= binds2 - -- In a value circuit the do-block lets are value-level; they form the body - -- of circuitLogic rather than ending up in the outer (bus-level) let. + -- In a value circuit the do-block lets are value-level; they form the + -- bodies of the generated logic functions rather than ending up in the + -- outer (bus-level) let -- except for lets that don't touch any + -- value-level variable, which stay in the outer let (so e.g. a let-bound + -- sub-circuit can still be used with @-<@). lets <- L.use circuitLets completes <- L.use circuitCompletes letTypes <- L.use circuitTypes - let logicLam = lamE [tupP inPats] (letE noSrcSpanA letTypes lets (tupE noSrcSpanA outExprs)) - logicBind = L loc $ patBind (varP noSrcSpanA logicName) logicLam - - -- (outBuses) = unbundle (fmap circuitLogic (bundle (inBuses))) - -- bundle/unbundle are only needed when there is more than one bus. With no - -- inputs at all the logic is constant, so it is mapped over @pure ()@. - let inVars = map (\i -> varE noSrcSpanA (var (inPrefix <> show i))) [0 .. numIns - 1] - outVarPs = map (\i -> varP noSrcSpanA (outPrefix <> show i)) [0 .. numOuts - 1] - - bundled = case inVars of - [] -> varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] - [e] -> e - es -> varE noSrcSpanA (thName 'bundle) `appE` tupE noSrcSpanA es - lifted = varE noSrcSpanA (thName 'fmap) `appE` varE noSrcSpanA (var logicName) `appE` bundled - - knotPat = case outVarPs of - [] -> nlWildPat - ps -> tupP ps - knotExpr = if numOuts > 1 - then varE noSrcSpanA (thName 'unbundle) `appE` lifted - else lifted - knotBind = L loc $ patBind knotPat knotExpr + -- see [value-components] + let valueNames = Set.fromList (concatMap patVarNames inPats <> concatMap bindDefinedNames lets) + valueFvs :: SYB.Data a => a -> Set.Set String + valueFvs a = Set.intersection (freeVarNames a) valueNames + + items = + [ (ItemIn i, Set.fromList (patVarNames p)) | (i, p) <- zip [0 ..] inPats ] <> + [ (ItemOut k, valueFvs e) | (k, e) <- zip [0 ..] outExprs ] <> + [ (ItemLet j, Set.fromList (bindDefinedNames b) `Set.union` valueFvs b) + | (j, b) <- zip [0 ..] lets ] + + itemSeq = \case + ItemIn i -> i + ItemOut k -> numIns + k + ItemLet j -> numIns + numOuts + j + isBoundary = \case ItemLet{} -> False; _ -> True + + groups = sortOn (minimum . map itemSeq . fst) (groupComponents items) + (innerGroups, outerGroups) = partition (any isBoundary . fst) groups + + -- lets disconnected from the value boundary stay in the outer let + outerLets = [ lets !! j | (its, _) <- outerGroups, ItemLet j <- its ] + + -- assign user type signatures to the group that binds their name, + -- splitting multi-name signatures if necessary + nameComp = Map.fromList + [ (n, ci) | (ci, (_, ns)) <- zip [0 :: Int ..] innerGroups, n <- Set.toList ns ] + sigComp (L _ rdr) = case unqualName rdr of + [n] -> Map.lookup n nameComp + _ -> Nothing + splitSigs = concatMap + (\lsig@(L l s) -> case s of + TypeSig x ids ty -> + [ (c, L l (TypeSig x ids' ty)) + | (c, ids') <- Map.toList (Map.fromListWith (flip (<>)) [ (sigComp i, [i]) | i <- ids ]) ] + _ -> [(Nothing, lsig)]) + letTypes + sigsForComp ci = [ s | (Just ci', s) <- splitSigs, ci' == ci ] + outerSigs = [ s | (Nothing, s) <- splitSigs ] + + -- One logic function and one lifted knot binding per group: + -- circuitLogic_cN = \(ins) -> let in (outs) + -- (outBuses) = unbundle (fmap circuitLogic_cN (bundle (inBuses))) + -- bundle/unbundle are only needed when there is more than one bus, and + -- with no inputs at all the logic is constant, so it is mapped over + -- @pure ()@. The generated bundle elements and knot patterns take the + -- source locations of the original Signal markers, so clock domain + -- mismatches are reported on the offending marker. Groups with no + -- outputs produce no value (their logic would be dead) and generate + -- nothing. + mkComp ci (its, _) = + let ins = sort [ i | ItemIn i <- its ] + outs = sort [ k | ItemOut k <- its ] + ls = sort [ j | ItemLet j <- its ] + logicNm = logicName <> "_c" <> show ci + logicLam = lamE [tupP (map (inPats !!) ins)] + (letE noSrcSpanA (sigsForComp ci) (map (lets !!) ls) + (tupE noSrcSpanA (map (outExprs !!) outs))) + logicBind = L loc $ patBind (varP noSrcSpanA logicNm) logicLam + + inVars = map (\i -> let (L l _) = inPats !! i in varE l (var (inPrefix <> show i))) ins + outVarPs = map (\k -> let (L l _) = outExprs !! k in varP l (outPrefix <> show k)) outs + + bundled = case inVars of + [] -> varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] + [e] -> e + es -> varE noSrcSpanA (thName 'bundle) `appE` tupE noSrcSpanA es + lifted = varE noSrcSpanA (thName 'fmap) `appE` varE noSrcSpanA (var logicNm) `appE` bundled + knotExpr = if length outs > 1 + then varE noSrcSpanA (thName 'unbundle) `appE` lifted + else lifted + knotBind = L loc $ patBind (tupP outVarPs) knotExpr + in if null outs then [] else [logicBind, knotBind] + + compDecs = concat (zipWith mkComp [0 ..] innerGroups) -- The bus plumbing is generated exactly as in 'circuitQQExpM'. let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) - let decs = logicBind : knotBind : completes <> map decFromBinding' binds2 + let decs = compDecs <> outerLets <> completes <> map decFromBinding' binds2 let pats = bindOutputs dflags Fwd masters1 slaves1 res = createInputs Bwd slaves1 masters1 body :: LHsExpr GhcPs - body = letE noSrcSpanA [] decs res + body = letE noSrcSpanA outerSigs decs res pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body +-- [value-components] +-- The value-level bindings of a @circuitS@ block are split into the +-- connected components of their shared-variable graph before lifting: an +-- input variable (Signal pattern), output expression (Signal expression) or +-- let binding belongs to the same group as anything it shares a value-level +-- variable with. Each group is lifted with its own fmap/bundle/unbundle, so +-- only buses whose values actually meet are bundled -- which is what allows +-- a single circuitS block to span several clock domains: per-cycle values +-- may only meet if their buses are synchronous, and 'bundle' enforces +-- exactly that per group. Sharing a variable across domains is an +-- (unsynchronized) clock domain crossing and is rejected by the type +-- checker; crossing domains must be done with explicit bus-level +-- synchronizer circuits. +-- +-- The analysis is purely syntactic and conservative: free variables are +-- over-approximated by all unqualified variable occurrences (no scope +-- tracking), so shadowing can only ever merge groups that strictly wouldn't +-- need merging (a false same-domain constraint), never split things that +-- belong together. + +-- | An occurrence of the value boundary (or a let between boundaries) in a +-- @circuitS@ block; the @Int@ indexes into the respective collection. +data ValueItem = ItemIn Int | ItemOut Int | ItemLet Int + +-- | Group items into connected components: items (transitively) sharing a +-- name end up in the same group. +groupComponents :: [(ValueItem, Set.Set String)] -> [([ValueItem], Set.Set String)] +groupComponents = foldl step [] + where + step groups (it, ns) = + let (touching, rest) = partition (\(_, gns) -> not (Set.disjoint ns gns)) groups + in (concatMap fst touching <> [it], Set.unions (ns : map snd touching)) : rest + +unqualName :: GHC.RdrName -> [String] +unqualName = \case + GHC.Unqual occ -> [OccName.occNameString occ] + _ -> [] + +-- | Variable names bound by a pattern (conservative, syntactic; as-pattern +-- names are not collected). +patVarNames :: LPat GhcPs -> [String] +patVarNames = SYB.everything (<>) (SYB.mkQ [] q) + where + q :: Pat GhcPs -> [String] + q = \case + VarPat _ (L _ rdr) -> unqualName rdr + _ -> [] + +-- | All unqualified variable occurrences: a conservative over-approximation +-- of the free variables (bound variables of nested lambdas/lets/cases are +-- included). +freeVarNames :: SYB.Data a => a -> Set.Set String +freeVarNames = Set.fromList . SYB.everything (<>) (SYB.mkQ [] q) + where + q :: HsExpr GhcPs -> [String] + q = \case + HsVar _ (L _ rdr) -> unqualName rdr + _ -> [] + +-- | The names a let binding defines. +bindDefinedNames :: LHsBind GhcPs -> [String] +bindDefinedNames (L _ b) = case b of + FunBind { fun_id = L _ rdr } -> unqualName rdr + PatBind { pat_lhs = lpat } -> patVarNames lpat + VarBind { var_id = rdr } -> unqualName rdr + _ -> [] + grr :: MonadIO m => OccName.NameSpace -> m () grr nm | nm == OccName.tcName = liftIO $ putStrLn "tcName" diff --git a/tests/error-location.hs b/tests/error-location.hs index 71fb071..65a5dbb 100644 --- a/tests/error-location.hs +++ b/tests/error-location.hs @@ -50,6 +50,11 @@ fixtures = -- shallow"); the SigTag the plugin generates should turn this into a -- direct Vec-vs-Signal mismatch on the offending pattern , Fixture ("tests" "fixtures" "ValueShapeError.hs") "value-shape-error-marker" Nothing + -- sharing a value-level variable across two clock domains; the merged + -- group's bundle demands one domain, so this must be a domain-mismatch + -- type error + , Fixture ("tests" "fixtures" "CrossDomainError.hs") "cross-domain-error-marker" + (Just "Couldn't match type") ] main :: IO () diff --git a/tests/fixtures/CrossDomainError.hs b/tests/fixtures/CrossDomainError.hs new file mode 100644 index 0000000..fe1eae1 --- /dev/null +++ b/tests/fixtures/CrossDomainError.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture sharing a value-level variable across two clock domains in a +-- @circuitS@ block: @acc + a + b@ mixes values sampled from a @domA@ bus and +-- a @domB@ bus, which is an (unsynchronized) clock domain crossing. The +-- shared variables put both buses in the same logic group, whose @bundle@ +-- demands a single domain, so GHC reports @Couldn't match type domA with +-- domB@. The blame lands on the head of the circuit (the constraint solver +-- unifies the domains via the generated bundle before it checks the slave +-- pattern), so the marker sits on the @circuitS@ line. +module CrossDomainError where + +import Circuit +import Clash.Prelude +import Clash.Signal.Internal (Signal ((:-))) + +registerC :: a -> Circuit (Signal dom a) (Signal dom a) +registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) + +crossDomainError :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int) +crossDomainError = circuitS \(Signal a, Signal b) -> do -- cross-domain-error-marker + Signal acc <- registerC 0 -< Signal (acc + a + b) + idC -< Signal acc diff --git a/tests/unittests.hs b/tests/unittests.hs index caf98e9..d0768e9 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -12,6 +12,7 @@ import System.Exit (exitFailure) import Clash.Prelude (NFDataX, Signal, System, Vec ((:>), Nil), fromList, sampleN) +import Circuit (Circuit) import Example () import ValueCircuits @@ -70,6 +71,18 @@ main = do , check "multicastC" (sample5 mcA, sample5 mcB) ([1, 2, 3, 4, 5], [1, 2, 3, 4, 5]) , check "passthrough" (sample5 (simulateC passthrough (fromList [3 ..]))) [3, 4, 5, 6, 7] + -- multiple clock domains (instantiated at the same domain here; the + -- different-domain property is the fact that the signatures compile) + , let (dcA, dcB) = simulateC + (dualCounter :: Circuit (Signal System Bool, Signal System Bool) (Signal System Int, Signal System Int)) + (pure False, pure False) + in check "dualCounter" (sample5 dcA, sample5 dcB) ([1, 2, 3, 4, 5], [9, 10, 11, 12, 13]) + , let (daA, daB) = simulateC + (dualAccum :: Circuit (Signal System Int, Signal System Int) (Signal System Int, Signal System Int)) + (fromList [1 ..], fromList [10, 20 ..]) + in check "dualAccum" (sample5 daA, sample5 daB) ([0, 1, 3, 6, 10], [0, 10, 30, 60, 100]) + , check "busLevelLet" (sample5 (simulateC busLevelLet (fromList [0 ..]))) [4, 6, 8, 10, 12] + -- nesting , check "nestedSInCircuit" (sample5 (simulateC nestedSInCircuit (fromList [0 ..]))) [0, 2, 4, 6, 8] , check "nestedCircuitInS" (sample5 (simulateC nestedCircuitInS (fromList [0 ..]))) [3, 6, 9, 12, 15] From 2aa3f11fa0ef2b6d3f9305212bb9fab4b3b3ee2c Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 08:52:21 +0100 Subject: [PATCH 07/21] Change name to circuitV --- CHANGELOG.md | 4 +- README.md | 10 ++--- example/ValueCircuits.hs | 72 ++++++++++++++++-------------- src/Circuit.hs | 2 +- src/CircuitNotation.hs | 66 ++++++++++++++------------- tests/error-location.hs | 8 ++-- tests/fixtures/CrossDomainError.hs | 6 +-- tests/fixtures/ValueExprError.hs | 4 +- tests/fixtures/ValueLetError.hs | 4 +- tests/fixtures/ValuePortError.hs | 4 +- tests/fixtures/ValueShapeError.hs | 4 +- tests/unittests.hs | 3 +- 12 files changed, 99 insertions(+), 88 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1ca4c27..ba82d8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,13 +2,13 @@ ## Unreleased -* Add value-level circuits via the new `circuitS` keyword. The circuit's +* Add value-level circuits via the new `circuitV` keyword. The circuit's logic is written over the values sampled each clock cycle (marked with `Signal`/`Fwd` patterns and expressions); the plugin lifts it back to the signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a lazy let binding. See the README and example/ValueCircuits.hs. - A `circuitS` block can span several clock domains: the value-level + A `circuitV` block can span several clock domains: the value-level bindings are split into groups connected by shared variables and each group is lifted with its own `fmap`/`bundle`/`unbundle`, so only buses whose values actually meet must share a domain. Sharing a value across diff --git a/README.md b/README.md index 84892bf..c963c0b 100644 --- a/README.md +++ b/README.md @@ -3,9 +3,9 @@ This is a plugin for manipulating circuits in clash with arrow notation. See example/Example.hs for example usage. Also see [clash-protocols](https://github.com/clash-lang/clash-protocols#). -## Value-level circuits (`circuitS`) +## Value-level circuits (`circuitV`) -The `circuitS` keyword describes a circuit's logic over the *values sampled +The `circuitV` keyword describes a circuit's logic over the *values sampled each clock cycle* instead of over whole buses. The boundary between bus land and value land is marked with `Signal` (or `Fwd`): @@ -17,7 +17,7 @@ Haskell, and feedback loops are written as ordinary recursive `let`s: ```haskell counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuitS \_bs -> do +counter3 = circuitV \_bs -> do Signal n <- registerC 0 -< Signal n' -- n :: Int (this cycle's value) Signal m <- registerC 8 -< Signal m' -- m :: Int let n' = n + 1 -- pure, value-level @@ -30,7 +30,7 @@ to the signal level with `fmap` (using `bundle`/`unbundle` to group the buses), and ties feedback knots with lazy let bindings. See example/ValueCircuits.hs for more examples and the expansion of `counter3`. -A single `circuitS` block can span several clock domains: the value-level +A single `circuitV` block can span several clock domains: the value-level bindings are split into groups connected by shared variables, and each group is lifted independently, so only buses whose values actually meet must share a clock domain. Two independent counters on two different domains can live @@ -45,7 +45,7 @@ Notes: plugin cannot (yet) know which types contain signals, so the boundary has to be explicit. Marking a bus that is not a `Signal` (e.g. a `Vec` of signals) is a type error on the offending statement. -- In a `circuitS` block, `let` statements that use value-level variables +- In a `circuitV` block, `let` statements that use value-level variables form the bodies of the generated logic functions; `let`s that don't touch value land (e.g. a let-bound sub-circuit) stay at the bus level and can be used with `-<`. diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 8da42f7..3dd23bd 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -7,7 +7,7 @@ ╚═════╝╚═╝╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝ ╚══════╝ (C) 2020, Christopher Chalmers -Examples of value-level circuits (the 'circuitS' keyword). These are +Examples of value-level circuits (the 'circuitV' keyword). These are simulated and checked by tests/unittests.hs. -} @@ -42,58 +42,62 @@ simulateC c aFwd = let (_ :-> bFwd) = runCircuit c (aFwd :-> unitBwd) in bFwd -- feedback. @a@ is the per-cycle 'Int' carried on the bus, not the bus -- itself; no @bundle@/@unbundle@ is generated for single buses. plusOne :: Circuit (Signal dom Int) (Signal dom Int) -plusOne = circuitS \(Signal a) -> do +plusOne = circuitV \(Signal a) -> do idC -< Signal (a + 1) +-- | The same as 'plusOne' without a do block: a bare expression body. +plusOneBare :: Circuit (Signal dom Int) (Signal dom Int) +plusOneBare = circuitV \(Signal a) -> Signal (a + 1) + -- | The @Fwd@ keyword can be used interchangeably with @Signal@ to mark the -- value boundary. plusOneFwd :: Circuit (Signal dom Int) (Signal dom Int) -plusOneFwd = circuitS \(Fwd a) -> do +plusOneFwd = circuitV \(Fwd a) -> do idC -< Fwd (a + 1) -- | No value inputs at all: the logic is constant. alwaysFive :: Circuit () (Signal dom Int) -alwaysFive = circuitS do +alwaysFive = circuitV do idC -< Signal (5 :: Int) -- | Two value inputs, one value output (a single @bundle@, no @unbundle@). addC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int) -addC = circuitS \(Signal a, Signal b) -> do +addC = circuitV \(Signal a, Signal b) -> do idC -< Signal (a + b) -- | One value input, two value outputs (a single @unbundle@, no @bundle@). fanOutC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) -fanOutC = circuitS \(Signal a) -> do +fanOutC = circuitV \(Signal a) -> do idC -< (Signal (a + 1), Signal (a * 2)) -- | Values can be matched out of a bus carrying a compound type ... splitC :: Circuit (Signal dom (Int, Bool)) (Signal dom Int, Signal dom Bool) -splitC = circuitS \(Signal (a, b)) -> do +splitC = circuitV \(Signal (a, b)) -> do idC -< (Signal a, Signal b) -- | ... and combined back onto one. joinC :: Circuit (Signal dom Int, Signal dom Bool) (Signal dom (Int, Bool)) -joinC = circuitS \(Signal a, Signal b) -> do +joinC = circuitV \(Signal a, Signal b) -> do idC -< Signal (a, b) -- | Ports nest like in ordinary circuit notation. nestedTupleC :: Circuit ((Signal dom Int, Signal dom Int), Signal dom Int) (Signal dom Int) -nestedTupleC = circuitS \((Signal a, Signal b), Signal c) -> do +nestedTupleC = circuitV \((Signal a, Signal b), Signal c) -> do idC -< Signal (a + b * c) -- | Value boundaries inside 'Vec' buses. vecInC :: Circuit (Vec 2 (Signal dom Int)) (Signal dom Int) -vecInC = circuitS \[Signal a, Signal b] -> do +vecInC = circuitV \[Signal a, Signal b] -> do idC -< Signal (a - b) vecOutC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) -vecOutC = circuitS \(Signal a) -> do +vecOutC = circuitV \(Signal a) -> do idC -< [Signal (a + 1), Signal (a - 1)] -- | Ports crossing the value boundary can be given bus-level type -- annotations like any other port. annotatedC :: forall dom. Circuit (Signal dom Int) (Signal dom Int) -annotatedC = circuitS \((Signal a) :: Signal dom Int) -> do +annotatedC = circuitV \((Signal a) :: Signal dom Int) -> do idC -< Signal (a + 1) -- Feedback ------------------------------------------------------------- @@ -102,7 +106,7 @@ annotatedC = circuitS \((Signal a) :: Signal dom Int) -> do -- @n'@ is defined in terms of its output @n@ by an ordinary recursive @let@; -- the plugin ties the knot at the signal level. counter :: Circuit () (Signal dom Int) -counter = circuitS do +counter = circuitV do Signal n <- registerC 0 -< Signal n' let n' = n + 1 idC -< Signal n @@ -110,7 +114,7 @@ counter = circuitS do -- | A Mealy-style accumulator: reads the per-cycle value off the input bus -- and feeds back state through a register. Written with a @$@ chain. accum :: Circuit (Signal dom Int) (Signal dom Int) -accum = circuitS $ \(Signal i) -> do +accum = circuitV $ \(Signal i) -> do Signal acc <- registerC 0 -< Signal acc' let acc' = acc + i idC -< Signal acc' @@ -118,7 +122,7 @@ accum = circuitS $ \(Signal i) -> do -- | Two interleaved feedback loops (the canonical example from the design -- notes). The bus input is ignored. counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuitS \_bs -> do +counter3 = circuitV \_bs -> do Signal n <- registerC 0 -< Signal n' Signal m <- registerC 8 -< Signal m' let n' = n + 1 @@ -151,14 +155,14 @@ counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> -- | Compound state fed back through a /single/ register: a fibonacci -- machine. The pair is destructured and rebuilt at the value level. fibC :: Circuit () (Signal dom Int) -fibC = circuitS do +fibC = circuitV do Signal (a, b) <- registerC (0, 1) -< Signal (b, a + b) idC -< Signal a -- | A chain of registers: a three-deep shift register (no feedback, but a -- value passes through several binds). shift3 :: Circuit (Signal dom Int) (Signal dom Int) -shift3 = circuitS \(Signal i) -> do +shift3 = circuitV \(Signal i) -> do Signal a <- registerC 0 -< Signal i Signal b <- registerC 0 -< Signal a Signal c <- registerC 0 -< Signal b @@ -167,7 +171,7 @@ shift3 = circuitS \(Signal i) -> do -- | Three rotating registers plus the bus input: a four-way bundle on both -- sides of the logic function. rotate3 :: Circuit (Signal dom Int) (Signal dom Int) -rotate3 = circuitS \(Signal i) -> do +rotate3 = circuitV \(Signal i) -> do Signal a <- registerC 1 -< Signal a' Signal b <- registerC 2 -< Signal b' Signal c <- registerC 3 -< Signal c' @@ -181,25 +185,25 @@ rotate3 = circuitS \(Signal i) -> do -- | Value-level and bus-level ports can be mixed: the second bus is routed -- through untouched while the first is sampled and modified. mixedC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int, Signal dom Int) -mixedC = circuitS \(Signal a, b) -> do +mixedC = circuitV \(Signal a, b) -> do idC -< (Signal (a + 1), b) -- | As 'mixedC' but with a 'DF' bus (whose backwards channel is not -- trivial) routed through. mixedDfC :: Circuit (Signal dom Int, DF dom Bool) (Signal dom Int, DF dom Bool) -mixedDfC = circuitS \(Signal a, df) -> do +mixedDfC = circuitV \(Signal a, df) -> do idC -< (Signal (a + 1), df) -- | A bus created from a value can be multicast like any other bus. multicastC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) -multicastC = circuitS \(Signal a) -> do +multicastC = circuitV \(Signal a) -> do b <- idC -< Signal (a + 1) idC -< (b, b) --- | Without any value-level (@Signal@/@Fwd@) markers, @circuitS@ behaves +-- | Without any value-level (@Signal@/@Fwd@) markers, @circuitV@ behaves -- exactly like @circuit@. passthrough :: Circuit (Signal dom Int) (Signal dom Int) -passthrough = circuitS \a -> a +passthrough = circuitV \a -> a -- Multiple clock domains ------------------------------------------------- -- @@ -209,10 +213,10 @@ passthrough = circuitS \a -> a -- value across domains is an (unsynchronized) clock domain crossing and is -- rejected by the type checker. --- | Two completely independent counters in one @circuitS@ block, on two +-- | Two completely independent counters in one @circuitV@ block, on two -- /different/ clock domains: nothing forces @domA@ and @domB@ together. dualCounter :: Circuit (Signal domA Bool, Signal domB Bool) (Signal domA Int, Signal domB Int) -dualCounter = circuitS \(_ea, _eb) -> do +dualCounter = circuitV \(_ea, _eb) -> do Signal n <- registerC 0 -< Signal n' Signal m <- registerC 8 -< Signal m' let n' = n + 1 @@ -222,7 +226,7 @@ dualCounter = circuitS \(_ea, _eb) -> do -- | Two independent accumulators, each reading values off its own input -- bus, on different clock domains. dualAccum :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int, Signal domB Int) -dualAccum = circuitS \(Signal i, Signal j) -> do +dualAccum = circuitV \(Signal i, Signal j) -> do Signal a <- registerC 0 -< Signal (a + i) Signal b <- registerC 0 -< Signal (b + j) idC -< (Signal a, Signal b) @@ -230,27 +234,27 @@ dualAccum = circuitS \(Signal i, Signal j) -> do -- | Lets that don't touch any value-level variable stay at the bus level, -- so sub-circuits can be bound in a let and used with @-<@. busLevelLet :: Circuit (Signal dom Int) (Signal dom Int) -busLevelLet = circuitS \(Signal x) -> do +busLevelLet = circuitV \(Signal x) -> do let inc = plusOne Signal y <- inc -< Signal (x + 1) idC -< Signal (y * 2) -- Nesting --------------------------------------------------------------- --- | A @circuitS@ used as a sub-circuit inside an ordinary @circuit@. +-- | A @circuitV@ used as a sub-circuit inside an ordinary @circuit@. nestedSInCircuit :: Circuit (Signal dom Int) (Signal dom Int) nestedSInCircuit = circuit $ \a -> do - b <- (circuitS \(Signal x) -> do idC -< Signal (x * 2)) -< a + b <- (circuitV \(Signal x) -> do idC -< Signal (x * 2)) -< a idC -< b --- | An ordinary @circuit@ used as a sub-circuit inside a @circuitS@. +-- | An ordinary @circuit@ used as a sub-circuit inside a @circuitV@. nestedCircuitInS :: Circuit (Signal dom Int) (Signal dom Int) -nestedCircuitInS = circuitS \(Signal x) -> do +nestedCircuitInS = circuitV \(Signal x) -> do Signal y <- (circuit \b -> b) -< Signal (x + 1) idC -< Signal (y * 3) --- | A @circuitS@ inside another @circuitS@. +-- | A @circuitV@ inside another @circuitV@. nestedSInS :: Circuit (Signal dom Int) (Signal dom Int) -nestedSInS = circuitS \(Signal x) -> do - Signal y <- (circuitS \(Signal a) -> do idC -< Signal (a + 1)) -< Signal x +nestedSInS = circuitV \(Signal x) -> do + Signal y <- (circuitV \(Signal a) -> do idC -< Signal (a + 1)) -< Signal x idC -< Signal (y * 2) diff --git a/src/Circuit.hs b/src/Circuit.hs index 9ffdff9..c1fbb98 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -209,7 +209,7 @@ pattern BusTagBundle a <- (taggedUnbundle -> a) where {-# COMPLETE BusTagBundle #-} -- | A tagged 'Signal' bus. Used by the plugin at the value boundary of --- 'circuitS' blocks: matching or constructing with 'SigTag' pins the bus +-- 'circuitV' blocks: matching or constructing with 'SigTag' pins the bus -- type itself (the tag) to be a 'Signal', which is what the value boundary -- requires. Since 'Fwd' is not injective, plain 'BusTag' would leave the bus -- type ambiguous and type inference for nested circuits would fail. diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index aa60adf..3ddcd7c 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -34,6 +34,7 @@ module CircuitNotation , mkPlugin , thName , ExternalNames (..) + , defExternalNames , Direction(..) ) where @@ -134,8 +135,8 @@ isCircuitVar :: p ~ GhcPs => HsExpr p -> Bool isCircuitVar = isSomeVar "circuit" -- | Is the variable for the value-level circuit keyword? -isCircuitSVar :: p ~ GhcPs => HsExpr p -> Bool -isCircuitSVar = isSomeVar "circuitS" +isCircuitVVar :: p ~ GhcPs => HsExpr p -> Bool +isCircuitVVar = isSomeVar "circuitV" isDollar :: p ~ GhcPs => HsExpr p -> Bool isDollar = isSomeVar "$" @@ -229,10 +230,10 @@ data PortDescription a | FwdExpr (LHsExpr GhcPs) | FwdPat (LPat GhcPs) | SigTagExpr (LHsExpr GhcPs) - -- ^ generated by @circuitS@: a value-boundary bus expression, tagged with + -- ^ generated by @circuitV@: a value-boundary bus expression, tagged with -- 'SigTag' to pin the bus type to a signal | SigTagPat (LPat GhcPs) - -- ^ generated by @circuitS@: a value-boundary bus pattern, tagged with + -- ^ generated by @circuitV@: a value-boundary bus pattern, tagged with -- 'SigTag' to pin the bus type to a signal | PortType (LHsType GhcPs) (PortDescription a) | PortErr SrcSpanAnnA MsgDoc @@ -264,7 +265,7 @@ data CircuitState dec exp nm = CircuitState { _cErrors :: Bag ErrMsg , _counter :: Int -- ^ unique counter for generated variables - , _circuitSlaves :: PortDescription nm + , _circuitVlaves :: PortDescription nm -- ^ the final statement in a circuit , _circuitTypes :: [LSig GhcPs] -- ^ type signatures in let bindings @@ -302,7 +303,7 @@ runCircuitM (CircuitM m) = do let emptyCircuitState = CircuitState { _cErrors = emptyBag , _counter = 0 - , _circuitSlaves = Tuple [] + , _circuitVlaves = Tuple [] , _circuitTypes = [] , _circuitLets = [] , _circuitCompletes = [] @@ -596,7 +597,7 @@ parseCircuit = \case -- a lambda to match the slave ports L _ (simpleLambda -> Just ([matchPats], body)) -> do - circuitSlaves .= bindSlave matchPats + circuitVlaves .= bindSlave matchPats circuitBody body -- a version without a lambda (i.e. no slaves) @@ -744,7 +745,7 @@ data Dir = Slave | Master checkCircuit :: p ~ GhcPs => CircuitM () checkCircuit = do - slaves <- L.use circuitSlaves + slaves <- L.use circuitVlaves masters <- L.use circuitMasters binds <- L.use circuitBinds @@ -780,7 +781,7 @@ checkCircuit = do p -> p -- update relevant master ports to be multicast - circuitSlaves %= L.transform modifyMulticast + circuitVlaves %= L.transform modifyMulticast circuitMasters %= L.transform modifyMulticast circuitBinds . L.mapped %= \b -> b { bIn = L.transform modifyMulticast (bIn b), @@ -1011,7 +1012,7 @@ circuitQQExpM = do lets <- L.use circuitLets completes <- L.use circuitCompletes letTypes <- L.use circuitTypes - slaves <- L.use circuitSlaves + slaves <- L.use circuitVlaves masters <- L.use circuitMasters -- Construction of the circuit expression. @@ -1035,7 +1036,7 @@ circuitQQExpM = do pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body --- Value circuits (circuitS) -------------------------------------------- +-- Value circuits (circuitV) -------------------------------------------- -- | The number of value-level ('FwdPat' / 'FwdExpr') ports in a port -- description. @@ -1070,7 +1071,7 @@ replaceFwdExprs prefix = L.transformM \case pure (SigTagExpr (varE loc (var (prefix <> show i)))) p -> pure p --- | The @circuitS@ (value-level circuit) version of 'circuitQQExpM'. +-- | The @circuitV@ (value-level circuit) version of 'circuitQQExpM'. -- -- Value-level circuits describe a circuit's logic over the values sampled -- each clock cycle. The boundary between bus land and value land is marked @@ -1090,11 +1091,11 @@ replaceFwdExprs prefix = L.transformM \case -- @ -- -- The buses themselves are wired up exactly as for an ordinary @circuit@. -circuitSQQExpM +circuitVQQExpM :: (p ~ GhcPs, ?nms :: ExternalNames) => CircuitM (LHsExpr p) -circuitSQQExpM = do - slaves0 <- L.use circuitSlaves +circuitVQQExpM = do + slaves0 <- L.use circuitVlaves masters0 <- L.use circuitMasters binds0 <- L.use circuitBinds @@ -1103,19 +1104,19 @@ circuitSQQExpM = do -- Without any value-level (Signal/Fwd) ports there is no boundary to lift; -- behave exactly like an ordinary circuit. - if boundaryCount == 0 then circuitQQExpM else circuitSQQExpM' + if boundaryCount == 0 then circuitQQExpM else circuitVQQExpM' -circuitSQQExpM' +circuitVQQExpM' :: (p ~ GhcPs, ?nms :: ExternalNames) => CircuitM (LHsExpr p) -circuitSQQExpM' = do +circuitVQQExpM' = do checkCircuit dflags <- GHC.getDynFlags loc <- L.use circuitLoc -- read the ports after checkCircuit, which may have rewritten them - slaves0 <- L.use circuitSlaves + slaves0 <- L.use circuitVlaves masters0 <- L.use circuitMasters binds0 <- L.use circuitBinds @@ -1138,7 +1139,7 @@ circuitSQQExpM' = do pure (bs, m) ((binds2, masters1), (numOuts, outExprs)) = runState outM (0, []) - circuitSlaves .= slaves1 + circuitVlaves .= slaves1 circuitMasters .= masters1 circuitBinds .= binds2 @@ -1240,13 +1241,13 @@ circuitSQQExpM' = do pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body -- [value-components] --- The value-level bindings of a @circuitS@ block are split into the +-- The value-level bindings of a @circuitV@ block are split into the -- connected components of their shared-variable graph before lifting: an -- input variable (Signal pattern), output expression (Signal expression) or -- let binding belongs to the same group as anything it shares a value-level -- variable with. Each group is lifted with its own fmap/bundle/unbundle, so -- only buses whose values actually meet are bundled -- which is what allows --- a single circuitS block to span several clock domains: per-cycle values +-- a single circuitV block to span several clock domains: per-cycle values -- may only meet if their buses are synchronous, and 'bundle' enforces -- exactly that per group. Sharing a variable across domains is an -- (unsynchronized) clock domain crossing and is rejected by the type @@ -1260,7 +1261,7 @@ circuitSQQExpM' = do -- belong together. -- | An occurrence of the value boundary (or a let between boundaries) in a --- @circuitS@ block; the @Int@ indexes into the respective collection. +-- @circuitV@ block; the @Int@ indexes into the respective collection. data ValueItem = ItemIn Int | ItemOut Int | ItemLet Int -- | Group items into connected components: items (transitively) sharing a @@ -1320,7 +1321,7 @@ completeUnderscores :: (?nms :: ExternalNames) => CircuitM () completeUnderscores = do binds <- L.use circuitBinds masters <- L.use circuitMasters - slaves <- L.use circuitSlaves + slaves <- L.use circuitVlaves let addDef :: String -> PortDescription PortName -> CircuitM () addDef suffix = \case Ref (PortName loc (unpackFS -> name@('_':_))) -> do @@ -1351,8 +1352,8 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where x <- parseCircuit lappB >> completeUnderscores >> circuitQQExpM when debug $ ppr x pure x - | isCircuitSVar circuitVar = runCircuitM $ do - x <- parseCircuit lappB >> completeUnderscores >> circuitSQQExpM + | isCircuitVVar circuitVar = runCircuitM $ do + x <- parseCircuit lappB >> completeUnderscores >> circuitVQQExpM when debug $ ppr x pure x @@ -1363,11 +1364,11 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where x <- parseCircuit appR >> completeUnderscores >> circuitQQExpM when debug $ ppr x pure (dollarChainReplaceCircuit "circuit" x c) - | isDollar infixVar && dollarChainIsCircuit "circuitS" circuitVar = do + | isDollar infixVar && dollarChainIsCircuit "circuitV" circuitVar = do runCircuitM $ do - x <- parseCircuit appR >> completeUnderscores >> circuitSQQExpM + x <- parseCircuit appR >> completeUnderscores >> circuitVQQExpM when debug $ ppr x - pure (dollarChainReplaceCircuit "circuitS" x c) + pure (dollarChainReplaceCircuit "circuitV" x c) transform' e = pure e @@ -1453,7 +1454,7 @@ data ExternalNames = ExternalNames , tagName :: GHC.RdrName , signalTagName :: GHC.RdrName -- ^ a (pattern synonym) variant of 'tagName' whose type pins the bus to be - -- a signal; used at the value boundary of @circuitS@ blocks + -- a signal; used at the value boundary of @circuitV@ blocks , tagTName :: GHC.RdrName , fwdBwdCon :: GHC.RdrName , fwdAndBwdTypes :: Direction -> GHC.RdrName @@ -1461,6 +1462,11 @@ data ExternalNames = ExternalNames , consPat :: GHC.RdrName } +-- | The names used by the plugin by default, referring to the @Circuit@ +-- module of this package. Custom plugins are encouraged to build their +-- names as a record update of this, so that newly added fields (which +-- happens when the notation grows new features) default to something +-- sensible. defExternalNames :: ExternalNames defExternalNames = ExternalNames { circuitCon = GHC.Unqual (OccName.mkDataOcc "TagCircuit") diff --git a/tests/error-location.hs b/tests/error-location.hs index 65a5dbb..1c701e8 100644 --- a/tests/error-location.hs +++ b/tests/error-location.hs @@ -3,7 +3,7 @@ -- When bus tagging (the @BusTag@ wrapping) was introduced, type errors on a -- bus stopped pointing at the offending statement and instead pointed at the -- end of the @circuit@ block, which made them very hard to act on. The same --- concern applies to @circuitS@ blocks, where the value-level expressions and +-- concern applies to @circuitV@ blocks, where the value-level expressions and -- lets are moved into a generated @circuitLogic@ function. -- -- Each fixture in 'fixtures' deliberately fails to compile, with the @@ -39,11 +39,11 @@ fixtures :: [Fixture] fixtures = [ -- type error on a bus in an ordinary circuit Fixture ("tests" "fixtures" "BusError.hs") "bus-error-marker" Nothing - -- type error on a value-level expression in a circuitS + -- type error on a value-level expression in a circuitV , Fixture ("tests" "fixtures" "ValueExprError.hs") "value-expr-error-marker" Nothing - -- type error inside a value-level let in a circuitS + -- type error inside a value-level let in a circuitV , Fixture ("tests" "fixtures" "ValueLetError.hs") "value-let-error-marker" Nothing - -- port error reported by the plugin itself in a circuitS + -- port error reported by the plugin itself in a circuitV , Fixture ("tests" "fixtures" "ValuePortError.hs") "value-port-error-marker" (Just "has no associated master") -- a Signal marker on a bus that is not a signal (the marker is "too diff --git a/tests/fixtures/CrossDomainError.hs b/tests/fixtures/CrossDomainError.hs index fe1eae1..61db014 100644 --- a/tests/fixtures/CrossDomainError.hs +++ b/tests/fixtures/CrossDomainError.hs @@ -5,13 +5,13 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture sharing a value-level variable across two clock domains in a --- @circuitS@ block: @acc + a + b@ mixes values sampled from a @domA@ bus and +-- @circuitV@ block: @acc + a + b@ mixes values sampled from a @domA@ bus and -- a @domB@ bus, which is an (unsynchronized) clock domain crossing. The -- shared variables put both buses in the same logic group, whose @bundle@ -- demands a single domain, so GHC reports @Couldn't match type domA with -- domB@. The blame lands on the head of the circuit (the constraint solver -- unifies the domains via the generated bundle before it checks the slave --- pattern), so the marker sits on the @circuitS@ line. +-- pattern), so the marker sits on the @circuitV@ line. module CrossDomainError where import Circuit @@ -22,6 +22,6 @@ registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) crossDomainError :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int) -crossDomainError = circuitS \(Signal a, Signal b) -> do -- cross-domain-error-marker +crossDomainError = circuitV \(Signal a, Signal b) -> do -- cross-domain-error-marker Signal acc <- registerC 0 -< Signal (acc + a + b) idC -< Signal acc diff --git a/tests/fixtures/ValueExprError.hs b/tests/fixtures/ValueExprError.hs index 3ff8d39..4418942 100644 --- a/tests/fixtures/ValueExprError.hs +++ b/tests/fixtures/ValueExprError.hs @@ -5,7 +5,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture with a deliberate type error on a /value-level/ expression in a --- @circuitS@ block: @a@ is an 'Int' (sampled off the input bus) but is used +-- @circuitV@ block: @a@ is an 'Int' (sampled off the input bus) but is used -- with @(&&)@. The erroring statement is not the last statement of the -- circuit; the error-location test asserts GHC points at the tagged line and -- not at the end of the block (where the generated @circuitLogic@ and @@ -20,6 +20,6 @@ registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) valueExprError :: Circuit (Signal dom Int) (Signal dom Int) -valueExprError = circuitS \(Signal a) -> do +valueExprError = circuitV \(Signal a) -> do Signal b <- registerC 0 -< Signal (a && True) -- value-expr-error-marker idC -< Signal (b + a) diff --git a/tests/fixtures/ValueLetError.hs b/tests/fixtures/ValueLetError.hs index 9ce5045..eb1ee3d 100644 --- a/tests/fixtures/ValueLetError.hs +++ b/tests/fixtures/ValueLetError.hs @@ -5,7 +5,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture with a deliberate type error inside a /value-level let/ of a --- @circuitS@ block: @a@ is an 'Int' (sampled off the input bus) but is +-- @circuitV@ block: @a@ is an 'Int' (sampled off the input bus) but is -- passed to 'not'. The let bindings move into the generated @circuitLogic@ -- function; this asserts they keep their source locations when they do. module ValueLetError where @@ -14,6 +14,6 @@ import Circuit import Clash.Prelude valueLetError :: Circuit (Signal dom Int) (Signal dom Int) -valueLetError = circuitS \(Signal a) -> do +valueLetError = circuitV \(Signal a) -> do let b = not a -- value-let-error-marker idC -< Signal (a + (if b then 1 else 0)) diff --git a/tests/fixtures/ValuePortError.hs b/tests/fixtures/ValuePortError.hs index 1b0c53d..adcc1c7 100644 --- a/tests/fixtures/ValuePortError.hs +++ b/tests/fixtures/ValuePortError.hs @@ -4,7 +4,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} --- | A fixture with a plugin-level port error in a @circuitS@ block: the bus +-- | A fixture with a plugin-level port error in a @circuitV@ block: the bus -- @b@ is bound but never used, so the plugin itself (not GHC's type checker) -- reports \"Slave port b has no associated master\" -- pointing at the -- binding. @@ -14,6 +14,6 @@ import Circuit import Clash.Prelude valuePortError :: Circuit (Signal dom Int) (Signal dom Int) -valuePortError = circuitS \(Signal a) -> do +valuePortError = circuitV \(Signal a) -> do b <- idC -< Signal (a + 1) -- value-port-error-marker idC -< Signal (a * 2) diff --git a/tests/fixtures/ValueShapeError.hs b/tests/fixtures/ValueShapeError.hs index 38fc73c..0c92828 100644 --- a/tests/fixtures/ValueShapeError.hs +++ b/tests/fixtures/ValueShapeError.hs @@ -4,7 +4,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} --- | A fixture marking a non-signal bus with @Signal@ in a @circuitS@ block: +-- | A fixture marking a non-signal bus with @Signal@ in a @circuitV@ block: -- @vecC@ produces a @Vec@ of signals, so the @Signal v@ pattern is \"too -- shallow\" (the value boundary must sit exactly at a 'Signal'). The -- generated @SigTag@ pins the bus type to a signal, so GHC reports a clear @@ -19,6 +19,6 @@ vecC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) vecC = Circuit $ \(s :-> _) -> (() :-> (s :> s :> Nil)) valueShapeError :: Circuit (Signal dom Int) (Signal dom Int) -valueShapeError = circuitS \(Signal a) -> do +valueShapeError = circuitV \(Signal a) -> do Signal v <- vecC -< Signal (a + 1) -- value-shape-error-marker idC -< Signal (a + 1) diff --git a/tests/unittests.hs b/tests/unittests.hs index d0768e9..890eaa9 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -37,7 +37,8 @@ main = do results <- sequence -- basic shapes - [ check "plusOne" (sample5 (simulateC plusOne (fromList [0 ..]))) [1, 2, 3, 4, 5] + [ check "plusOne" (sample5 (simulateC plusOne (fromList [0 ..]))) [1, 2, 3, 4, 5] + , check "plusOneBare" (sample5 (simulateC plusOneBare (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) From 2a1bb946a475219c83c1c45909cb47a1f637c52c Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 09:33:36 +0100 Subject: [PATCH 08/21] Make a new SignalBus class for handling Fwd with circuitV --- CHANGELOG.md | 22 ++++++++--- README.md | 21 +++++++++-- example/ValueCircuits.hs | 41 +++++++++++++++++++- src/Circuit.hs | 72 +++++++++++++++++++++++++++++++++--- src/CircuitNotation.hs | 80 +++++++++++++++++++++++++--------------- tests/unittests.hs | 9 +++++ 6 files changed, 199 insertions(+), 46 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ba82d8c..b338abd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,12 +15,22 @@ domains is rejected by the type checker. Lets that don't touch value land stay at the bus level, so let-bound sub-circuits can be used with `-<`. - The value boundary is generated with the new `SigTag` pattern synonym - (`Circuit` module), which pins the bus type to a `Signal` so that type - inference survives nested circuits (the `Fwd` family is not injective) and - "too shallow" `Signal` markers report a direct `Vec`-vs-`Signal` style - mismatch. **Breaking**: `ExternalNames` gained a `signalTagName` field, so - custom plugins (e.g. clash-protocols style) need to supply it. + The two boundary markers have distinct semantics: `Signal x` asserts the + bus is a `Signal` (best inference — it works against fully generic + sub-circuits), while `Fwd x` samples/drives the forward channel of any + signal-like bus via the new `SignalBus` class (`Signal`s, `Vec`s and + tuples of them, custom buses) but needs the bus type determined by + context. In bus-level `circuit` blocks the two keywords remain + interchangeable. + + The value boundary is generated with the new `SigTag` and `FwdTag` pattern + synonyms (`Circuit` module); `SigTag` pins the bus type to a `Signal` so + that type inference survives nested circuits (the `Fwd` family is not + injective) and "too shallow" `Signal` markers report a direct + `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` gained + `signalTagName` and `fwdTagName` fields, so custom plugins (e.g. + clash-protocols style) need to supply them — `defExternalNames` is now + exported so they can be record updates of the defaults. * Add a per-GHC `checks` output to the flake, so `nix flake check` (or `nix build .#checks..`) builds the package and runs all test suites against every supported GHC. The CI nix job now uses it. The diff --git a/README.md b/README.md index c963c0b..73a2298 100644 --- a/README.md +++ b/README.md @@ -7,11 +7,23 @@ example usage. Also see [clash-protocols](https://github.com/clash-lang/clash-pr The `circuitV` keyword describes a circuit's logic over the *values sampled each clock cycle* instead of over whole buses. The boundary between bus land -and value land is marked with `Signal` (or `Fwd`): +and value land is marked with `Signal` or `Fwd`: - `Signal n <- … -< …` binds `n` to the per-cycle value carried on that bus. - `… -< Signal e` injects the per-cycle value `e` back onto a bus. +The two markers differ in what buses they accept: + +- `Signal x` asserts the bus *is* a `Signal dom a`; it pins the bus type and + so gives the best type inference (it works against fully generic + sub-circuits like `idC`). +- `Fwd x` samples (or drives) the forward channel of *any* signal-like bus — + any `SignalBus` instance: `Signal`s, `Vec`s and tuples of signal-like + buses (sampled as `Vec`s/tuples of values), and custom buses given a + one-line instance. In exchange, the bus type must be determined by + context (the circuit's signature or a concretely typed sub-circuit), and + pattern uses need a trivial backwards channel (`TrivialBwd (Bwd t)`). + Everything in between — the `let` bindings of the do block — is ordinary pure Haskell, and feedback loops are written as ordinary recursive `let`s: @@ -41,10 +53,11 @@ instead). Notes: -- Pattern match down to *exactly* the `Signal` layer, no shallower; the +- Pattern match down to *exactly* the signal layer, no shallower; the plugin cannot (yet) know which types contain signals, so the boundary has - to be explicit. Marking a bus that is not a `Signal` (e.g. a `Vec` of - signals) is a type error on the offending statement. + to be explicit. Marking a bus with `Signal` when it is not a `Signal` + (e.g. a `Vec` of signals) is a type error on the offending statement — + use `Fwd` to sample such buses whole. - In a `circuitV` block, `let` statements that use value-level variables form the bodies of the generated logic functions; `let`s that don't touch value land (e.g. a let-bound sub-circuit) stay at the bus level and can be diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 3dd23bd..76640f5 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -14,7 +14,9 @@ simulated and checked by tests/unittests.hs. {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS -fplugin=CircuitNotation #-} {-# OPTIONS -Wall #-} @@ -49,12 +51,47 @@ plusOne = circuitV \(Signal a) -> do plusOneBare :: Circuit (Signal dom Int) (Signal dom Int) plusOneBare = circuitV \(Signal a) -> Signal (a + 1) --- | The @Fwd@ keyword can be used interchangeably with @Signal@ to mark the --- value boundary. +-- | The @Fwd@ keyword also marks the value boundary, but works on /any/ +-- signal-like bus (any 'SignalBus' instance) rather than only literal +-- 'Signal's. The trade-off: the bus type must be determined by context +-- (here, the signature). plusOneFwd :: Circuit (Signal dom Int) (Signal dom Int) plusOneFwd = circuitV \(Fwd a) -> do idC -< Fwd (a + 1) +-- | A whole 'Vec' of signal buses sampled as a single @Vec n Int@ value per +-- cycle (via the 'SignalBus' instance for 'Vec'). +vecSampleC :: Circuit (Vec 2 (Signal dom Int)) (Signal dom Int) +vecSampleC = circuitV \(Fwd v) -> do + idC -< Signal (sum v) + +-- | ... and emitted back as one: a @Vec 2 Int@ value drives both buses. +vecEmitC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) +vecEmitC = circuitV \(Signal a) -> do + idC -< Fwd (a :> (a + 1) :> Nil) + +-- | @Signal@ and @Fwd@ markers can meet in the same logic group. +mixedMarkersC :: Circuit (Signal dom Int, Vec 2 (Signal dom Int)) (Signal dom Int) +mixedMarkersC = circuitV \(Signal a, Fwd v) -> do + idC -< Signal (a + sum v) + +-- | A custom signal-like bus: a stream of optionally-valid values with no +-- backpressure. The 'SignalBus' instance is all that's needed for @Fwd@ +-- markers to sample and drive it in @circuitV@ blocks. +data VStream (dom :: Domain) a +type instance Fwd (VStream dom a) = Signal dom (Maybe a) +type instance Bwd (VStream dom a) = () + +instance SignalBus (VStream dom a) where + type BusDom (VStream dom a) = dom + type SampleOf (VStream dom a) = Maybe a + sigFromBus = unBusTag + sigToBus = BusTag + +vstreamC :: Circuit (VStream dom Int) (VStream dom Int) +vstreamC = circuitV \(Fwd m) -> do + idC -< Fwd (fmap (+ 1) m) + -- | No value inputs at all: the logic is constant. alwaysFive :: Circuit () (Signal dom Int) alwaysFive = circuitV do diff --git a/src/Circuit.hs b/src/Circuit.hs index c1fbb98..4cac2e1 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -208,11 +208,73 @@ pattern BusTagBundle a <- (taggedUnbundle -> a) where BusTagBundle a = taggedBundle a {-# COMPLETE BusTagBundle #-} --- | A tagged 'Signal' bus. Used by the plugin at the value boundary of --- 'circuitV' blocks: matching or constructing with 'SigTag' pins the bus --- type itself (the tag) to be a 'Signal', which is what the value boundary --- requires. Since 'Fwd' is not injective, plain 'BusTag' would leave the bus --- type ambiguous and type inference for nested circuits would fail. +-- | A tagged 'Signal' bus. Used by the plugin for @Signal@ markers at the +-- value boundary of 'circuitV' blocks: matching or constructing with +-- 'SigTag' pins the bus type itself (the tag) to be a 'Signal', which +-- drives type inference. Since 'Fwd' is not injective, plain 'BusTag' would +-- leave the bus type ambiguous and type inference for nested circuits would +-- fail. pattern SigTag :: Signal dom a -> BusTag (Signal dom a) (Signal dom a) pattern SigTag s = BusTag s {-# COMPLETE SigTag #-} + +-- | Buses whose forward channel carries a single value per clock cycle, +-- i.e. is convertible to a single 'Signal'. The @Fwd@ markers at the value +-- boundary of @circuitV@ blocks work on any such bus: 'Signal's themselves, +-- 'Vec's and tuples of signal-like buses (all in the same domain), and any +-- custom bus given an instance. +class SignalBus t where + type BusDom t :: Domain + type SampleOf t + -- | Sample the forward channel of a tagged bus as a signal of values. + sigFromBus :: BusTag t (Fwd t) -> Signal (BusDom t) (SampleOf t) + -- | Drive the forward channel of a tagged bus from a signal of values. + sigToBus :: Signal (BusDom t) (SampleOf t) -> BusTag t (Fwd t) + +instance SignalBus (Signal dom a) where + type BusDom (Signal dom a) = dom + type SampleOf (Signal dom a) = a + sigFromBus = unBusTag + sigToBus = BusTag + +-- | A 'Vec' of signal-like buses is sampled as a 'Vec' of their values. +instance (SignalBus t, KnownNat n) => SignalBus (Vec n t) where + type BusDom (Vec n t) = BusDom t + type SampleOf (Vec n t) = Vec n (SampleOf t) + sigFromBus (BusTag v) = bundle (map (\f -> sigFromBus (BusTag f :: BusTag t (Fwd t))) v) + sigToBus s = BusTag (map (\x -> unBusTag (sigToBus x :: BusTag t (Fwd t))) (unbundle s)) + +instance (SignalBus a, SignalBus b, BusDom a ~ BusDom b) => SignalBus (a, b) where + type BusDom (a, b) = BusDom a + type SampleOf (a, b) = (SampleOf a, SampleOf b) + sigFromBus (BusTag (fa, fb)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) ) + sigToBus s = case unbundle s of + (sa, sb) -> BusTag + ( unBusTag (sigToBus sa :: BusTag a (Fwd a)) + , unBusTag (sigToBus sb :: BusTag b (Fwd b)) ) + +instance (SignalBus a, SignalBus b, SignalBus c, BusDom a ~ BusDom b, BusDom b ~ BusDom c) + => SignalBus (a, b, c) where + type BusDom (a, b, c) = BusDom a + type SampleOf (a, b, c) = (SampleOf a, SampleOf b, SampleOf c) + sigFromBus (BusTag (fa, fb, fc)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) ) + sigToBus s = case unbundle s of + (sa, sb, sc) -> BusTag + ( unBusTag (sigToBus sa :: BusTag a (Fwd a)) + , unBusTag (sigToBus sb :: BusTag b (Fwd b)) + , unBusTag (sigToBus sc :: BusTag c (Fwd c)) ) + +-- | Like 'SigTag' but for any signal-like bus. Used by the plugin for @Fwd@ +-- markers at the value boundary of @circuitV@ blocks. Unlike 'SigTag' it +-- cannot drive type inference (several buses can share a forward type), so +-- the bus type has to be determined by context, e.g. the circuit's +-- signature or a concretely typed sub-circuit. +pattern FwdTag :: SignalBus t => Signal (BusDom t) (SampleOf t) -> BusTag t (Fwd t) +pattern FwdTag s <- (sigFromBus -> s) where + FwdTag s = sigToBus s +{-# COMPLETE FwdTag #-} diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 3ddcd7c..ad524dc 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -221,20 +221,28 @@ data PortName = PortName SrcSpanAnnA GHC.FastString instance Show PortName where show (PortName _ fs) = GHC.unpackFS fs +-- | Which keyword marked a value boundary. @Signal@ asserts the bus /is/ a +-- 'Signal' (generating the concrete @SigTag@, which drives type inference); +-- @Fwd@ samples the forward channel of any signal-like bus (generating the +-- class-constrained @FwdTag@, which requires the bus type to be determined +-- by context). In ordinary (bus-level) @circuit@ blocks the two are +-- interchangeable. +data SigMarker = SignalMarker | FwdMarker + data PortDescription a = Tuple [PortDescription a] | Vec SrcSpanAnnA [PortDescription a] | Ref a | RefMulticast a | Lazy SrcSpanAnnA (PortDescription a) - | FwdExpr (LHsExpr GhcPs) - | FwdPat (LPat GhcPs) - | SigTagExpr (LHsExpr GhcPs) - -- ^ generated by @circuitV@: a value-boundary bus expression, tagged with - -- 'SigTag' to pin the bus type to a signal - | SigTagPat (LPat GhcPs) + | FwdExpr SigMarker (LHsExpr GhcPs) + | FwdPat SigMarker (LPat GhcPs) + | SigTagExpr SigMarker (LHsExpr GhcPs) + -- ^ generated by @circuitV@: a value-boundary bus expression, tagged + -- with @SigTag@/@FwdTag@ according to the marker + | SigTagPat SigMarker (LPat GhcPs) -- ^ generated by @circuitV@: a value-boundary bus pattern, tagged with - -- 'SigTag' to pin the bus type to a signal + -- @SigTag@/@FwdTag@ according to the marker | PortType (LHsType GhcPs) (PortDescription a) | PortErr SrcSpanAnnA MsgDoc deriving (Foldable, Functor, Traversable) @@ -669,7 +677,7 @@ bindSlave (L loc expr) = case expr of TuplePat _ lpat _ -> Tuple $ fmap bindSlave lpat ParPatP lpat -> bindSlave lpat ConPat _ (L _ (GHC.Unqual occ)) (PrefixCon [] [lpat]) - | OccName.occNameString occ `elem` fwdNames -> FwdPat lpat + | Just mk <- markerFromName occ -> FwdPat mk lpat -- empty list is done as the constructor ConPat _ (L _ rdr) _ | rdr == thName '[] -> Vec loc [] @@ -693,7 +701,7 @@ bindMaster (L loc expr) = case expr of | rdrName == thName '[] -> Vec loc [] -- XXX: vloc? | otherwise -> Ref (PortName loc (fromRdrName rdrName)) -- XXX: vloc? HsApp _xapp (L _ (HsVar _ (L _ (GHC.Unqual occ)))) sig - | OccName.occNameString occ `elem` fwdNames -> FwdExpr sig + | Just mk <- markerFromName occ -> FwdExpr mk sig ExplicitTuple _ tups _ -> let vals = fmap (\(Present _ e) -> e) tups in Tuple $ fmap bindMaster vals @@ -701,7 +709,7 @@ bindMaster (L loc expr) = case expr of Vec loc $ fmap bindMaster exprs -- XXX: Untested? HsProc _ _ (L _ (HsCmdTop _ (L _ (HsCmdArrApp _xapp (L _ (HsVar _ (L _ (GHC.Unqual occ)))) sig _ _)))) - | OccName.occNameString occ `elem` fwdNames -> FwdExpr sig + | Just mk <- markerFromName occ -> FwdExpr mk sig ExprWithTySig _ expr' ty -> PortType (hsSigWcType ty) (bindMaster expr') HsParP expr' -> bindMaster expr' @@ -804,10 +812,10 @@ bindWithSuffix dflags dir = \case mkLongErrMsg dflags (locA loc) Outputable.alwaysQualify (Outputable.text "Unhandled bind") msgdoc Lazy loc p -> tildeP loc $ bindWithSuffix dflags dir p -- XXX: propagate location - FwdExpr (L _ _) -> nlWildPat - FwdPat lpat -> tagP lpat - SigTagExpr (L _ _) -> nlWildPat - SigTagPat lpat -> sigTagP lpat + FwdExpr _ (L _ _) -> nlWildPat + FwdPat _ lpat -> tagP lpat + SigTagExpr _ (L _ _) -> nlWildPat + SigTagPat mk lpat -> sigTagP mk lpat PortType ty p -> tagTypeP dir ty $ bindWithSuffix dflags dir p revDirec :: Direction -> Direction @@ -840,12 +848,12 @@ expWithSuffix dir = \case -- laziness only affects the pattern side Lazy _ p -> expWithSuffix dir p PortErr _ _ -> error "expWithSuffix PortErr!" - FwdExpr lexpr -> tagE lexpr - FwdPat (L l _) -> tagE $ varE l (trivialBwd ?nms) - SigTagExpr lexpr -> sigTagE lexpr + FwdExpr _ lexpr -> tagE lexpr + FwdPat _ (L l _) -> tagE $ varE l (trivialBwd ?nms) + SigTagExpr mk lexpr -> sigTagE mk lexpr -- the backwards channel of a signal bus is trivial, so a plain (untyped) -- tag suffices; the forwards occurrence pins the bus type - SigTagPat (L l _) -> tagE $ varE l (trivialBwd ?nms) + SigTagPat _ (L l _) -> tagE $ varE l (trivialBwd ?nms) PortType ty p -> tagTypeE dir ty (expWithSuffix dir p) createInputs @@ -914,11 +922,16 @@ tagE a = varE noSrcSpanA (tagName ?nms) `appE` a -- the SigTag wrappers take the location of what they wrap so that type -- errors on the value boundary (e.g. marking a non-signal bus with @Signal@) -- point at the marked pattern or expression -sigTagP :: (p ~ GhcPs, ?nms :: ExternalNames) => LPat p -> LPat p -sigTagP a@(L l _) = L l (conPatIn (noLoc (signalTagName ?nms)) (prefixCon [a])) +sigTagP :: (p ~ GhcPs, ?nms :: ExternalNames) => SigMarker -> LPat p -> LPat p +sigTagP mk a@(L l _) = L l (conPatIn (noLoc (markerTagName mk)) (prefixCon [a])) + +sigTagE :: (p ~ GhcPs, ?nms :: ExternalNames) => SigMarker -> LHsExpr p -> LHsExpr p +sigTagE mk a@(L l _) = varE l (markerTagName mk) `appE` a -sigTagE :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsExpr p -> LHsExpr p -sigTagE a@(L l _) = varE l (signalTagName ?nms) `appE` a +markerTagName :: (?nms :: ExternalNames) => SigMarker -> GHC.RdrName +markerTagName = \case + SignalMarker -> signalTagName ?nms + FwdMarker -> fwdTagName ?nms tagTypeCon :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsType GhcPs tagTypeCon = @@ -1051,10 +1064,10 @@ replaceFwdPats -> PortDescription PortName -> State (Int, [LPat GhcPs]) (PortDescription PortName) replaceFwdPats prefix = L.transformM \case - FwdPat lpat@(L loc _) -> do + FwdPat mk lpat@(L loc _) -> do (i, pats) <- get put (i + 1, pats <> [lpat]) - pure (SigTagPat (varP loc (prefix <> show i))) + pure (SigTagPat mk (varP loc (prefix <> show i))) p -> pure p -- | Replace each value-level ('Signal' / 'Fwd') expression with a reference @@ -1065,10 +1078,10 @@ replaceFwdExprs -> PortDescription PortName -> State (Int, [LHsExpr GhcPs]) (PortDescription PortName) replaceFwdExprs prefix = L.transformM \case - FwdExpr lexpr@(L loc _) -> do + FwdExpr mk lexpr@(L loc _) -> do (i, exprs) <- get put (i + 1, exprs <> [lexpr]) - pure (SigTagExpr (varE loc (var (prefix <> show i)))) + pure (SigTagExpr mk (varE loc (var (prefix <> show i)))) p -> pure p -- | The @circuitV@ (value-level circuit) version of 'circuitQQExpM'. @@ -1443,8 +1456,12 @@ showC a = show (typeOf a) <> " " <> show (Data.toConstr a) -- Names --------------------------------------------------------------- -fwdNames :: [String] -fwdNames = ["Fwd", "Signal"] +-- | Recognise the value-boundary marker keywords (see 'SigMarker'). +markerFromName :: OccName.OccName -> Maybe SigMarker +markerFromName occ = case OccName.occNameString occ of + "Signal" -> Just SignalMarker + "Fwd" -> Just FwdMarker + _ -> Nothing -- | Collection of names external to circuit-notation. data ExternalNames = ExternalNames @@ -1454,7 +1471,11 @@ data ExternalNames = ExternalNames , tagName :: GHC.RdrName , signalTagName :: GHC.RdrName -- ^ a (pattern synonym) variant of 'tagName' whose type pins the bus to be - -- a signal; used at the value boundary of @circuitV@ blocks + -- a signal; used for @Signal@ markers at the value boundary of @circuitV@ + -- blocks + , fwdTagName :: GHC.RdrName + -- ^ like 'signalTagName' but class-constrained, accepting any signal-like + -- bus; used for @Fwd@ markers at the value boundary of @circuitV@ blocks , tagTName :: GHC.RdrName , fwdBwdCon :: GHC.RdrName , fwdAndBwdTypes :: Direction -> GHC.RdrName @@ -1474,6 +1495,7 @@ defExternalNames = ExternalNames , tagBundlePat = GHC.Unqual (OccName.mkDataOcc "BusTagBundle") , tagName = GHC.Unqual (OccName.mkDataOcc "BusTag") , signalTagName = GHC.Unqual (OccName.mkDataOcc "SigTag") + , fwdTagName = GHC.Unqual (OccName.mkDataOcc "FwdTag") , tagTName = GHC.Unqual (OccName.mkTcOcc "BusTag") , fwdBwdCon = GHC.Unqual (OccName.mkDataOcc ":->") , fwdAndBwdTypes = \case diff --git a/tests/unittests.hs b/tests/unittests.hs index 890eaa9..91fd843 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -39,6 +39,15 @@ main = do -- basic shapes [ check "plusOne" (sample5 (simulateC plusOne (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "plusOneBare" (sample5 (simulateC plusOneBare (fromList [0 ..]))) [1, 2, 3, 4, 5] + , check "vecSampleC" (sample5 (simulateC vecSampleC (fromList [1 ..] :> fromList [10, 20 ..] :> Nil))) + [11, 22, 33, 44, 55] + , check "vecEmitC" (fmap sample5 (simulateC vecEmitC (fromList [0 ..]))) + ([0, 1, 2, 3, 4] :> [1, 2, 3, 4, 5] :> Nil) + , check "mixedMarkersC" + (sample5 (simulateC mixedMarkersC (fromList [100, 200 ..], fromList [1 ..] :> fromList [10, 20 ..] :> Nil))) + [111, 222, 333, 444, 555] + , check "vstreamC" (sample5 (simulateC vstreamC (fromList (fmap Just [0 ..])))) + [Just 1, Just 2, Just 3, Just 4, Just 5] , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) From 0e6d5d8e549910a013d45a23a519fc95cc74c56b Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 12:37:27 +0100 Subject: [PATCH 09/21] Fix poly-kinded issue --- example/ValueCircuits.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 76640f5..27088da 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -78,7 +78,9 @@ mixedMarkersC = circuitV \(Signal a, Fwd v) -> do -- | A custom signal-like bus: a stream of optionally-valid values with no -- backpressure. The 'SignalBus' instance is all that's needed for @Fwd@ -- markers to sample and drive it in @circuitV@ blocks. -data VStream (dom :: Domain) a +-- the explicit result kind matters: without it, PolyKinds (on by default in +-- GHC2021+) would infer a poly-kinded @a@ for this empty data declaration +data VStream (dom :: Domain) (a :: Type) type instance Fwd (VStream dom a) = Signal dom (Maybe a) type instance Bwd (VStream dom a) = () From f0c5fa05f9013d662234b2e9747cfdcbc72dce73 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 12:51:06 +0100 Subject: [PATCH 10/21] Switch to using SignalV at the pattern instead of circuitV --- CHANGELOG.md | 33 ++--- README.md | 59 ++++----- example/ValueCircuits.hs | 195 +++++++++++++++-------------- src/Circuit.hs | 6 +- src/CircuitNotation.hs | 126 ++++++++++--------- tests/fixtures/CrossDomainError.hs | 10 +- tests/fixtures/ValueExprError.hs | 8 +- tests/fixtures/ValueLetError.hs | 6 +- tests/fixtures/ValuePortError.hs | 8 +- tests/fixtures/ValueShapeError.hs | 12 +- tests/unittests.hs | 3 + 11 files changed, 241 insertions(+), 225 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b338abd..72b8fa7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,31 +2,32 @@ ## Unreleased -* Add value-level circuits via the new `circuitV` keyword. The circuit's - logic is written over the values sampled each clock cycle (marked with - `Signal`/`Fwd` patterns and expressions); the plugin lifts it back to the - signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a - lazy let binding. See the README and example/ValueCircuits.hs. +* Add value-level ports via the new `SignalV` and `FwdV` markers in + `circuit` blocks. The circuit's logic is written over the values sampled + each clock cycle; the plugin lifts it back to the signal level with + `fmap`/`bundle`/`unbundle` and ties feedback loops with a lazy let + binding. The bus-level `Signal`/`Fwd` markers keep their existing meaning + and the two levels can be mixed freely in one block. See the README and + example/ValueCircuits.hs. - A `circuitV` block can span several clock domains: the value-level - bindings are split into groups connected by shared variables and each - group is lifted with its own `fmap`/`bundle`/`unbundle`, so only buses - whose values actually meet must share a domain. Sharing a value across - domains is rejected by the type checker. Lets that don't touch value land - stay at the bus level, so let-bound sub-circuits can be used with `-<`. + A block can span several clock domains: the value-level bindings are + split into groups connected by shared variables and each group is lifted + with its own `fmap`/`bundle`/`unbundle`, so only buses whose values + actually meet must share a domain. Sharing a value across domains is + rejected by the type checker. Lets that don't touch value land stay at + the bus level, so let-bound sub-circuits can be used with `-<`. - The two boundary markers have distinct semantics: `Signal x` asserts the + The two value markers have distinct semantics: `SignalV x` asserts the bus is a `Signal` (best inference — it works against fully generic - sub-circuits), while `Fwd x` samples/drives the forward channel of any + sub-circuits), while `FwdV x` samples/drives the forward channel of any signal-like bus via the new `SignalBus` class (`Signal`s, `Vec`s and tuples of them, custom buses) but needs the bus type determined by - context. In bus-level `circuit` blocks the two keywords remain - interchangeable. + context. The value boundary is generated with the new `SigTag` and `FwdTag` pattern synonyms (`Circuit` module); `SigTag` pins the bus type to a `Signal` so that type inference survives nested circuits (the `Fwd` family is not - injective) and "too shallow" `Signal` markers report a direct + injective) and "too shallow" `SignalV` markers report a direct `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` gained `signalTagName` and `fwdTagName` fields, so custom plugins (e.g. clash-protocols style) need to supply them — `defExternalNames` is now diff --git a/README.md b/README.md index 73a2298..de06ff5 100644 --- a/README.md +++ b/README.md @@ -3,24 +3,28 @@ This is a plugin for manipulating circuits in clash with arrow notation. See example/Example.hs for example usage. Also see [clash-protocols](https://github.com/clash-lang/clash-protocols#). -## Value-level circuits (`circuitV`) +## Value-level ports (`SignalV` / `FwdV`) -The `circuitV` keyword describes a circuit's logic over the *values sampled -each clock cycle* instead of over whole buses. The boundary between bus land -and value land is marked with `Signal` or `Fwd`: +The `SignalV` and `FwdV` markers describe a circuit's logic over the *values +sampled each clock cycle* instead of over whole buses, right inside an +ordinary `circuit` block: -- `Signal n <- … -< …` binds `n` to the per-cycle value carried on that bus. -- `… -< Signal e` injects the per-cycle value `e` back onto a bus. +- `SignalV n <- … -< …` binds `n` to the per-cycle value carried on that bus. +- `… -< SignalV e` injects the per-cycle value `e` back onto a bus. -The two markers differ in what buses they accept: +(The bus-level `Signal`/`Fwd` markers, which bind the raw forward channel, +keep their existing meaning; the two levels can be mixed freely in one +block.) -- `Signal x` asserts the bus *is* a `Signal dom a`; it pins the bus type and - so gives the best type inference (it works against fully generic +The two value markers differ in what buses they accept: + +- `SignalV x` asserts the bus *is* a `Signal dom a`; it pins the bus type + and so gives the best type inference (it works against fully generic sub-circuits like `idC`). -- `Fwd x` samples (or drives) the forward channel of *any* signal-like bus — - any `SignalBus` instance: `Signal`s, `Vec`s and tuples of signal-like - buses (sampled as `Vec`s/tuples of values), and custom buses given a - one-line instance. In exchange, the bus type must be determined by +- `FwdV x` samples (or drives) the forward channel of *any* signal-like + bus — any `SignalBus` instance: `Signal`s, `Vec`s and tuples of + signal-like buses (sampled as `Vec`s/tuples of values), and custom buses + given a one-line instance. In exchange, the bus type must be determined by context (the circuit's signature or a concretely typed sub-circuit), and pattern uses need a trivial backwards channel (`TrivialBwd (Bwd t)`). @@ -29,12 +33,12 @@ Haskell, and feedback loops are written as ordinary recursive `let`s: ```haskell counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuitV \_bs -> do - Signal n <- registerC 0 -< Signal n' -- n :: Int (this cycle's value) - Signal m <- registerC 8 -< Signal m' -- m :: Int +counter3 = circuit \_bs -> do + SignalV n <- registerC 0 -< SignalV n' -- n :: Int (this cycle's value) + SignalV m <- registerC 8 -< SignalV m' -- m :: Int let n' = n + 1 -- pure, value-level m' = m + 1 - idC -< Signal (n' + m') + idC -< SignalV (n' + m') ``` The plugin collects the value-level bindings into pure functions, lifts them @@ -42,11 +46,11 @@ to the signal level with `fmap` (using `bundle`/`unbundle` to group the buses), and ties feedback knots with lazy let bindings. See example/ValueCircuits.hs for more examples and the expansion of `counter3`. -A single `circuitV` block can span several clock domains: the value-level -bindings are split into groups connected by shared variables, and each group -is lifted independently, so only buses whose values actually meet must share -a clock domain. Two independent counters on two different domains can live -in one block; making their values meet (e.g. `Signal (n + m)`) is an +A single block can span several clock domains: the value-level bindings are +split into groups connected by shared variables, and each group is lifted +independently, so only buses whose values actually meet must share a clock +domain. Two independent counters on two different domains can live in one +block; making their values meet (e.g. `SignalV (n + m)`) is an unsynchronized clock domain crossing and is rejected by the type checker (cross between domains with explicit bus-level synchronizer circuits instead). @@ -55,13 +59,12 @@ Notes: - Pattern match down to *exactly* the signal layer, no shallower; the plugin cannot (yet) know which types contain signals, so the boundary has - to be explicit. Marking a bus with `Signal` when it is not a `Signal` + to be explicit. Marking a bus with `SignalV` when it is not a `Signal` (e.g. a `Vec` of signals) is a type error on the offending statement — - use `Fwd` to sample such buses whole. -- In a `circuitV` block, `let` statements that use value-level variables - form the bodies of the generated logic functions; `let`s that don't touch - value land (e.g. a let-bound sub-circuit) stay at the bus level and can be - used with `-<`. + use `FwdV` to sample such buses whole. +- `let` statements that use value-level variables form the bodies of the + generated logic functions; `let`s that don't touch value land (e.g. a + let-bound sub-circuit) stay at the bus level and can be used with `-<`. - The grouping is syntactic and conservative: shadowing a value-level name inside a `let` can merge groups that wouldn't strictly need to share a domain (never the other way around). diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 27088da..0e3f4e4 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -7,8 +7,8 @@ ╚═════╝╚═╝╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝ ╚══════╝ (C) 2020, Christopher Chalmers -Examples of value-level circuits (the 'circuitV' keyword). These are -simulated and checked by tests/unittests.hs. +Examples of value-level ports (the 'SignalV' and 'FwdV' markers) in circuit +blocks. These are simulated and checked by tests/unittests.hs. -} {-# LANGUAGE BlockArguments #-} @@ -44,42 +44,42 @@ simulateC c aFwd = let (_ :-> bFwd) = runCircuit c (aFwd :-> unitBwd) in bFwd -- feedback. @a@ is the per-cycle 'Int' carried on the bus, not the bus -- itself; no @bundle@/@unbundle@ is generated for single buses. plusOne :: Circuit (Signal dom Int) (Signal dom Int) -plusOne = circuitV \(Signal a) -> do - idC -< Signal (a + 1) +plusOne = circuit \(SignalV a) -> do + idC -< SignalV (a + 1) -- | The same as 'plusOne' without a do block: a bare expression body. plusOneBare :: Circuit (Signal dom Int) (Signal dom Int) -plusOneBare = circuitV \(Signal a) -> Signal (a + 1) +plusOneBare = circuit \(SignalV a) -> SignalV (a + 1) --- | The @Fwd@ keyword also marks the value boundary, but works on /any/ +-- | The @FwdV@ marker also marks the value boundary, but works on /any/ -- signal-like bus (any 'SignalBus' instance) rather than only literal -- 'Signal's. The trade-off: the bus type must be determined by context -- (here, the signature). plusOneFwd :: Circuit (Signal dom Int) (Signal dom Int) -plusOneFwd = circuitV \(Fwd a) -> do - idC -< Fwd (a + 1) +plusOneFwd = circuit \(FwdV a) -> do + idC -< FwdV (a + 1) -- | A whole 'Vec' of signal buses sampled as a single @Vec n Int@ value per -- cycle (via the 'SignalBus' instance for 'Vec'). vecSampleC :: Circuit (Vec 2 (Signal dom Int)) (Signal dom Int) -vecSampleC = circuitV \(Fwd v) -> do - idC -< Signal (sum v) +vecSampleC = circuit \(FwdV v) -> do + idC -< SignalV (sum v) -- | ... and emitted back as one: a @Vec 2 Int@ value drives both buses. vecEmitC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) -vecEmitC = circuitV \(Signal a) -> do - idC -< Fwd (a :> (a + 1) :> Nil) +vecEmitC = circuit \(SignalV a) -> do + idC -< FwdV (a :> (a + 1) :> Nil) --- | @Signal@ and @Fwd@ markers can meet in the same logic group. +-- | @SignalV@ and @FwdV@ markers can meet in the same logic group. mixedMarkersC :: Circuit (Signal dom Int, Vec 2 (Signal dom Int)) (Signal dom Int) -mixedMarkersC = circuitV \(Signal a, Fwd v) -> do - idC -< Signal (a + sum v) +mixedMarkersC = circuit \(SignalV a, FwdV v) -> do + idC -< SignalV (a + sum v) -- | A custom signal-like bus: a stream of optionally-valid values with no --- backpressure. The 'SignalBus' instance is all that's needed for @Fwd@ --- markers to sample and drive it in @circuitV@ blocks. --- the explicit result kind matters: without it, PolyKinds (on by default in --- GHC2021+) would infer a poly-kinded @a@ for this empty data declaration +-- backpressure. The 'SignalBus' instance is all that's needed for @FwdV@ +-- markers to sample and drive it in circuit blocks. +-- The explicit result kind matters: without it, PolyKinds (on by default in +-- GHC2021+) would infer a poly-kinded @a@ for this empty data declaration. data VStream (dom :: Domain) (a :: Type) type instance Fwd (VStream dom a) = Signal dom (Maybe a) type instance Bwd (VStream dom a) = () @@ -91,53 +91,53 @@ instance SignalBus (VStream dom a) where sigToBus = BusTag vstreamC :: Circuit (VStream dom Int) (VStream dom Int) -vstreamC = circuitV \(Fwd m) -> do - idC -< Fwd (fmap (+ 1) m) +vstreamC = circuit \(FwdV m) -> do + idC -< FwdV (fmap (+ 1) m) -- | No value inputs at all: the logic is constant. alwaysFive :: Circuit () (Signal dom Int) -alwaysFive = circuitV do - idC -< Signal (5 :: Int) +alwaysFive = circuit do + idC -< SignalV (5 :: Int) -- | Two value inputs, one value output (a single @bundle@, no @unbundle@). addC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int) -addC = circuitV \(Signal a, Signal b) -> do - idC -< Signal (a + b) +addC = circuit \(SignalV a, SignalV b) -> do + idC -< SignalV (a + b) -- | One value input, two value outputs (a single @unbundle@, no @bundle@). fanOutC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) -fanOutC = circuitV \(Signal a) -> do - idC -< (Signal (a + 1), Signal (a * 2)) +fanOutC = circuit \(SignalV a) -> do + idC -< (SignalV (a + 1), SignalV (a * 2)) -- | Values can be matched out of a bus carrying a compound type ... splitC :: Circuit (Signal dom (Int, Bool)) (Signal dom Int, Signal dom Bool) -splitC = circuitV \(Signal (a, b)) -> do - idC -< (Signal a, Signal b) +splitC = circuit \(SignalV (a, b)) -> do + idC -< (SignalV a, SignalV b) -- | ... and combined back onto one. joinC :: Circuit (Signal dom Int, Signal dom Bool) (Signal dom (Int, Bool)) -joinC = circuitV \(Signal a, Signal b) -> do - idC -< Signal (a, b) +joinC = circuit \(SignalV a, SignalV b) -> do + idC -< SignalV (a, b) -- | Ports nest like in ordinary circuit notation. nestedTupleC :: Circuit ((Signal dom Int, Signal dom Int), Signal dom Int) (Signal dom Int) -nestedTupleC = circuitV \((Signal a, Signal b), Signal c) -> do - idC -< Signal (a + b * c) +nestedTupleC = circuit \((SignalV a, SignalV b), SignalV c) -> do + idC -< SignalV (a + b * c) -- | Value boundaries inside 'Vec' buses. vecInC :: Circuit (Vec 2 (Signal dom Int)) (Signal dom Int) -vecInC = circuitV \[Signal a, Signal b] -> do - idC -< Signal (a - b) +vecInC = circuit \[SignalV a, SignalV b] -> do + idC -< SignalV (a - b) vecOutC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) -vecOutC = circuitV \(Signal a) -> do - idC -< [Signal (a + 1), Signal (a - 1)] +vecOutC = circuit \(SignalV a) -> do + idC -< [SignalV (a + 1), SignalV (a - 1)] -- | Ports crossing the value boundary can be given bus-level type -- annotations like any other port. annotatedC :: forall dom. Circuit (Signal dom Int) (Signal dom Int) -annotatedC = circuitV \((Signal a) :: Signal dom Int) -> do - idC -< Signal (a + 1) +annotatedC = circuit \((SignalV a) :: Signal dom Int) -> do + idC -< SignalV (a + 1) -- Feedback ------------------------------------------------------------- @@ -145,28 +145,28 @@ annotatedC = circuitV \((Signal a) :: Signal dom Int) -> do -- @n'@ is defined in terms of its output @n@ by an ordinary recursive @let@; -- the plugin ties the knot at the signal level. counter :: Circuit () (Signal dom Int) -counter = circuitV do - Signal n <- registerC 0 -< Signal n' +counter = circuit do + SignalV n <- registerC 0 -< SignalV n' let n' = n + 1 - idC -< Signal n + idC -< SignalV n -- | A Mealy-style accumulator: reads the per-cycle value off the input bus -- and feeds back state through a register. Written with a @$@ chain. accum :: Circuit (Signal dom Int) (Signal dom Int) -accum = circuitV $ \(Signal i) -> do - Signal acc <- registerC 0 -< Signal acc' +accum = circuit $ \(SignalV i) -> do + SignalV acc <- registerC 0 -< SignalV acc' let acc' = acc + i - idC -< Signal acc' + idC -< SignalV acc' -- | Two interleaved feedback loops (the canonical example from the design -- notes). The bus input is ignored. counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuitV \_bs -> do - Signal n <- registerC 0 -< Signal n' - Signal m <- registerC 8 -< Signal m' +counter3 = circuit \_bs -> do + SignalV n <- registerC 0 -< SignalV n' + SignalV m <- registerC 8 -< SignalV m' let n' = n + 1 m' = m + 1 - idC -< Signal (n' + m') + idC -< SignalV (n' + m') -- | What 'counter3' expands to (modulo generated names). The value-level -- bindings are collected into one pure function, @circuitLogic@, which is @@ -194,55 +194,62 @@ counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> -- | Compound state fed back through a /single/ register: a fibonacci -- machine. The pair is destructured and rebuilt at the value level. fibC :: Circuit () (Signal dom Int) -fibC = circuitV do - Signal (a, b) <- registerC (0, 1) -< Signal (b, a + b) - idC -< Signal a +fibC = circuit do + SignalV (a, b) <- registerC (0, 1) -< SignalV (b, a + b) + idC -< SignalV a -- | A chain of registers: a three-deep shift register (no feedback, but a -- value passes through several binds). shift3 :: Circuit (Signal dom Int) (Signal dom Int) -shift3 = circuitV \(Signal i) -> do - Signal a <- registerC 0 -< Signal i - Signal b <- registerC 0 -< Signal a - Signal c <- registerC 0 -< Signal b - idC -< Signal c +shift3 = circuit \(SignalV i) -> do + SignalV a <- registerC 0 -< SignalV i + SignalV b <- registerC 0 -< SignalV a + SignalV c <- registerC 0 -< SignalV b + idC -< SignalV c -- | Three rotating registers plus the bus input: a four-way bundle on both -- sides of the logic function. rotate3 :: Circuit (Signal dom Int) (Signal dom Int) -rotate3 = circuitV \(Signal i) -> do - Signal a <- registerC 1 -< Signal a' - Signal b <- registerC 2 -< Signal b' - Signal c <- registerC 3 -< Signal c' +rotate3 = circuit \(SignalV i) -> do + SignalV a <- registerC 1 -< SignalV a' + SignalV b <- registerC 2 -< SignalV b' + SignalV c <- registerC 3 -< SignalV c' let a' = b b' = c c' = a + i - idC -< Signal (a + b + c) + idC -< SignalV (a + b + c) -- Mixing value land and bus land ---------------------------------------- -- | Value-level and bus-level ports can be mixed: the second bus is routed -- through untouched while the first is sampled and modified. mixedC :: Circuit (Signal dom Int, Signal dom Int) (Signal dom Int, Signal dom Int) -mixedC = circuitV \(Signal a, b) -> do - idC -< (Signal (a + 1), b) +mixedC = circuit \(SignalV a, b) -> do + idC -< (SignalV (a + 1), b) -- | As 'mixedC' but with a 'DF' bus (whose backwards channel is not -- trivial) routed through. mixedDfC :: Circuit (Signal dom Int, DF dom Bool) (Signal dom Int, DF dom Bool) -mixedDfC = circuitV \(Signal a, df) -> do - idC -< (Signal (a + 1), df) +mixedDfC = circuit \(SignalV a, df) -> do + idC -< (SignalV (a + 1), df) + +-- | Bus-level markers (@Fwd@/@Signal@, which bind the raw forward channel) +-- and value-level markers (@FwdV@/@SignalV@) can be used side by side in +-- one block: here the 'Vec' bus is rearranged at the bus level while the +-- signal is sampled. +mixedLevelsC :: Circuit (Vec 2 (Signal dom Int), Signal dom Int) (Vec 2 (Signal dom Int), Signal dom Int) +mixedLevelsC = circuit \(Fwd v, SignalV a) -> do + idC -< (Fwd (rotateLeftS v d1), SignalV (a + 1)) -- | A bus created from a value can be multicast like any other bus. multicastC :: Circuit (Signal dom Int) (Signal dom Int, Signal dom Int) -multicastC = circuitV \(Signal a) -> do - b <- idC -< Signal (a + 1) +multicastC = circuit \(SignalV a) -> do + b <- idC -< SignalV (a + 1) idC -< (b, b) --- | Without any value-level (@Signal@/@Fwd@) markers, @circuitV@ behaves --- exactly like @circuit@. +-- | Without any value-level markers this is just ordinary circuit notation. passthrough :: Circuit (Signal dom Int) (Signal dom Int) -passthrough = circuitV \a -> a +passthrough = circuit \a -> a -- Multiple clock domains ------------------------------------------------- -- @@ -252,48 +259,48 @@ passthrough = circuitV \a -> a -- value across domains is an (unsynchronized) clock domain crossing and is -- rejected by the type checker. --- | Two completely independent counters in one @circuitV@ block, on two --- /different/ clock domains: nothing forces @domA@ and @domB@ together. +-- | Two completely independent counters in one block, on two /different/ +-- clock domains: nothing forces @domA@ and @domB@ together. dualCounter :: Circuit (Signal domA Bool, Signal domB Bool) (Signal domA Int, Signal domB Int) -dualCounter = circuitV \(_ea, _eb) -> do - Signal n <- registerC 0 -< Signal n' - Signal m <- registerC 8 -< Signal m' +dualCounter = circuit \(_ea, _eb) -> do + SignalV n <- registerC 0 -< SignalV n' + SignalV m <- registerC 8 -< SignalV m' let n' = n + 1 m' = m + 1 - idC -< (Signal n', Signal m') + idC -< (SignalV n', SignalV m') -- | Two independent accumulators, each reading values off its own input -- bus, on different clock domains. dualAccum :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int, Signal domB Int) -dualAccum = circuitV \(Signal i, Signal j) -> do - Signal a <- registerC 0 -< Signal (a + i) - Signal b <- registerC 0 -< Signal (b + j) - idC -< (Signal a, Signal b) +dualAccum = circuit \(SignalV i, SignalV j) -> do + SignalV a <- registerC 0 -< SignalV (a + i) + SignalV b <- registerC 0 -< SignalV (b + j) + idC -< (SignalV a, SignalV b) -- | Lets that don't touch any value-level variable stay at the bus level, -- so sub-circuits can be bound in a let and used with @-<@. busLevelLet :: Circuit (Signal dom Int) (Signal dom Int) -busLevelLet = circuitV \(Signal x) -> do +busLevelLet = circuit \(SignalV x) -> do let inc = plusOne - Signal y <- inc -< Signal (x + 1) - idC -< Signal (y * 2) + SignalV y <- inc -< SignalV (x + 1) + idC -< SignalV (y * 2) -- Nesting --------------------------------------------------------------- --- | A @circuitV@ used as a sub-circuit inside an ordinary @circuit@. +-- | A value-level circuit used as a sub-circuit inside a bus-level one. nestedSInCircuit :: Circuit (Signal dom Int) (Signal dom Int) nestedSInCircuit = circuit $ \a -> do - b <- (circuitV \(Signal x) -> do idC -< Signal (x * 2)) -< a + b <- (circuit \(SignalV x) -> do idC -< SignalV (x * 2)) -< a idC -< b --- | An ordinary @circuit@ used as a sub-circuit inside a @circuitV@. +-- | A bus-level circuit used as a sub-circuit inside a value-level one. nestedCircuitInS :: Circuit (Signal dom Int) (Signal dom Int) -nestedCircuitInS = circuitV \(Signal x) -> do - Signal y <- (circuit \b -> b) -< Signal (x + 1) - idC -< Signal (y * 3) +nestedCircuitInS = circuit \(SignalV x) -> do + SignalV y <- (circuit \b -> b) -< SignalV (x + 1) + idC -< SignalV (y * 3) --- | A @circuitV@ inside another @circuitV@. +-- | A value-level circuit inside another value-level circuit. nestedSInS :: Circuit (Signal dom Int) (Signal dom Int) -nestedSInS = circuitV \(Signal x) -> do - Signal y <- (circuitV \(Signal a) -> do idC -< Signal (a + 1)) -< Signal x - idC -< Signal (y * 2) +nestedSInS = circuit \(SignalV x) -> do + SignalV y <- (circuit \(SignalV a) -> do idC -< SignalV (a + 1)) -< SignalV x + idC -< SignalV (y * 2) diff --git a/src/Circuit.hs b/src/Circuit.hs index 4cac2e1..3eed7b6 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -209,7 +209,7 @@ pattern BusTagBundle a <- (taggedUnbundle -> a) where {-# COMPLETE BusTagBundle #-} -- | A tagged 'Signal' bus. Used by the plugin for @Signal@ markers at the --- value boundary of 'circuitV' blocks: matching or constructing with +-- value boundary of circuit blocks: matching or constructing with -- 'SigTag' pins the bus type itself (the tag) to be a 'Signal', which -- drives type inference. Since 'Fwd' is not injective, plain 'BusTag' would -- leave the bus type ambiguous and type inference for nested circuits would @@ -220,7 +220,7 @@ pattern SigTag s = BusTag s -- | Buses whose forward channel carries a single value per clock cycle, -- i.e. is convertible to a single 'Signal'. The @Fwd@ markers at the value --- boundary of @circuitV@ blocks work on any such bus: 'Signal's themselves, +-- boundary of @circuit@ blocks work on any such bus: 'Signal's themselves, -- 'Vec's and tuples of signal-like buses (all in the same domain), and any -- custom bus given an instance. class SignalBus t where @@ -270,7 +270,7 @@ instance (SignalBus a, SignalBus b, SignalBus c, BusDom a ~ BusDom b, BusDom b ~ , unBusTag (sigToBus sc :: BusTag c (Fwd c)) ) -- | Like 'SigTag' but for any signal-like bus. Used by the plugin for @Fwd@ --- markers at the value boundary of @circuitV@ blocks. Unlike 'SigTag' it +-- markers at the value boundary of @circuit@ blocks. Unlike 'SigTag' it -- cannot drive type inference (several buses can share a forward type), so -- the bus type has to be determined by context, e.g. the circuit's -- signature or a concretely typed sub-circuit. diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index ad524dc..043c11d 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -134,10 +134,6 @@ isSomeVar s = \case isCircuitVar :: p ~ GhcPs => HsExpr p -> Bool isCircuitVar = isSomeVar "circuit" --- | Is the variable for the value-level circuit keyword? -isCircuitVVar :: p ~ GhcPs => HsExpr p -> Bool -isCircuitVVar = isSomeVar "circuitV" - isDollar :: p ~ GhcPs => HsExpr p -> Bool isDollar = isSomeVar "$" @@ -221,13 +217,21 @@ data PortName = PortName SrcSpanAnnA GHC.FastString instance Show PortName where show (PortName _ fs) = GHC.unpackFS fs --- | Which keyword marked a value boundary. @Signal@ asserts the bus /is/ a --- 'Signal' (generating the concrete @SigTag@, which drives type inference); --- @Fwd@ samples the forward channel of any signal-like bus (generating the --- class-constrained @FwdTag@, which requires the bus type to be determined --- by context). In ordinary (bus-level) @circuit@ blocks the two are --- interchangeable. -data SigMarker = SignalMarker | FwdMarker +-- | Which keyword marked a port. @Signal@ and @Fwd@ are bus-level (and +-- interchangeable): they bind/inject the raw forward channel. @SignalV@ and +-- @FwdV@ mark the /value/ boundary, binding or injecting the per-cycle +-- value: @SignalV@ asserts the bus /is/ a 'Signal' (generating the concrete +-- @SigTag@, which drives type inference) while @FwdV@ samples the forward +-- channel of any signal-like bus (generating the class-constrained +-- @FwdTag@, which requires the bus type to be determined by context). +data SigMarker = SignalMarker | FwdMarker | SignalVMarker | FwdVMarker + +-- | Is this marker a value boundary (@SignalV@/@FwdV@)? +isValueMarker :: SigMarker -> Bool +isValueMarker = \case + SignalVMarker -> True + FwdVMarker -> True + _ -> False data PortDescription a = Tuple [PortDescription a] @@ -238,10 +242,10 @@ data PortDescription a | FwdExpr SigMarker (LHsExpr GhcPs) | FwdPat SigMarker (LPat GhcPs) | SigTagExpr SigMarker (LHsExpr GhcPs) - -- ^ generated by @circuitV@: a value-boundary bus expression, tagged + -- ^ generated for value markers: a value-boundary bus expression, tagged -- with @SigTag@/@FwdTag@ according to the marker | SigTagPat SigMarker (LPat GhcPs) - -- ^ generated by @circuitV@: a value-boundary bus pattern, tagged with + -- ^ generated for value markers: a value-boundary bus pattern, tagged with -- @SigTag@/@FwdTag@ according to the marker | PortType (LHsType GhcPs) (PortDescription a) | PortErr SrcSpanAnnA MsgDoc @@ -273,7 +277,7 @@ data CircuitState dec exp nm = CircuitState { _cErrors :: Bag ErrMsg , _counter :: Int -- ^ unique counter for generated variables - , _circuitVlaves :: PortDescription nm + , _circuitSlaves :: PortDescription nm -- ^ the final statement in a circuit , _circuitTypes :: [LSig GhcPs] -- ^ type signatures in let bindings @@ -311,7 +315,7 @@ runCircuitM (CircuitM m) = do let emptyCircuitState = CircuitState { _cErrors = emptyBag , _counter = 0 - , _circuitVlaves = Tuple [] + , _circuitSlaves = Tuple [] , _circuitTypes = [] , _circuitLets = [] , _circuitCompletes = [] @@ -605,7 +609,7 @@ parseCircuit = \case -- a lambda to match the slave ports L _ (simpleLambda -> Just ([matchPats], body)) -> do - circuitVlaves .= bindSlave matchPats + circuitSlaves .= bindSlave matchPats circuitBody body -- a version without a lambda (i.e. no slaves) @@ -753,7 +757,7 @@ data Dir = Slave | Master checkCircuit :: p ~ GhcPs => CircuitM () checkCircuit = do - slaves <- L.use circuitVlaves + slaves <- L.use circuitSlaves masters <- L.use circuitMasters binds <- L.use circuitBinds @@ -789,7 +793,7 @@ checkCircuit = do p -> p -- update relevant master ports to be multicast - circuitVlaves %= L.transform modifyMulticast + circuitSlaves %= L.transform modifyMulticast circuitMasters %= L.transform modifyMulticast circuitBinds . L.mapped %= \b -> b { bIn = L.transform modifyMulticast (bIn b), @@ -928,10 +932,13 @@ sigTagP mk a@(L l _) = L l (conPatIn (noLoc (markerTagName mk)) (prefixCon [a])) sigTagE :: (p ~ GhcPs, ?nms :: ExternalNames) => SigMarker -> LHsExpr p -> LHsExpr p sigTagE mk a@(L l _) = varE l (markerTagName mk) `appE` a +-- only value markers reach the SigTag* constructors, but keep this total markerTagName :: (?nms :: ExternalNames) => SigMarker -> GHC.RdrName markerTagName = \case - SignalMarker -> signalTagName ?nms - FwdMarker -> fwdTagName ?nms + SignalVMarker -> signalTagName ?nms + FwdVMarker -> fwdTagName ?nms + SignalMarker -> signalTagName ?nms + FwdMarker -> fwdTagName ?nms tagTypeCon :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsType GhcPs tagTypeCon = @@ -1014,10 +1021,10 @@ tyEq a b = -- Final construction -------------------------------------------------- -circuitQQExpM +busCircuitQQExpM :: (p ~ GhcPs, ?nms :: ExternalNames) => CircuitM (LHsExpr p) -circuitQQExpM = do +busCircuitQQExpM = do checkCircuit dflags <- GHC.getDynFlags @@ -1025,7 +1032,7 @@ circuitQQExpM = do lets <- L.use circuitLets completes <- L.use circuitCompletes letTypes <- L.use circuitTypes - slaves <- L.use circuitVlaves + slaves <- L.use circuitSlaves masters <- L.use circuitMasters -- Construction of the circuit expression. @@ -1049,12 +1056,14 @@ circuitQQExpM = do pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body --- Value circuits (circuitV) -------------------------------------------- +-- Value-level ports (SignalV/FwdV markers) ---------------------------- --- | The number of value-level ('FwdPat' / 'FwdExpr') ports in a port +-- | The number of value-level (@SignalV@/@FwdV@-marked) ports in a port -- description. -countFwdPorts :: PortDescription PortName -> Int -countFwdPorts p = length [() | FwdPat{} <- L.universe p] + length [() | FwdExpr{} <- L.universe p] +countValuePorts :: PortDescription PortName -> Int +countValuePorts p = + length [() | FwdPat mk _ <- L.universe p, isValueMarker mk] + + length [() | FwdExpr mk _ <- L.universe p, isValueMarker mk] -- | Replace each value-level ('Signal' / 'Fwd') pattern with a reference to a -- generated signal bus variable (@prefix <> show i@), collecting the original @@ -1064,7 +1073,7 @@ replaceFwdPats -> PortDescription PortName -> State (Int, [LPat GhcPs]) (PortDescription PortName) replaceFwdPats prefix = L.transformM \case - FwdPat mk lpat@(L loc _) -> do + FwdPat mk lpat@(L loc _) | isValueMarker mk -> do (i, pats) <- get put (i + 1, pats <> [lpat]) pure (SigTagPat mk (varP loc (prefix <> show i))) @@ -1078,18 +1087,18 @@ replaceFwdExprs -> PortDescription PortName -> State (Int, [LHsExpr GhcPs]) (PortDescription PortName) replaceFwdExprs prefix = L.transformM \case - FwdExpr mk lexpr@(L loc _) -> do + FwdExpr mk lexpr@(L loc _) | isValueMarker mk -> do (i, exprs) <- get put (i + 1, exprs <> [lexpr]) pure (SigTagExpr mk (varE loc (var (prefix <> show i)))) p -> pure p --- | The @circuitV@ (value-level circuit) version of 'circuitQQExpM'. +-- | The value-aware entry point for @circuit@ blocks. -- --- Value-level circuits describe a circuit's logic over the values sampled +-- Value-level ports describe a circuit's logic over the values sampled -- each clock cycle. The boundary between bus land and value land is marked --- with @Signal@ (or @Fwd@): @Signal n <- ...@ binds @n@ to the per-cycle --- value carried on that bus, and @... -< Signal e@ injects the per-cycle +-- with @SignalV@ (or @FwdV@): @SignalV n <- ...@ binds @n@ to the per-cycle +-- value carried on that bus, and @... -< SignalV e@ injects the per-cycle -- value @e@ back onto a bus. -- -- All the value-level bindings (the @let@s of the do block) are collected @@ -1104,32 +1113,32 @@ replaceFwdExprs prefix = L.transformM \case -- @ -- -- The buses themselves are wired up exactly as for an ordinary @circuit@. -circuitVQQExpM +circuitQQExpM :: (p ~ GhcPs, ?nms :: ExternalNames) => CircuitM (LHsExpr p) -circuitVQQExpM = do - slaves0 <- L.use circuitVlaves +circuitQQExpM = do + slaves0 <- L.use circuitSlaves masters0 <- L.use circuitMasters binds0 <- L.use circuitBinds let boundaryCount = - sum (map countFwdPorts (slaves0 : masters0 : concatMap (\b -> [bIn b, bOut b]) binds0)) + sum (map countValuePorts (slaves0 : masters0 : concatMap (\b -> [bIn b, bOut b]) binds0)) - -- Without any value-level (Signal/Fwd) ports there is no boundary to lift; - -- behave exactly like an ordinary circuit. - if boundaryCount == 0 then circuitQQExpM else circuitVQQExpM' + -- Without any value-level (SignalV/FwdV) ports there is no boundary to + -- lift; generate plain bus plumbing. + if boundaryCount == 0 then busCircuitQQExpM else valueCircuitQQExpM -circuitVQQExpM' +valueCircuitQQExpM :: (p ~ GhcPs, ?nms :: ExternalNames) => CircuitM (LHsExpr p) -circuitVQQExpM' = do +valueCircuitQQExpM = do checkCircuit dflags <- GHC.getDynFlags loc <- L.use circuitLoc -- read the ports after checkCircuit, which may have rewritten them - slaves0 <- L.use circuitVlaves + slaves0 <- L.use circuitSlaves masters0 <- L.use circuitMasters binds0 <- L.use circuitBinds @@ -1152,7 +1161,7 @@ circuitVQQExpM' = do pure (bs, m) ((binds2, masters1), (numOuts, outExprs)) = runState outM (0, []) - circuitVlaves .= slaves1 + circuitSlaves .= slaves1 circuitMasters .= masters1 circuitBinds .= binds2 @@ -1241,7 +1250,7 @@ circuitVQQExpM' = do compDecs = concat (zipWith mkComp [0 ..] innerGroups) - -- The bus plumbing is generated exactly as in 'circuitQQExpM'. + -- The bus plumbing is generated exactly as in 'busCircuitQQExpM'. let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) let decs = compDecs <> outerLets <> completes <> map decFromBinding' binds2 @@ -1254,13 +1263,13 @@ circuitVQQExpM' = do pure $ circuitConstructor noSrcSpanA `appE` lamE [pats] body -- [value-components] --- The value-level bindings of a @circuitV@ block are split into the +-- The value-level bindings of a @circuit@ block are split into the -- connected components of their shared-variable graph before lifting: an -- input variable (Signal pattern), output expression (Signal expression) or -- let binding belongs to the same group as anything it shares a value-level -- variable with. Each group is lifted with its own fmap/bundle/unbundle, so -- only buses whose values actually meet are bundled -- which is what allows --- a single circuitV block to span several clock domains: per-cycle values +-- a single circuit block to span several clock domains: per-cycle values -- may only meet if their buses are synchronous, and 'bundle' enforces -- exactly that per group. Sharing a variable across domains is an -- (unsynchronized) clock domain crossing and is rejected by the type @@ -1274,7 +1283,7 @@ circuitVQQExpM' = do -- belong together. -- | An occurrence of the value boundary (or a let between boundaries) in a --- @circuitV@ block; the @Int@ indexes into the respective collection. +-- @circuit@ block; the @Int@ indexes into the respective collection. data ValueItem = ItemIn Int | ItemOut Int | ItemLet Int -- | Group items into connected components: items (transitively) sharing a @@ -1334,7 +1343,7 @@ completeUnderscores :: (?nms :: ExternalNames) => CircuitM () completeUnderscores = do binds <- L.use circuitBinds masters <- L.use circuitMasters - slaves <- L.use circuitVlaves + slaves <- L.use circuitSlaves let addDef :: String -> PortDescription PortName -> CircuitM () addDef suffix = \case Ref (PortName loc (unpackFS -> name@('_':_))) -> do @@ -1365,10 +1374,6 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where x <- parseCircuit lappB >> completeUnderscores >> circuitQQExpM when debug $ ppr x pure x - | isCircuitVVar circuitVar = runCircuitM $ do - x <- parseCircuit lappB >> completeUnderscores >> circuitVQQExpM - when debug $ ppr x - pure x -- `circuit $` application transform' (L _ (OpApp _xapp c@(L _ circuitVar) (L _ infixVar) appR)) @@ -1377,11 +1382,6 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where x <- parseCircuit appR >> completeUnderscores >> circuitQQExpM when debug $ ppr x pure (dollarChainReplaceCircuit "circuit" x c) - | isDollar infixVar && dollarChainIsCircuit "circuitV" circuitVar = do - runCircuitM $ do - x <- parseCircuit appR >> completeUnderscores >> circuitVQQExpM - when debug $ ppr x - pure (dollarChainReplaceCircuit "circuitV" x c) transform' e = pure e @@ -1456,12 +1456,14 @@ showC a = show (typeOf a) <> " " <> show (Data.toConstr a) -- Names --------------------------------------------------------------- --- | Recognise the value-boundary marker keywords (see 'SigMarker'). +-- | Recognise the port marker keywords (see 'SigMarker'). markerFromName :: OccName.OccName -> Maybe SigMarker markerFromName occ = case OccName.occNameString occ of - "Signal" -> Just SignalMarker - "Fwd" -> Just FwdMarker - _ -> Nothing + "Signal" -> Just SignalMarker + "Fwd" -> Just FwdMarker + "SignalV" -> Just SignalVMarker + "FwdV" -> Just FwdVMarker + _ -> Nothing -- | Collection of names external to circuit-notation. data ExternalNames = ExternalNames diff --git a/tests/fixtures/CrossDomainError.hs b/tests/fixtures/CrossDomainError.hs index 61db014..207ad36 100644 --- a/tests/fixtures/CrossDomainError.hs +++ b/tests/fixtures/CrossDomainError.hs @@ -5,13 +5,13 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture sharing a value-level variable across two clock domains in a --- @circuitV@ block: @acc + a + b@ mixes values sampled from a @domA@ bus and +-- @circuit@ block: @acc + a + b@ mixes values sampled from a @domA@ bus and -- a @domB@ bus, which is an (unsynchronized) clock domain crossing. The -- shared variables put both buses in the same logic group, whose @bundle@ -- demands a single domain, so GHC reports @Couldn't match type domA with -- domB@. The blame lands on the head of the circuit (the constraint solver -- unifies the domains via the generated bundle before it checks the slave --- pattern), so the marker sits on the @circuitV@ line. +-- pattern), so the marker sits on the @circuit@ line. module CrossDomainError where import Circuit @@ -22,6 +22,6 @@ registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) crossDomainError :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int) -crossDomainError = circuitV \(Signal a, Signal b) -> do -- cross-domain-error-marker - Signal acc <- registerC 0 -< Signal (acc + a + b) - idC -< Signal acc +crossDomainError = circuit \(SignalV a, SignalV b) -> do -- cross-domain-error-marker + SignalV acc <- registerC 0 -< SignalV (acc + a + b) + idC -< SignalV acc diff --git a/tests/fixtures/ValueExprError.hs b/tests/fixtures/ValueExprError.hs index 4418942..eb8f5ed 100644 --- a/tests/fixtures/ValueExprError.hs +++ b/tests/fixtures/ValueExprError.hs @@ -5,7 +5,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture with a deliberate type error on a /value-level/ expression in a --- @circuitV@ block: @a@ is an 'Int' (sampled off the input bus) but is used +-- @circuit@ block: @a@ is an 'Int' (sampled off the input bus) but is used -- with @(&&)@. The erroring statement is not the last statement of the -- circuit; the error-location test asserts GHC points at the tagged line and -- not at the end of the block (where the generated @circuitLogic@ and @@ -20,6 +20,6 @@ registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) valueExprError :: Circuit (Signal dom Int) (Signal dom Int) -valueExprError = circuitV \(Signal a) -> do - Signal b <- registerC 0 -< Signal (a && True) -- value-expr-error-marker - idC -< Signal (b + a) +valueExprError = circuit \(SignalV a) -> do + SignalV b <- registerC 0 -< SignalV (a && True) -- value-expr-error-marker + idC -< SignalV (b + a) diff --git a/tests/fixtures/ValueLetError.hs b/tests/fixtures/ValueLetError.hs index eb1ee3d..d58a986 100644 --- a/tests/fixtures/ValueLetError.hs +++ b/tests/fixtures/ValueLetError.hs @@ -5,7 +5,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} -- | A fixture with a deliberate type error inside a /value-level let/ of a --- @circuitV@ block: @a@ is an 'Int' (sampled off the input bus) but is +-- @circuit@ block: @a@ is an 'Int' (sampled off the input bus) but is -- passed to 'not'. The let bindings move into the generated @circuitLogic@ -- function; this asserts they keep their source locations when they do. module ValueLetError where @@ -14,6 +14,6 @@ import Circuit import Clash.Prelude valueLetError :: Circuit (Signal dom Int) (Signal dom Int) -valueLetError = circuitV \(Signal a) -> do +valueLetError = circuit \(SignalV a) -> do let b = not a -- value-let-error-marker - idC -< Signal (a + (if b then 1 else 0)) + idC -< SignalV (a + (if b then 1 else 0)) diff --git a/tests/fixtures/ValuePortError.hs b/tests/fixtures/ValuePortError.hs index adcc1c7..cf862b7 100644 --- a/tests/fixtures/ValuePortError.hs +++ b/tests/fixtures/ValuePortError.hs @@ -4,7 +4,7 @@ {-# OPTIONS -fplugin=CircuitNotation #-} --- | A fixture with a plugin-level port error in a @circuitV@ block: the bus +-- | A fixture with a plugin-level port error in a @circuit@ block: the bus -- @b@ is bound but never used, so the plugin itself (not GHC's type checker) -- reports \"Slave port b has no associated master\" -- pointing at the -- binding. @@ -14,6 +14,6 @@ import Circuit import Clash.Prelude valuePortError :: Circuit (Signal dom Int) (Signal dom Int) -valuePortError = circuitV \(Signal a) -> do - b <- idC -< Signal (a + 1) -- value-port-error-marker - idC -< Signal (a * 2) +valuePortError = circuit \(SignalV a) -> do + b <- idC -< SignalV (a + 1) -- value-port-error-marker + idC -< SignalV (a * 2) diff --git a/tests/fixtures/ValueShapeError.hs b/tests/fixtures/ValueShapeError.hs index 0c92828..b7cb956 100644 --- a/tests/fixtures/ValueShapeError.hs +++ b/tests/fixtures/ValueShapeError.hs @@ -4,11 +4,11 @@ {-# OPTIONS -fplugin=CircuitNotation #-} --- | A fixture marking a non-signal bus with @Signal@ in a @circuitV@ block: --- @vecC@ produces a @Vec@ of signals, so the @Signal v@ pattern is \"too +-- | A fixture marking a non-signal bus with @Signal@ in a @circuit@ block: +-- @vecC@ produces a @Vec@ of signals, so the @SignalV v@ pattern is \"too -- shallow\" (the value boundary must sit exactly at a 'Signal'). The -- generated @SigTag@ pins the bus type to a signal, so GHC reports a clear --- @Vec ... /~ Signal ...@ mismatch; this asserts it points at the offending +-- @Vec ... /~ SignalV ...@ mismatch; this asserts it points at the offending -- statement. module ValueShapeError where @@ -19,6 +19,6 @@ vecC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) vecC = Circuit $ \(s :-> _) -> (() :-> (s :> s :> Nil)) valueShapeError :: Circuit (Signal dom Int) (Signal dom Int) -valueShapeError = circuitV \(Signal a) -> do - Signal v <- vecC -< Signal (a + 1) -- value-shape-error-marker - idC -< Signal (a + 1) +valueShapeError = circuit \(SignalV a) -> do + SignalV v <- vecC -< SignalV (a + 1) -- value-shape-error-marker + idC -< SignalV (a + 1) diff --git a/tests/unittests.hs b/tests/unittests.hs index 91fd843..fec34b8 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -48,6 +48,9 @@ main = do [111, 222, 333, 444, 555] , check "vstreamC" (sample5 (simulateC vstreamC (fromList (fmap Just [0 ..])))) [Just 1, Just 2, Just 3, Just 4, Just 5] + , let (mlV, mlA) = simulateC mixedLevelsC (fromList [1 ..] :> fromList [10, 20 ..] :> Nil, fromList [0 ..]) + in check "mixedLevelsC" (fmap sample5 mlV, sample5 mlA) + ([10, 20, 30, 40, 50] :> [1, 2, 3, 4, 5] :> Nil, [1, 2, 3, 4, 5]) , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) From 0a88fdd8f1b1c7e2af1f1543b4d7851273579822 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 16:31:01 +0100 Subject: [PATCH 11/21] Add support for DSignalV --- CHANGELOG.md | 26 ++++--- README.md | 7 ++ example/ValueCircuits.hs | 36 ++++++++++ src/Circuit.hs | 14 ++++ src/CircuitNotation.hs | 105 ++++++++++++++++++++--------- tests/error-location.hs | 8 +++ tests/fixtures/CrossDelayError.hs | 20 ++++++ tests/fixtures/MixedMarkerError.hs | 21 ++++++ tests/unittests.hs | 14 +++- 9 files changed, 205 insertions(+), 46 deletions(-) create mode 100644 tests/fixtures/CrossDelayError.hs create mode 100644 tests/fixtures/MixedMarkerError.hs diff --git a/CHANGELOG.md b/CHANGELOG.md index 72b8fa7..51e8bdf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,21 +17,25 @@ rejected by the type checker. Lets that don't touch value land stay at the bus level, so let-bound sub-circuits can be used with `-<`. - The two value markers have distinct semantics: `SignalV x` asserts the + The value markers have distinct semantics: `SignalV x` asserts the bus is a `Signal` (best inference — it works against fully generic - sub-circuits), while `FwdV x` samples/drives the forward channel of any + sub-circuits); `FwdV x` samples/drives the forward channel of any signal-like bus via the new `SignalBus` class (`Signal`s, `Vec`s and tuples of them, custom buses) but needs the bus type determined by - context. + context; and `DSignalV x` is `SignalV` for delayed signals — the delay + index is part of the bus type, so a logic group's values must all sit at + the same pipeline depth, and its outputs are produced at that depth. + Mixing plain and delayed markers in one group is reported by the plugin. - The value boundary is generated with the new `SigTag` and `FwdTag` pattern - synonyms (`Circuit` module); `SigTag` pins the bus type to a `Signal` so - that type inference survives nested circuits (the `Fwd` family is not - injective) and "too shallow" `SignalV` markers report a direct - `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` gained - `signalTagName` and `fwdTagName` fields, so custom plugins (e.g. - clash-protocols style) need to supply them — `defExternalNames` is now - exported so they can be record updates of the defaults. + The value boundary is generated with the new `SigTag`, `FwdTag` and + `DSigTag` pattern synonyms (`Circuit` module); `SigTag`/`DSigTag` pin the + bus type so that type inference survives nested circuits (the `Fwd` + family is not injective) and "too shallow" `SignalV` markers report a + direct `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` + gained `signalTagName`, `fwdTagName` and `dSignalTagName` fields, so + custom plugins (e.g. clash-protocols style) need to supply them — + `defExternalNames` is now exported so they can be record updates of the + defaults. * Add a per-GHC `checks` output to the flake, so `nix flake check` (or `nix build .#checks..`) builds the package and runs all test suites against every supported GHC. The CI nix job now uses it. The diff --git a/README.md b/README.md index de06ff5..5af60b6 100644 --- a/README.md +++ b/README.md @@ -27,6 +27,13 @@ The two value markers differ in what buses they accept: given a one-line instance. In exchange, the bus type must be determined by context (the circuit's signature or a concretely typed sub-circuit), and pattern uses need a trivial backwards channel (`TrivialBwd (Bwd t)`). +- `DSignalV x` is `SignalV` for delayed signals (`DSignal dom d a`). The + delay index is part of the bus type, so everything in one logic group must + sit at the *same pipeline depth* (combining values from different stages + is a type error, like mixing clock domains), and since the lifted logic is + combinational, a group's outputs are produced at the delay its inputs are + sampled at. Groups at different depths can coexist in one block. Plain and + delayed values can't meet in one group; the plugin reports mixing them. Everything in between — the `let` bindings of the do block — is ordinary pure Haskell, and feedback loops are written as ordinary recursive `let`s: diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 0e3f4e4..e8c7cc0 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -17,6 +17,7 @@ blocks. These are simulated and checked by tests/unittests.hs. {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# OPTIONS -fplugin=CircuitNotation #-} {-# OPTIONS -Wall #-} @@ -251,6 +252,41 @@ multicastC = circuit \(SignalV a) -> do passthrough :: Circuit (Signal dom Int) (Signal dom Int) passthrough = circuit \a -> a +-- Delayed signals -------------------------------------------------------- +-- +-- @DSignalV@ marks the value boundary on 'DSignal' buses. The generated +-- @DSigTag@ pins the bus type /including the delay index/, and a delayed +-- group's bundle unifies the delays of everything in it: all values that +-- meet must come from (and go to) buses at the same pipeline depth. The +-- lifted logic is combinational, so a group's outputs are produced at the +-- same delay its inputs are sampled at. Groups at different delays can +-- coexist in one block. + +-- | A delayed register: the output is one cycle (and one delay index) +-- behind the input. +dregisterC :: a -> Circuit (DSignal dom d a) (DSignal dom (d + 1) a) +dregisterC a = Circuit $ \(s :-> ()) -> (() :-> unsafeFromSignal (a :- toSignal s)) + +-- | Delay-polymorphic pass-through: works at any pipeline depth, and pins +-- input and output to the /same/ depth. +dplusOne :: Circuit (DSignal dom d Int) (DSignal dom d Int) +dplusOne = circuit \(DSignalV a) -> do + idC -< DSignalV (a + 1) + +-- | Two delayed values meeting in one group: their buses must agree on the +-- delay (and domain), which the signature expresses with a single @d@. +daddC :: Circuit (DSignal dom d Int, DSignal dom d Int) (DSignal dom d Int) +daddC = circuit \(DSignalV a, DSignalV b) -> do + idC -< DSignalV (a + b) + +-- | A two-stage pipeline: the @i@ group sits at delay @d@ and the @a@ group +-- at delay @d + 1@ -- two value groups at different pipeline depths in one +-- block, linked by the delayed register at the bus level. +dpipeC :: Circuit (DSignal dom d Int) (DSignal dom (d + 1) Int) +dpipeC = circuit \(DSignalV i) -> do + DSignalV a <- dregisterC 0 -< DSignalV (i + 1) + idC -< DSignalV (a * 2) + -- Multiple clock domains ------------------------------------------------- -- -- The plugin splits the value-level logic into groups connected by shared diff --git a/src/Circuit.hs b/src/Circuit.hs index 3eed7b6..3e14486 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -77,6 +77,9 @@ type instance Bwd (a,b,c) = (Bwd a, Bwd b, Bwd c) type instance Fwd (Signal dom a) = Signal dom a type instance Bwd (Signal dom a) = () +type instance Fwd (DSignal dom d a) = DSignal dom d a +type instance Bwd (DSignal dom d a) = () + -- | Circuit type. newtype Circuit a b = Circuit { runCircuit :: CircuitT a b } type CircuitT a b = (Fwd a :-> Bwd b) -> (Bwd a :-> Fwd b) @@ -218,6 +221,17 @@ pattern SigTag :: Signal dom a -> BusTag (Signal dom a) (Signal dom a) pattern SigTag s = BusTag s {-# COMPLETE SigTag #-} +-- | Like 'SigTag' but for delayed signals, used for @DSignalV@ markers: +-- pins the bus type to be a 'DSignal', /including its delay index/. The +-- markers of one logic group all flow through one (delayed) bundle, so a +-- group's buses must agree on the delay as well as the domain — combining +-- values from different pipeline stages is rejected by the type checker. +-- Since the lifted logic is combinational, the group's outputs are produced +-- at the same delay its inputs are sampled at. +pattern DSigTag :: DSignal dom d a -> BusTag (DSignal dom d a) (DSignal dom d a) +pattern DSigTag s = BusTag s +{-# COMPLETE DSigTag #-} + -- | Buses whose forward channel carries a single value per clock cycle, -- i.e. is convertible to a single 'Signal'. The @Fwd@ markers at the value -- boundary of @circuit@ blocks work on any such bus: 'Signal's themselves, diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 043c11d..35ca0c7 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -99,6 +99,7 @@ import GHC.Types.Unique.Map.Extra -- clash-prelude import Clash.Prelude (Vec((:>), Nil), bundle, unbundle) +import qualified Clash.Signal.Delayed.Bundle as DBundle -- lens import qualified Control.Lens as L @@ -224,14 +225,25 @@ instance Show PortName where -- @SigTag@, which drives type inference) while @FwdV@ samples the forward -- channel of any signal-like bus (generating the class-constrained -- @FwdTag@, which requires the bus type to be determined by context). -data SigMarker = SignalMarker | FwdMarker | SignalVMarker | FwdVMarker +data SigMarker = SignalMarker | FwdMarker | SignalVMarker | FwdVMarker | DSignalVMarker --- | Is this marker a value boundary (@SignalV@/@FwdV@)? +-- | Is this marker a value boundary (@SignalV@/@FwdV@/@DSignalV@)? isValueMarker :: SigMarker -> Bool isValueMarker = \case - SignalVMarker -> True - FwdVMarker -> True - _ -> False + SignalVMarker -> True + FwdVMarker -> True + DSignalVMarker -> True + _ -> False + +-- | Value groups come in two flavors, lifted with the matching bundle: +-- plain signal values (@SignalV@/@FwdV@) and delayed signal values +-- (@DSignalV@). The flavors cannot meet in one group. +data GroupFlavor = SignalGroup | DSignalGroup deriving Eq + +valueMarkerFlavor :: SigMarker -> GroupFlavor +valueMarkerFlavor = \case + DSignalVMarker -> DSignalGroup + _ -> SignalGroup data PortDescription a = Tuple [PortDescription a] @@ -935,10 +947,11 @@ sigTagE mk a@(L l _) = varE l (markerTagName mk) `appE` a -- only value markers reach the SigTag* constructors, but keep this total markerTagName :: (?nms :: ExternalNames) => SigMarker -> GHC.RdrName markerTagName = \case - SignalVMarker -> signalTagName ?nms - FwdVMarker -> fwdTagName ?nms - SignalMarker -> signalTagName ?nms - FwdMarker -> fwdTagName ?nms + SignalVMarker -> signalTagName ?nms + FwdVMarker -> fwdTagName ?nms + DSignalVMarker -> dSignalTagName ?nms + SignalMarker -> signalTagName ?nms + FwdMarker -> fwdTagName ?nms tagTypeCon :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsType GhcPs tagTypeCon = @@ -1071,11 +1084,11 @@ countValuePorts p = replaceFwdPats :: String -> PortDescription PortName - -> State (Int, [LPat GhcPs]) (PortDescription PortName) + -> State (Int, [(SigMarker, LPat GhcPs)]) (PortDescription PortName) replaceFwdPats prefix = L.transformM \case FwdPat mk lpat@(L loc _) | isValueMarker mk -> do (i, pats) <- get - put (i + 1, pats <> [lpat]) + put (i + 1, pats <> [(mk, lpat)]) pure (SigTagPat mk (varP loc (prefix <> show i))) p -> pure p @@ -1085,11 +1098,11 @@ replaceFwdPats prefix = L.transformM \case replaceFwdExprs :: String -> PortDescription PortName - -> State (Int, [LHsExpr GhcPs]) (PortDescription PortName) + -> State (Int, [(SigMarker, LHsExpr GhcPs)]) (PortDescription PortName) replaceFwdExprs prefix = L.transformM \case FwdExpr mk lexpr@(L loc _) | isValueMarker mk -> do (i, exprs) <- get - put (i + 1, exprs <> [lexpr]) + put (i + 1, exprs <> [(mk, lexpr)]) pure (SigTagExpr mk (varE loc (var (prefix <> show i)))) p -> pure p @@ -1175,13 +1188,13 @@ valueCircuitQQExpM = do letTypes <- L.use circuitTypes -- see [value-components] - let valueNames = Set.fromList (concatMap patVarNames inPats <> concatMap bindDefinedNames lets) + let valueNames = Set.fromList (concatMap (patVarNames . snd) inPats <> concatMap bindDefinedNames lets) valueFvs :: SYB.Data a => a -> Set.Set String valueFvs a = Set.intersection (freeVarNames a) valueNames items = - [ (ItemIn i, Set.fromList (patVarNames p)) | (i, p) <- zip [0 ..] inPats ] <> - [ (ItemOut k, valueFvs e) | (k, e) <- zip [0 ..] outExprs ] <> + [ (ItemIn i, Set.fromList (patVarNames p)) | (i, (_, p)) <- zip [0 ..] inPats ] <> + [ (ItemOut k, valueFvs e) | (k, (_, e)) <- zip [0 ..] outExprs ] <> [ (ItemLet j, Set.fromList (bindDefinedNames b) `Set.union` valueFvs b) | (j, b) <- zip [0 ..] lets ] @@ -1214,41 +1227,63 @@ valueCircuitQQExpM = do sigsForComp ci = [ s | (Just ci', s) <- splitSigs, ci' == ci ] outerSigs = [ s | (Nothing, s) <- splitSigs ] + -- Each group is lifted with the bundle matching its markers' flavor; + -- plain (SignalV/FwdV) and delayed (DSignalV) values cannot meet in one + -- group, since neither bundle accepts both bus kinds. + flavors <- forM innerGroups \(its, _) -> do + let mks = [ (fst (inPats !! i), getLoc (snd (inPats !! i))) | ItemIn i <- its ] + <> [ (fst (outExprs !! k), getLoc (snd (outExprs !! k))) | ItemOut k <- its ] + dLocs = [ l | (mk, l) <- mks, valueMarkerFlavor mk == DSignalGroup ] + sLocs = [ l | (mk, l) <- mks, valueMarkerFlavor mk == SignalGroup ] + case (dLocs, sLocs) of + (dl : _, _ : _) -> do + errM (locA dl) $ + "This value group mixes DSignalV with SignalV/FwdV markers. " + <> "Delayed and undelayed values cannot meet in one logic group; " + <> "convert between Signal and DSignal explicitly at the bus level " + <> "instead." + pure DSignalGroup + (_ : _, []) -> pure DSignalGroup + _ -> pure SignalGroup + -- One logic function and one lifted knot binding per group: -- circuitLogic_cN = \(ins) -> let in (outs) -- (outBuses) = unbundle (fmap circuitLogic_cN (bundle (inBuses))) -- bundle/unbundle are only needed when there is more than one bus, and -- with no inputs at all the logic is constant, so it is mapped over -- @pure ()@. The generated bundle elements and knot patterns take the - -- source locations of the original Signal markers, so clock domain - -- mismatches are reported on the offending marker. Groups with no - -- outputs produce no value (their logic would be dead) and generate + -- source locations of the original markers, so clock domain (and + -- delay) mismatches are reported on the offending marker. Groups with + -- no outputs produce no value (their logic would be dead) and generate -- nothing. - mkComp ci (its, _) = + let mkComp ci flavor (its, _) = let ins = sort [ i | ItemIn i <- its ] outs = sort [ k | ItemOut k <- its ] ls = sort [ j | ItemLet j <- its ] + (bundleNm, unbundleNm) = case flavor of + SignalGroup -> (thName 'bundle, thName 'unbundle) + DSignalGroup -> (thName 'DBundle.bundle, thName 'DBundle.unbundle) logicNm = logicName <> "_c" <> show ci - logicLam = lamE [tupP (map (inPats !!) ins)] + logicLam = lamE [tupP (map (snd . (inPats !!)) ins)] (letE noSrcSpanA (sigsForComp ci) (map (lets !!) ls) - (tupE noSrcSpanA (map (outExprs !!) outs))) + (tupE noSrcSpanA (map (snd . (outExprs !!)) outs))) logicBind = L loc $ patBind (varP noSrcSpanA logicNm) logicLam - inVars = map (\i -> let (L l _) = inPats !! i in varE l (var (inPrefix <> show i))) ins - outVarPs = map (\k -> let (L l _) = outExprs !! k in varP l (outPrefix <> show k)) outs + inVars = map (\i -> let (L l _) = snd (inPats !! i) in varE l (var (inPrefix <> show i))) ins + outVarPs = map (\k -> let (L l _) = snd (outExprs !! k) in varP l (outPrefix <> show k)) outs bundled = case inVars of [] -> varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] [e] -> e - es -> varE noSrcSpanA (thName 'bundle) `appE` tupE noSrcSpanA es + es -> varE noSrcSpanA bundleNm `appE` tupE noSrcSpanA es lifted = varE noSrcSpanA (thName 'fmap) `appE` varE noSrcSpanA (var logicNm) `appE` bundled knotExpr = if length outs > 1 - then varE noSrcSpanA (thName 'unbundle) `appE` lifted + then varE noSrcSpanA unbundleNm `appE` lifted else lifted knotBind = L loc $ patBind (tupP outVarPs) knotExpr in if null outs then [] else [logicBind, knotBind] - compDecs = concat (zipWith mkComp [0 ..] innerGroups) + compDecs = concat (zipWith3 mkComp [0 ..] flavors innerGroups) -- The bus plumbing is generated exactly as in 'busCircuitQQExpM'. let decFromBinding' b@Binding{bCircuit = L cloc _} = L cloc (decFromBinding dflags b) @@ -1459,11 +1494,12 @@ showC a = show (typeOf a) <> " " <> show (Data.toConstr a) -- | Recognise the port marker keywords (see 'SigMarker'). markerFromName :: OccName.OccName -> Maybe SigMarker markerFromName occ = case OccName.occNameString occ of - "Signal" -> Just SignalMarker - "Fwd" -> Just FwdMarker - "SignalV" -> Just SignalVMarker - "FwdV" -> Just FwdVMarker - _ -> Nothing + "Signal" -> Just SignalMarker + "Fwd" -> Just FwdMarker + "SignalV" -> Just SignalVMarker + "FwdV" -> Just FwdVMarker + "DSignalV" -> Just DSignalVMarker + _ -> Nothing -- | Collection of names external to circuit-notation. data ExternalNames = ExternalNames @@ -1477,7 +1513,9 @@ data ExternalNames = ExternalNames -- blocks , fwdTagName :: GHC.RdrName -- ^ like 'signalTagName' but class-constrained, accepting any signal-like - -- bus; used for @Fwd@ markers at the value boundary of @circuitV@ blocks + -- bus; used for @FwdV@ markers at the value boundary of @circuit@ blocks + , dSignalTagName :: GHC.RdrName + -- ^ like 'signalTagName' for delayed signals; used for @DSignalV@ markers , tagTName :: GHC.RdrName , fwdBwdCon :: GHC.RdrName , fwdAndBwdTypes :: Direction -> GHC.RdrName @@ -1498,6 +1536,7 @@ defExternalNames = ExternalNames , tagName = GHC.Unqual (OccName.mkDataOcc "BusTag") , signalTagName = GHC.Unqual (OccName.mkDataOcc "SigTag") , fwdTagName = GHC.Unqual (OccName.mkDataOcc "FwdTag") + , dSignalTagName = GHC.Unqual (OccName.mkDataOcc "DSigTag") , tagTName = GHC.Unqual (OccName.mkTcOcc "BusTag") , fwdBwdCon = GHC.Unqual (OccName.mkDataOcc ":->") , fwdAndBwdTypes = \case diff --git a/tests/error-location.hs b/tests/error-location.hs index 1c701e8..26c4671 100644 --- a/tests/error-location.hs +++ b/tests/error-location.hs @@ -55,6 +55,14 @@ fixtures = -- type error , Fixture ("tests" "fixtures" "CrossDomainError.hs") "cross-domain-error-marker" (Just "Couldn't match type") + -- sharing a value-level variable between two pipeline depths; the + -- merged group's delayed bundle demands one delay index + , Fixture ("tests" "fixtures" "CrossDelayError.hs") "cross-delay-error-marker" + (Just "Couldn't match type") + -- mixing plain and delayed value markers in one group is reported by + -- the plugin itself, at the offending marker + , Fixture ("tests" "fixtures" "MixedMarkerError.hs") "mixed-marker-error-marker" + (Just "mixes DSignalV with SignalV/FwdV") ] main :: IO () diff --git a/tests/fixtures/CrossDelayError.hs b/tests/fixtures/CrossDelayError.hs new file mode 100644 index 0000000..a7bd611 --- /dev/null +++ b/tests/fixtures/CrossDelayError.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture sharing a value-level variable between two 'DSignal' buses at +-- /different/ pipeline depths: @a + b@ mixes a delay-0 and a delay-1 value. +-- The shared variables put both buses in the same logic group, whose +-- delayed bundle demands a single delay index, so GHC reports a +-- @0@-vs-@1@ mismatch. Like the cross-domain case, the blame lands on the +-- head of the circuit. +module CrossDelayError where + +import Circuit +import Clash.Prelude + +crossDelayError :: Circuit (DSignal dom 0 Int, DSignal dom 1 Int) (DSignal dom 0 Int) +crossDelayError = circuit \(DSignalV a, DSignalV b) -> do -- cross-delay-error-marker + idC -< DSignalV (a + b) diff --git a/tests/fixtures/MixedMarkerError.hs b/tests/fixtures/MixedMarkerError.hs new file mode 100644 index 0000000..8153179 --- /dev/null +++ b/tests/fixtures/MixedMarkerError.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture mixing plain (@SignalV@) and delayed (@DSignalV@) value +-- markers in one logic group: neither the plain nor the delayed bundle +-- accepts both bus kinds, so the plugin itself reports the conflict -- +-- pointing at the offending @DSignalV@ marker. +module MixedMarkerError where + +import Circuit +import Clash.Prelude + +mixedMarkerError :: Circuit (Signal dom Int, DSignal dom 0 Int) (Signal dom Int) +mixedMarkerError = circuit + \( SignalV a + , DSignalV b -- mixed-marker-error-marker + ) -> do + idC -< SignalV (a + b) diff --git a/tests/unittests.hs b/tests/unittests.hs index fec34b8..52bb326 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -9,8 +9,9 @@ module Main where import Control.Monad (unless) import System.Exit (exitFailure) -import Clash.Prelude (NFDataX, Signal, System, Vec ((:>), Nil), - fromList, sampleN) +import Clash.Prelude (DSignal, NFDataX, Signal, System, + Vec ((:>), Nil), fromList, fromSignal, + sampleN, toSignal) import Circuit (Circuit) import Example () @@ -21,6 +22,9 @@ import ValueCircuits sample5 :: NFDataX a => Signal System a -> [a] sample5 s = sampleN 5 s +dsig :: NFDataX a => [a] -> DSignal System 0 a +dsig = fromSignal . fromList + check :: (Eq a, Show a) => String -> a -> a -> IO Bool check name actual expected | actual == expected = pure True @@ -51,6 +55,12 @@ main = do , let (mlV, mlA) = simulateC mixedLevelsC (fromList [1 ..] :> fromList [10, 20 ..] :> Nil, fromList [0 ..]) in check "mixedLevelsC" (fmap sample5 mlV, sample5 mlA) ([10, 20, 30, 40, 50] :> [1, 2, 3, 4, 5] :> Nil, [1, 2, 3, 4, 5]) + + -- delayed signals + , check "dplusOne" (sample5 (toSignal (simulateC dplusOne (dsig [0 ..])))) [1, 2, 3, 4, 5] + , check "daddC" (sample5 (toSignal (simulateC daddC (dsig [1 ..], dsig [10, 20 ..])))) + [11, 22, 33, 44, 55] + , check "dpipeC" (sample5 (toSignal (simulateC dpipeC (dsig [1 ..])))) [0, 4, 6, 8, 10] , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) From f2643a80e201d5a544977e493c91a8971af19c13 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Wed, 10 Jun 2026 22:53:30 +0100 Subject: [PATCH 12/21] Make Signal and DSignal enforce types --- CHANGELOG.md | 8 +++--- README.md | 11 ++++---- circuit-notation.cabal | 2 +- example/ValueCircuits.hs | 34 ++++++++++++----------- src/CircuitNotation.hs | 58 +++++++++++++++++++++++----------------- tests/unittests.hs | 9 ++++--- 6 files changed, 70 insertions(+), 52 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 51e8bdf..1f8aef6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,13 +1,15 @@ # Revision history for `circuit-notations` -## Unreleased +## 0.3.0.0 -- Unreleased * Add value-level ports via the new `SignalV` and `FwdV` markers in `circuit` blocks. The circuit's logic is written over the values sampled each clock cycle; the plugin lifts it back to the signal level with `fmap`/`bundle`/`unbundle` and ties feedback loops with a lazy let - binding. The bus-level `Signal`/`Fwd` markers keep their existing meaning - and the two levels can be mixed freely in one block. See the README and + binding. The bus-level markers still bind the raw forward channel and mix + freely with value markers in one block; `Fwd` works on any bus, while the + bus-level `Signal` (and new `DSignal`) markers now additionally enforce + the bus type, which also drives type inference. See the README and example/ValueCircuits.hs. A block can span several clock domains: the value-level bindings are diff --git a/README.md b/README.md index 5af60b6..4e9d870 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,10 @@ ordinary `circuit` block: - `SignalV n <- … -< …` binds `n` to the per-cycle value carried on that bus. - `… -< SignalV e` injects the per-cycle value `e` back onto a bus. -(The bus-level `Signal`/`Fwd` markers, which bind the raw forward channel, -keep their existing meaning; the two levels can be mixed freely in one -block.) +(The bus-level markers, which bind the raw forward channel, still exist and +can be mixed freely with value markers in one block: `Fwd` works on any bus, +while `Signal` and `DSignal` additionally enforce that the bus is a `Signal` +or `DSignal` — which also helps type inference, since it pins the bus type.) The two value markers differ in what buses they accept: @@ -39,8 +40,8 @@ Everything in between — the `let` bindings of the do block — is ordinary pur Haskell, and feedback loops are written as ordinary recursive `let`s: ```haskell -counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuit \_bs -> do +counter3 :: Circuit () (Signal dom Int) +counter3 = circuit do SignalV n <- registerC 0 -< SignalV n' -- n :: Int (this cycle's value) SignalV m <- registerC 8 -< SignalV m' -- m :: Int let n' = n + 1 -- pure, value-level diff --git a/circuit-notation.cabal b/circuit-notation.cabal index de1345d..e828865 100644 --- a/circuit-notation.cabal +++ b/circuit-notation.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: circuit-notation -version: 0.2.0.0 +version: 0.3.0.0 synopsis: Source plugin for manipulating circuits in Clash using arrow notation description: Source plugin for manipulating circuits in Clash using arrow notation. diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index e8c7cc0..6bfd5c7 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -160,9 +160,9 @@ accum = circuit $ \(SignalV i) -> do idC -< SignalV acc' -- | Two interleaved feedback loops (the canonical example from the design --- notes). The bus input is ignored. -counter3 :: Circuit (Signal dom Bool) (Signal dom Int) -counter3 = circuit \_bs -> do +-- notes). +counter3 :: Circuit () (Signal dom Int) +counter3 = circuit do SignalV n <- registerC 0 -< SignalV n' SignalV m <- registerC 8 -< SignalV m' let n' = n + 1 @@ -175,8 +175,8 @@ counter3 = circuit \_bs -> do -- buses and a lazy let binding ties the feedback knot. 'SigTag' is 'BusTag' -- with its bus type pinned to a signal, which keeps inference going where -- the non-injective 'Fwd' family would otherwise lose it. -counter3Expanded :: Circuit (Signal dom Bool) (Signal dom Int) -counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> +counter3Expanded :: Circuit () (Signal dom Int) +counter3Expanded = TagCircuit $ \(~(BusTagBundle ()) :-> _) -> let circuitLogic = \(n, m) -> let n' = n + 1 @@ -188,9 +188,7 @@ counter3Expanded = TagCircuit $ \(_bs_Fwd :-> _) -> (_ :-> SigTag valIn0) = runTagCircuit (registerC 0) (SigTag valOut0 :-> BusTag unitBwd) (_ :-> SigTag valIn1) = runTagCircuit (registerC 8) (SigTag valOut1 :-> BusTag unitBwd) - - _bs_Bwd = BusTag def - in (_bs_Bwd :-> SigTag valOut2) + in (BusTagBundle () :-> SigTag valOut2) -- | Compound state fed back through a /single/ register: a fibonacci -- machine. The pair is destructured and rebuilt at the value level. @@ -273,6 +271,14 @@ dplusOne :: Circuit (DSignal dom d Int) (DSignal dom d Int) dplusOne = circuit \(DSignalV a) -> do idC -< DSignalV (a + 1) +-- | The bus-level @DSignal@ marker: binds the raw delayed signal (here +-- mapped over directly) while enforcing that the bus is a 'DSignal'. The +-- bus-level @Signal@ marker enforces 'Signal' the same way; @Fwd@ remains +-- the generic bus-level marker. +dmapC :: Circuit (DSignal dom d Int) (DSignal dom d Int) +dmapC = circuit \(DSignal s) -> do + idC -< DSignal (fmap (+ 1) s) + -- | Two delayed values meeting in one group: their buses must agree on the -- delay (and domain), which the signature expresses with a single @d@. daddC :: Circuit (DSignal dom d Int, DSignal dom d Int) (DSignal dom d Int) @@ -295,15 +301,13 @@ dpipeC = circuit \(DSignalV i) -> do -- value across domains is an (unsynchronized) clock domain crossing and is -- rejected by the type checker. --- | Two completely independent counters in one block, on two /different/ +-- | Two independently enabled counters in one block, on two /different/ -- clock domains: nothing forces @domA@ and @domB@ together. dualCounter :: Circuit (Signal domA Bool, Signal domB Bool) (Signal domA Int, Signal domB Int) -dualCounter = circuit \(_ea, _eb) -> do - SignalV n <- registerC 0 -< SignalV n' - SignalV m <- registerC 8 -< SignalV m' - let n' = n + 1 - m' = m + 1 - idC -< (SignalV n', SignalV m') +dualCounter = circuit \(SignalV enA, SignalV enB) -> do + SignalV n <- registerC 0 -< SignalV (if enA then n + 1 else n) + SignalV m <- registerC 0 -< SignalV (if enB then m + 1 else m) + idC -< (SignalV n, SignalV m) -- | Two independent accumulators, each reading values off its own input -- bus, on different clock domains. diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 35ca0c7..463aabb 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -218,14 +218,21 @@ data PortName = PortName SrcSpanAnnA GHC.FastString instance Show PortName where show (PortName _ fs) = GHC.unpackFS fs --- | Which keyword marked a port. @Signal@ and @Fwd@ are bus-level (and --- interchangeable): they bind/inject the raw forward channel. @SignalV@ and --- @FwdV@ mark the /value/ boundary, binding or injecting the per-cycle --- value: @SignalV@ asserts the bus /is/ a 'Signal' (generating the concrete --- @SigTag@, which drives type inference) while @FwdV@ samples the forward --- channel of any signal-like bus (generating the class-constrained --- @FwdTag@, which requires the bus type to be determined by context). -data SigMarker = SignalMarker | FwdMarker | SignalVMarker | FwdVMarker | DSignalVMarker +-- | Which keyword marked a port. +-- +-- The bus-level markers bind/inject the raw forward channel: @Fwd@ works on +-- any bus, while @Signal@ and @DSignal@ additionally /enforce/ (via the +-- concrete @SigTag@/@DSigTag@, which also drives type inference) that the +-- bus is a 'Signal' or @DSignal@ respectively. +-- +-- The @...V@ markers mark the /value/ boundary, binding or injecting the +-- per-cycle value: @SignalV@ and @DSignalV@ assert the bus type like their +-- bus-level counterparts, while @FwdV@ samples the forward channel of any +-- signal-like bus (generating the class-constrained @FwdTag@, which +-- requires the bus type to be determined by context). +data SigMarker + = SignalMarker | FwdMarker | DSignalMarker + | SignalVMarker | FwdVMarker | DSignalVMarker -- | Is this marker a value boundary (@SignalV@/@FwdV@/@DSignalV@)? isValueMarker :: SigMarker -> Bool @@ -829,7 +836,7 @@ bindWithSuffix dflags dir = \case Lazy loc p -> tildeP loc $ bindWithSuffix dflags dir p -- XXX: propagate location FwdExpr _ (L _ _) -> nlWildPat - FwdPat _ lpat -> tagP lpat + FwdPat mk lpat -> sigTagP mk lpat SigTagExpr _ (L _ _) -> nlWildPat SigTagPat mk lpat -> sigTagP mk lpat PortType ty p -> tagTypeP dir ty $ bindWithSuffix dflags dir p @@ -864,7 +871,7 @@ expWithSuffix dir = \case -- laziness only affects the pattern side Lazy _ p -> expWithSuffix dir p PortErr _ _ -> error "expWithSuffix PortErr!" - FwdExpr _ lexpr -> tagE lexpr + FwdExpr mk lexpr -> sigTagE mk lexpr FwdPat _ (L l _) -> tagE $ varE l (trivialBwd ?nms) SigTagExpr mk lexpr -> sigTagE mk lexpr -- the backwards channel of a signal bus is trivial, so a plain (untyped) @@ -944,14 +951,16 @@ sigTagP mk a@(L l _) = L l (conPatIn (noLoc (markerTagName mk)) (prefixCon [a])) sigTagE :: (p ~ GhcPs, ?nms :: ExternalNames) => SigMarker -> LHsExpr p -> LHsExpr p sigTagE mk a@(L l _) = varE l (markerTagName mk) `appE` a --- only value markers reach the SigTag* constructors, but keep this total +-- | The tag wrapped around a marked port: plain 'BusTag' for the generic +-- bus-level @Fwd@, the type-enforcing tags for everything else. markerTagName :: (?nms :: ExternalNames) => SigMarker -> GHC.RdrName markerTagName = \case + FwdMarker -> tagName ?nms + SignalMarker -> signalTagName ?nms + DSignalMarker -> dSignalTagName ?nms SignalVMarker -> signalTagName ?nms FwdVMarker -> fwdTagName ?nms DSignalVMarker -> dSignalTagName ?nms - SignalMarker -> signalTagName ?nms - FwdMarker -> fwdTagName ?nms tagTypeCon :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsType GhcPs tagTypeCon = @@ -1412,30 +1421,30 @@ transform debug = SYB.everywhereM (SYB.mkM transform') where -- `circuit $` application transform' (L _ (OpApp _xapp c@(L _ circuitVar) (L _ infixVar) appR)) - | isDollar infixVar && dollarChainIsCircuit "circuit" circuitVar = do + | isDollar infixVar && dollarChainIsCircuit circuitVar = do runCircuitM $ do x <- parseCircuit appR >> completeUnderscores >> circuitQQExpM when debug $ ppr x - pure (dollarChainReplaceCircuit "circuit" x c) + pure (dollarChainReplaceCircuit x c) transform' e = pure e --- | check if the named circuit keyword is applied via `a $ chain $ of $ dollars`. -dollarChainIsCircuit :: GHC.FastString -> HsExpr GhcPs -> Bool -dollarChainIsCircuit nm = \case - HsVar _ (L _ v) -> v == GHC.mkVarUnqual nm - OpApp _xapp _appL (L _ infixVar) (L _ appR) -> isDollar infixVar && dollarChainIsCircuit nm appR +-- | check if circuit is applied via `a $ chain $ of $ dollars`. +dollarChainIsCircuit :: HsExpr GhcPs -> Bool +dollarChainIsCircuit = \case + HsVar _ (L _ v) -> v == GHC.mkVarUnqual "circuit" + OpApp _xapp _appL (L _ infixVar) (L _ appR) -> isDollar infixVar && dollarChainIsCircuit appR _ -> False -- | Replace the circuit if it's part of a chain of `$`. -dollarChainReplaceCircuit :: GHC.FastString -> LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs -dollarChainReplaceCircuit nm circuitExpr (L loc app) = case app of +dollarChainReplaceCircuit :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs +dollarChainReplaceCircuit circuitExpr (L loc app) = case app of HsVar _ (L _loc v) - -> if v == GHC.mkVarUnqual nm + -> if v == GHC.mkVarUnqual "circuit" then circuitExpr else error "dollarChainAddCircuit: not a circuit" OpApp xapp appL (L infixLoc infixVar) appR - -> L loc $ OpApp xapp appL (L infixLoc infixVar) (dollarChainReplaceCircuit nm circuitExpr appR) + -> L loc $ OpApp xapp appL (L infixLoc infixVar) (dollarChainReplaceCircuit circuitExpr appR) t -> error $ "dollarChainAddCircuit unhandled case " <> showC t -- | The plugin for circuit notation. @@ -1496,6 +1505,7 @@ markerFromName :: OccName.OccName -> Maybe SigMarker markerFromName occ = case OccName.occNameString occ of "Signal" -> Just SignalMarker "Fwd" -> Just FwdMarker + "DSignal" -> Just DSignalMarker "SignalV" -> Just SignalVMarker "FwdV" -> Just FwdVMarker "DSignalV" -> Just DSignalVMarker diff --git a/tests/unittests.hs b/tests/unittests.hs index 52bb326..2f2c133 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -61,6 +61,7 @@ main = do , check "daddC" (sample5 (toSignal (simulateC daddC (dsig [1 ..], dsig [10, 20 ..])))) [11, 22, 33, 44, 55] , check "dpipeC" (sample5 (toSignal (simulateC dpipeC (dsig [1 ..])))) [0, 4, 6, 8, 10] + , check "dmapC" (sample5 (toSignal (simulateC dmapC (dsig [0 ..])))) [1, 2, 3, 4, 5] , check "plusOneFwd" (sample5 (simulateC plusOneFwd (fromList [0 ..]))) [1, 2, 3, 4, 5] , check "alwaysFive" (sample5 (simulateC alwaysFive ())) [5, 5, 5, 5, 5] , check "addC" (sample5 (simulateC addC (fromList [1 ..], fromList [10, 20 ..]))) @@ -83,8 +84,8 @@ main = do -- feedback , check "counter" (sample5 (simulateC counter ())) [0, 1, 2, 3, 4] , check "accum" (sample5 (simulateC accum (fromList [1 ..]))) [1, 3, 6, 10, 15] - , check "counter3" (sample5 (simulateC counter3 (pure False))) [10, 12, 14, 16, 18] - , check "counter3Expanded" (sample5 (simulateC counter3Expanded (pure False))) [10, 12, 14, 16, 18] + , check "counter3" (sample5 (simulateC counter3 ())) [10, 12, 14, 16, 18] + , check "counter3Expanded" (sample5 (simulateC counter3Expanded ())) [10, 12, 14, 16, 18] , check "fibC" (sample5 (simulateC fibC ())) [0, 1, 1, 2, 3] , check "shift3" (sample5 (simulateC shift3 (fromList [1 ..]))) [0, 0, 0, 1, 2] , check "rotate3" (sample5 (simulateC rotate3 (pure 1))) [6, 7, 8, 9, 10] @@ -98,8 +99,8 @@ main = do -- different-domain property is the fact that the signatures compile) , let (dcA, dcB) = simulateC (dualCounter :: Circuit (Signal System Bool, Signal System Bool) (Signal System Int, Signal System Int)) - (pure False, pure False) - in check "dualCounter" (sample5 dcA, sample5 dcB) ([1, 2, 3, 4, 5], [9, 10, 11, 12, 13]) + (fromList (cycle [True, False]), pure True) + in check "dualCounter" (sample5 dcA, sample5 dcB) ([0, 1, 1, 2, 2], [0, 1, 2, 3, 4]) , let (daA, daB) = simulateC (dualAccum :: Circuit (Signal System Int, Signal System Int) (Signal System Int, Signal System Int)) (fromList [1 ..], fromList [10, 20 ..]) From 10ba3c186eff07a37bf5ffe646cf0a32b75c8203 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Fri, 19 Jun 2026 12:05:32 +0100 Subject: [PATCH 13/21] Lower value-group inputs lazily Value-group logic is lifted to the signal level with `fmap` over a `bundle` of the group's inputs. Two strictness points there can make combinational feedback between value groups deadlock simulation: * `bundle` lifts its first element with `fmap` / `mapSignal#`, which forces that element's spine. Prepend a lazy unit so no real input sits in that spine-forcing head slot. * The logic function matched its inputs strictly, so a constructor pattern at the boundary (destructuring the sampled value) forced its input to produce *any* of the group's outputs -- even outputs that do not use it. That deadlocks when the input depends, through the circuit, on such an output. Match each value input lazily (irrefutable), as the bus-level plumbing already does, so an output only forces the inputs it actually uses. Both keep value-group feedback well founded without changing the lifted logic. The library and error-location test suites still pass. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/CircuitNotation.hs | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 463aabb..b5d1069 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -1273,7 +1273,22 @@ valueCircuitQQExpM = do SignalGroup -> (thName 'bundle, thName 'unbundle) DSignalGroup -> (thName 'DBundle.bundle, thName 'DBundle.unbundle) logicNm = logicName <> "_c" <> show ci - logicLam = lamE [tupP (map (snd . (inPats !!)) ins)] + -- A leading lazy unit keeps every real input out of 'bundle's + -- spine-forcing head slot ('bundle' lifts its first element with + -- 'fmap' / 'mapSignal#', which forces that element's spine), so + -- combinational feedback between value groups does not deadlock + -- simulation. + pureUnitE = varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] + -- Each value-input pattern is matched lazily (irrefutable), as the + -- bus-level plumbing already is. A strict value pattern (e.g. a + -- constructor pattern that destructures the sampled value at the + -- boundary) would force its input to produce ANY of the group's + -- outputs -- even outputs that don't use it -- which deadlocks when + -- that input depends, through the circuit, on such an output. + logicPat = case ins of + [] -> tupP [] + _ -> tupP (L noSrcSpanA (WildPat noExtField) : map (tildeP noSrcSpanA . snd . (inPats !!)) ins) + logicLam = lamE [logicPat] (letE noSrcSpanA (sigsForComp ci) (map (lets !!) ls) (tupE noSrcSpanA (map (snd . (outExprs !!)) outs))) logicBind = L loc $ patBind (varP noSrcSpanA logicNm) logicLam @@ -1282,9 +1297,8 @@ valueCircuitQQExpM = do outVarPs = map (\k -> let (L l _) = snd (outExprs !! k) in varP l (outPrefix <> show k)) outs bundled = case inVars of - [] -> varE noSrcSpanA (thName 'pure) `appE` tupE noSrcSpanA [] - [e] -> e - es -> varE noSrcSpanA bundleNm `appE` tupE noSrcSpanA es + [] -> pureUnitE + es -> varE noSrcSpanA bundleNm `appE` tupE noSrcSpanA (pureUnitE : es) lifted = varE noSrcSpanA (thName 'fmap) `appE` varE noSrcSpanA (var logicNm) `appE` bundled knotExpr = if length outs > 1 then varE noSrcSpanA unbundleNm `appE` lifted From 611c6e0583b76fa0af2056eefc1ca5a8d5e4269d Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Thu, 2 Jul 2026 10:36:16 +0100 Subject: [PATCH 14/21] Trim the value-level ports changelog entry Keep the summary and the breaking ExternalNames change; the marker semantics and multi-domain details live in the README and haddocks. Co-Authored-By: Claude Fable 5 --- CHANGELOG.md | 30 ++++-------------------------- 1 file changed, 4 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1f8aef6..2515b46 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,32 +12,10 @@ the bus type, which also drives type inference. See the README and example/ValueCircuits.hs. - A block can span several clock domains: the value-level bindings are - split into groups connected by shared variables and each group is lifted - with its own `fmap`/`bundle`/`unbundle`, so only buses whose values - actually meet must share a domain. Sharing a value across domains is - rejected by the type checker. Lets that don't touch value land stay at - the bus level, so let-bound sub-circuits can be used with `-<`. - - The value markers have distinct semantics: `SignalV x` asserts the - bus is a `Signal` (best inference — it works against fully generic - sub-circuits); `FwdV x` samples/drives the forward channel of any - signal-like bus via the new `SignalBus` class (`Signal`s, `Vec`s and - tuples of them, custom buses) but needs the bus type determined by - context; and `DSignalV x` is `SignalV` for delayed signals — the delay - index is part of the bus type, so a logic group's values must all sit at - the same pipeline depth, and its outputs are produced at that depth. - Mixing plain and delayed markers in one group is reported by the plugin. - - The value boundary is generated with the new `SigTag`, `FwdTag` and - `DSigTag` pattern synonyms (`Circuit` module); `SigTag`/`DSigTag` pin the - bus type so that type inference survives nested circuits (the `Fwd` - family is not injective) and "too shallow" `SignalV` markers report a - direct `Vec`-vs-`Signal` style mismatch. **Breaking**: `ExternalNames` - gained `signalTagName`, `fwdTagName` and `dSignalTagName` fields, so - custom plugins (e.g. clash-protocols style) need to supply them — - `defExternalNames` is now exported so they can be record updates of the - defaults. + **Breaking**: `ExternalNames` gained `signalTagName`, `fwdTagName` and + `dSignalTagName` fields, so custom plugins (e.g. clash-protocols style) + need to supply them — `defExternalNames` is now exported so they can be + record updates of the defaults. * Add a per-GHC `checks` output to the flake, so `nix flake check` (or `nix build .#checks..`) builds the package and runs all test suites against every supported GHC. The CI nix job now uses it. The From 58ff61d9e20602ffe36da8892bebe55225405529 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Thu, 2 Jul 2026 10:36:16 +0100 Subject: [PATCH 15/21] Extend SignalBus and supporting instances to 12-tuples SignalBus previously stopped at 3-tuples. Extend it (and the Fwd/Bwd, TrivialBwd and BusTagBundle instances it leans on) to 12-tuples, and exercise a tuple bus with an FwdV marker in the examples and tests. Co-Authored-By: Claude Fable 5 --- example/ValueCircuits.hs | 10 ++ src/Circuit.hs | 295 +++++++++++++++++++++++++++++++++++++-- tests/unittests.hs | 7 + 3 files changed, 303 insertions(+), 9 deletions(-) diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 6bfd5c7..5f2fc84 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -71,6 +71,16 @@ vecEmitC :: Circuit (Signal dom Int) (Vec 2 (Signal dom Int)) vecEmitC = circuit \(SignalV a) -> do idC -< FwdV (a :> (a + 1) :> Nil) +-- | A whole tuple of signal-like buses sampled as a single tuple of values +-- per cycle (via the 'SignalBus' instances for tuples, which go up to +-- 12-tuples). +tupleSampleC + :: Circuit + (Signal dom Int, Vec 2 (Signal dom Int), Signal dom Int, Signal dom Int) + (Signal dom Int) +tupleSampleC = circuit \(FwdV (a, v, b, c)) -> do + idC -< SignalV (a + sum v + b + c) + -- | @SignalV@ and @FwdV@ markers can meet in the same logic group. mixedMarkersC :: Circuit (Signal dom Int, Vec 2 (Signal dom Int)) (Signal dom Int) mixedMarkersC = circuit \(SignalV a, FwdV v) -> do diff --git a/src/Circuit.hs b/src/Circuit.hs index 3e14486..21323b8 100644 --- a/src/Circuit.hs +++ b/src/Circuit.hs @@ -74,6 +74,33 @@ type instance Bwd (a,b) = (Bwd a, Bwd b) type instance Fwd (a,b,c) = (Fwd a, Fwd b, Fwd c) type instance Bwd (a,b,c) = (Bwd a, Bwd b, Bwd c) +type instance Fwd (a,b,c,d) = (Fwd a, Fwd b, Fwd c, Fwd d) +type instance Bwd (a,b,c,d) = (Bwd a, Bwd b, Bwd c, Bwd d) + +type instance Fwd (a,b,c,d,e) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e) +type instance Bwd (a,b,c,d,e) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e) + +type instance Fwd (a,b,c,d,e,f) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f) +type instance Bwd (a,b,c,d,e,f) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f) + +type instance Fwd (a,b,c,d,e,f,g) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g) +type instance Bwd (a,b,c,d,e,f,g) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g) + +type instance Fwd (a,b,c,d,e,f,g,h) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g, Fwd h) +type instance Bwd (a,b,c,d,e,f,g,h) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g, Bwd h) + +type instance Fwd (a,b,c,d,e,f,g,h,i) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g, Fwd h, Fwd i) +type instance Bwd (a,b,c,d,e,f,g,h,i) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g, Bwd h, Bwd i) + +type instance Fwd (a,b,c,d,e,f,g,h,i,j) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g, Fwd h, Fwd i, Fwd j) +type instance Bwd (a,b,c,d,e,f,g,h,i,j) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g, Bwd h, Bwd i, Bwd j) + +type instance Fwd (a,b,c,d,e,f,g,h,i,j,k) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g, Fwd h, Fwd i, Fwd j, Fwd k) +type instance Bwd (a,b,c,d,e,f,g,h,i,j,k) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g, Bwd h, Bwd i, Bwd j, Bwd k) + +type instance Fwd (a,b,c,d,e,f,g,h,i,j,k,l) = (Fwd a, Fwd b, Fwd c, Fwd d, Fwd e, Fwd f, Fwd g, Fwd h, Fwd i, Fwd j, Fwd k, Fwd l) +type instance Bwd (a,b,c,d,e,f,g,h,i,j,k,l) = (Bwd a, Bwd b, Bwd c, Bwd d, Bwd e, Bwd f, Bwd g, Bwd h, Bwd i, Bwd j, Bwd k, Bwd l) + type instance Fwd (Signal dom a) = Signal dom a type instance Bwd (Signal dom a) = () @@ -143,6 +170,12 @@ instance (TrivialBwd a, TrivialBwd b, TrivialBwd c, TrivialBwd d, TrivialBwd e, instance (TrivialBwd a, TrivialBwd b, TrivialBwd c, TrivialBwd d, TrivialBwd e, TrivialBwd f, TrivialBwd g, TrivialBwd h, TrivialBwd i, TrivialBwd j) => TrivialBwd (a,b,c,d,e,f,g,h,i,j) where unitBwd = (unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd) +instance (TrivialBwd a, TrivialBwd b, TrivialBwd c, TrivialBwd d, TrivialBwd e, TrivialBwd f, TrivialBwd g, TrivialBwd h, TrivialBwd i, TrivialBwd j, TrivialBwd k) => TrivialBwd (a,b,c,d,e,f,g,h,i,j,k) where + unitBwd = (unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd) + +instance (TrivialBwd a, TrivialBwd b, TrivialBwd c, TrivialBwd d, TrivialBwd e, TrivialBwd f, TrivialBwd g, TrivialBwd h, TrivialBwd i, TrivialBwd j, TrivialBwd k, TrivialBwd l) => TrivialBwd (a,b,c,d,e,f,g,h,i,j,k,l) where + unitBwd = (unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd, unitBwd) + instance TrivialBwd a => TrivialBwd (BusTag t a) where unitBwd = BusTag unitBwd @@ -201,6 +234,16 @@ instance BusTagBundle (ta, tb, tc, td, te, tf, tg, th, ti, tj) (a, b, c, d, e, f taggedBundle (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j) = BusTag (a, b, c, d, e, f, g, h, i, j) taggedUnbundle (BusTag (a, b, c, d, e, f, g, h, i, j)) = (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j) +instance BusTagBundle (ta, tb, tc, td, te, tf, tg, th, ti, tj, tk) (a, b, c, d, e, f, g, h, i, j, k) where + type BusTagUnbundled (ta, tb, tc, td, te, tf, tg, th, ti, tj, tk) (a, b, c, d, e, f, g, h, i, j, k) = (BusTag ta a, BusTag tb b, BusTag tc c, BusTag td d, BusTag te e, BusTag tf f, BusTag tg g, BusTag th h, BusTag ti i, BusTag tj j, BusTag tk k) + taggedBundle (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j, BusTag k) = BusTag (a, b, c, d, e, f, g, h, i, j, k) + taggedUnbundle (BusTag (a, b, c, d, e, f, g, h, i, j, k)) = (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j, BusTag k) + +instance BusTagBundle (ta, tb, tc, td, te, tf, tg, th, ti, tj, tk, tl) (a, b, c, d, e, f, g, h, i, j, k, l) where + type BusTagUnbundled (ta, tb, tc, td, te, tf, tg, th, ti, tj, tk, tl) (a, b, c, d, e, f, g, h, i, j, k, l) = (BusTag ta a, BusTag tb b, BusTag tc c, BusTag td d, BusTag te e, BusTag tf f, BusTag tg g, BusTag th h, BusTag ti i, BusTag tj j, BusTag tk k, BusTag tl l) + taggedBundle (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j, BusTag k, BusTag l) = BusTag (a, b, c, d, e, f, g, h, i, j, k, l) + taggedUnbundle (BusTag (a, b, c, d, e, f, g, h, i, j, k, l)) = (BusTag a, BusTag b, BusTag c, BusTag d, BusTag e, BusTag f, BusTag g, BusTag h, BusTag i, BusTag j, BusTag k, BusTag l) + instance BusTagBundle (Vec n t) (Vec n a) where type BusTagUnbundled (Vec n t) (Vec n a) = Vec n (BusTag t a) taggedBundle = BusTag . fmap unBusTag @@ -264,10 +307,10 @@ instance (SignalBus a, SignalBus b, BusDom a ~ BusDom b) => SignalBus (a, b) whe sigFromBus (BusTag (fa, fb)) = bundle ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) , sigFromBus (BusTag fb :: BusTag b (Fwd b)) ) - sigToBus s = case unbundle s of - (sa, sb) -> BusTag - ( unBusTag (sigToBus sa :: BusTag a (Fwd a)) - , unBusTag (sigToBus sb :: BusTag b (Fwd b)) ) + sigToBus vs = case unbundle vs of + (va, vb) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) ) instance (SignalBus a, SignalBus b, SignalBus c, BusDom a ~ BusDom b, BusDom b ~ BusDom c) => SignalBus (a, b, c) where @@ -277,11 +320,245 @@ instance (SignalBus a, SignalBus b, SignalBus c, BusDom a ~ BusDom b, BusDom b ~ ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) , sigFromBus (BusTag fb :: BusTag b (Fwd b)) , sigFromBus (BusTag fc :: BusTag c (Fwd c)) ) - sigToBus s = case unbundle s of - (sa, sb, sc) -> BusTag - ( unBusTag (sigToBus sa :: BusTag a (Fwd a)) - , unBusTag (sigToBus sb :: BusTag b (Fwd b)) - , unBusTag (sigToBus sc :: BusTag c (Fwd c)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d ) + => SignalBus (a, b, c, d) where + type BusDom (a, b, c, d) = BusDom a + type SampleOf (a, b, c, d) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d) + sigFromBus (BusTag (fa, fb, fc, fd)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e ) + => SignalBus (a, b, c, d, e) where + type BusDom (a, b, c, d, e) = BusDom a + type SampleOf (a, b, c, d, e) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e) + sigFromBus (BusTag (fa, fb, fc, fd, fe)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f ) + => SignalBus (a, b, c, d, e, f) where + type BusDom (a, b, c, d, e, f) = BusDom a + type SampleOf (a, b, c, d, e, f) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g ) + => SignalBus (a, b, c, d, e, f, g) where + type BusDom (a, b, c, d, e, f, g) = BusDom a + type SampleOf (a, b, c, d, e, f, g) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g, SignalBus h + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g, BusDom g ~ BusDom h ) + => SignalBus (a, b, c, d, e, f, g, h) where + type BusDom (a, b, c, d, e, f, g, h) = BusDom a + type SampleOf (a, b, c, d, e, f, g, h) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g, SampleOf h) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg, fh)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) + , sigFromBus (BusTag fh :: BusTag h (Fwd h)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg, vh) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) + , unBusTag (sigToBus vh :: BusTag h (Fwd h)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g, SignalBus h, SignalBus i + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g, BusDom g ~ BusDom h, BusDom h ~ BusDom i ) + => SignalBus (a, b, c, d, e, f, g, h, i) where + type BusDom (a, b, c, d, e, f, g, h, i) = BusDom a + type SampleOf (a, b, c, d, e, f, g, h, i) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g, SampleOf h, SampleOf i) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg, fh, fi)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) + , sigFromBus (BusTag fh :: BusTag h (Fwd h)) + , sigFromBus (BusTag fi :: BusTag i (Fwd i)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg, vh, vi) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) + , unBusTag (sigToBus vh :: BusTag h (Fwd h)) + , unBusTag (sigToBus vi :: BusTag i (Fwd i)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g, SignalBus h, SignalBus i, SignalBus j + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g, BusDom g ~ BusDom h, BusDom h ~ BusDom i, BusDom i ~ BusDom j ) + => SignalBus (a, b, c, d, e, f, g, h, i, j) where + type BusDom (a, b, c, d, e, f, g, h, i, j) = BusDom a + type SampleOf (a, b, c, d, e, f, g, h, i, j) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g, SampleOf h, SampleOf i, SampleOf j) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg, fh, fi, fj)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) + , sigFromBus (BusTag fh :: BusTag h (Fwd h)) + , sigFromBus (BusTag fi :: BusTag i (Fwd i)) + , sigFromBus (BusTag fj :: BusTag j (Fwd j)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg, vh, vi, vj) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) + , unBusTag (sigToBus vh :: BusTag h (Fwd h)) + , unBusTag (sigToBus vi :: BusTag i (Fwd i)) + , unBusTag (sigToBus vj :: BusTag j (Fwd j)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g, SignalBus h, SignalBus i, SignalBus j, SignalBus k + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g, BusDom g ~ BusDom h, BusDom h ~ BusDom i, BusDom i ~ BusDom j, BusDom j ~ BusDom k ) + => SignalBus (a, b, c, d, e, f, g, h, i, j, k) where + type BusDom (a, b, c, d, e, f, g, h, i, j, k) = BusDom a + type SampleOf (a, b, c, d, e, f, g, h, i, j, k) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g, SampleOf h, SampleOf i, SampleOf j, SampleOf k) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg, fh, fi, fj, fk)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) + , sigFromBus (BusTag fh :: BusTag h (Fwd h)) + , sigFromBus (BusTag fi :: BusTag i (Fwd i)) + , sigFromBus (BusTag fj :: BusTag j (Fwd j)) + , sigFromBus (BusTag fk :: BusTag k (Fwd k)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg, vh, vi, vj, vk) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) + , unBusTag (sigToBus vh :: BusTag h (Fwd h)) + , unBusTag (sigToBus vi :: BusTag i (Fwd i)) + , unBusTag (sigToBus vj :: BusTag j (Fwd j)) + , unBusTag (sigToBus vk :: BusTag k (Fwd k)) ) + +instance + ( SignalBus a, SignalBus b, SignalBus c, SignalBus d, SignalBus e, SignalBus f, SignalBus g, SignalBus h, SignalBus i, SignalBus j, SignalBus k, SignalBus l + , BusDom a ~ BusDom b, BusDom b ~ BusDom c, BusDom c ~ BusDom d, BusDom d ~ BusDom e, BusDom e ~ BusDom f, BusDom f ~ BusDom g, BusDom g ~ BusDom h, BusDom h ~ BusDom i, BusDom i ~ BusDom j, BusDom j ~ BusDom k, BusDom k ~ BusDom l ) + => SignalBus (a, b, c, d, e, f, g, h, i, j, k, l) where + type BusDom (a, b, c, d, e, f, g, h, i, j, k, l) = BusDom a + type SampleOf (a, b, c, d, e, f, g, h, i, j, k, l) = (SampleOf a, SampleOf b, SampleOf c, SampleOf d, SampleOf e, SampleOf f, SampleOf g, SampleOf h, SampleOf i, SampleOf j, SampleOf k, SampleOf l) + sigFromBus (BusTag (fa, fb, fc, fd, fe, ff, fg, fh, fi, fj, fk, fl)) = bundle + ( sigFromBus (BusTag fa :: BusTag a (Fwd a)) + , sigFromBus (BusTag fb :: BusTag b (Fwd b)) + , sigFromBus (BusTag fc :: BusTag c (Fwd c)) + , sigFromBus (BusTag fd :: BusTag d (Fwd d)) + , sigFromBus (BusTag fe :: BusTag e (Fwd e)) + , sigFromBus (BusTag ff :: BusTag f (Fwd f)) + , sigFromBus (BusTag fg :: BusTag g (Fwd g)) + , sigFromBus (BusTag fh :: BusTag h (Fwd h)) + , sigFromBus (BusTag fi :: BusTag i (Fwd i)) + , sigFromBus (BusTag fj :: BusTag j (Fwd j)) + , sigFromBus (BusTag fk :: BusTag k (Fwd k)) + , sigFromBus (BusTag fl :: BusTag l (Fwd l)) ) + sigToBus vs = case unbundle vs of + (va, vb, vc, vd, ve, vf, vg, vh, vi, vj, vk, vl) -> BusTag + ( unBusTag (sigToBus va :: BusTag a (Fwd a)) + , unBusTag (sigToBus vb :: BusTag b (Fwd b)) + , unBusTag (sigToBus vc :: BusTag c (Fwd c)) + , unBusTag (sigToBus vd :: BusTag d (Fwd d)) + , unBusTag (sigToBus ve :: BusTag e (Fwd e)) + , unBusTag (sigToBus vf :: BusTag f (Fwd f)) + , unBusTag (sigToBus vg :: BusTag g (Fwd g)) + , unBusTag (sigToBus vh :: BusTag h (Fwd h)) + , unBusTag (sigToBus vi :: BusTag i (Fwd i)) + , unBusTag (sigToBus vj :: BusTag j (Fwd j)) + , unBusTag (sigToBus vk :: BusTag k (Fwd k)) + , unBusTag (sigToBus vl :: BusTag l (Fwd l)) ) -- | Like 'SigTag' but for any signal-like bus. Used by the plugin for @Fwd@ -- markers at the value boundary of @circuit@ blocks. Unlike 'SigTag' it diff --git a/tests/unittests.hs b/tests/unittests.hs index 2f2c133..3d84ae1 100644 --- a/tests/unittests.hs +++ b/tests/unittests.hs @@ -47,6 +47,13 @@ main = do [11, 22, 33, 44, 55] , check "vecEmitC" (fmap sample5 (simulateC vecEmitC (fromList [0 ..]))) ([0, 1, 2, 3, 4] :> [1, 2, 3, 4, 5] :> Nil) + , check "tupleSampleC" + (sample5 (simulateC tupleSampleC + ( fromList [1 ..] + , fromList [10, 20 ..] :> fromList [100, 200 ..] :> Nil + , fromList [1000, 2000 ..] + , fromList [10000, 20000 ..] ))) + [11111, 22222, 33333, 44444, 55555] , check "mixedMarkersC" (sample5 (simulateC mixedMarkersC (fromList [100, 200 ..], fromList [1 ..] :> fromList [10, 20 ..] :> Nil))) [111, 222, 333, 444, 555] From 17d343647fc4c1b0854837fdcb4717cbd70595dd Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Thu, 2 Jul 2026 10:36:36 +0100 Subject: [PATCH 16/21] Blame whole-bundle type errors on the ports' span Generated tuple patterns and expressions had no source location, so a type error on a whole bundle -- e.g. a cross-domain mismatch discovered while checking the slave pattern of a value circuit -- fell back to the head of the circuit expression. Give them the combined span of the ports they bundle, so the error points at the pattern that introduces the offending ports. The CrossDomainError fixture now puts its markers on a different line than the circuit keyword to pin this down. Co-Authored-By: Claude Fable 5 --- CHANGELOG.md | 5 ++- src/CircuitNotation.hs | 50 +++++++++++++++++++++--------- tests/fixtures/CrossDomainError.hs | 13 ++++---- 3 files changed, 47 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2515b46..e504990 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,7 +25,10 @@ * Fix the source location of type errors on a bus. Since bus tagging was introduced, such errors pointed at the end of the `circuit` block rather than at the offending statement. Generated bindings are now located at their - circuit expression so GHC blames the right line. + circuit expression so GHC blames the right line. Generated bundle patterns + and expressions also take the span of the ports they bundle, so + whole-bundle errors (e.g. sharing a value-level variable across clock + domains) are blamed on the ports rather than on the head of the circuit. ## 0.2.0.0 -- 2026-04-23 diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index b5d1069..134686b 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -381,9 +381,9 @@ noLoc :: e -> GenLocated (SrcAnn ann) e noLoc = noEpAnn . GHC.noLoc #endif -tupP :: p ~ GhcPs => [LPat p] -> LPat p -tupP [pat] = pat -tupP pats = noLoc $ TuplePat noExt pats GHC.Boxed +tupP :: p ~ GhcPs => SrcSpanAnnA -> [LPat p] -> LPat p +tupP _ [pat] = pat +tupP loc pats = L loc $ TuplePat noExt pats GHC.Boxed vecP :: (?nms :: ExternalNames) => SrcSpanAnnA -> [LPat GhcPs] -> LPat GhcPs vecP srcLoc = \case @@ -823,10 +823,30 @@ checkCircuit = do data Direction = Fwd | Bwd deriving Show +-- | Best-effort source span of a port description: the combination of the +-- spans of everything in it. Generated tuple patterns and expressions take +-- this span so that type errors on a whole bus (e.g. a clock domain +-- mismatch between the ports of one bundle) point at the offending ports +-- rather than at the head of the @circuit@ block. +portDescLoc :: PortDescription PortName -> SrcSpan +portDescLoc = \case + Tuple ps -> foldr (combineSrcSpans . portDescLoc) noSrcSpan ps + Vec s _ -> locA s + Ref (PortName s _) -> locA s + RefMulticast (PortName s _) -> locA s + Lazy s _ -> locA s + FwdExpr _ (L s _) -> locA s + FwdPat _ (L s _) -> locA s + SigTagExpr _ (L s _) -> locA s + SigTagPat _ (L s _) -> locA s + PortType _ p -> portDescLoc p + PortErr s _ -> locA s + bindWithSuffix :: (p ~ GhcPs, ?nms :: ExternalNames) => GHC.DynFlags -> Direction -> PortDescription PortName -> LPat p bindWithSuffix dflags dir = \case - Tuple ps -> tildeP noSrcSpanA $ taggedBundleP $ tupP $ fmap (bindWithSuffix dflags dir) ps - Vec s ps -> taggedBundleP $ vecP s $ fmap (bindWithSuffix dflags dir) ps + p@(Tuple ps) -> let loc = noAnnSrcSpan (portDescLoc p) + in tildeP loc $ taggedBundleP loc $ tupP loc $ fmap (bindWithSuffix dflags dir) ps + Vec s ps -> taggedBundleP s $ vecP s $ fmap (bindWithSuffix dflags dir) ps Ref (PortName loc fs) -> varP loc (GHC.unpackFS fs <> "_" <> show dir) RefMulticast (PortName loc fs) -> case dir of Bwd -> L loc (WildPat noExtField) @@ -862,8 +882,9 @@ bindOutputs dflags direc slaves masters = noLoc $ conPatIn (noLoc (fwdBwdCon ?nm expWithSuffix :: (p ~ GhcPs, ?nms :: ExternalNames) => Direction -> PortDescription PortName -> LHsExpr p expWithSuffix dir = \case - Tuple ps -> taggedBundleE $ tupE noSrcSpanA $ fmap (expWithSuffix dir) ps - Vec s ps -> taggedBundleE $ vecE s $ fmap (expWithSuffix dir) ps + p@(Tuple ps) -> let loc = noAnnSrcSpan (portDescLoc p) + in taggedBundleE loc $ tupE loc $ fmap (expWithSuffix dir) ps + Vec s ps -> taggedBundleE s $ vecE s $ fmap (expWithSuffix dir) ps Ref (PortName loc fs) -> varE loc (var $ GHC.unpackFS fs <> "_" <> show dir) RefMulticast (PortName loc fs) -> case dir of Bwd -> varE noSrcSpanA (trivialBwd ?nms) @@ -930,11 +951,11 @@ runCircuitFun loc = varE loc (runCircuitName ?nms) prefixCon :: [arg] -> HsConDetails tyarg arg rec prefixCon a = PrefixCon [] a -taggedBundleP :: (p ~ GhcPs, ?nms :: ExternalNames) => LPat p -> LPat p -taggedBundleP a = noLoc (conPatIn (noLoc (tagBundlePat ?nms)) (prefixCon [a])) +taggedBundleP :: (p ~ GhcPs, ?nms :: ExternalNames) => SrcSpanAnnA -> LPat p -> LPat p +taggedBundleP loc a = L loc (conPatIn (noLoc (tagBundlePat ?nms)) (prefixCon [a])) -taggedBundleE :: (p ~ GhcPs, ?nms :: ExternalNames) => LHsExpr p -> LHsExpr p -taggedBundleE a = varE noSrcSpanA (tagBundlePat ?nms) `appE` a +taggedBundleE :: (p ~ GhcPs, ?nms :: ExternalNames) => SrcSpanAnnA -> LHsExpr p -> LHsExpr p +taggedBundleE loc a = varE loc (tagBundlePat ?nms) `appE` a tagP :: (p ~ GhcPs, ?nms :: ExternalNames) => LPat p -> LPat p tagP a = noLoc (conPatIn (noLoc (tagName ?nms)) (prefixCon [a])) @@ -1286,8 +1307,8 @@ valueCircuitQQExpM = do -- outputs -- even outputs that don't use it -- which deadlocks when -- that input depends, through the circuit, on such an output. logicPat = case ins of - [] -> tupP [] - _ -> tupP (L noSrcSpanA (WildPat noExtField) : map (tildeP noSrcSpanA . snd . (inPats !!)) ins) + [] -> tupP noSrcSpanA [] + _ -> tupP noSrcSpanA (L noSrcSpanA (WildPat noExtField) : map (tildeP noSrcSpanA . snd . (inPats !!)) ins) logicLam = lamE [logicPat] (letE noSrcSpanA (sigsForComp ci) (map (lets !!) ls) (tupE noSrcSpanA (map (snd . (outExprs !!)) outs))) @@ -1303,7 +1324,8 @@ valueCircuitQQExpM = do knotExpr = if length outs > 1 then varE noSrcSpanA unbundleNm `appE` lifted else lifted - knotBind = L loc $ patBind (tupP outVarPs) knotExpr + outsLoc = noAnnSrcSpan (foldr (combineSrcSpans . getLocA) noSrcSpan outVarPs) + knotBind = L loc $ patBind (tupP outsLoc outVarPs) knotExpr in if null outs then [] else [logicBind, knotBind] compDecs = concat (zipWith3 mkComp [0 ..] flavors innerGroups) diff --git a/tests/fixtures/CrossDomainError.hs b/tests/fixtures/CrossDomainError.hs index 207ad36..f28d8d0 100644 --- a/tests/fixtures/CrossDomainError.hs +++ b/tests/fixtures/CrossDomainError.hs @@ -9,9 +9,9 @@ -- a @domB@ bus, which is an (unsynchronized) clock domain crossing. The -- shared variables put both buses in the same logic group, whose @bundle@ -- demands a single domain, so GHC reports @Couldn't match type domA with --- domB@. The blame lands on the head of the circuit (the constraint solver --- unifies the domains via the generated bundle before it checks the slave --- pattern), so the marker sits on the @circuit@ line. +-- domB@. The generated slave pattern takes the span of its ports, so the +-- blame lands on the lambda pattern introducing @a@ and @b@ — which is on +-- a different line than the @circuit@ keyword here, to pin that down. module CrossDomainError where import Circuit @@ -22,6 +22,7 @@ registerC :: a -> Circuit (Signal dom a) (Signal dom a) registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) crossDomainError :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int) -crossDomainError = circuit \(SignalV a, SignalV b) -> do -- cross-domain-error-marker - SignalV acc <- registerC 0 -< SignalV (acc + a + b) - idC -< SignalV acc +crossDomainError = circuit + \(SignalV a, SignalV b) -> do -- cross-domain-error-marker + SignalV acc <- registerC 0 -< SignalV (acc + a + b) + idC -< SignalV acc From ff4075d0baabf244d600d0bd69dd1d28300768f6 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Sat, 11 Jul 2026 10:16:27 +0100 Subject: [PATCH 17/21] Add write-ghc-environment-files to cabal.project So that a plain `cabal build && cabal test` drops a .ghc.environment file, letting the error-location test's bare `ghc` find the circuit-notation plugin without the CI-only --write-ghc-environment-files flag. Addresses review feedback from @rowanG077 on #36. Co-Authored-By: Claude Opus 4.8 (1M context) --- cabal.project | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cabal.project b/cabal.project index b764c34..facc4ac 100644 --- a/cabal.project +++ b/cabal.project @@ -1,2 +1,7 @@ packages: . +-- So that a plain `cabal build && cabal test` drops a .ghc.environment file, +-- letting the error-location test's bare `ghc` find the circuit-notation +-- plugin (the same mechanism CI uses to compile the Example module). +write-ghc-environment-files: always + From d69c3008492ae1fc24108b6d5b2ca90ce5fabc0f Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Sat, 11 Jul 2026 10:16:38 +0100 Subject: [PATCH 18/21] Use register instead of Signal internals in error fixtures The ValueExprError and CrossDomainError fixtures defined a local register circuit via Clash.Signal.Internal's (:-). Use the public `register` instead, as suggested by @rowanG077 on #36. The deliberate errors still land on their marked lines (checked by the error-location test). Co-Authored-By: Claude Opus 4.8 (1M context) --- tests/fixtures/CrossDomainError.hs | 7 ++++--- tests/fixtures/ValueExprError.hs | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/tests/fixtures/CrossDomainError.hs b/tests/fixtures/CrossDomainError.hs index f28d8d0..43a4988 100644 --- a/tests/fixtures/CrossDomainError.hs +++ b/tests/fixtures/CrossDomainError.hs @@ -16,10 +16,11 @@ module CrossDomainError where import Circuit import Clash.Prelude -import Clash.Signal.Internal (Signal ((:-))) -registerC :: a -> Circuit (Signal dom a) (Signal dom a) -registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) +registerC + :: (HiddenClockResetEnable dom, NFDataX a) + => a -> Circuit (Signal dom a) (Signal dom a) +registerC a = Circuit $ \(s :-> ()) -> (() :-> register a s) crossDomainError :: Circuit (Signal domA Int, Signal domB Int) (Signal domA Int) crossDomainError = circuit diff --git a/tests/fixtures/ValueExprError.hs b/tests/fixtures/ValueExprError.hs index eb8f5ed..45d39a1 100644 --- a/tests/fixtures/ValueExprError.hs +++ b/tests/fixtures/ValueExprError.hs @@ -14,10 +14,11 @@ module ValueExprError where import Circuit import Clash.Prelude -import Clash.Signal.Internal (Signal ((:-))) -registerC :: a -> Circuit (Signal dom a) (Signal dom a) -registerC a = Circuit $ \(s :-> ()) -> (() :-> (a :- s)) +registerC + :: (HiddenClockResetEnable dom, NFDataX a) + => a -> Circuit (Signal dom a) (Signal dom a) +registerC a = Circuit $ \(s :-> ()) -> (() :-> register a s) valueExprError :: Circuit (Signal dom Int) (Signal dom Int) valueExprError = circuit \(SignalV a) -> do From 231cf5682dca7c99deca35ea5f95e46a00c0fbce Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Sat, 11 Jul 2026 10:17:04 +0100 Subject: [PATCH 19/21] Refine value ports: dead groups, let pragmas, as-patterns Three fixes from @rowanG077's review of #36: * Type-check value groups with no outputs. Previously a value group that produced no output (e.g. an unused `let bad = not a`) was dropped entirely, so a broken circuit compiled silently. The group's logic is now still bound (to a wildcard) so its expressions are type-checked; with nothing downstream to pin the value, the mismatch surfaces where the input value enters the circuit. Regression: tests/fixtures/DeadLetError.hs. * Move INLINE/NOINLINE pragmas and fixity declarations with a value-level `let` when it is relocated into a group's generated logic function. Previously only type signatures were routed to the group, so a local pragma was orphaned in the outer let and GHC rejected it as "lacks an accompanying binding". Example: localLetPragmas in ValueCircuits.hs. * Support as-patterns on value markers: `SignalV p@(a, b)` now binds `p` as well as `a` and `b` (patVarNames collects the as-pattern binder). Example: valueAsPattern in ValueCircuits.hs. Co-Authored-By: Claude Opus 4.8 (1M context) --- example/ValueCircuits.hs | 22 +++++++++++++++++++ src/CircuitNotation.hs | 39 +++++++++++++++++++++++++++------- tests/error-location.hs | 4 ++++ tests/fixtures/DeadLetError.hs | 23 ++++++++++++++++++++ 4 files changed, 80 insertions(+), 8 deletions(-) create mode 100644 tests/fixtures/DeadLetError.hs diff --git a/example/ValueCircuits.hs b/example/ValueCircuits.hs index 5f2fc84..2b50944 100644 --- a/example/ValueCircuits.hs +++ b/example/ValueCircuits.hs @@ -335,6 +335,28 @@ busLevelLet = circuit \(SignalV x) -> do SignalV y <- inc -< SignalV (x + 1) idC -< SignalV (y * 2) +-- | A value-level @let@ may carry pragmas and fixity declarations. When the +-- binding moves into the group's generated logic function, its @INLINE@ +-- pragma and fixity declaration move with it (rather than being orphaned in +-- the outer let, which GHC would reject as \"lacks an accompanying binding\"). +localLetPragmas :: Circuit (Signal dom Int) (Signal dom Int) +localLetPragmas = circuit \(SignalV a) -> do + let + {-# INLINE inc #-} + inc :: Int -> Int + inc x = x + 1 + + infixl 6 .+. + (.+.) :: Int -> Int -> Int + x .+. y = x + y + idC -< SignalV (inc a .+. 1) + +-- | An as-pattern on a value marker binds both the whole value and its +-- components: @p\@(a, b)@ makes @p@, @a@ and @b@ all available. +valueAsPattern :: Circuit (Signal dom (Int, Int)) (Signal dom Int) +valueAsPattern = circuit \(SignalV p@(a, b)) -> do + idC -< SignalV (fst p + a + b) + -- Nesting --------------------------------------------------------------- -- | A value-level circuit used as a sub-circuit inside a bus-level one. diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 134686b..1999f2f 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -1247,11 +1247,24 @@ valueCircuitQQExpM = do sigComp (L _ rdr) = case unqualName rdr of [n] -> Map.lookup n nameComp _ -> Nothing + -- split a sig carrying a list of names into one sig per component, + -- rebuilding it with just the names that belong to that component + splitByNames l rebuild ids = + [ (c, L l (rebuild ids')) + | (c, ids') <- Map.toList (Map.fromListWith (flip (<>)) [ (sigComp i, [i]) | i <- ids ]) ] + -- Route each let signature to the group that binds its name(s), so that + -- not just type signatures but also INLINE/NOINLINE pragmas and fixity + -- declarations follow their binding when it moves into a group's inner + -- let (otherwise GHC complains the pragma "lacks an accompanying + -- binding"). Sigs on names that stay in the outer let route to 'Nothing'. splitSigs = concatMap (\lsig@(L l s) -> case s of TypeSig x ids ty -> - [ (c, L l (TypeSig x ids' ty)) - | (c, ids') <- Map.toList (Map.fromListWith (flip (<>)) [ (sigComp i, [i]) | i <- ids ]) ] + splitByNames l (\ids' -> TypeSig x ids' ty) ids + FixSig x (FixitySig xf ids fx) -> + splitByNames l (\ids' -> FixSig x (FixitySig xf ids' fx)) ids + InlineSig x nm prag -> + [(sigComp nm, L l (InlineSig x nm prag))] _ -> [(Nothing, lsig)]) letTypes sigsForComp ci = [ s | (Just ci', s) <- splitSigs, ci' == ci ] @@ -1284,8 +1297,8 @@ valueCircuitQQExpM = do -- @pure ()@. The generated bundle elements and knot patterns take the -- source locations of the original markers, so clock domain (and -- delay) mismatches are reported on the offending marker. Groups with - -- no outputs produce no value (their logic would be dead) and generate - -- nothing. + -- no outputs tie nothing back, but their logic is still bound (to a + -- wildcard) so the dead group's expressions are typechecked. let mkComp ci flavor (its, _) = let ins = sort [ i | ItemIn i <- its ] outs = sort [ k | ItemOut k <- its ] @@ -1326,7 +1339,15 @@ valueCircuitQQExpM = do else lifted outsLoc = noAnnSrcSpan (foldr (combineSrcSpans . getLocA) noSrcSpan outVarPs) knotBind = L loc $ patBind (tupP outsLoc outVarPs) knotExpr - in if null outs then [] else [logicBind, knotBind] + -- A group with no outputs still has its logic typechecked: bind the + -- lifted result to a wildcard so the input buses pin the value + -- types (otherwise the group's lets and expressions -- e.g. an + -- unused @let bad = not a@ -- would never be checked and a broken + -- circuit would compile). 'lifted' already applies the logic + -- function to the bundled inputs, so the mismatch is blamed on the + -- offending expression. + deadBind = L loc $ patBind (L noSrcSpanA (WildPat noExtField)) lifted + in if null outs then [logicBind, deadBind] else [logicBind, knotBind] compDecs = concat (zipWith3 mkComp [0 ..] flavors innerGroups) @@ -1380,14 +1401,16 @@ unqualName = \case GHC.Unqual occ -> [OccName.occNameString occ] _ -> [] --- | Variable names bound by a pattern (conservative, syntactic; as-pattern --- names are not collected). +-- | Variable names bound by a pattern (conservative, syntactic). Both plain +-- variable patterns and the binder of an as-pattern (@p\@(a, b)@ binds @p@ as +-- well as @a@ and @b@) are collected. patVarNames :: LPat GhcPs -> [String] patVarNames = SYB.everything (<>) (SYB.mkQ [] q) where q :: Pat GhcPs -> [String] q = \case - VarPat _ (L _ rdr) -> unqualName rdr + VarPat _ (L _ rdr) -> unqualName rdr + AsPat _ (L _ rdr) _ -> unqualName rdr _ -> [] -- | All unqualified variable occurrences: a conservative over-approximation diff --git a/tests/error-location.hs b/tests/error-location.hs index 26c4671..5974f05 100644 --- a/tests/error-location.hs +++ b/tests/error-location.hs @@ -63,6 +63,10 @@ fixtures = -- the plugin itself, at the offending marker , Fixture ("tests" "fixtures" "MixedMarkerError.hs") "mixed-marker-error-marker" (Just "mixes DSignalV with SignalV/FwdV") + -- an unused value-level let (a group with no outputs) is still + -- typechecked; the mismatch surfaces where the input value enters + , Fixture ("tests" "fixtures" "DeadLetError.hs") "dead-let-error-marker" + (Just "Couldn't match type") ] main :: IO () diff --git a/tests/fixtures/DeadLetError.hs b/tests/fixtures/DeadLetError.hs new file mode 100644 index 0000000..84bbd5a --- /dev/null +++ b/tests/fixtures/DeadLetError.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS -fplugin=CircuitNotation #-} + +-- | A fixture where a value-level @let@ in a @circuit@ block is never used as +-- an output: @bad = not a@ where @a@ is an 'Int' sampled off the input bus. +-- Such a value group has no outputs, so its logic used to be dropped entirely +-- and the broken @let@ was silently accepted. Its logic is now still bound (to +-- a wildcard) so the group is typechecked; with nothing downstream to pin @a@, +-- the @Int@-vs-@Bool@ mismatch surfaces where the input value enters the +-- circuit (the @SignalV a@ marker), rather than being accepted. +module DeadLetError where + +import Circuit +import Clash.Prelude +import qualified Prelude as P + +deadLetError :: Circuit (Signal dom Int) (Signal dom Bool) +deadLetError = circuit \(SignalV a) -> do -- dead-let-error-marker + let bad = P.not a + idC -< SignalV True From 34d8e8004e72d7bf8de57e7afb03df65e0179b21 Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Sat, 11 Jul 2026 11:12:25 +0100 Subject: [PATCH 20/21] Fix AsPat arity for GHC < 9.12 AsPat carries a separate `@`-token field on GHC 9.4-9.10 (4 fields) that 9.12 folded into its extension field (3 fields). CPP-guard the pattern so the as-pattern support builds on all supported GHCs, not just 9.12. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/CircuitNotation.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index 1999f2f..e5dc06b 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -1409,8 +1409,13 @@ patVarNames = SYB.everything (<>) (SYB.mkQ [] q) where q :: Pat GhcPs -> [String] q = \case - VarPat _ (L _ rdr) -> unqualName rdr + VarPat _ (L _ rdr) -> unqualName rdr +-- GHC 9.12 folded the @\@@ token into AsPat's extension field, dropping a field. +#if __GLASGOW_HASKELL__ >= 912 AsPat _ (L _ rdr) _ -> unqualName rdr +#else + AsPat _ (L _ rdr) _ _ -> unqualName rdr +#endif _ -> [] -- | All unqualified variable occurrences: a conservative over-approximation From 89d84d0c1d4195af033a307037031ebfcdc6377d Mon Sep 17 00:00:00 2001 From: Christopher Chalmers Date: Sat, 11 Jul 2026 23:41:47 +0100 Subject: [PATCH 21/21] Correct AsPat arity boundary to GHC 9.10 The `@`-token field was dropped from AsPat in GHC 9.10, not 9.12 as the previous fix assumed (9.10.3 then failed with the 4-field pattern). Guard on `>= 910`. Verified by building and running the test suites on all four supported GHCs (9.6.7, 9.8.4, 9.10.3, 9.12.4) via the flake. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/CircuitNotation.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/CircuitNotation.hs b/src/CircuitNotation.hs index e5dc06b..51ecaa8 100644 --- a/src/CircuitNotation.hs +++ b/src/CircuitNotation.hs @@ -1410,8 +1410,8 @@ patVarNames = SYB.everything (<>) (SYB.mkQ [] q) q :: Pat GhcPs -> [String] q = \case VarPat _ (L _ rdr) -> unqualName rdr --- GHC 9.12 folded the @\@@ token into AsPat's extension field, dropping a field. -#if __GLASGOW_HASKELL__ >= 912 +-- GHC 9.10 folded the @\@@ token into AsPat's extension field, dropping a field. +#if __GLASGOW_HASKELL__ >= 910 AsPat _ (L _ rdr) _ -> unqualName rdr #else AsPat _ (L _ rdr) _ _ -> unqualName rdr