{- | To create new Checks simply:

       1. create an element of type 'Check g n e'

       2. add it to the list 'checksList'

    If necessary create new 'INError' values and
    extend the 'show' function definition.
-}
module INChecks
    (
    -- * Data-types
      INError(..)
    , ErrorLoc
    , CheckOp
    , Check

    -- * List of available check operations
    , checksList

    , iNCheck

    -- * Check operations combinators
    , join
    , joins

    -- * Other functions useful elsewhere
    , undefinedAgents
    ) where

import Document
import Network
import Ports
import INRule
import Palette hiding (join)
import Common
import Shape
import SpecialSymbols

import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List

-- | Interaction Nets Errors
data INError g n e
	= DisconnectedPorts [(NodeNr, Node n, [Port])] -- ^ Disconnected ports
	| ErrorString String -- ^ General error
	| MultiDef String Int -- ^ Symbol is defined multiple times in palette
	| UndefAgent (Node n) -- ^ Undefined agent
	| BadInterfaceSymbol Shape Ports -- ^ Bad interface symbol definition
	| BadInterfaceAgent (Node n) -- ^ Bad interface agent
	| SymbolNoPorts String -- ^ Symbol without ports
	| SymbolRepeatedPorts String [(String, Int)] -- ^ Symbol with repeated port names
	| SymbolDiffPorts String Ports Ports -- ^ Symbol definition differ from default one.
	| AgentNoPorts (Node n) -- ^ Agent without ports
	| MappingNoDom Mapping NodeNr -- ^ Bad mapping which refers one element in domain that do not exist.
	| MappingNoRang Mapping NodeNr -- ^ Bad mapping which refers one element in range that do not exist.
	| MappingNotInj Mapping NodeNr -- ^ Mapping is not injective with respect to LHS node given.
	| MappingNotFunc Mapping NodeNr -- ^ Mapping is not a function with respect to RHS node given.
	| UnMappedInterface (Node n) -- ^ Interface agent is not mapped to another.
	| Not2Agents [Node n] -- ^ rule LHS don't have exactly 2 agents.
	| NoActivePair (Node n) (Node n) -- ^ No active pair between the nodes given
	| ExtraEdge EdgeNr (NodeNr, PortName) (NodeNr, PortName) -- ^ Edge other than edge between principal ports found between agents in LHS.
	| InterfaceBadConnected NodeNr (EdgeNr) -- ^ Interface agent is not connected to free ports of active pair.
	| MultRulesSameLHS String String [String] -- ^ Multiple rules with same LHS active pair, i.e. between shape1 and shape2.

-- 	| NewError ... -- ^ 

