    {-# 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.Except (runExceptT)
    import Data.Aeson           (object, (.=))
    import Data.Foldable        (for_)
    import Data.Text.Lazy       (pack)
    import System.FilePath      ((</>))

    -- External imports: auxiliary
    import System.Directory.Extra ( copyTemplate )

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

    -- Internal imports: auxiliary
    import Command.Errors      (ErrorTriplet (..))
    import Command.Result      (Result (..))
    import Data.Diagram.Parser (DiagramFormat (..), readDiagram)
    import Data.ExprPair       (ExprPair (..), ExprPairT (..))
    import Data.Location       (Location (..))
    import Paths_ogma_core     (getDataDir)

    -- Internal imports: language ASTs, transformers
    import           Language.SMV.Substitution      (substituteBoolExpr)
    import           Language.Trans.Diagram2Copilot (DiagramMode (..),
                                                     diagram2CopilotSpec)
    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@, @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.
        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 (mOutput, result) = diagramResult fp copilotSpecElems

        -- If the result is success, expand the template.
        for_ mOutput $ \([Char]
    streamDefs, [Char]
    triggers) -> do
          let subst :: Value
    subst = [Pair] -> Value
    object
                        [ Key
    "streamDefs" Key -> Text -> Pair
    forall v. ToJSON v => Key -> v -> Pair
    forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
    .= [Char] -> Text
    pack [Char]
    streamDefs
                        , Key
    "specName"   Key -> Text -> Pair
    forall v. ToJSON v => Key -> v -> Pair
    forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramFilename DiagramOptions
    options)
                        , Key
    "input"      Key -> Text -> Pair
    forall v. ToJSON v => Key -> v -> Pair
    forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramInputVar DiagramOptions
    options)
                        , Key
    "state"      Key -> Text -> Pair
    forall v. ToJSON v => Key -> v -> Pair
    forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
    .= [Char] -> Text
    pack (DiagramOptions -> [Char]
    diagramStateVar DiagramOptions
    options)
                        , Key
    "triggers"   Key -> Text -> Pair
    forall v. ToJSON v => Key -> v -> Pair
    forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
    .= [Char] -> Text
    pack [Char]
    triggers
                        ]

          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
                             dataDir <- IO [Char]
    getDataDir
                             return $ dataDir </> "templates" </> "diagram"

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

          copyTemplate templateDir subst targetDir

        return 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@, @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
      diagramE <- ExceptT ErrorTriplet IO Diagram -> IO (Either ErrorTriplet Diagram)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT ErrorTriplet IO Diagram
     -> IO (Either ErrorTriplet Diagram))
    -> ExceptT ErrorTriplet IO Diagram
    -> IO (Either ErrorTriplet Diagram)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    -> DiagramFormat -> ExprPair -> ExceptT ErrorTriplet IO Diagram
    readDiagram [Char]
    fp (DiagramOptions -> DiagramFormat
    diagramFormat DiagramOptions
    options) ExprPair
    exprP
      case diagramE of
        Left (ErrorTriplet Int
    _ec [Char]
    msg Location
    _loc) -> Either [Char] ([Char], [Char])
    -> IO (Either [Char] ([Char], [Char]))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (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
    $ [Char] -> Either [Char] ([Char], [Char])
    forall a b. a -> Either a b
    Left [Char]
    msg
        Right Diagram
    diagramR ->
          Either [Char] ([Char], [Char])
    -> IO (Either [Char] ([Char], [Char]))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (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
    $ ([Char], [Char]) -> Either [Char] ([Char], [Char])
    forall a b. b -> Either a b
    Right (([Char], [Char]) -> Either [Char] ([Char], [Char]))
    -> ([Char], [Char]) -> Either [Char] ([Char], [Char])
    forall a b. (a -> b) -> a -> b
    $ Diagram -> DiagramMode -> ([Char], [Char])
    diagram2CopilotSpec 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
      }

    -- | 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.

    -- | Return a handler depending on the format used for edge or transition
    -- properties.
    exprPair :: DiagramPropFormat -> ExprPair
    exprPair :: DiagramPropFormat -> ExprPair
    exprPair DiagramPropFormat
    Lustre = ExprPairT BoolSpec -> ExprPair
    forall a. ExprPairT a -> ExprPair
    ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
    forall a b. (a -> b) -> a -> b
    $
      ([Char] -> Either [Char] BoolSpec)
    -> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
    -> (BoolSpec -> [Char])
    -> (BoolSpec -> [[Char]])
    -> BoolSpec
    -> ExprPairT BoolSpec
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> a
    -> ExprPairT a
    ExprPairT
        ([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
        (Ident -> BoolSpec
    Lustre.BoolSpecSignal ([Char] -> Ident
    Lustre.Ident [Char]
    "undefined"))
    exprPair DiagramPropFormat
    Inputs = ExprPairT Int -> ExprPair
    forall a. ExprPairT a -> ExprPair
    ExprPair (ExprPairT Int -> ExprPair) -> ExprPairT Int -> ExprPair
    forall a b. (a -> b) -> a -> b
    $
      ([Char] -> Either [Char] Int)
    -> ([([Char], [Char])] -> Int -> Int)
    -> (Int -> [Char])
    -> (Int -> [[Char]])
    -> Int
    -> ExprPairT Int
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> a
    -> ExprPairT a
    ExprPairT
        ((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 [])
        (-Int
    1)
    exprPair DiagramPropFormat
    Literal = ExprPairT [Char] -> ExprPair
    forall a. ExprPairT a -> ExprPair
    ExprPair (ExprPairT [Char] -> ExprPair) -> ExprPairT [Char] -> ExprPair
    forall a b. (a -> b) -> a -> b
    $
      ([Char] -> Either [Char] [Char])
    -> ([([Char], [Char])] -> [Char] -> [Char])
    -> ([Char] -> [Char])
    -> ([Char] -> [[Char]])
    -> [Char]
    -> ExprPairT [Char]
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> a
    -> ExprPairT a
    ExprPairT
        [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 [])
        [Char]
    "undefined"
    exprPair DiagramPropFormat
    SMV = ExprPairT BoolSpec -> ExprPair
    forall a. ExprPairT a -> ExprPair
    ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
    forall a b. (a -> b) -> a -> b
    $
      ([Char] -> Either [Char] BoolSpec)
    -> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
    -> (BoolSpec -> [Char])
    -> (BoolSpec -> [[Char]])
    -> BoolSpec
    -> ExprPairT BoolSpec
    forall a.
    ([Char] -> Either [Char] a)
    -> ([([Char], [Char])] -> a -> a)
    -> (a -> [Char])
    -> (a -> [[Char]])
    -> a
    -> ExprPairT a
    ExprPairT
        ([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
        (Ident -> BoolSpec
    SMV.BoolSpecSignal ([Char] -> Ident
    SMV.Ident [Char]
    "undefined"))

    -- * Backend