{- |

Well-formedness checks for finite state machines.

-}

-- Copyright (c) 2009 Andy Gimblett - http://www.cs.swan.ac.uk/~csandy/
-- BSD Licence (see http://www.opensource.org/licenses/bsd-license.php)

module Data.FsmActions.WellFormed (
    WellFormed(..),
    isWellFormed,
    polishFSM
) where

import Control.Monad.Error
import qualified Data.Map as M
import qualified Data.List as L

import Data.FsmActions
import Data.FsmActions.Error
import {-# SOURCE #-} Data.FsmActions.Graph (weakCCs)

-- | An 'FSM' is well-formed if all its actions are the same length,
-- none of its actions contain destinations which are out of range,
-- and it is not disjoint.
data WellFormed sy
    -- | Lengths of Actions in the 'FSM' don't all match.  Carries a
    -- sorted list of (symbol, 'Action' length) pairs, one for every
    -- symbol in the alphabet of the 'FSM'.
    = BadLengths [(sy, Int)]
    -- | Some 'Action's contain out-of-range (negative or too-high)
    -- destinations.  Carries a sorted list of all such actions and
    -- their corresponding symbols.
    | BadActions [(sy, Action)]
    -- | The FSM is disconnected, i.e. not even weakly-connected.
    -- Carries a list of its weakly-connected components (each is a
    -- list of 'State's).
    | Disconnected [[State]]
    -- | Well-formed.
    | WellFormed
      deriving (Eq, Show)

-- | Check if an 'FSM' is well-formed or not.
isWellFormed :: Ord sy => FSM sy -> WellFormed sy
isWellFormed fsm
    | not $ allSame $ L.map snd actionLengths =
        BadLengths (L.sort actionLengths)
    | not $ M.null badParts = BadActions (L.sort $ M.toList badParts)
    | length wccs /= 1 = Disconnected wccs
    | otherwise = WellFormed
    where -- All (symbol, Action length) pairs in FSM.
          actionLengths = fsmMap (\s a -> (s, aLength a)) fsm
          -- Submap containing only Actions with bad destinations.
          -- XXX Re-improve this function; add natural map to FSM?
          badParts = M.filter isBad $ M.fromList $ toList fsm
          -- Check if an Action has any bad destinations.
          isBad a = any badDest (flatten a)
              where -- Flatten lists of destination states in an Action.
                    flatten (Action xs) = L.concatMap destinations xs
          -- Check if a destination is bad (negative or too high).
          badDest x = (x<0) || (x >= length  (states fsm))
          -- Compute the length of an action
          aLength (Action xs) = length xs
          -- Compute the FSM's undirected strongly-connected
          -- components.
          wccs = weakCCs fsm

-- | Given an FSM, normalise it and check it's well-formed.
--
-- This should be called whenever an FSM is read/computed from an
-- outside source.  If parsing, the right time to call this is
-- immediately after you've decided if the parse of the FSM was
-- successful or not.  (In other words, here are some static checks!)
polishFSM :: (Ord sy, Show sy) => FSM sy -> ReadFsmMonad (FSM sy)
polishFSM fsm =
    let norm = normalise fsm in
    case isWellFormed norm of
                WellFormed -> return norm
                Disconnected wccs ->
                    throwError (FsmError "FSM disconnected" (show wccs))
                err -> throwError (FsmError "FSM ill-formed" (show err))



-- Check if every element of a list is identical.
allSame :: Eq a => [a] -> Bool
allSame [] = True
allSame [_] = True
allSame (x:y:xs) = (x == y) && allSame (y:xs)