    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE FlexibleContexts          #-}
    {-# LANGUAGE OverloadedStrings         #-}
    -- Copyright 2024 United States Government as represented by the Administrator
    -- of the National Aeronautics and Space Administration. All Rights Reserved.
    --
    -- Disclaimers
    --
    -- Licensed under the Apache License, Version 2.0 (the "License"); you may
    -- not use this file except in compliance with the License. You may obtain a
    -- copy of the License at
    --
    --      https://www.apache.org/licenses/LICENSE-2.0
    --
    -- Unless required by applicable law or agreed to in writing, software
    -- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
    -- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
    -- License for the specific language governing permissions and limitations
    -- under the License.
    --
    -- | Transform a state diagram into a Copilot specification.
    module Command.Diagram
        ( diagram
        , DiagramOptions(..)
        , DiagramFormat(..)
        , DiagramMode(..)
        , DiagramPropFormat(..)
        , ErrorCode
        )
      where

    -- External imports
    import           Control.Exception                 as E
    import           Control.Monad                     (when)
    import           Data.Aeson                        (object, (.=))
    import           Data.ByteString.Lazy              (toStrict)
    import qualified Data.ByteString.Lazy              as B
    import           Data.Either                       (isLeft)
    import           Data.Foldable                     (for_)
    import           Data.Functor.Identity             (Identity)
    import           Data.GraphViz                     (graphEdges)
    import qualified Data.GraphViz                     as G
    import qualified Data.GraphViz.Attributes.Complete as Attributes
    import           Data.GraphViz.Commands.IO         (toUTF8)
    import qualified Data.GraphViz.Parsing             as G
    import           Data.GraphViz.PreProcessing       (preProcess)
    import qualified Data.GraphViz.Types.Generalised   as Gs
    import           Data.List                         (intercalate, nub, sort)
    import qualified Data.Set                          as Set
    import           Data.Text                         (Text)
    import qualified Data.Text                         as T
    import qualified Data.Text.Encoding                as T
    import           Data.Text.Lazy                    (pack)
    import qualified Data.Text.Lazy                    as LT
    import           Data.Void                         (Void)
    import           System.FilePath                   ((</>))
    import           Text.Megaparsec                   (ErrorFancy (ErrorFail),
                                                        ParsecT, empty,
                                                        errorBundlePretty,
                                                        fancyFailure, many,
                                                        manyTill, noneOf, parse)
    import           Text.Megaparsec.Char              (alphaNumChar, char,
                                                        digitChar, newline, space1,
                                                        string)
    import qualified Text.Megaparsec.Char.Lexer        as L

    -- External imports: auxiliary
    import Data.ByteString.Extra  as B ( safeReadFile )
    import System.Directory.Extra ( copyTemplate )

    -- External imports: parsing expressions.
    import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec)
    import qualified Language.SMV.ParSMV       as SMV (myLexer, pBoolSpec)

    -- Internal imports: auxiliary
    import Command.Result  (Result (..))
    import Data.Location   (Location (..))
    import Paths_ogma_core (getDataDir)

    -- Internal imports: language ASTs, transformers
    import           Language.SMV.Substitution     (substituteBoolExpr)
    import qualified Language.Trans.Lustre2Copilot as Lustre (boolSpec2Copilot,
                                                              boolSpecNames)
    import           Language.Trans.SMV2Copilot    as SMV (boolSpec2Copilot,
                                                           boolSpecNames)

    -- | Generate a new Copilot monitor that implements a state machine described
    -- in a diagram given as an input file.
    --
    -- PRE: The file given is readable, contains a valid file with recognizable
    -- format, the formulas in the file do not use any identifiers that exist in
    -- Copilot, or any of @stateMachine@, @externalState@, @noneOf@,
    -- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,
    -- @notPreviousNot@. All identifiers used are valid C99 identifiers. The
    -- template, if provided, exists and uses the variables needed by the diagram
    -- application generator. The target directory is writable and there's enough
    -- disk space to copy the files over.
    diagram :: FilePath       -- ^ Path to a file containing a diagram
            -> DiagramOptions -- ^ Customization options
            -> IO (Result ErrorCode)
    diagram :: [Char] -> DiagramOptions -> IO (Result Int)
    diagram [Char]
    fp DiagramOptions
    options = do
      (SomeException -> IO (Result Int))
    -> IO (Result Int) -> IO (Result Int)
    forall e a. Exception e => (e -> IO a) -> IO a -> IO a
    E.handle (Result Int -> IO (Result Int)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result Int -> IO (Result Int))
    -> (SomeException -> Result Int)
    -> SomeException
    -> IO (Result Int)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> SomeException -> Result Int
    diagramTemplateError [Char]
    fp) (IO (Result Int) -> IO (Result Int))
    -> IO (Result Int) -> IO (Result Int)
    forall a b. (a -> b) -> a -> b
    $ do
        -- Sub-parser for edge expressions.
        let functions :: ExprPair
    functions = DiagramPropFormat -> ExprPair
    exprPair (DiagramOptions -> DiagramPropFormat
    diagramPropFormat DiagramOptions
    options)

        -- Convert the diagram into elements in a Copilot spec.
        Either [Char] ([Char], [Char])
    copilotSpecElems <- [Char]
    -> DiagramOptions
    -> ExprPair
    -> IO (Either [Char] ([Char], [Char]))
    diagram' [Char]
    fp DiagramOptions
    options ExprPair
    functions

        -- Convert the elements into a success or error result.
        let (Maybe ([Char], [Char])
    mOutput, Result Int
    result) = [Char]
    -> Either [Char] ([Char], [Char])
    -> (Maybe ([Char], [Char]), Result Int)
    forall a. [Char] -> Either [Char] a -> (Maybe a, Result Int)
    diagramResult [Char]
    fp Either [Char] ([Char], [Char])
    copilotSpecElems

        -- If the result is success, expand the template.
        Maybe ([Char], [Char]) -> (([Char], [Char]) -> IO ()) -> IO ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    t a -> (a -> f b) -> f ()
    for_ Maybe ([Char], [Char])
    mOutput ((([Char], [Char]) -> IO ()) -> IO ())
    -> (([Char], [Char]) -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ \([Char]
    streamDefs, [Char]
    handlerInputs) -> do
          let subst :: Value
    subst = [Pair] -> Value
    object
                        [ Key
    "streamDefs"    Key -> Text -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    forall v. ToJSON v => Key -> v -> Pair
    .= [Char] -> Text
    pack [Char]
    streamDefs
                        , Key
    "specName"      Key -> Text -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    forall v. ToJSON v => Key -> v -> Pair
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramFilename DiagramOptions
    options)
                        , Key
    "input"         Key -> Text -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    forall v. ToJSON v => Key -> v -> Pair
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramInputVar DiagramOptions
    options)
                        , Key
    "state"         Key -> Text -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    forall v. ToJSON v => Key -> v -> Pair
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramStateVar DiagramOptions
    options)
                        , Key
    "handlerInputs" Key -> Text -> Pair
    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
    forall v. ToJSON v => Key -> v -> Pair
    .= [Char] -> Text
    pack [Char]
    handlerInputs
                        ]

          [Char]
    templateDir <- case DiagramOptions -> Maybe [Char]
    diagramTemplateDir DiagramOptions
    options of
                           Just [Char]
    x  -> [Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Char]
    x
                           Maybe [Char]
    Nothing -> do
                             [Char]
    dataDir <- IO [Char]
    getDataDir
                             [Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    dataDir [Char] -> [Char] -> [Char]
    </> [Char]
    "templates" [Char] -> [Char] -> [Char]
    </> [Char]
    "diagram"

          let targetDir :: [Char]
    targetDir = DiagramOptions -> [Char]
    diagramTargetDir DiagramOptions
    options

          [Char] -> Value -> [Char] -> IO ()
    copyTemplate [Char]
    templateDir Value
    subst [Char]
    targetDir

        Result Int -> IO (Result Int)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result Int
    result

    -- | Generate a new Copilot monitor that implements a state machine described
    -- in a diagram given as an input file, using a subexpression handler.
    --
    -- PRE: The file given is readable, contains a valid file with recognizable
    -- format, the formulas in the file do not use any identifiers that exist in
    -- Copilot, or any of @stateMachine@, @externalState@, @noneOf@,
    -- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,
    -- @notPreviousNot@. All identifiers used are valid C99 identifiers. The
    -- template, if provided, exists and uses the variables needed by the diagram
    -- application generator. The target directory is writable and there's enough
    -- disk space to copy the files over.
    diagram' :: FilePath
             -> DiagramOptions
             -> ExprPair
             -> IO (Either String (String, String))
    diagram' :: [Char]
    -> DiagramOptions
    -> ExprPair
    -> IO (Either [Char] ([Char], [Char]))
    diagram' [Char]
    fp DiagramOptions
    options ExprPair
    exprP = do
      Either [Char] ByteString
    contentEither <- [Char] -> IO (Either [Char] ByteString)
    B.safeReadFile [Char]
    fp
      Either [Char] ([Char], [Char])
    -> IO (Either [Char] ([Char], [Char]))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either [Char] ([Char], [Char])
     -> IO (Either [Char] ([Char], [Char])))
    -> Either [Char] ([Char], [Char])
    -> IO (Either [Char] ([Char], [Char]))
    forall a b. (a -> b) -> a -> b
    $ do
        -- All of the following operations use Either to return error messages. The
        -- use of the monadic bind to pass arguments from one function to the next
        -- will cause the program to stop at the earliest error.
        ByteString
    diagFileContent <- Either [Char] ByteString
    contentEither

        -- Abtract representation of a state machine diagram.
        Diagram
    diagramR <- DiagramFormat -> ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagram (DiagramOptions -> DiagramFormat
    diagramFormat DiagramOptions
    options) ByteString
    diagFileContent ExprPair
    exprP

        ([Char], [Char]) -> Either [Char] ([Char], [Char])
    forall a. a -> Either [Char] a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Char], [Char]) -> Either [Char] ([Char], [Char]))
    -> ([Char], [Char]) -> Either [Char] ([Char], [Char])
    forall a b. (a -> b) -> a -> b
    $ Diagram -> DiagramMode -> ([Char], [Char])
    diagramToCopilot Diagram
    diagramR (DiagramOptions -> DiagramMode
    diagramMode DiagramOptions
    options)

    -- | Options used to customize the conversion of diagrams to Copilot code.
    data DiagramOptions = DiagramOptions
      { DiagramOptions -> [Char]
    diagramTargetDir   :: FilePath
      , DiagramOptions -> Maybe [Char]
    diagramTemplateDir :: Maybe FilePath
      , DiagramOptions -> DiagramFormat
    diagramFormat      :: DiagramFormat
      , DiagramOptions -> DiagramPropFormat
    diagramPropFormat  :: DiagramPropFormat
      , DiagramOptions -> [Char]
    diagramFilename    :: String
      , DiagramOptions -> DiagramMode
    diagramMode        :: DiagramMode
      , DiagramOptions -> [Char]
    diagramStateVar    :: String
      , DiagramOptions -> [Char]
    diagramInputVar    :: String
      }

    -- | Modes of operation.
    data DiagramMode = CheckState   -- ^ Check if given state matches expectation
                     | ComputeState -- ^ Compute expected state
                     | CheckMoves   -- ^ Check if transitioning to a state would be
                                    --   possible.
      deriving (DiagramMode -> DiagramMode -> Bool
    (DiagramMode -> DiagramMode -> Bool)
    -> (DiagramMode -> DiagramMode -> Bool) -> Eq DiagramMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DiagramMode -> DiagramMode -> Bool
    == :: DiagramMode -> DiagramMode -> Bool
    $c/= :: DiagramMode -> DiagramMode -> Bool
    /= :: DiagramMode -> DiagramMode -> Bool
    Eq, Int -> DiagramMode -> [Char] -> [Char]
    [DiagramMode] -> [Char] -> [Char]
    DiagramMode -> [Char]
    (Int -> DiagramMode -> [Char] -> [Char])
    -> (DiagramMode -> [Char])
    -> ([DiagramMode] -> [Char] -> [Char])
    -> Show DiagramMode
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> DiagramMode -> [Char] -> [Char]
    showsPrec :: Int -> DiagramMode -> [Char] -> [Char]
    $cshow :: DiagramMode -> [Char]
    show :: DiagramMode -> [Char]
    $cshowList :: [DiagramMode] -> [Char] -> [Char]
    showList :: [DiagramMode] -> [Char] -> [Char]
    Show)

    -- | Diagram formats supported.
    data DiagramFormat = Mermaid
                       | Dot
      deriving (DiagramFormat -> DiagramFormat -> Bool
    (DiagramFormat -> DiagramFormat -> Bool)
    -> (DiagramFormat -> DiagramFormat -> Bool) -> Eq DiagramFormat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DiagramFormat -> DiagramFormat -> Bool
    == :: DiagramFormat -> DiagramFormat -> Bool
    $c/= :: DiagramFormat -> DiagramFormat -> Bool
    /= :: DiagramFormat -> DiagramFormat -> Bool
    Eq, Int -> DiagramFormat -> [Char] -> [Char]
    [DiagramFormat] -> [Char] -> [Char]
    DiagramFormat -> [Char]
    (Int -> DiagramFormat -> [Char] -> [Char])
    -> (DiagramFormat -> [Char])
    -> ([DiagramFormat] -> [Char] -> [Char])
    -> Show DiagramFormat
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> DiagramFormat -> [Char] -> [Char]
    showsPrec :: Int -> DiagramFormat -> [Char] -> [Char]
    $cshow :: DiagramFormat -> [Char]
    show :: DiagramFormat -> [Char]
    $cshowList :: [DiagramFormat] -> [Char] -> [Char]
    showList :: [DiagramFormat] -> [Char] -> [Char]
    Show)

    -- | Property formats supported.
    data DiagramPropFormat = Lustre
                           | Inputs
                           | Literal
                           | SMV
      deriving (DiagramPropFormat -> DiagramPropFormat -> Bool
    (DiagramPropFormat -> DiagramPropFormat -> Bool)
    -> (DiagramPropFormat -> DiagramPropFormat -> Bool)
    -> Eq DiagramPropFormat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DiagramPropFormat -> DiagramPropFormat -> Bool
    == :: DiagramPropFormat -> DiagramPropFormat -> Bool
    $c/= :: DiagramPropFormat -> DiagramPropFormat -> Bool
    /= :: DiagramPropFormat -> DiagramPropFormat -> Bool
    Eq, Int -> DiagramPropFormat -> [Char] -> [Char]
    [DiagramPropFormat] -> [Char] -> [Char]
    DiagramPropFormat -> [Char]
    (Int -> DiagramPropFormat -> [Char] -> [Char])
    -> (DiagramPropFormat -> [Char])
    -> ([DiagramPropFormat] -> [Char] -> [Char])
    -> Show DiagramPropFormat
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> DiagramPropFormat -> [Char] -> [Char]
    showsPrec :: Int -> DiagramPropFormat -> [Char] -> [Char]
    $cshow :: DiagramPropFormat -> [Char]
    show :: DiagramPropFormat -> [Char]
    $cshowList :: [DiagramPropFormat] -> [Char] -> [Char]
    showList :: [DiagramPropFormat] -> [Char] -> [Char]
    Show)

    -- * Error codes

    -- | Encoding of reasons why the command can fail.
    --
    -- The error code used is 1 for user error.
    type ErrorCode = Int

    -- | Error: the input file cannot be read due to it being unreadable or the
    -- format being incorrect.
    ecDiagramError :: ErrorCode
    ecDiagramError :: Int
    ecDiagramError = Int
    1

    -- | Error: diagram component generation failed during the copy/write
    -- process.
    ecDiagramTemplateError :: ErrorCode
    ecDiagramTemplateError :: Int
    ecDiagramTemplateError = Int
    2

    -- * Result

    -- | Process the result of the transformation function.
    diagramResult :: FilePath
                  -> Either String a
                  -> (Maybe a, Result ErrorCode)
    diagramResult :: forall a. [Char] -> Either [Char] a -> (Maybe a, Result Int)
    diagramResult [Char]
    fp Either [Char] a
    result = case Either [Char] a
    result of
      Left [Char]
    msg -> (Maybe a
    forall a. Maybe a
    Nothing, Int -> [Char] -> Location -> Result Int
    forall a. a -> [Char] -> Location -> Result a
    Error Int
    ecDiagramError [Char]
    msg ([Char] -> Location
    LocationFile [Char]
    fp))
      Right a
    t  -> (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    t,  Result Int
    forall a. Result a
    Success)

    -- | Report an error when trying to open or copy the template.
    diagramTemplateError :: FilePath
                         -> E.SomeException
                         -> Result ErrorCode
    diagramTemplateError :: [Char] -> SomeException -> Result Int
    diagramTemplateError [Char]
    fp SomeException
    exception =
        Int -> [Char] -> Location -> Result Int
    forall a. a -> [Char] -> Location -> Result a
    Error Int
    ecDiagramTemplateError [Char]
    msg ([Char] -> Location
    LocationFile [Char]
    fp)
      where
        msg :: [Char]
    msg =
          [Char]
    "Diagram monitor generation failed during copy/write operation. Check"
          [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " that there's free space in the disk and that you have the necessary"
          [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " permissions to write in the destination directory. "
          [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SomeException -> [Char]
    forall a. Show a => a -> [Char]
    show SomeException
    exception

    -- * Handler for boolean expressions in edges or transitions between states.

    -- | Handler for boolean expressions that knows how to parse them, replace
    -- variables in them, and convert them to Copilot.
    data ExprPair = forall a . ExprPair
      { ()
    _exprParse   :: String -> Either String a
      , ()
    _exprReplace :: [(String, String)] -> a -> a
      , ()
    _exprPrint   :: a -> String
      , ()
    _exprIdents  :: a -> [String]
      }

    -- | Return a handler depending on the format used for edge or transition
    -- properties.
    exprPair :: DiagramPropFormat -> ExprPair
    exprPair :: DiagramPropFormat -> ExprPair
    exprPair DiagramPropFormat
    Lustre  = ([Char] -> Either [Char] BoolSpec)
    -> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
    -> (BoolSpec -> [Char])
    -> (BoolSpec -> [[Char]])
    -> ExprPair
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> ExprPair
    ExprPair ([Token] -> Either [Char] BoolSpec
    Lustre.pBoolSpec ([Token] -> Either [Char] BoolSpec)
    -> ([Char] -> [Token]) -> [Char] -> Either [Char] BoolSpec
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [Token]
    Lustre.myLexer)
                                (\[([Char], [Char])]
    _ -> BoolSpec -> BoolSpec
    forall a. a -> a
    id)
                                BoolSpec -> [Char]
    Lustre.boolSpec2Copilot
                                BoolSpec -> [[Char]]
    Lustre.boolSpecNames
    exprPair DiagramPropFormat
    Inputs  = ([Char] -> Either [Char] Int)
    -> ([([Char], [Char])] -> Int -> Int)
    -> (Int -> [Char])
    -> (Int -> [[Char]])
    -> ExprPair
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> ExprPair
    ExprPair ((Int -> Either [Char] Int
    forall a b. b -> Either a b
    Right (Int -> Either [Char] Int)
    -> ([Char] -> Int) -> [Char] -> Either [Char] Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Int
    forall a. Read a => [Char] -> a
    read) :: String -> Either String Int)
                                (\[([Char], [Char])]
    _ -> Int -> Int
    forall a. a -> a
    id)
                                (\Int
    x -> [Char]
    "input == " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    x)
                                ([[Char]] -> Int -> [[Char]]
    forall a b. a -> b -> a
    const [])
    exprPair DiagramPropFormat
    Literal = ([Char] -> Either [Char] [Char])
    -> ([([Char], [Char])] -> [Char] -> [Char])
    -> ([Char] -> [Char])
    -> ([Char] -> [[Char]])
    -> ExprPair
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> ExprPair
    ExprPair [Char] -> Either [Char] [Char]
    forall a b. b -> Either a b
    Right
                                (\[([Char], [Char])]
    _ -> [Char] -> [Char]
    forall a. a -> a
    id)
                                [Char] -> [Char]
    forall a. a -> a
    id
                                ([[Char]] -> [Char] -> [[Char]]
    forall a b. a -> b -> a
    const [])
    exprPair DiagramPropFormat
    SMV     = ([Char] -> Either [Char] BoolSpec)
    -> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
    -> (BoolSpec -> [Char])
    -> (BoolSpec -> [[Char]])
    -> ExprPair
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> ExprPair
    ExprPair ([Token] -> Either [Char] BoolSpec
    SMV.pBoolSpec ([Token] -> Either [Char] BoolSpec)
    -> ([Char] -> [Token]) -> [Char] -> Either [Char] BoolSpec
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [Token]
    SMV.myLexer)
                                [([Char], [Char])] -> BoolSpec -> BoolSpec
    forall {t :: * -> *}.
    Foldable t =>
    t ([Char], [Char]) -> BoolSpec -> BoolSpec
    substituteBoolExpr
                                BoolSpec -> [Char]
    SMV.boolSpec2Copilot
                                BoolSpec -> [[Char]]
    SMV.boolSpecNames

    -- | Parse and print a value using an auxiliary Expression Pair.
    --
    -- Fails if the value has no valid parse.
    exprPairShow :: ExprPair -> String -> String
    exprPairShow :: ExprPair -> [Char] -> [Char]
    exprPairShow (ExprPair [Char] -> Either [Char] a
    parseProp [([Char], [Char])] -> a -> a
    _replace a -> [Char]
    printProp a -> [[Char]]
    _ids) =
      a -> [Char]
    printProp (a -> [Char]) -> ([Char] -> a) -> [Char] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Either [Char] a -> a
    forall a b. Either a b -> b
    fromRight' (Either [Char] a -> a)
    -> ([Char] -> Either [Char] a) -> [Char] -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Either [Char] a
    parseProp

    -- * Diagrams

    -- | Internal representation for diagrams.
    newtype Diagram = Diagram
        { Diagram -> [(Int, [Char], Int)]
    diagramTransitions :: [(Int, String, Int)]
        }
      deriving (Int -> Diagram -> [Char] -> [Char]
    [Diagram] -> [Char] -> [Char]
    Diagram -> [Char]
    (Int -> Diagram -> [Char] -> [Char])
    -> (Diagram -> [Char])
    -> ([Diagram] -> [Char] -> [Char])
    -> Show Diagram
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> Diagram -> [Char] -> [Char]
    showsPrec :: Int -> Diagram -> [Char] -> [Char]
    $cshow :: Diagram -> [Char]
    show :: Diagram -> [Char]
    $cshowList :: [Diagram] -> [Char] -> [Char]
    showList :: [Diagram] -> [Char] -> [Char]
    Show, Diagram -> Diagram -> Bool
    (Diagram -> Diagram -> Bool)
    -> (Diagram -> Diagram -> Bool) -> Eq Diagram
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Diagram -> Diagram -> Bool
    == :: Diagram -> Diagram -> Bool
    $c/= :: Diagram -> Diagram -> Bool
    /= :: Diagram -> Diagram -> Bool
    Eq)

    -- * Diagram parsers

    -- | Generic function to parse a diagram.
    parseDiagram :: DiagramFormat          -- ^ Format of the input file
                 -> B.ByteString           -- ^ Contents of the diagram
                 -> ExprPair               -- ^ Subparser for conditions or edge
                                           -- expressions
                 -> Either String Diagram
    parseDiagram :: DiagramFormat -> ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagram DiagramFormat
    Dot     = ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagramDot
    parseDiagram DiagramFormat
    Mermaid = ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagramMermaid

    -- ** Dot parser

    -- | Parse a DOT / Graphviz diagram.
    parseDiagramDot :: B.ByteString -> ExprPair -> Either String Diagram
    parseDiagramDot :: ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagramDot ByteString
    contents ExprPair
    exprP = do
        let contentsUTF8 :: Text
    contentsUTF8 = ByteString -> Text
    toUTF8 ByteString
    contents
        DotGraph Text
    dg <- (Either [Char] (DotGraph Text), Text)
    -> Either [Char] (DotGraph Text)
    forall a b. (a, b) -> a
    fst ((Either [Char] (DotGraph Text), Text)
     -> Either [Char] (DotGraph Text))
    -> (Either [Char] (DotGraph Text), Text)
    -> Either [Char] (DotGraph Text)
    forall a b. (a -> b) -> a -> b
    $ Parse (DotGraph Text)
    -> Text -> (Either [Char] (DotGraph Text), Text)
    forall a. Parse a -> Text -> (Either [Char] a, Text)
    G.runParser Parse (DotGraph Text)
    forall a. ParseDot a => Parse a
    G.parse (Text -> (Either [Char] (DotGraph Text), Text))
    -> Text -> (Either [Char] (DotGraph Text), Text)
    forall a b. (a -> b) -> a -> b
    $ Text -> Text
    preProcess Text
    contentsUTF8
        Diagram -> Either [Char] Diagram
    forall a. a -> Either [Char] a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Diagram -> Either [Char] Diagram)
    -> Diagram -> Either [Char] Diagram
    forall a b. (a -> b) -> a -> b
    $ DotGraph Text -> Diagram
    makeDiagram DotGraph Text
    dg
      where
        makeDiagram :: Gs.DotGraph LT.Text -> Diagram
        makeDiagram :: DotGraph Text -> Diagram
    makeDiagram DotGraph Text
    g = [(Int, [Char], Int)] -> Diagram
    Diagram [(Int, [Char], Int)]
    links
          where
            links :: [(Int, [Char], Int)]
    links = (DotEdge Text -> (Int, [Char], Int))
    -> [DotEdge Text] -> [(Int, [Char], Int)]
    forall a b. (a -> b) -> [a] -> [b]
    map DotEdge Text -> (Int, [Char], Int)
    forall {a} {c}. (Read a, Read c) => DotEdge Text -> (a, [Char], c)
    edgeToLink (DotGraph Text -> [DotEdge Text]
    forall (dg :: * -> *) n. DotRepr dg n => dg n -> [DotEdge n]
    graphEdges DotGraph Text
    g)

            edgeToLink :: DotEdge Text -> (a, [Char], c)
    edgeToLink DotEdge Text
    edge =
                ( [Char] -> a
    forall a. Read a => [Char] -> a
    read (Text -> [Char]
    LT.unpack Text
    o)
                , ExprPair -> [Char] -> [Char]
    exprPairShow ExprPair
    exprP (Text -> [Char]
    LT.unpack Text
    e)
                , [Char] -> c
    forall a. Read a => [Char] -> a
    read (Text -> [Char]
    LT.unpack Text
    d)
                )
              where
                o :: Text
    o = DotEdge Text -> Text
    forall n. DotEdge n -> n
    G.fromNode DotEdge Text
    edge
                d :: Text
    d = DotEdge Text -> Text
    forall n. DotEdge n -> n
    G.toNode DotEdge Text
    edge
                e :: Text
    e = [Attribute] -> Text
    getLabel (DotEdge Text -> [Attribute]
    forall n. DotEdge n -> [Attribute]
    G.edgeAttributes DotEdge Text
    edge)

                -- Extract the label from a list of attributes. If no label is
                -- found, it's assumed that the condition is the literal true.
                getLabel :: [Attribute] -> Text
    getLabel [] = Text
    "true"
                getLabel ((Attributes.Label (Attributes.StrLabel Text
    l)) : [Attribute]
    _) = Text
    l
                getLabel (Attribute
    _ : [Attribute]
    as) = [Attribute] -> Text
    getLabel [Attribute]
    as

    -- ** Mermaid parser

    -- | Parse a mermaid diagram.
    parseDiagramMermaid :: B.ByteString -> ExprPair -> Either String Diagram
    parseDiagramMermaid :: ByteString -> ExprPair -> Either [Char] Diagram
    parseDiagramMermaid ByteString
    txtDia ExprPair
    exprP =
        case Either (ParseErrorBundle Text Void) Diagram
    parsingResult of
          Left ParseErrorBundle Text Void
    e  -> [Char] -> Either [Char] Diagram
    forall a b. a -> Either a b
    Left (ParseErrorBundle Text Void -> [Char]
    forall s e.
    (VisualStream s, TraversableStream s, ShowErrorComponent e) =>
    ParseErrorBundle s e -> [Char]
    errorBundlePretty ParseErrorBundle Text Void
    e)
          Right Diagram
    x -> Diagram -> Either [Char] Diagram
    forall a b. b -> Either a b
    Right Diagram
    x
      where
        txt :: Text
    txt           = ByteString -> Text
    T.decodeUtf8 (ByteString -> ByteString
    toStrict ByteString
    txtDia)
        parsingResult :: Either (ParseErrorBundle Text Void) Diagram
    parsingResult = Parsec Void Text Diagram
    -> [Char] -> Text -> Either (ParseErrorBundle Text Void) Diagram
    forall e s a.
    Parsec e s a -> [Char] -> s -> Either (ParseErrorBundle s e) a
    parse (MermaidParser ()
    spaces MermaidParser ()
    -> Parsec Void Text Diagram -> Parsec Void Text Diagram
    forall a b.
    ParsecT Void Text Identity a
    -> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> ExprPair -> Parsec Void Text Diagram
    pDiagram ExprPair
    exprP) [Char]
    "<input>" Text
    txt

    -- | Type for parser for memaid diagrams.
    type MermaidParser = ParsecT Void Text Identity

    -- | Parser for a mermaid diagram.
    --
    -- This parser depends on an auxiliary parser for the expressions associated to
    -- the edges or connections between states.
    pDiagram :: ExprPair -> MermaidParser Diagram
    pDiagram :: ExprPair -> Parsec Void Text Diagram
    pDiagram ExprPair
    exprP = do
      Tokens Text
    _ <- Tokens Text -> ParsecT Void Text Identity (Tokens Text)
    forall e s (m :: * -> *).
    MonadParsec e s m =>
    Tokens s -> m (Tokens s)
    string Tokens Text
    "graph" ParsecT Void Text Identity (Tokens Text)
    -> MermaidParser () -> ParsecT Void Text Identity (Tokens Text)
    forall a b.
    ParsecT Void Text Identity a
    -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* MermaidParser ()
    spaces
      Text
    _name <- [Char] -> Text
    T.pack ([Char] -> Text)
    -> ParsecT Void Text Identity [Char]
    -> ParsecT Void Text Identity Text
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Void Text Identity Char
    -> ParsecT Void Text Identity Char
    -> ParsecT Void Text Identity [Char]
    forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
    manyTill ParsecT Void Text Identity Char
    ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m (Token s)
    alphaNumChar (Token Text -> ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    Token s -> m (Token s)
    char Char
    Token Text
    ';')
      Char
    _ <- ParsecT Void Text Identity Char
    ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m (Token s)
    newline

      [(Int, [Char], Int)]
    transitions <- ParsecT Void Text Identity (Int, [Char], Int)
    -> ParsecT Void Text Identity [(Int, [Char], Int)]
    forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
    many (ExprPair -> ParsecT Void Text Identity (Int, [Char], Int)
    pTransition ExprPair
    exprP)

      Diagram -> Parsec Void Text Diagram
    forall a. a -> ParsecT Void Text Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Diagram -> Parsec Void Text Diagram)
    -> Diagram -> Parsec Void Text Diagram
    forall a b. (a -> b) -> a -> b
    $ [(Int, [Char], Int)] -> Diagram
    Diagram [(Int, [Char], Int)]
    transitions

    -- | Parser for an edge in a state diagram.
    --
    -- This parser depends on an auxiliary parser for the expressions associated to
    -- the edges or connections between states.
    pTransition :: ExprPair -> MermaidParser (Int, String, Int)
    pTransition :: ExprPair -> ParsecT Void Text Identity (Int, [Char], Int)
    pTransition ep :: ExprPair
    ep@(ExprPair { _exprParse :: ()
    _exprParse = [Char] -> Either [Char] a
    parseProp }) = do
      ()
    _ <- MermaidParser ()
    spaces
      [Char]
    stateFrom <- ParsecT Void Text Identity Char
    -> ParsecT Void Text Identity [Char]
    forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
    many ParsecT Void Text Identity Char
    ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m (Token s)
    digitChar
      Tokens Text
    _ <- Tokens Text -> ParsecT Void Text Identity (Tokens Text)
    forall e s (m :: * -> *).
    MonadParsec e s m =>
    Tokens s -> m (Tokens s)
    string Tokens Text
    "-->|"
      [Char]
    edge <- ParsecT Void Text Identity Char
    -> ParsecT Void Text Identity [Char]
    forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
    many ([Token Text] -> ParsecT Void Text Identity (Token Text)
    forall (f :: * -> *) e s (m :: * -> *).
    (Foldable f, MonadParsec e s m) =>
    f (Token s) -> m (Token s)
    noneOf ([Char]
    "|" :: [Char]))

      let x :: Either [Char] a
    x = [Char] -> Either [Char] a
    parseProp [Char]
    edge
      Bool -> MermaidParser () -> MermaidParser ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Either [Char] a -> Bool
    forall a b. Either a b -> Bool
    isLeft Either [Char] a
    x) (MermaidParser () -> MermaidParser ())
    -> MermaidParser () -> MermaidParser ()
    forall a b. (a -> b) -> a -> b
    $ Set (ErrorFancy Void) -> MermaidParser ()
    forall e s (m :: * -> *) a.
    MonadParsec e s m =>
    Set (ErrorFancy e) -> m a
    fancyFailure (Set (ErrorFancy Void) -> MermaidParser ())
    -> Set (ErrorFancy Void) -> MermaidParser ()
    forall a b. (a -> b) -> a -> b
    $ ErrorFancy Void -> Set (ErrorFancy Void)
    forall a. a -> Set a
    Set.singleton (ErrorFancy Void -> Set (ErrorFancy Void))
    -> ErrorFancy Void -> Set (ErrorFancy Void)
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ErrorFancy Void
    forall e. [Char] -> ErrorFancy e
    ErrorFail ([Char] -> ErrorFancy Void) -> [Char] -> ErrorFancy Void
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Edge property has incorrect format: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    forall a. Show a => a -> [Char]
    show [Char]
    edge

      Char
    _ <- Token Text -> ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    Token s -> m (Token s)
    char Char
    Token Text
    '|'
      [Char]
    stateTo <- ParsecT Void Text Identity Char
    -> ParsecT Void Text Identity [Char]
    forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
    many ParsecT Void Text Identity Char
    ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m (Token s)
    digitChar
      Char
    _ <- Token Text -> ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    Token s -> m (Token s)
    char Char
    Token Text
    ';'
      Char
    _ <- ParsecT Void Text Identity Char
    ParsecT Void Text Identity (Token Text)
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m (Token s)
    newline
      (Int, [Char], Int) -> ParsecT Void Text Identity (Int, [Char], Int)
    forall a. a -> ParsecT Void Text Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> Int
    forall a. Read a => [Char] -> a
    read [Char]
    stateFrom, ExprPair -> [Char] -> [Char]
    exprPairShow ExprPair
    ep [Char]
    edge, [Char] -> Int
    forall a. Read a => [Char] -> a
    read [Char]
    stateTo)

    -- | Consume spaces
    spaces :: MermaidParser ()
    spaces :: MermaidParser ()
    spaces = MermaidParser ()
    -> MermaidParser () -> MermaidParser () -> MermaidParser ()
    forall e s (m :: * -> *).
    MonadParsec e s m =>
    m () -> m () -> m () -> m ()
    L.space MermaidParser ()
    forall e s (m :: * -> *).
    (MonadParsec e s m, Token s ~ Char) =>
    m ()
    space1 MermaidParser ()
    forall a. ParsecT Void Text Identity a
    forall (f :: * -> *) a. Alternative f => f a
    empty MermaidParser ()
    forall a. ParsecT Void Text Identity a
    forall (f :: * -> *) a. Alternative f => f a
    empty

    -- * Backend

    -- | Convert the diagram into a set of Copilot definitions, and a list of
    -- arguments for the top-level handler.
    diagramToCopilot :: Diagram -> DiagramMode -> (String, String)
    diagramToCopilot :: Diagram -> DiagramMode -> ([Char], [Char])
    diagramToCopilot Diagram
    diag DiagramMode
    mode = ([Char]
    machine, [Char]
    arguments)
      where
        machine :: [Char]
    machine = [[Char]] -> [Char]
    unlines
          [ [Char]
    "stateMachineProp :: Stream Bool"
          , [Char]
    "stateMachineProp = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    propExpr
          , [Char]
    ""
          , [Char]
    "stateMachine1 :: Stream Word8"
          , [Char]
    "stateMachine1 = stateMachineGF (initialState, finalState, noInput, "
            [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "transitions, badState)"
          , [Char]
    ""
          , [Char]
    "-- Check"
          , [Char]
    "initialState :: Word8"
          , [Char]
    "initialState = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    initialState
          , [Char]
    ""
          , [Char]
    "-- Check"
          , [Char]
    "finalState :: Word8"
          , [Char]
    "finalState = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    finalState
          , [Char]
    ""
          , [Char]
    "noInput :: Stream Bool"
          , [Char]
    "noInput = false"
          , [Char]
    ""
          , [Char]
    "badState :: Word8"
          , [Char]
    "badState = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    badState
          , [Char]
    ""
          , [Char]
    "transitions = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    showTransitions
          ]

        -- Elements of the spec.
        propExpr :: [Char]
    propExpr     = case DiagramMode
    mode of
                         DiagramMode
    CheckState   -> [Char]
    "stateMachine1 == externalState"
                         DiagramMode
    ComputeState -> [Char]
    "true"
                         DiagramMode
    CheckMoves   -> [Char]
    "true"
        initialState :: Int
    initialState = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [Int]
    states
        finalState :: Int
    finalState   = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Int]
    states
        badState :: Int
    badState     = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Int]
    states Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1

        -- Arguments for the handler.
        arguments :: [Char]
    arguments = [Char]
    "[ " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    ", " (([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "arg " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) [[Char]]
    argExprs) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " ]"

        argExprs :: [[Char]]
    argExprs = case DiagramMode
    mode of
          DiagramMode
    CheckState   -> [ [Char]
    "stateMachine1", [Char]
    "externalState", [Char]
    "input" ]
          DiagramMode
    ComputeState -> [ [Char]
    "stateMachine1", [Char]
    "externalState", [Char]
    "input" ]
          DiagramMode
    CheckMoves   -> (Int -> [Char]) -> [Int] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> [Char]
    forall a. Show a => a -> [Char]
    stateCheckExpr [Int]
    states

        stateCheckExpr :: a -> [Char]
    stateCheckExpr a
    stateId =
          [Char]
    "(checkValidTransition transitions externalState " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    stateId [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")"

        -- States and transitions from the diagram.
        transitions :: [(Int, [Char], Int)]
    transitions = Diagram -> [(Int, [Char], Int)]
    diagramTransitions Diagram
    diag
        states :: [Int]
    states      = [Int] -> [Int]
    forall a. Eq a => [a] -> [a]
    nub ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Int] -> [Int]
    forall a. Ord a => [a] -> [a]
    sort ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [[Int]] -> [Int]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Int
    x, Int
    y] | (Int
    x, [Char]
    _, Int
    y) <- [(Int, [Char], Int)]
    transitions ]

        showTransitions :: String
        showTransitions :: [Char]
    showTransitions = [Char]
    "[" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(Int, [Char], Int)] -> [Char]
    showTransitions' [(Int, [Char], Int)]
    transitions

        showTransitions' :: [(Int, String, Int)] -> String
        showTransitions' :: [(Int, [Char], Int)] -> [Char]
    showTransitions' []         = [Char]
    "]"
        showTransitions' ((Int, [Char], Int)
    x1:(Int, [Char], Int)
    x2:[(Int, [Char], Int)]
    xs) =
          (Int, [Char], Int) -> [Char]
    showTransition (Int, [Char], Int)
    x1 [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(Int, [Char], Int)] -> [Char]
    showTransitions' ((Int, [Char], Int)
    x2(Int, [Char], Int) -> [(Int, [Char], Int)] -> [(Int, [Char], Int)]
    forall a. a -> [a] -> [a]
    :[(Int, [Char], Int)]
    xs)
        showTransitions' ((Int, [Char], Int)
    x2:[])    = (Int, [Char], Int) -> [Char]
    showTransition (Int, [Char], Int)
    x2 [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "]"

        showTransition :: (Int, String, Int) -> String
        showTransition :: (Int, [Char], Int) -> [Char]
    showTransition (Int
    a, [Char]
    b, Int
    c) =
          [Char]
    "(" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    a [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    b [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    c [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")"

    -- * Auxiliary functions

    -- | Unsafe fromRight. Fails if the value is a 'Left'.
    fromRight' :: Either a b -> b
    fromRight' :: forall a b. Either a b -> b
    fromRight' (Right b
    v) = b
    v
    fromRight' Either a b
    _         = [Char] -> b
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "fromRight' applied to Left value."