From 4f156a0bb8210d15fcabe0a6922521f866a07d50 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 20 Jan 2025 06:58:20 -0500 Subject: [PATCH 1/2] Allow multiple triggers with the same name. Refs #30. `copilot-c99-4.2` (part of the overall Copilot 4.2 release) now allows multiple triggers with the same handler, provided that the triggers always have the same type signatures. See https://github.com/Copilot-Language/copilot/issues/296 (as well as the fix in https://github.com/Copilot-Language/copilot/pull/572). Since `copilot-bluespec` wishes to achieve feature parity with `copilot-c99`, we would like to add this ability to `copilot-bluespec` as well. This commit adds multiple triggers support for `copilot-bluespec`, piggybacking off of the implementation in https://github.com/Copilot-Language/copilot/pull/572. --- copilot-bluespec.cabal | 1 + src/Copilot/Compile/Bluespec/CodeGen.hs | 13 ++-- src/Copilot/Compile/Bluespec/Compile.hs | 78 +++++++++++++++---- .../Compile/Bluespec/Representation.hs | 22 ++++++ 4 files changed, 96 insertions(+), 18 deletions(-) create mode 100644 src/Copilot/Compile/Bluespec/Representation.hs diff --git a/copilot-bluespec.cabal b/copilot-bluespec.cabal index 8b5d5c7..1a6369e 100644 --- a/copilot-bluespec.cabal +++ b/copilot-bluespec.cabal @@ -56,6 +56,7 @@ library , Copilot.Compile.Bluespec.External , Copilot.Compile.Bluespec.FloatingPoint , Copilot.Compile.Bluespec.Name + , Copilot.Compile.Bluespec.Representation , Copilot.Compile.Bluespec.Settings , Copilot.Compile.Bluespec.Type diff --git a/src/Copilot/Compile/Bluespec/CodeGen.hs b/src/Copilot/Compile/Bluespec/CodeGen.hs index 7a382ed..6d9fde0 100644 --- a/src/Copilot/Compile/Bluespec/CodeGen.hs +++ b/src/Copilot/Compile/Bluespec/CodeGen.hs @@ -35,6 +35,7 @@ import Copilot.Core import Copilot.Compile.Bluespec.Expr import Copilot.Compile.Bluespec.External import Copilot.Compile.Bluespec.Name +import Copilot.Compile.Bluespec.Representation import Copilot.Compile.Bluespec.Type -- | Write a generator function for a stream. @@ -151,22 +152,24 @@ mkSpecIfcFields triggers exts = mkField name $ tReg `BS.TAp` transType ty -- | Define a rule for a trigger function. -mkTriggerRule :: Trigger -> BS.CRule -mkTriggerRule (Trigger name _ args) = +mkTriggerRule :: UniqueTrigger -> BS.CRule +mkTriggerRule (UniqueTrigger uniqueName (Trigger name _ args)) = BS.CRule [] - (Just $ cLit $ BS.LString name) + (Just $ cLit $ BS.LString uniqueName) [ BS.CQFilter $ BS.CVar $ BS.mkId BS.NoPos $ - fromString $ guardName name + fromString $ guardName uniqueName ] (BS.CApply nameExpr args') where ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + -- Note that we use 'name' here instead of 'uniqueName', as 'name' is the + -- name of the actual external function. nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name nameExpr = BS.CSelect (BS.CVar ifcArgId) nameId - args' = take (length args) (map argCall (argNames name)) + args' = take (length args) (map argCall (argNames uniqueName)) argCall = BS.CVar . BS.mkId BS.NoPos . fromString -- | Writes the @step@ rule that updates all streams. diff --git a/src/Copilot/Compile/Bluespec/Compile.hs b/src/Copilot/Compile/Bluespec/Compile.hs index d4a14ac..c4701ea 100644 --- a/src/Copilot/Compile/Bluespec/Compile.hs +++ b/src/Copilot/Compile/Bluespec/Compile.hs @@ -8,9 +8,10 @@ module Copilot.Compile.Bluespec.Compile ) where -- External imports -import Data.List (nub, union) +import Data.List (nub, nubBy, union) import Data.Maybe (catMaybes, maybeToList) import Data.String (IsString (..)) +import Data.Type.Equality (testEquality, (:~:)(Refl)) import Data.Typeable (Typeable) import qualified Language.Bluespec.Classic.AST as BS import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS @@ -29,6 +30,7 @@ import Copilot.Compile.Bluespec.CodeGen import Copilot.Compile.Bluespec.External import Copilot.Compile.Bluespec.FloatingPoint import Copilot.Compile.Bluespec.Name +import Copilot.Compile.Bluespec.Representation import Copilot.Compile.Bluespec.Settings -- | Compile a specification to a Bluespec file. @@ -39,12 +41,20 @@ import Copilot.Compile.Bluespec.Settings -- that are generated. compileWith :: BluespecSettings -> String -> Spec -> IO () compileWith bsSettings prefix spec - | null (specTriggers spec) + | null triggers = do hPutStrLn stderr $ "Copilot error: attempt at compiling empty specification.\n" ++ "You must define at least one trigger to generate Bluespec monitors." exitFailure + | incompatibleTriggers triggers + = do hPutStrLn stderr $ + "Copilot error: attempt at compiling specification with conflicting " + ++ "trigger definitions.\n" + ++ "Multiple triggers have the same name, but different argument " + ++ "types.\n" + exitFailure + | otherwise = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec ifcBsFile = render $ pPrint $ compileIfcBS bsSettings prefix spec @@ -57,6 +67,24 @@ compileWith bsSettings prefix spec writeFile (dir "bs_fp.c") copilotBluespecFloatingPointC writeFile (dir "BluespecFP.bsv") copilotBluespecFloatingPointBSV writeFile (dir prefix ++ ".bs") bsFile + where + triggers = specTriggers spec + + -- Check that two triggers do no conflict, that is: if their names are + -- equal, the types of their arguments should be equal as well. + incompatibleTriggers :: [Trigger] -> Bool + incompatibleTriggers = pairwiseAny conflict + where + conflict :: Trigger -> Trigger -> Bool + conflict t1@(Trigger name1 _ _) t2@(Trigger name2 _ _) = + name1 == name2 && not (compareTrigger t1 t2) + + -- True if the function holds for any pair of elements. We assume that + -- the function is commutative. + pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool + pairwiseAny _ [] = False + pairwiseAny _ (_:[]) = False + pairwiseAny f (x:xs) = any (f x) xs || pairwiseAny f xs -- | Compile a specification to a Bluespec. -- @@ -136,11 +164,12 @@ compileBS _bsSettings prefix spec = ifcModId = BS.mkId BS.NoPos "ifcMod" rules :: [BS.CRule] - rules = map mkTriggerRule triggers ++ maybeToList (mkStepRule streams) + rules = map mkTriggerRule uniqueTriggers ++ maybeToList (mkStepRule streams) - streams = specStreams spec - triggers = specTriggers spec - exts = gatherExts streams triggers + streams = specStreams spec + triggers = specTriggers spec + uniqueTriggers = mkUniqueTriggers triggers + exts = gatherExts streams triggers ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix ifcFields = mkSpecIfcFields triggers exts @@ -169,7 +198,7 @@ compileBS _bsSettings prefix spec = genFuns :: [BS.CDefl] genFuns = map accessDecln streams ++ map streamGen streams - ++ concatMap triggerGen triggers + ++ concatMap triggerGen uniqueTriggers where accessDecln :: Stream -> BS.CDefl accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff @@ -177,11 +206,12 @@ compileBS _bsSettings prefix spec = streamGen :: Stream -> BS.CDefl streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty - triggerGen :: Trigger -> [BS.CDefl] - triggerGen (Trigger name guard args) = guardDef : argDefs + triggerGen :: UniqueTrigger -> [BS.CDefl] + triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) = + guardDef : argDefs where - guardDef = mkGenFun (guardName name) guard Bool - argDefs = map argGen (zip (argNames name) args) + guardDef = mkGenFun (guardName uniqueName) guard Bool + argDefs = map argGen (zip (argNames uniqueName) args) argGen :: (String, UExpr) -> BS.CDefl argGen (argName, UExpr ty expr) = mkGenFun argName expr ty @@ -212,9 +242,11 @@ compileIfcBS _bsSettings prefix spec = ifcFields = mkSpecIfcFields triggers exts streams = specStreams spec - triggers = specTriggers spec exts = gatherExts streams triggers + -- Remove duplicates due to multiple guards for the same trigger. + triggers = nubBy compareTrigger (specTriggers spec) + ifcDef :: BS.CDefn ifcDef = BS.Cstruct True @@ -244,7 +276,9 @@ compileTypesBS _bsSettings prefix spec = exprs = gatherExprs streams triggers streams = specStreams spec - triggers = specTriggers spec + + -- Remove duplicates due to multiple guards for the same trigger. + triggers = nubBy compareTrigger (specTriggers spec) -- Generate type declarations. mkTypeDeclns :: [UExpr] -> [BS.CDefn] @@ -296,3 +330,21 @@ gatherExprs streams triggers = map streamUExpr streams where streamUExpr (Stream _ _ expr ty) = UExpr ty expr triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args + +-- | We consider triggers to be equal, if their names match and the number and +-- types of arguments. +compareTrigger :: Trigger -> Trigger -> Bool +compareTrigger (Trigger name1 _ args1) (Trigger name2 _ args2) + = name1 == name2 && compareArguments args1 args2 + + where + compareArguments :: [UExpr] -> [UExpr] -> Bool + compareArguments [] [] = True + compareArguments [] _ = False + compareArguments _ [] = False + compareArguments (x:xs) (y:ys) = compareUExpr x y && compareArguments xs ys + + compareUExpr :: UExpr -> UExpr -> Bool + compareUExpr (UExpr ty1 _) (UExpr ty2 _) + | Just Refl <- testEquality ty1 ty2 = True + | otherwise = False diff --git a/src/Copilot/Compile/Bluespec/Representation.hs b/src/Copilot/Compile/Bluespec/Representation.hs new file mode 100644 index 0000000..d5bc442 --- /dev/null +++ b/src/Copilot/Compile/Bluespec/Representation.hs @@ -0,0 +1,22 @@ +-- | Bluespec backend specific versions of selected `Copilot.Core` datatypes. +module Copilot.Compile.Bluespec.Representation + ( UniqueTrigger (..) + , UniqueTriggerId + , mkUniqueTriggers + ) + where + +import Copilot.Core ( Trigger (..) ) + +-- | Internal unique name for a trigger. +type UniqueTriggerId = String + +-- | A `Copilot.Core.Trigger` with an unique name. +data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger + +-- | Given a list of triggers, make their names unique. +mkUniqueTriggers :: [Trigger] -> [UniqueTrigger] +mkUniqueTriggers ts = zipWith mkUnique ts [0..] + where + mkUnique :: Trigger -> Integer -> UniqueTrigger + mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t From b6ec8e95cdfcf4dff4482234334aa428b49c3e9d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 6 Jan 2025 11:39:37 -0600 Subject: [PATCH 2/2] Document changes in CHANGELOG. Refs #30. --- CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG b/CHANGELOG index 5e16d03..3ac15c8 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,6 @@ -2024-11-11 +2025-01-20 * Implement missing floating-point operations. (#28) + * Allow using same trigger name in multiple declarations. (#30) 2024-11-08 * Version bump (4.1). (#25)