instance (Show g, Show n, Show e) => Show (INError g n e) where
	showsPrec _ (DisconnectedPorts l) =
		showString badPortMsg . showChar '\n' . showString (showBadPortsNet 1 l)
	showsPrec _ (ErrorString str) = showString str
	showsPrec _ (MultiDef symb reps) =
		showString "Symbol \"" . showString symb . showString "\" is defined "
		. shows reps . showString " times in palette of symbols."
	showsPrec _ (UndefAgent node) =
		showString "Agent \"" . showString (Network.getName node)
		. showString "\" @ " . shows (getPosition node)
		. showString " is not defined in the palette of symbols."
	showsPrec _ (BadInterfaceSymbol shape ports) =
		showString ("A symbol called interface is defined, so its definition should be :\n"
			    ++ "\tshape = Circle { shapeStyle = ShapeStyle { styleStrokeWidth  = 2\n"
			    ++ "\t                                          , styleStrokeColour = RGB 255 255 255\n"
			    ++ "\t                                          , styleFill = RGB 255 255 255 }\n"
			    ++ "\t               , shapeRadius = 0.25 }\n"
			    ++ "\tports = Just [(\"interface\", DoublePoint 0.0 0.25)]\n"
			    ++ "but something different were found:")
		. showString "\tshape = " . shows shape
		. showString "\tports = " . shows ports
	showsPrec _ (BadInterfaceAgent node) =
		showString "Agent \"" . showString (Network.getName node)
		. showString "\" @ " . shows (getPosition node)
		. showString " is a bad interface agent."
	showsPrec _ (SymbolNoPorts symb) =
		showString "Symbol \"" . showString symb . showString "\" don't have ports."
	showsPrec _ (SymbolRepeatedPorts symb reps) =
		showString "Symbol \"" . showString symb . showString "\" have the following repeated port names:\n"
		. showString (unlines $ map showPortRep reps)
	showsPrec _ (SymbolDiffPorts symb ports defaultPorts) =
		showString "Symbol \"" . showString symb . showString "\" is defined with ports \n."
		. shows ports . showString "\nwhich differ from the default definition with ports \n"
		. shows defaultPorts
	showsPrec _ (AgentNoPorts node) =
		showString "Agent \"" . showString (Network.getName node)
		. showString "\" @ " . shows (getPosition node)
		. showString " don't have ports."
	showsPrec _ (MappingNoDom mapping nNr) =
		showString "Interface node " . shows nNr
		. showString " do not exist in LHS but is referred in domain of mapping\n"
		. showsMapping mapping
	showsPrec _ (MappingNoRang mapping nNr) =
		 showString "Interface node " . shows nNr
		. showString" do not exist in RHS but is referred in range of mapping\n"
		. showsMapping mapping
	showsPrec _ (MappingNotInj mapping nNr) =
		showString "Mapping is not injective with respect to LHS interface node "
		. shows nNr
		. showChar '\n'
		. showsMapping mapping
	showsPrec _ (MappingNotFunc mapping nNr) =
		showString "Mapping is not a function with respect to RHS interface node "
		. shows nNr
		. showChar '\n'
		. showsMapping mapping
	showsPrec _ (UnMappedInterface node) =
		showString "Interface \"" . showString (Network.getName node)
		. showString "\" @ " . shows (getPosition node)
		. showString " is not mapped to other interface in the other side of the rule."
	showsPrec _ (Not2Agents lNs) =
		showString "The rule LHS should have exactly 2 agents but those "
		. shows (length lNs) . showString " were found:" . showsAgents lNs
	showsPrec _ (NoActivePair node1 node2) =
		showString "No active pair between agent \"" . showString (Network.getName node1)
		. showString "\" @ " . shows (getPosition node1)
		. showString "\nand agent \"" . showString (Network.getName node2)
		. showString "\" @ " . shows (getPosition node2)
	showsPrec _ (ExtraEdge edgeNr (nNr1, port1) (nNr2, port2)) =
		showString "Edge " . shows edgeNr
		. showString "is not the edge between principal ports but also found between agents \"Node "
		. shows nNr1 . showString "\" at port " . showString port1
		. showString " and \"Node " . shows nNr2 .  showString "\" at port "
		. showString port2
	showsPrec _ (InterfaceBadConnected nNr edgeNr) =
		showString "Interface \"Node " . shows nNr
		. showString "\" should be connected to one of the free ports of active pair \"Edge "
		. shows edgeNr . showString "\" but it isn't."
	showsPrec _ (MultRulesSameLHS shape1 shape2 rules) =
		showString "There should be at most one rule for pair of agents but for agents \""
		. showString shape1 . showString "\" and \"" . showString shape2
		. showString "\" there are this rules whose LHS is an active pair between such agents :"
		. showString (commasAnd rules)

--	showsPrec _ (NewError ...) = ...

showsAgent :: Node n -> ShowS
showsAgent node =
		showString "Agent \"" . showString (Network.getName node)
		. showString "\" of symbol \""
		. showString (getShape node)
		. showString "\" @ " . shows (getPosition node)
	where err = error ""

showsAgents :: [Node n] -> ShowS
showsAgents [] = showString ""
showsAgents (x:xs) = showsAgent x . showChar '\n' . showsAgents xs

