{-# 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
--
-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
-- IT "AS IS."
--
-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
-- AGREEMENT.
--
-- | 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."