    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE DeriveGeneric             #-}
    {-# LANGUAGE MultiWayIf                #-}
    {-# LANGUAGE OverloadedStrings         #-}
    {-# LANGUAGE ScopedTypeVariables       #-}
    -- Copyright 2020 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 specification into a standalone Copilot specification.
    module Command.Standalone
        ( command
        , commandLogic
        , AppData
        , CommandOptions(..)
        , ErrorCode
        )
      where

    -- External imports
    import Control.Applicative  ((<|>))
    import Control.Exception    as E
    import Control.Monad.Except (ExceptT (..), liftEither)
    import Data.Aeson           (ToJSON (..))
    import Data.Maybe           (fromMaybe)
    import GHC.Generics         (Generic)

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

    -- Internal imports
    import Command.Common
    import Command.Errors                 (ErrorCode, ErrorTriplet(..))
    import Command.Result                 (Result (..))
    import Data.Aeson.Extra               (mergeObjects)
    import Data.Either.Extra              (mapLeft)
    import Data.ExprPair                  (ExprPair(..), ExprPairT(..), exprPair)
    import Data.Location                  (Location (..))
    import Data.Spec.Extra                (addMissingIdentifiers)
    import Data.Spec.Parser               (readInputExpr)
    import Language.Trans.Diagram2Copilot (DiagramMode (..), diagram2CopilotSpec)
    import Language.Trans.Spec2Copilot    (spec2Copilot, specAnalyze)

    -- | Generate a new standalone Copilot monitor that implements the spec in 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 @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers
    -- used are valid C99 identifiers. The template, if provided, exists and uses
    -- the variables needed by the standalone application generator. The target
    -- directory is writable and there's enough disk space to copy the files over.
    command :: CommandOptions -- ^ Customization options
            -> IO (Result ErrorCode)
    command :: CommandOptions -> IO (Result ErrorCode)
    command CommandOptions
    options = ExceptT ErrorTriplet IO () -> IO (Result ErrorCode)
    forall (m :: * -> *) a.
    Monad m =>
    ExceptT ErrorTriplet m a -> m (Result ErrorCode)
    processResult (ExceptT ErrorTriplet IO () -> IO (Result ErrorCode))
    -> ExceptT ErrorTriplet IO () -> IO (Result ErrorCode)
    forall a b. (a -> b) -> a -> b
    $ do
        -- Obtain template dir
        templateDir <- Maybe FilePath -> FilePath -> ExceptT ErrorTriplet IO FilePath
    forall e. Maybe FilePath -> FilePath -> ExceptT e IO FilePath
    locateTemplateDir Maybe FilePath
    mTemplateDir FilePath
    "standalone"

        templateVars <- parseTemplateVarsFile templateVarsF

        appData <- command' options functions

        let subst = Value -> Value -> Value
    mergeObjects (AppData -> Value
    forall a. ToJSON a => a -> Value
    toJSON AppData
    appData) Value
    templateVars

        -- Expand template
        ExceptT $ fmap (makeLeftE cannotCopyTemplate) $ E.try $
          copyTemplate templateDir subst targetDir

      where

        targetDir :: FilePath
    targetDir     = CommandOptions -> FilePath
    commandTargetDir CommandOptions
    options
        mTemplateDir :: Maybe FilePath
    mTemplateDir  = CommandOptions -> Maybe FilePath
    commandTemplateDir CommandOptions
    options
        functions :: ExprPair
    functions     = FilePath -> ExprPair
    exprPair (CommandOptions -> FilePath
    commandPropFormat CommandOptions
    options)
        templateVarsF :: Maybe FilePath
    templateVarsF = CommandOptions -> Maybe FilePath
    commandExtraVars CommandOptions
    options

    -- | Generate a new standalone Copilot monitor that implements the spec in 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 @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers
    -- used are valid C99 identifiers. The template, if provided, exists and uses
    -- the variables needed by the standalone application generator. The target
    -- directory is writable and there's enough disk space to copy the files over.
    command' :: CommandOptions
             -> ExprPair
             -> ExceptT ErrorTriplet IO AppData
    command' :: CommandOptions -> ExprPair -> ExceptT ErrorTriplet IO AppData
    command' CommandOptions
    options (ExprPair ExprPairT a
    exprT) = do

        -- Read spec and complement the specification with any missing/implicit
        -- definitions.
        specT <- ExceptT ErrorTriplet IO (Maybe (InputFile a))
    -> (FilePath -> ExceptT ErrorTriplet IO (Maybe (InputFile a)))
    -> Maybe FilePath
    -> ExceptT ErrorTriplet IO (Maybe (InputFile a))
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Maybe (InputFile a)
    -> ExceptT ErrorTriplet IO (Maybe (InputFile a))
    forall a. a -> ExceptT ErrorTriplet IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (InputFile a)
    forall a. Maybe a
    Nothing) (\FilePath
    e -> InputFile a -> Maybe (InputFile a)
    forall a. a -> Maybe a
    Just (InputFile a -> Maybe (InputFile a))
    -> (Spec a -> InputFile a) -> Spec a -> Maybe (InputFile a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Spec a -> InputFile a
    forall a. Spec a -> InputFile a
    InputFileSpec (Spec a -> Maybe (InputFile a))
    -> ExceptT ErrorTriplet IO (Spec a)
    -> ExceptT ErrorTriplet IO (Maybe (InputFile a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FilePath -> ExceptT ErrorTriplet IO (Spec a)
    readInputExpr' FilePath
    e) Maybe FilePath
    triggerExprM
        specF <- if null fpA
                      then return Nothing
                      else do
                        fpA' <- mapM readInputFile' fpA
                        let fpA'' = [InputFile a] -> [InputFile a]
    forall a. [InputFile a] -> [InputFile a]
    combineInputFiles [InputFile a]
    fpA'
                        if length fpA'' > 1
                          then liftEither $ Left commandMultipleInputTypes
                          else pure $ Just $ head fpA''

        let spec = Maybe (InputFile a)
    specT Maybe (InputFile a) -> Maybe (InputFile a) -> Maybe (InputFile a)
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Maybe (InputFile a)
    specF

        case spec of
          Maybe (InputFile a)
    Nothing    -> Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
    forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
    liftEither (Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData)
    -> Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
    forall a b. (a -> b) -> a -> b
    $ ErrorTriplet -> Either ErrorTriplet AppData
    forall a b. a -> Either a b
    Left (ErrorTriplet -> Either ErrorTriplet AppData)
    -> ErrorTriplet -> Either ErrorTriplet AppData
    forall a b. (a -> b) -> a -> b
    $ ErrorTriplet
    commandMissingSpec
          Just InputFile a
    spec' -> Maybe FilePath
    -> [FilePath]
    -> FilePath
    -> [(FilePath, FilePath)]
    -> ExprPairT a
    -> InputFile a
    -> ExceptT ErrorTriplet IO AppData
    forall a.
    Maybe FilePath
    -> [FilePath]
    -> FilePath
    -> [(FilePath, FilePath)]
    -> ExprPairT a
    -> InputFile a
    -> ExceptT ErrorTriplet IO AppData
    commandLogic Maybe FilePath
    triggerExprM [FilePath]
    fpA FilePath
    name [(FilePath, FilePath)]
    typeMaps ExprPairT a
    exprT InputFile a
    spec'

      where
        triggerExprM :: Maybe FilePath
    triggerExprM   = CommandOptions -> Maybe FilePath
    commandConditionExpr CommandOptions
    options
        fpA :: [FilePath]
    fpA            = CommandOptions -> [FilePath]
    commandInputFiles CommandOptions
    options
        name :: FilePath
    name           = CommandOptions -> FilePath
    commandFilename CommandOptions
    options
        typeMaps :: [(FilePath, FilePath)]
    typeMaps       = [(FilePath, FilePath)] -> [(FilePath, FilePath)]
    typeToCopilotTypeMapping (CommandOptions -> [(FilePath, FilePath)]
    commandTypeMapping CommandOptions
    options)
        formatName :: FilePath
    formatName     = CommandOptions -> FilePath
    commandFormat CommandOptions
    options
        propFormatName :: FilePath
    propFormatName = CommandOptions -> FilePath
    commandPropFormat CommandOptions
    options
        propVia :: Maybe FilePath
    propVia        = CommandOptions -> Maybe FilePath
    commandPropVia CommandOptions
    options

        readInputExpr' :: FilePath -> ExceptT ErrorTriplet IO (Spec a)
    readInputExpr' FilePath
    e =
          FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (Spec a)
    forall a.
    FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (Spec a)
    readInputExpr FilePath
    e FilePath
    propFormatName Maybe FilePath
    propVia ExprPairT a
    exprT

        readInputFile' :: FilePath -> ExceptT ErrorTriplet IO (InputFile a)
    readInputFile' FilePath
    f =
          FilePath
    -> FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (InputFile a)
    forall a.
    FilePath
    -> FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (InputFile a)
    parseInputFile FilePath
    f FilePath
    formatName FilePath
    propFormatName Maybe FilePath
    propVia ExprPairT a
    exprT

    -- | Generate the data of a new standalone Copilot monitor that implements the
    -- spec, using a subexpression handler.
    commandLogic :: Maybe String
                 -> [FilePath]
                 -> String
                 -> [(String, String)]
                 -> ExprPairT a
                 -> InputFile a
                 -> ExceptT ErrorTriplet IO AppData
    commandLogic :: forall a.
    Maybe FilePath
    -> [FilePath]
    -> FilePath
    -> [(FilePath, FilePath)]
    -> ExprPairT a
    -> InputFile a
    -> ExceptT ErrorTriplet IO AppData
    commandLogic Maybe FilePath
    expr [FilePath]
    fps FilePath
    name [(FilePath, FilePath)]
    typeMaps ExprPairT a
    exprT (InputFileDiagram Diagram
    d) =
        AppData -> ExceptT ErrorTriplet IO AppData
    forall a. a -> ExceptT ErrorTriplet IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AppData -> ExceptT ErrorTriplet IO AppData)
    -> AppData -> ExceptT ErrorTriplet IO AppData
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> FilePath -> FilePath -> FilePath -> AppData
    AppData [] FilePath
    int [] FilePath
    trigs FilePath
    name
      where
        (FilePath
    int, FilePath
    trigs) = Diagram -> DiagramMode -> (FilePath, FilePath)
    diagram2CopilotSpec Diagram
    d DiagramMode
    ComputeState

    commandLogic Maybe FilePath
    expr [FilePath]
    fps FilePath
    name [(FilePath, FilePath)]
    typeMaps ExprPairT a
    exprT (InputFileSpec Spec a
    input) = do
        let spec :: Spec a
    spec = (a -> [FilePath]) -> Spec a -> Spec a
    forall a. (a -> [FilePath]) -> Spec a -> Spec a
    addMissingIdentifiers a -> [FilePath]
    ids Spec a
    input
        -- Analyze the spec for incorrect identifiers and convert it to Copilot.
        -- If there is an error, we change the error to a message we control.
        let appData :: Either ErrorTriplet AppData
    appData = (FilePath -> ErrorTriplet)
    -> Either FilePath AppData -> Either ErrorTriplet AppData
    forall a c b. (a -> c) -> Either a b -> Either c b
    mapLeft FilePath -> ErrorTriplet
    commandIncorrectSpec' (Either FilePath AppData -> Either ErrorTriplet AppData)
    -> Either FilePath AppData -> Either ErrorTriplet AppData
    forall a b. (a -> b) -> a -> b
    $ do
              spec' <- Spec a -> Either FilePath (Spec a)
    forall a. Spec a -> Either FilePath (Spec a)
    specAnalyze Spec a
    spec
              res   <- spec2Copilot name typeMaps replace print spec'

              -- Pack the results
              let (ext, int, reqs, trigs, specN) = res

              return $ AppData ext int reqs trigs specN

        Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
    forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
    liftEither Either ErrorTriplet AppData
    appData

      where

        commandIncorrectSpec' :: FilePath -> ErrorTriplet
    commandIncorrectSpec' = case (Maybe FilePath
    expr, [FilePath]
    fps) of
          (Maybe FilePath
    Nothing,    [])   -> FilePath -> FilePath -> ErrorTriplet
    forall a. HasCallStack => FilePath -> a
    error FilePath
    "Both expression and file are missing"
          (Maybe FilePath
    Nothing,    [FilePath]
    fps') -> FilePath -> ErrorTriplet
    commandIncorrectSpecF
          (Just FilePath
    expr', [FilePath]
    _)    -> FilePath -> FilePath -> ErrorTriplet
    commandIncorrectSpecE FilePath
    expr'

        ExprPairT FilePath -> Either FilePath a
    parse [(FilePath, FilePath)] -> a -> a
    replace a -> FilePath
    print a -> [FilePath]
    ids a
    def = ExprPairT a
    exprT

    -- ** Argument processing

    -- | Options used to customize the conversion of specifications to Copilot
    -- code.
    data CommandOptions = CommandOptions
      { CommandOptions -> Maybe FilePath
    commandConditionExpr :: Maybe String
      , CommandOptions -> [FilePath]
    commandInputFiles  :: [FilePath]         -- ^ Input specification file(s).
      , CommandOptions -> FilePath
    commandTargetDir   :: FilePath           -- ^ Target directory where the
                                                 -- application should be created.
      , CommandOptions -> Maybe FilePath
    commandTemplateDir :: Maybe FilePath     -- ^ Directory where the template
                                                 -- is to be found.
      , CommandOptions -> FilePath
    commandFormat      :: String             -- ^ Format of the input file.
      , CommandOptions -> FilePath
    commandPropFormat  :: String             -- ^ Format used for input
                                                 -- properties.
      , CommandOptions -> [(FilePath, FilePath)]
    commandTypeMapping :: [(String, String)]
      , CommandOptions -> FilePath
    commandFilename    :: String
      , CommandOptions -> Maybe FilePath
    commandPropVia     :: Maybe String       -- ^ Use external command to
                                                 -- pre-process system properties.
      , CommandOptions -> Maybe FilePath
    commandExtraVars   :: Maybe FilePath -- ^ File containing additional
                                             -- variables to make available to the
                                             -- template.
      }

    -- * Mapping of types from input format to Copilot
    typeToCopilotTypeMapping :: [(String, String)] -> [(String, String)]
    typeToCopilotTypeMapping :: [(FilePath, FilePath)] -> [(FilePath, FilePath)]
    typeToCopilotTypeMapping [(FilePath, FilePath)]
    types =
        [ (FilePath
    "bool",    FilePath
    "Bool")
        , (FilePath
    "int",     FilePath
    intType)
        , (FilePath
    "integer", FilePath
    intType)
        , (FilePath
    "real",    FilePath
    realType)
        , (FilePath
    "string",  FilePath
    "String")
        , (FilePath
    "",        FilePath
    "_")
        ]
      where
        intType :: FilePath
    intType  = FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    "Int64" (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup FilePath
    "int" [(FilePath, FilePath)]
    types
        realType :: FilePath
    realType = FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    "Float" (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup FilePath
    "real" [(FilePath, FilePath)]
    types

    -- | Data that may be relevant to generate a ROS application.
    data AppData = AppData
        { AppData -> FilePath
    externs   :: String
        , AppData -> FilePath
    internals :: String
        , AppData -> FilePath
    reqs      :: String
        , AppData -> FilePath
    triggers  :: String
        , AppData -> FilePath
    specName  :: String
        }
      deriving ((forall x. AppData -> Rep AppData x)
    -> (forall x. Rep AppData x -> AppData) -> Generic AppData
    forall x. Rep AppData x -> AppData
    forall x. AppData -> Rep AppData x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. AppData -> Rep AppData x
    from :: forall x. AppData -> Rep AppData x
    $cto :: forall x. Rep AppData x -> AppData
    to :: forall x. Rep AppData x -> AppData
    Generic)

    instance ToJSON AppData

    -- | Error message associated to not having a spec of any kind.
    commandMissingSpec :: ErrorTriplet
    commandMissingSpec :: ErrorTriplet
    commandMissingSpec =
        ErrorCode -> FilePath -> Location -> ErrorTriplet
    ErrorTriplet ErrorCode
    ecMissingSpec FilePath
    msg Location
    LocationNothing
      where
        msg :: FilePath
    msg =
          FilePath
    "No input specification has been provided."

    -- | Error message associated to having multiple input files of incompatible
    -- types.
    commandMultipleInputTypes :: ErrorTriplet
    commandMultipleInputTypes :: ErrorTriplet
    commandMultipleInputTypes =
        ErrorCode -> FilePath -> Location -> ErrorTriplet
    ErrorTriplet ErrorCode
    ecMultipleInputTypes FilePath
    msg Location
    LocationNothing
      where
        msg :: FilePath
    msg =
          FilePath
    "Too many inputs provided. Provide one diagram or multiple specs."

    -- | Error message associated to not being able to formalize the input spec.
    commandIncorrectSpecF :: String -> ErrorTriplet
    commandIncorrectSpecF :: FilePath -> ErrorTriplet
    commandIncorrectSpecF FilePath
    e =
        ErrorCode -> FilePath -> Location -> ErrorTriplet
    ErrorTriplet ErrorCode
    ecIncorrectSpec FilePath
    msg Location
    LocationNothing
      where
        msg :: FilePath
    msg =
          FilePath
    "The input specification(s) canbot be formalized: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    e

    -- | Error message associated to not being able to formalize the input spec.
    commandIncorrectSpecE :: String -> String -> ErrorTriplet
    commandIncorrectSpecE :: FilePath -> FilePath -> ErrorTriplet
    commandIncorrectSpecE FilePath
    expr FilePath
    e =
        ErrorCode -> FilePath -> Location -> ErrorTriplet
    ErrorTriplet ErrorCode
    ecIncorrectSpec FilePath
    msg Location
    LocationNothing
      where
        msg :: FilePath
    msg =
          FilePath
    "The input specification " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    expr FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " cannot be formalized: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    e

    -- ** Error codes

    -- | Error: there is no input argument.
    ecMissingSpec :: ErrorCode
    ecMissingSpec :: ErrorCode
    ecMissingSpec = ErrorCode
    1

    -- | Error: multiple inputs of incompatible types.
    ecMultipleInputTypes :: ErrorCode
    ecMultipleInputTypes :: ErrorCode
    ecMultipleInputTypes = ErrorCode
    1

    -- | Error: the input specification cannot be formalized.
    ecIncorrectSpec :: ErrorCode
    ecIncorrectSpec :: ErrorCode
    ecIncorrectSpec = ErrorCode
    1