showPortRep :: (PortName, Int) -> String
showPortRep (portname, n) = '\t':portname ++ " ~ " ++ show n ++ " times"

data Side = Lhs | Rhs deriving (Eq,Ord)
instance Show Side where
	show Lhs = "LHS"
	show Rhs = "RHS"

data ErrorLoc = PALETTE | NET | RULES | RULE RuleName (Maybe Side) deriving (Eq, Ord)

instance Show ErrorLoc where
	show PALETTE = "PALETTE"
	show NET = "NET"
	show RULES = "RULES"
	show (RULE ruleName mSide) =
		showString "RULE \"" . showString ruleName . showChar '\"'
		. maybe id (\v -> showChar ' ' . shows v) mSide $ ""


type CheckOp g n e = Document g n e -> Map ErrorLoc [INError g n e] -- ^ errors by location
type Check g n e =
               ( String -- Check operation name to be displayed
               , String -- Check description
               , String -- Message when the check is passed successfully
               , String -- Message when the check fails
               , CheckOp g n e -- Check function
               )

-- | Join two check operations; concatenate errors.
join :: CheckOp g n e -> CheckOp g n e -> CheckOp g n e
join check1 check2 = uncurry (Map.unionWith (++)) . (check1 /\ check2)

-- | Join a list of check operations.
joins :: [CheckOp g n e] -> CheckOp g n e
joins = foldr1 join

-- | List of available checks.
checksList :: [Check g n e]
checksList =
       [ badPortsCheck
       , iNCheck
       , manCheck
--     , newCheck
       ]



--------------------------------------------------------
-- | Useful function that transverse a 'Document' in a very common way to collect 'INError's.
doc2Errors :: (Network g n e -> [INError g n e])
	-> (INRule g n e -> [(Maybe Side, [INError g n e])] )
	-> CheckOp g n e
doc2Errors funcNet funcRule =
	uncurry (foldl updtAc)
	. ( (emptyOrSingle NET . funcNet . getNetwork)
	  /\
	  getRules)
  where
	-- updtAc :: Map ErrorLoc [INError g n e] -> INRule g n e -> Map ErrorLoc [INError g n e]
	updtAc mapp rule = foldl (aux $ INRule.getName rule) mapp $ funcRule rule

	aux :: RuleName -> Map ErrorLoc [INError g n e] -> (Maybe Side, [INError g n e])
		-> Map ErrorLoc [INError g n e]
	aux _ mapp (_,[]) = mapp
	aux ruleName mapp (mSide, errs) = Map.insertWith (++) (RULE ruleName mSide) errs mapp

-- | If the list of values is empty create the empty 'Map'. Else creates the singleton 'map' with key @k@.
emptyOrSingle :: k -> [v] -> Map k [v]
emptyOrSingle k l = if null l then Map.empty else Map.singleton k l

-- Bad Ports ------------------------------------------------------------------------------------------------

badPortMsg = "Disconnected or with multiple connections ports found"

badPortsCheck :: Check g n e
badPortsCheck =
	( "Check bad ports"
	, "Every port must be connected exactly once."
	, "No disconnected or with multiple connections ports found."
	, badPortMsg
	, pureBadPorts
	)

-- | Every net in INblobs must have exactly one edge connected at each port.
badPortsNet :: Palette n -> Network g n e -> [(NodeNr, Node n, [Port])]
badPortsNet palette network =
	filter f . map badPortsN $ getNodeAssocs network
	where
	      f (_,_,t) = not $ null t
	      -- Gives list of bad ports for this node.
              badPortsN :: (NodeNr, Node n) -> (NodeNr, Node n, [Port])
              badPortsN (nNr, node) = (nNr, node, case getPorts palette network nNr of
                                                     Nothing -> error $ "Unexpected situation: no ports found in agent "
									++ show nNr ++ " of type " ++ getShape node
						     Just ports -> filter (g nNr . fst) ports)
              g :: NodeNr -> PortName -> Bool
              g nnr port = maybe True (== (nnr,port)) $ otherExtremeOfEdgeConnectedOnPort network nnr port

