@@ -8,9 +8,10 @@ module Copilot.Compile.Bluespec.Compile
88 ) where
99
1010-- External imports
11- import Data.List (nub , union )
11+ import Data.List (nub , nubBy , union )
1212import Data.Maybe (catMaybes , maybeToList )
1313import Data.String (IsString (.. ))
14+ import Data.Type.Equality (testEquality , (:~:) (Refl ))
1415import Data.Typeable (Typeable )
1516import qualified Language.Bluespec.Classic.AST as BS
1617import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
@@ -29,6 +30,7 @@ import Copilot.Compile.Bluespec.CodeGen
2930import Copilot.Compile.Bluespec.External
3031import Copilot.Compile.Bluespec.FloatingPoint
3132import Copilot.Compile.Bluespec.Name
33+ import Copilot.Compile.Bluespec.Representation
3234import Copilot.Compile.Bluespec.Settings
3335
3436-- | Compile a specification to a Bluespec file.
@@ -39,12 +41,20 @@ import Copilot.Compile.Bluespec.Settings
3941-- that are generated.
4042compileWith :: BluespecSettings -> String -> Spec -> IO ()
4143compileWith bsSettings prefix spec
42- | null (specTriggers spec)
44+ | null triggers
4345 = do hPutStrLn stderr $
4446 " Copilot error: attempt at compiling empty specification.\n "
4547 ++ " You must define at least one trigger to generate Bluespec monitors."
4648 exitFailure
4749
50+ | incompatibleTriggers triggers
51+ = do hPutStrLn stderr $
52+ " Copilot error: attempt at compiling specification with conflicting "
53+ ++ " trigger definitions.\n "
54+ ++ " Multiple triggers have the same name, but different argument "
55+ ++ " types.\n "
56+ exitFailure
57+
4858 | otherwise
4959 = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec
5060 ifcBsFile = render $ pPrint $ compileIfcBS bsSettings prefix spec
@@ -57,6 +67,24 @@ compileWith bsSettings prefix spec
5767 writeFile (dir </> " bs_fp.c" ) copilotBluespecFloatingPointC
5868 writeFile (dir </> " BluespecFP.bsv" ) copilotBluespecFloatingPointBSV
5969 writeFile (dir </> prefix ++ " .bs" ) bsFile
70+ where
71+ triggers = specTriggers spec
72+
73+ -- Check that two triggers do no conflict, that is: if their names are
74+ -- equal, the types of their arguments should be equal as well.
75+ incompatibleTriggers :: [Trigger ] -> Bool
76+ incompatibleTriggers = pairwiseAny conflict
77+ where
78+ conflict :: Trigger -> Trigger -> Bool
79+ conflict t1@ (Trigger name1 _ _) t2@ (Trigger name2 _ _) =
80+ name1 == name2 && not (compareTrigger t1 t2)
81+
82+ -- True if the function holds for any pair of elements. We assume that
83+ -- the function is commutative.
84+ pairwiseAny :: (a -> a -> Bool ) -> [a ] -> Bool
85+ pairwiseAny _ [] = False
86+ pairwiseAny _ (_: [] ) = False
87+ pairwiseAny f (x: xs) = any (f x) xs || pairwiseAny f xs
6088
6189-- | Compile a specification to a Bluespec.
6290--
@@ -136,11 +164,12 @@ compileBS _bsSettings prefix spec =
136164 ifcModId = BS. mkId BS. NoPos " ifcMod"
137165
138166 rules :: [BS. CRule ]
139- rules = map mkTriggerRule triggers ++ maybeToList (mkStepRule streams)
167+ rules = map mkTriggerRule uniqueTriggers ++ maybeToList (mkStepRule streams)
140168
141- streams = specStreams spec
142- triggers = specTriggers spec
143- exts = gatherExts streams triggers
169+ streams = specStreams spec
170+ triggers = specTriggers spec
171+ uniqueTriggers = mkUniqueTriggers triggers
172+ exts = gatherExts streams triggers
144173
145174 ifcId = BS. mkId BS. NoPos $ fromString $ specIfcName prefix
146175 ifcFields = mkSpecIfcFields triggers exts
@@ -169,19 +198,20 @@ compileBS _bsSettings prefix spec =
169198 genFuns :: [BS. CDefl ]
170199 genFuns = map accessDecln streams
171200 ++ map streamGen streams
172- ++ concatMap triggerGen triggers
201+ ++ concatMap triggerGen uniqueTriggers
173202 where
174203 accessDecln :: Stream -> BS. CDefl
175204 accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff
176205
177206 streamGen :: Stream -> BS. CDefl
178207 streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty
179208
180- triggerGen :: Trigger -> [BS. CDefl ]
181- triggerGen (Trigger name guard args) = guardDef : argDefs
209+ triggerGen :: UniqueTrigger -> [BS. CDefl ]
210+ triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) =
211+ guardDef : argDefs
182212 where
183- guardDef = mkGenFun (guardName name ) guard Bool
184- argDefs = map argGen (zip (argNames name ) args)
213+ guardDef = mkGenFun (guardName uniqueName ) guard Bool
214+ argDefs = map argGen (zip (argNames uniqueName ) args)
185215
186216 argGen :: (String , UExpr ) -> BS. CDefl
187217 argGen (argName, UExpr ty expr) = mkGenFun argName expr ty
@@ -212,9 +242,11 @@ compileIfcBS _bsSettings prefix spec =
212242 ifcFields = mkSpecIfcFields triggers exts
213243
214244 streams = specStreams spec
215- triggers = specTriggers spec
216245 exts = gatherExts streams triggers
217246
247+ -- Remove duplicates due to multiple guards for the same trigger.
248+ triggers = nubBy compareTrigger (specTriggers spec)
249+
218250 ifcDef :: BS. CDefn
219251 ifcDef = BS. Cstruct
220252 True
@@ -244,7 +276,9 @@ compileTypesBS _bsSettings prefix spec =
244276
245277 exprs = gatherExprs streams triggers
246278 streams = specStreams spec
247- triggers = specTriggers spec
279+
280+ -- Remove duplicates due to multiple guards for the same trigger.
281+ triggers = nubBy compareTrigger (specTriggers spec)
248282
249283 -- Generate type declarations.
250284 mkTypeDeclns :: [UExpr ] -> [BS. CDefn ]
@@ -296,3 +330,21 @@ gatherExprs streams triggers = map streamUExpr streams
296330 where
297331 streamUExpr (Stream _ _ expr ty) = UExpr ty expr
298332 triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args
333+
334+ -- | We consider triggers to be equal, if their names match and the number and
335+ -- types of arguments.
336+ compareTrigger :: Trigger -> Trigger -> Bool
337+ compareTrigger (Trigger name1 _ args1) (Trigger name2 _ args2)
338+ = name1 == name2 && compareArguments args1 args2
339+
340+ where
341+ compareArguments :: [UExpr ] -> [UExpr ] -> Bool
342+ compareArguments [] [] = True
343+ compareArguments [] _ = False
344+ compareArguments _ [] = False
345+ compareArguments (x: xs) (y: ys) = compareUExpr x y && compareArguments xs ys
346+
347+ compareUExpr :: UExpr -> UExpr -> Bool
348+ compareUExpr (UExpr ty1 _) (UExpr ty2 _)
349+ | Just Refl <- testEquality ty1 ty2 = True
350+ | otherwise = False
0 commit comments