Allow multiple triggers with the same name. Refs #30.

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)

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
 

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.

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,19 +198,20 @@ 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
 
         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

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