-- | Collects all bad ports by location.
pureBadPorts :: CheckOp g n e
pureBadPorts doc = doc2Errors funcNet funcRule doc
  where -- funcNet :: Network g n e -> [INError g n e]
	funcNet = insertIfN . badPortsNet palette

	-- funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
	funcRule =
		uncurry (++)
		. ((insertIfR Lhs . badPortsNet palette . getLHS)
		  /\
		  (insertIfR Rhs . badPortsNet palette . getRHS))

	insertIfN netCheck = if null netCheck then [] else [DisconnectedPorts netCheck]
	insertIfR side netCheck = if null netCheck then [] else [(Just side, [DisconnectedPorts netCheck])]

	palette = getPalette doc

showBadPortsNet :: Int -> [(NodeNr, Node n, [Port])] -> String
showBadPortsNet n l = unlines' $ map showNode l
    where showNode (_, node, lPorts) = unlines' $ (replicate n '\t' ++ Network.getName node
					++ " # " ++ getShape node ++ " @ "
					++ show (getPosition node) ++ "   in port(s):") : map showPort lPorts
          showPort (name,_) = replicate (n+1) '\t' ++ name
------------------------------------------------------------------------------------------------------------------


-- valid IN system ------------------------------------------------------------------------------------------------
iNCheck :: Check g n e
iNCheck =
	( "Valid IN system"
	, unlines
		[ "Check if it is a valid IN system.\n"
		, "An IN system is valid in INblobs if:"
		, " * every symbol have distinguished port names"
		, " * every port is connected exactly once in net and in LHS and RHS of every rule"
		, " * the LHS of every rule is one active pair, plus interface agents"
		, " * every interface agent in the LHS (respectively RHS) of a rule is mapped to one interface agent in the RHS (respectively LHS)"
		, " * there are at most one rule per pair of agents"
		, " * every agent mentioned in the net or any rule is declared in the palette of symbols"
		]
	, "Valid IN system"
	, "Invalid IN system"
	, validIN
	)

{- | An IN system is valid in INblobs if:

  * every symbol have distinguished port names

  * every port is connected exactly once in net and in LHS and RHS of every rule

  * the LHS of every rule is one active pair, plus interface agents

  * every interface agent in the LHS (respectively RHS) of a rule is mapped to
     one interface agent in the RHS (respectively LHS)

  * there are at most one rule per pair of agents

  * every agent mentioned in the net or any rule is declared in the palette of symbols

-}
validIN :: CheckOp g n e
validIN = joins [
		  pureBadPorts
		, checkAgents
		, checkEachRule
		, checkNoRepeatedRules
		]

sepInterface :: Network g n e -> ( [(NodeNr,Node n)] -- interface nodes
				 , [(NodeNr,Node n)] -- none interface nodes
				 )
sepInterface = partition isInterfaceNode . getNodeAssocs

-- | 'checkLHS' and 'checkMapping'
checkEachRule :: CheckOp g n e
checkEachRule doc = doc2Errors funcNet funcRule doc
  where funcNet :: Network g n e -> [INError g n e]
	funcNet = const []

	-- funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
	funcRule rule = (Just Lhs, checkLHS (getPalette doc) lhs)
			: checkMapping (getMapping rule)
					(fst $ sepInterface lhs)
					(fst . sepInterface $ getRHS rule)
		where lhs = getLHS rule

--  | LHS should be exactly two agents different from interface connected trough their
--  principal ports with the rest of the ports connected to one interface agent.
checkLHS :: Palette n -> Network g n e -> [INError g n e]
checkLHS palette = either (const []) id . checkLHS' palette

