1 {- | To create new Checks simply:
3 1. create an element of type 'Check g n e'
5 2. add it to the list 'checksList'
7 If necessary create new 'INError' values and
8 extend the 'show' function definition.
18 -- * List of available check operations
23 -- * Check operations combinators
27 -- * Other functions useful elsewhere
35 import Palette hiding (join)
42 import qualified Data.Map as Map
45 -- | Interaction Nets Errors
47 = DisconnectedPorts [(NodeNr, Node n, [Port])] -- ^ Disconnected ports
48 | ErrorString String -- ^ General error
49 | MultiDef String Int -- ^ Symbol is defined multiple times in palette
50 | UndefAgent (Node n) -- ^ Undefined agent
51 | BadInterfaceSymbol Shape Ports -- ^ Bad interface symbol definition
52 | BadInterfaceAgent (Node n) -- ^ Bad interface agent
53 | SymbolNoPorts String -- ^ Symbol without ports
54 | SymbolRepeatedPorts String [(String, Int)] -- ^ Symbol with repeated port names
55 | SymbolDiffPorts String Ports Ports -- ^ Symbol definition differ from default one.
56 | AgentNoPorts (Node n) -- ^ Agent without ports
57 | MappingNoDom Mapping NodeNr -- ^ Bad mapping which refers one element in domain that do not exist.
58 | MappingNoRang Mapping NodeNr -- ^ Bad mapping which refers one element in range that do not exist.
59 | MappingNotInj Mapping NodeNr -- ^ Mapping is not injective with respect to LHS node given.
60 | MappingNotFunc Mapping NodeNr -- ^ Mapping is not a function with respect to RHS node given.
61 | UnMappedInterface (Node n) -- ^ Interface agent is not mapped to another.
62 | Not2Agents [Node n] -- ^ rule LHS don't have exactly 2 agents.
63 | NoActivePair (Node n) (Node n) -- ^ No active pair between the nodes given
64 | ExtraEdge EdgeNr (NodeNr, PortName) (NodeNr, PortName) -- ^ Edge other than edge between principal ports found between agents in LHS.
65 | InterfaceBadConnected NodeNr (EdgeNr) -- ^ Interface agent is not connected to free ports of active pair.
66 | MultRulesSameLHS String String [String] -- ^ Multiple rules with same LHS active pair, i.e. between shape1 and shape2.
68 -- | NewError ... -- ^
70 instance (Show g, Show n, Show e) => Show (INError g n e) where
71 showsPrec _ (DisconnectedPorts l) =
72 showString badPortMsg . showChar '\n' . showString (showBadPortsNet 1 l)
73 showsPrec _ (ErrorString str) = showString str
74 showsPrec _ (MultiDef symb reps) =
75 showString "Symbol \"" . showString symb . showString "\" is defined "
76 . shows reps . showString " times in palette of symbols."
77 showsPrec _ (UndefAgent node) =
78 showString "Agent \"" . showString (Network.getName node)
79 . showString "\" @ " . shows (getPosition node)
80 . showString " is not defined in the palette of symbols."
81 showsPrec _ (BadInterfaceSymbol shape ports) =
82 showString ("A symbol called interface is defined, so its definition should be :\n"
83 ++ "\tshape = Circle { shapeStyle = ShapeStyle { styleStrokeWidth = 2\n"
84 ++ "\t , styleStrokeColour = RGB 255 255 255\n"
85 ++ "\t , styleFill = RGB 255 255 255 }\n"
86 ++ "\t , shapeRadius = 0.25 }\n"
87 ++ "\tports = Just [(\"interface\", DoublePoint 0.0 0.25)]\n"
88 ++ "but something different were found:")
89 . showString "\tshape = " . shows shape
90 . showString "\tports = " . shows ports
91 showsPrec _ (BadInterfaceAgent node) =
92 showString "Agent \"" . showString (Network.getName node)
93 . showString "\" @ " . shows (getPosition node)
94 . showString " is a bad interface agent."
95 showsPrec _ (SymbolNoPorts symb) =
96 showString "Symbol \"" . showString symb . showString "\" don't have ports."
97 showsPrec _ (SymbolRepeatedPorts symb reps) =
98 showString "Symbol \"" . showString symb . showString "\" have the following repeated port names:\n"
99 . showString (unlines $ map showPortRep reps)
100 showsPrec _ (SymbolDiffPorts symb ports defaultPorts) =
101 showString "Symbol \"" . showString symb . showString "\" is defined with ports \n."
102 . shows ports . showString "\nwhich differ from the default definition with ports \n"
104 showsPrec _ (AgentNoPorts node) =
105 showString "Agent \"" . showString (Network.getName node)
106 . showString "\" @ " . shows (getPosition node)
107 . showString " don't have ports."
108 showsPrec _ (MappingNoDom mapping nNr) =
109 showString "Interface node " . shows nNr
110 . showString " do not exist in LHS but is referred in domain of mapping\n"
111 . showsMapping mapping
112 showsPrec _ (MappingNoRang mapping nNr) =
113 showString "Interface node " . shows nNr
114 . showString" do not exist in RHS but is referred in range of mapping\n"
115 . showsMapping mapping
116 showsPrec _ (MappingNotInj mapping nNr) =
117 showString "Mapping is not injective with respect to LHS interface node "
120 . showsMapping mapping
121 showsPrec _ (MappingNotFunc mapping nNr) =
122 showString "Mapping is not a function with respect to RHS interface node "
125 . showsMapping mapping
126 showsPrec _ (UnMappedInterface node) =
127 showString "Interface \"" . showString (Network.getName node)
128 . showString "\" @ " . shows (getPosition node)
129 . showString " is not mapped to other interface in the other side of the rule."
130 showsPrec _ (Not2Agents lNs) =
131 showString "The rule LHS should have exactly 2 agents but those "
132 . shows (length lNs) . showString " were found:" . showsAgents lNs
133 showsPrec _ (NoActivePair node1 node2) =
134 showString "No active pair between agent \"" . showString (Network.getName node1)
135 . showString "\" @ " . shows (getPosition node1)
136 . showString "\nand agent \"" . showString (Network.getName node2)
137 . showString "\" @ " . shows (getPosition node2)
138 showsPrec _ (ExtraEdge edgeNr (nNr1, port1) (nNr2, port2)) =
139 showString "Edge " . shows edgeNr
140 . showString "is not the edge between principal ports but also found between agents \"Node "
141 . shows nNr1 . showString "\" at port " . showString port1
142 . showString " and \"Node " . shows nNr2 . showString "\" at port "
144 showsPrec _ (InterfaceBadConnected nNr edgeNr) =
145 showString "Interface \"Node " . shows nNr
146 . showString "\" should be connected to one of the free ports of active pair \"Edge "
147 . shows edgeNr . showString "\" but it isn't."
148 showsPrec _ (MultRulesSameLHS shape1 shape2 rules) =
149 showString "There should be at most one rule for pair of agents but for agents \""
150 . showString shape1 . showString "\" and \"" . showString shape2
151 . showString "\" there are this rules whose LHS is an active pair between such agents :"
152 . showString (commasAnd rules)
154 -- showsPrec _ (NewError ...) = ...
156 showsAgent :: Node n -> ShowS
158 showString "Agent \"" . showString (Network.getName node)
159 . showString "\" of symbol \""
160 . showString (getShape node)
161 . showString "\" @ " . shows (getPosition node)
164 showsAgents :: [Node n] -> ShowS
165 showsAgents [] = showString ""
166 showsAgents (x:xs) = showsAgent x . showChar '\n' . showsAgents xs
168 showPortRep :: (PortName, Int) -> String
169 showPortRep (portname, n) = '\t':portname ++ " ~ " ++ show n ++ " times"
171 data Side = Lhs | Rhs deriving (Eq,Ord)
172 instance Show Side where
176 data ErrorLoc = PALETTE | NET | RULES | RULE RuleName (Maybe Side) deriving (Eq, Ord)
178 instance Show ErrorLoc where
179 show PALETTE = "PALETTE"
182 show (RULE ruleName mSide) =
183 showString "RULE \"" . showString ruleName . showChar '\"'
184 . maybe id (\v -> showChar ' ' . shows v) mSide $ ""
187 type CheckOp g n e = Document g n e -> Map ErrorLoc [INError g n e] -- ^ errors by location
189 ( String -- Check operation name to be displayed
190 , String -- Check description
191 , String -- Message when the check is passed successfully
192 , String -- Message when the check fails
193 , CheckOp g n e -- Check function
196 -- | Join two check operations; concatenate errors.
197 join :: CheckOp g n e -> CheckOp g n e -> CheckOp g n e
198 join check1 check2 = uncurry (Map.unionWith (++)) . (check1 /\ check2)
200 -- | Join a list of check operations.
201 joins :: [CheckOp g n e] -> CheckOp g n e
204 -- | List of available checks.
205 checksList :: [Check g n e]
215 --------------------------------------------------------
216 -- | Useful function that transverse a 'Document' in a very common way to collect 'INError's.
217 doc2Errors :: (Network g n e -> [INError g n e])
218 -> (INRule g n e -> [(Maybe Side, [INError g n e])] )
220 doc2Errors funcNet funcRule =
221 uncurry (foldl updtAc)
222 . ( (emptyOrSingle NET . funcNet . getNetwork)
226 -- updtAc :: Map ErrorLoc [INError g n e] -> INRule g n e -> Map ErrorLoc [INError g n e]
227 updtAc mapp rule = foldl (aux $ INRule.getName rule) mapp $ funcRule rule
229 aux :: RuleName -> Map ErrorLoc [INError g n e] -> (Maybe Side, [INError g n e])
230 -> Map ErrorLoc [INError g n e]
231 aux _ mapp (_,[]) = mapp
232 aux ruleName mapp (mSide, errs) = Map.insertWith (++) (RULE ruleName mSide) errs mapp
234 -- | If the list of values is empty create the empty 'Map'. Else creates the singleton 'map' with key @k@.
235 emptyOrSingle :: k -> [v] -> Map k [v]
236 emptyOrSingle k l = if null l then Map.empty else Map.singleton k l
238 -- Bad Ports ------------------------------------------------------------------------------------------------
240 badPortMsg = "Disconnected or with multiple connections ports found"
242 badPortsCheck :: Check g n e
245 , "Every port must be connected exactly once."
246 , "No disconnected or with multiple connections ports found."
251 -- | Every net in INblobs must have exactly one edge connected at each port.
252 badPortsNet :: Palette n -> Network g n e -> [(NodeNr, Node n, [Port])]
253 badPortsNet palette network =
254 filter f . map badPortsN $ getNodeAssocs network
256 f (_,_,t) = not $ null t
257 -- Gives list of bad ports for this node.
258 badPortsN :: (NodeNr, Node n) -> (NodeNr, Node n, [Port])
259 badPortsN (nNr, node) = (nNr, node, case getPorts palette network nNr of
260 Nothing -> error $ "Unexpected situation: no ports found in agent "
261 ++ show nNr ++ " of type " ++ getShape node
262 Just ports -> filter (g nNr . fst) ports)
263 g :: NodeNr -> PortName -> Bool
264 g nnr port = maybe True (== (nnr,port)) $ otherExtremeOfEdgeConnectedOnPort network nnr port
266 -- | Collects all bad ports by location.
267 pureBadPorts :: CheckOp g n e
268 pureBadPorts doc = doc2Errors funcNet funcRule doc
269 where -- funcNet :: Network g n e -> [INError g n e]
270 funcNet = insertIfN . badPortsNet palette
272 -- funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
275 . ((insertIfR Lhs . badPortsNet palette . getLHS)
277 (insertIfR Rhs . badPortsNet palette . getRHS))
279 insertIfN netCheck = if null netCheck then [] else [DisconnectedPorts netCheck]
280 insertIfR side netCheck = if null netCheck then [] else [(Just side, [DisconnectedPorts netCheck])]
282 palette = getPalette doc
284 showBadPortsNet :: Int -> [(NodeNr, Node n, [Port])] -> String
285 showBadPortsNet n l = unlines' $ map showNode l
286 where showNode (_, node, lPorts) = unlines' $ (replicate n '\t' ++ Network.getName node
287 ++ " # " ++ getShape node ++ " @ "
288 ++ show (getPosition node) ++ " in port(s):") : map showPort lPorts
289 showPort (name,_) = replicate (n+1) '\t' ++ name
290 ------------------------------------------------------------------------------------------------------------------
293 -- valid IN system ------------------------------------------------------------------------------------------------
294 iNCheck :: Check g n e
298 [ "Check if it is a valid IN system.\n"
299 , "An IN system is valid in INblobs if:"
300 , " * every symbol have distinguished port names"
301 , " * every port is connected exactly once in net and in LHS and RHS of every rule"
302 , " * the LHS of every rule is one active pair, plus interface agents"
303 , " * every interface agent in the LHS (respectively RHS) of a rule is mapped to one interface agent in the RHS (respectively LHS)"
304 , " * there are at most one rule per pair of agents"
305 , " * every agent mentioned in the net or any rule is declared in the palette of symbols"
308 , "Invalid IN system"
312 {- | An IN system is valid in INblobs if:
314 * every symbol have distinguished port names
316 * every port is connected exactly once in net and in LHS and RHS of every rule
318 * the LHS of every rule is one active pair, plus interface agents
320 * every interface agent in the LHS (respectively RHS) of a rule is mapped to
321 one interface agent in the RHS (respectively LHS)
323 * there are at most one rule per pair of agents
325 * every agent mentioned in the net or any rule is declared in the palette of symbols
328 validIN :: CheckOp g n e
333 , checkNoRepeatedRules
336 sepInterface :: Network g n e -> ( [(NodeNr,Node n)] -- interface nodes
337 , [(NodeNr,Node n)] -- none interface nodes
339 sepInterface = partition isInterfaceNode . getNodeAssocs
341 -- | 'checkLHS' and 'checkMapping'
342 checkEachRule :: CheckOp g n e
343 checkEachRule doc = doc2Errors funcNet funcRule doc
344 where funcNet :: Network g n e -> [INError g n e]
347 -- funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
348 funcRule rule = (Just Lhs, checkLHS (getPalette doc) lhs)
349 : checkMapping (getMapping rule)
350 (fst $ sepInterface lhs)
351 (fst . sepInterface $ getRHS rule)
352 where lhs = getLHS rule
354 -- | LHS should be exactly two agents different from interface connected trough their
355 -- principal ports with the rest of the ports connected to one interface agent.
356 checkLHS :: Palette n -> Network g n e -> [INError g n e]
357 checkLHS palette = either (const []) id . checkLHS' palette
359 checkLHS' :: Palette n -> Network g n e -> Either (String, String) [INError g n e]
360 checkLHS' palette net =
361 case sepInterface net of
362 (iNs, [(xNr,x), (yNr,y)]) ->
363 case (getPorts palette net xNr, getPorts palette net yNr) of
364 (Just (px:pxs), Just (py:pys)) ->
365 case findEdge xNr (fst px) yNr (fst py) net of
366 Nothing -> Right [NoActivePair x y]
368 let mINs = map (otherExtremeOfEdgeConnectedOnPort net xNr . fst) pxs
369 ++ map (otherExtremeOfEdgeConnectedOnPort net yNr . fst) pys
370 in if all isJust mINs
372 let iNs' = map (id >< const "interface") iNs
373 cons = map fromJust mINs
374 dif1 = cons \\ iNs' -- multiple edges between agents x and y
375 dif2 = iNs' \\ cons -- interface nodes not connected to agent x or y
376 in if null dif1 && null dif2
377 then Left (getShape x,getShape y)
378 else Right $ toError1 dif1 ++ map (toError2 ed) dif2
379 else Right [] -- disconnected ports checked in another piece of code
383 (psx, psy) -> Right . map (AgentNoPorts . snd) $ filter (maybe True null . fst) [(psx,x),(psy,y)]
384 (_, lAs) -> Right [Not2Agents $ map snd lAs]
386 toError1 :: [(NodeNr, PortName)] -> [INError g n e]
387 toError1 = map aux3 . groupBy aux2 . map aux
388 aux = id /\ fromJust . uncurry (edgeConnectedOnPort net)
389 aux2 a b = snd a == snd b
390 aux3 :: [((NodeNr,PortName),EdgeNr)] -> INError g n e
391 aux3 [(from,edge), (to,_)] = ExtraEdge edge from to
392 aux3 _ = error "unexpected situation"
393 toError2 ed (nNr,_) = InterfaceBadConnected nNr ed
396 -- | Every interface agent in the LHS (respectively RHS) of a rule is mapped to
397 -- one interface agent in the RHS (respectively LHS).
398 checkMapping :: Mapping -> [(NodeNr,Node n)] -> [(NodeNr,Node n)] -> [(Maybe Side, [INError g n e])]
399 checkMapping mapR lhsI rhsI =
400 [ (Just Lhs, map errL $ lhs \\ domMap )
401 , (Just Rhs, map errR $ rhs \\ rangeMap)
402 , (Nothing, (uncurry (++) . (map errNotInj >< map errNoDom ) . partition (`elem` lhs) $ domMap \\ lhs )
404 (uncurry (++) . (map errNotFunc >< map errNoRang) . partition (`elem` rhs) $ rangeMap \\ rhs )
409 (domMap, rangeMap) = unzip mapR :: ([NodeNr], [NodeNr])
413 errL nNr = UnMappedInterface . fromJust $ lookup nNr lhsI
414 errR nNr = UnMappedInterface . fromJust $ lookup nNr rhsI
415 errNotInj = MappingNotInj mapR
416 errNoDom = MappingNoDom mapR
417 errNotFunc = MappingNotFunc mapR
418 errNoRang = MappingNoRang mapR
420 insertIf :: Ord k => k -> [a] -> Map k [a] -> Map k [a]
421 insertIf k a mapp | null a = mapp
422 | otherwise = Map.insertWith (++) k a mapp
424 checkAgents :: CheckOp g n e
426 insertIf PALETTE (map toError3 . filter badInterface $ shaps)
427 . insertIf PALETTE (map toError4 $ filter repeatedPorts shaps)
428 . insertIf PALETTE (map toError2 $ filter noPorts shaps)
429 . insertIf PALETTE (map toError . repeateds $ symbs)
430 $ undefinedAgents symbs doc
432 shaps = shapes $ getPalette doc
433 symbs = map fst shaps
434 toError (symb, i) = MultiDef symb i
435 toError2 = SymbolNoPorts . fst
436 toError3 (_, (shape, mPorts, _)) = BadInterfaceSymbol shape mPorts
437 toError4 (shapeName, (_, ports, _)) = SymbolRepeatedPorts shapeName . filter ((/=1) . snd) . repeateds $ map fst ports
438 noPorts = null . snd3 . snd
439 repeatedPorts = haveRepeateds . map fst . snd3 . snd
440 fstsnd (a,b,_) = (a,b)
442 badInterface ("interface", (_, [("interface",_)], _)) = False
443 badInterface ("interface", _) = True
444 badInterface _ = False
446 -- | Check if there are undefined agents.
447 undefinedAgents :: [String] -> CheckOp g n e
448 undefinedAgents symbols = doc2Errors funcNet funcRule
449 where funcNet :: Network g n e -> [INError g n e]
450 funcNet = undefinedAgentNet symbols
452 funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
454 [ (Just Lhs, undefinedAgentNet symbols $ getLHS rule)
455 , (Just Rhs, undefinedAgentNet symbols $ getRHS rule)
458 undefinedAgentNet :: [String] -> Network g n e -> [INError g n e]
459 undefinedAgentNet symbols = uncurry (++)
460 . ( (map UndefAgent . filter undefs) /\ (map BadInterfaceAgent . filter badInterfaceNode) )
463 undefs = (`notElem` symbols) . getShape
464 badInterfaceNode node = (\str -> str == fst interfaceSymbol && not (isInterfaceNode (0,node)) )
467 -- | Checks if there are at most one rule per pair of agents.
468 checkNoRepeatedRules :: CheckOp g n e
469 checkNoRepeatedRules doc =
470 (\lErrors -> insertIf RULES lErrors Map.empty)
471 . map toError . filter dups . groupBy activePair
472 . map left . filter isLeft
473 . map (INRule.getName /\ checkLHS' (getPalette doc) .getLHS) . getRules
476 isLeft = either (const True) (const False) . snd
477 left = id >< either id (error "This shouldn't happen")
478 activePair :: (RuleName, (String,String)) -> (RuleName, (String,String)) -> Bool
479 activePair (_,shapes1) (_,shapes2) = shapes1 == shapes2 || shapes1 == swap shapes2
480 dups = (> 1) . length
481 toError :: [(RuleName, (String,String))] -> INError g n e
482 toError ( (ruleName,(shape1,shape2)):xs) = MultRulesSameLHS shape1 shape2 $ ruleName : map fst xs
483 ------------------------------------------------------------------------------------------------------------------
485 -- | Checks if declared management agents are defined in the exactly same way that they are in the default palette.
486 -- Useful to avoid posterior problems with templates.
487 manCheck :: Check g n e
489 ( "Check management agents"
490 , "Check if management agents are defined in the exact same way that in 'ManagementAgents.INblobpalette' to avoid troubles with templates."
491 , "Management agents definitions match."
492 , "Management agent(s) definitions don't match"
496 manCheck' :: CheckOp g n e
498 emptyOrSingle PALETTE
500 . mapMaybeWithKey aux
501 . uncurry ( Map.intersectionWith (,) )
502 . ( Map.fromList >< Map.fromList )
503 $ (shapes $ getPalette doc, shapes specialSymbols)
505 where aux :: String -> ((a,Ports,c),(a,Ports,c)) -> Maybe (INError g n e)
506 aux k ((_, ports1,_), (_, ports2,_))
507 | ports1 == ports2 = Nothing
508 | otherwise = Just $ SymbolDiffPorts k ports1 ports2
510 mapMaybeWithKey :: Ord k => (k -> a -> Maybe b) -> Map k a -> Map k b
512 -- mapMaybeWithKey = Map.mapMaybeWithKey
513 -- Allowing retro-compatibility with GHC 6.4
514 mapMaybeWithKey f = Map.foldWithKey aux Map.empty
515 where -- aux :: k -> a -> Map k b -> Map k b
516 aux k a = case f k a of
518 Just b -> Map.insert k b