checkLHS' :: Palette n -> Network g n e -> Either (String, String) [INError g n e]
checkLHS' palette net =
    case sepInterface net of
	(iNs, [(xNr,x), (yNr,y)]) ->
	  case (getPorts palette net xNr, getPorts palette net yNr) of
	    (Just (px:pxs), Just (py:pys)) ->
	 	case findEdge xNr (fst px) yNr (fst py) net of
		  Nothing -> Right [NoActivePair x y]
		  Just ed ->
		   let mINs = map (otherExtremeOfEdgeConnectedOnPort net xNr . fst) pxs
				++ map (otherExtremeOfEdgeConnectedOnPort net yNr . fst) pys
		   in if all isJust mINs
			then
			  let iNs' = map (id >< const "interface") iNs
			      cons = map fromJust mINs
			      dif1 = cons \\ iNs' -- multiple edges between agents x and y
			      dif2 = iNs' \\ cons -- interface nodes not connected to agent x or y
			  in if null dif1 && null dif2
				then Left (getShape x,getShape y)
				else Right $ toError1 dif1 ++ map (toError2 ed) dif2
			else Right [] -- disconnected ports checked in another piece of code



	    (psx, psy) -> Right . map (AgentNoPorts . snd) $ filter (maybe True null . fst) [(psx,x),(psy,y)]
	(_, lAs)     -> Right [Not2Agents $ map snd lAs]
  where
	toError1 :: [(NodeNr, PortName)] -> [INError g n e]
	toError1 = map aux3 . groupBy aux2 . map aux
	aux = id /\ fromJust . uncurry (edgeConnectedOnPort net)
	aux2 a b = snd a == snd b
	aux3 :: [((NodeNr,PortName),EdgeNr)] -> INError g n e
	aux3 [(from,edge), (to,_)] = ExtraEdge edge from to
	aux3 _ = error "unexpected situation"
	toError2 ed (nNr,_) = InterfaceBadConnected nNr ed


-- | Every interface agent in the LHS (respectively RHS) of a rule is mapped to
--   one interface agent in the RHS (respectively LHS).
checkMapping :: Mapping -> [(NodeNr,Node n)] -> [(NodeNr,Node n)] -> [(Maybe Side, [INError g n e])]
checkMapping mapR lhsI rhsI =
	[ (Just Lhs, map errL $ lhs \\ domMap )
	, (Just Rhs, map errR $ rhs \\ rangeMap)
	, (Nothing, (uncurry (++) . (map errNotInj >< map errNoDom  ) . partition (`elem` lhs) $ domMap   \\ lhs )
			++
		    (uncurry (++) . (map errNotFunc >< map errNoRang) . partition (`elem` rhs) $ rangeMap \\ rhs )

	  )
	]
  where
	(domMap, rangeMap) = unzip mapR :: ([NodeNr], [NodeNr])
	lhs = map fst lhsI
	rhs = map fst rhsI

	errL nNr   = UnMappedInterface . fromJust $ lookup nNr lhsI
	errR nNr   = UnMappedInterface . fromJust $ lookup nNr rhsI
	errNotInj  = MappingNotInj  mapR
	errNoDom   = MappingNoDom   mapR
	errNotFunc = MappingNotFunc mapR
	errNoRang  = MappingNoRang  mapR

insertIf :: Ord k => k -> [a] -> Map k [a] -> Map k [a]
insertIf k a mapp | null a = mapp
		  | otherwise = Map.insertWith (++) k a mapp

checkAgents :: CheckOp g n e
checkAgents doc =
	insertIf PALETTE (map toError3 . filter badInterface $ shaps)
	. insertIf PALETTE (map toError4 $ filter repeatedPorts shaps)
	. insertIf PALETTE (map toError2 $ filter noPorts shaps)
	. insertIf PALETTE (map toError . repeateds $ symbs)
	$ undefinedAgents symbs doc
  where
	shaps = shapes $ getPalette doc
	symbs = map fst shaps
	toError (symb, i) = MultiDef symb i
	toError2 = SymbolNoPorts . fst
	toError3 (_, (shape, mPorts, _)) = BadInterfaceSymbol shape mPorts
	toError4 (shapeName, (_, ports, _)) = SymbolRepeatedPorts shapeName . filter ((/=1) . snd) . repeateds $ map fst ports
	noPorts = null . snd3 . snd
	repeatedPorts = haveRepeateds . map fst . snd3 . snd
	fstsnd (a,b,_) = (a,b)

	badInterface ("interface", (_, [("interface",_)], _)) = False
	badInterface ("interface", _) = True
	badInterface _ = False

-- | Check if there are undefined agents.
undefinedAgents :: [String] -> CheckOp g n e
undefinedAgents symbols = doc2Errors funcNet funcRule
  where funcNet :: Network g n e -> [INError g n e]
	funcNet = undefinedAgentNet symbols

	funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
	funcRule rule =
		[ (Just Lhs, undefinedAgentNet symbols $ getLHS rule)
		, (Just Rhs, undefinedAgentNet symbols $ getRHS rule)
		]

undefinedAgentNet :: [String] -> Network g n e -> [INError g n e]
undefinedAgentNet symbols = uncurry (++)
	. ( (map UndefAgent . filter undefs) /\ (map BadInterfaceAgent . filter badInterfaceNode) )
	. getNodes
  where
	undefs = (`notElem` symbols) . getShape
	badInterfaceNode node = (\str -> str == fst interfaceSymbol && not (isInterfaceNode (0,node)) )
				  $ getShape node

-- | Checks if there are at most one rule per pair of agents.
checkNoRepeatedRules :: CheckOp g n e
checkNoRepeatedRules doc =
	(\lErrors -> insertIf RULES lErrors Map.empty)
	. map toError . filter dups . groupBy activePair
	. map left . filter isLeft
	. map (INRule.getName /\ checkLHS' (getPalette doc) .getLHS) . getRules
	$ doc
  where
	isLeft = either (const True) (const False) . snd
	left = id >< either id (error "This shouldn't happen")
	activePair :: (RuleName, (String,String)) -> (RuleName, (String,String)) -> Bool
	activePair (_,shapes1) (_,shapes2) = shapes1 == shapes2 || shapes1 == swap shapes2
	dups = (> 1) . length
	toError :: [(RuleName, (String,String))] -> INError g n e
	toError ( (ruleName,(shape1,shape2)):xs) = MultRulesSameLHS shape1 shape2 $ ruleName : map fst xs
------------------------------------------------------------------------------------------------------------------

-- | Checks if declared management agents are defined in the exactly same way that they are in the default palette.
-- Useful to avoid posterior problems with templates.
manCheck :: Check g n e
manCheck =
	( "Check management agents"
	, "Check if management agents are defined in the exact same way that in 'ManagementAgents.INblobpalette' to avoid troubles with templates."
	, "Management agents definitions match."
	, "Management agent(s) definitions don't match"
	, manCheck'
	)

manCheck' :: CheckOp g n e
manCheck' doc =
	emptyOrSingle PALETTE
	. Map.elems
	. mapMaybeWithKey aux
	. uncurry ( Map.intersectionWith (,) )
	. ( Map.fromList >< Map.fromList )
	$ (shapes $ getPalette doc, shapes specialSymbols)

	where aux :: String -> ((a,Ports,c),(a,Ports,c)) -> Maybe (INError g n e)
	      aux k ((_, ports1,_), (_, ports2,_))
			| ports1 == ports2 = Nothing
			| otherwise = Just $ SymbolDiffPorts k ports1 ports2

mapMaybeWithKey :: Ord k => (k -> a -> Maybe b) -> Map k a -> Map k b
-- In GHC 6.6:
-- mapMaybeWithKey = Map.mapMaybeWithKey
-- Allowing retro-compatibility with GHC 6.4
mapMaybeWithKey f = Map.foldWithKey aux Map.empty
	where -- aux :: k -> a -> Map k b -> Map k b
	      aux k a = case f k a of
			    Nothing -> id
			    Just b  -> Map.insert k b