    {-# LANGUAGE DeriveGeneric #-}
    -- 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.
    --
    -- | Produce a report of the diagrams and requirements in the input files.
    module Command.Report
        ( command
        , CommandOptions(..)
        , CommandSummary(..)
        , ErrorCode
        )
      where

    -- External imports
    import qualified Control.Exception      as E
    import           Control.Monad.Except   (ExceptT (..), liftEither, withExceptT)
    import           Control.Monad.IO.Class (liftIO)
    import           Data.Aeson             (ToJSON (..))
    import           GHC.Generics           (Generic)

    -- External imports: Ogma
    import Data.OgmaSpec          (Requirement (..), Spec (..))
    import Data.String.Extra      (sanitizeUCIdentifier)
    import System.Directory.Extra (copyTemplate)

    -- Internal imports
    import           Command.Common              (InputFile (..),
                                                  cannotCopyTemplate,
                                                  locateTemplateDir, makeLeftE,
                                                  parseInputFile, processResult)
    import           Command.Errors              (ErrorCode, ErrorTriplet (..))
    import           Command.Result              (Result (..))
    import           Data.Diagram.Analysis       (AnalysisResult (..),
                                                  analyzeDiagram)
    import           Data.ExprPair               (ExprPair (..), ExprPairT (..),
                                                  exprPair)
    import           Data.Location               (Location (..))
    import qualified Data.Spec.Analysis          as SpecAnalysis
    import           Data.Spec.Extra             (addMissingIdentifiers)
    import qualified Language.Trans.Spec2Copilot as Spec2Copilot

    -- | Generate report of a spec or diagram given 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@. The template,
    -- if provided, exists and uses the variables needed by the report 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
    "report"

        let functions = FilePath -> ExprPair
    exprPair (CommandOptions -> FilePath
    commandPropFormat CommandOptions
    options)

        reportData <- command' options functions

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

      where

        targetDir :: FilePath
    targetDir    = CommandOptions -> FilePath
    commandTargetDir CommandOptions
    options
        mTemplateDir :: Maybe FilePath
    mTemplateDir = CommandOptions -> Maybe FilePath
    commandTemplateDir CommandOptions
    options

    -- | Generate report of a spec or diagram given 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@. The template,
    -- if provided, exists and uses the variables needed by the report application
    -- generator. The target directory is writable and there's enough disk space to
    -- copy the files over.
    command' :: CommandOptions
             -> ExprPair
             -> ExceptT ErrorTriplet IO CommandSummary
    command' :: CommandOptions
    -> ExprPair -> ExceptT ErrorTriplet IO CommandSummary
    command' CommandOptions
    options (ExprPair ExprPairT a
    exprT) = do
        res <- 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
    fp FilePath
    formatName FilePath
    propFormatName Maybe FilePath
    propVia ExprPairT a
    exprT
        case res of
          InputFileDiagram Diagram
    diagramR -> do
            analysisResult <- IO AnalysisResult -> ExceptT ErrorTriplet IO AnalysisResult
    forall a. IO a -> ExceptT ErrorTriplet IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AnalysisResult -> ExceptT ErrorTriplet IO AnalysisResult)
    -> IO AnalysisResult -> ExceptT ErrorTriplet IO AnalysisResult
    forall a b. (a -> b) -> a -> b
    $ Diagram -> IO AnalysisResult
    analyzeDiagram Diagram
    diagramR
            let diagramDetails = ErrorCode -> Bool -> DiagramDetails
    DiagramDetails
                                   (AnalysisResult -> ErrorCode
    numStates AnalysisResult
    analysisResult)
                                   (AnalysisResult -> Bool
    deterministic AnalysisResult
    analysisResult)

            pure $ CommandSummary
                     { commandExternalVariables      = 0
                     , commandInternalVariables      = 0
                     , commandRequirementsAny        = False
                     , commandRequirements           = 0
                     , commandRequirementsTrue       = 0
                     , commandRequirementsFalse      = 0
                     , commandRequirementsConsistent = True
                     , commandRequirementList        = []
                     , commandDiagramsAny            = True
                     , commandDiagrams               = 1
                     , commandDiagramList            = [diagramDetails]
                     }

          InputFileSpec Spec a
    spec -> (FilePath -> ErrorTriplet)
    -> ExceptT FilePath IO CommandSummary
    -> ExceptT ErrorTriplet IO CommandSummary
    forall (m :: * -> *) e e' a.
    Functor m =>
    (e -> e') -> ExceptT e m a -> ExceptT e' m a
    withExceptT FilePath -> ErrorTriplet
    commandCannotAnalyzeF (ExceptT FilePath IO CommandSummary
     -> ExceptT ErrorTriplet IO CommandSummary)
    -> ExceptT FilePath IO CommandSummary
    -> ExceptT ErrorTriplet IO CommandSummary
    forall a b. (a -> b) -> a -> b
    $ do
            let specCompleted :: Spec a
    specCompleted = (a -> [FilePath]) -> Spec a -> Spec a
    forall a. (a -> [FilePath]) -> Spec a -> Spec a
    addMissingIdentifiers a -> [FilePath]
    ids Spec a
    spec
            specAnalyzed <- Either FilePath (Spec a) -> ExceptT FilePath IO (Spec a)
    forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
    liftEither (Either FilePath (Spec a) -> ExceptT FilePath IO (Spec a))
    -> Either FilePath (Spec a) -> ExceptT FilePath IO (Spec a)
    forall a b. (a -> b) -> a -> b
    $ Spec a -> Either FilePath (Spec a)
    forall a. Spec a -> Either FilePath (Spec a)
    Spec2Copilot.specAnalyze Spec a
    specCompleted

            specFormalAnalysis <- ExceptT $
              SpecAnalysis.specAnalyze [] replace printExpr specCompleted

            let numExterns  = [ExternalVariableDef] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length ([ExternalVariableDef] -> ErrorCode)
    -> [ExternalVariableDef] -> ErrorCode
    forall a b. (a -> b) -> a -> b
    $ Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    specAnalyzed
                numInternal = [InternalVariableDef] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length ([InternalVariableDef] -> ErrorCode)
    -> [InternalVariableDef] -> ErrorCode
    forall a b. (a -> b) -> a -> b
    $ Spec a -> [InternalVariableDef]
    forall a. Spec a -> [InternalVariableDef]
    internalVariables Spec a
    specAnalyzed

                numReqs        = [Requirement a] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length [Requirement a]
    reqList
                reqList        = Spec a -> [Requirement a]
    forall a. Spec a -> [Requirement a]
    requirements Spec a
    specAnalyzed
                reqListDetails = (Requirement a -> RequirementDetails)
    -> [Requirement a] -> [RequirementDetails]
    forall a b. (a -> b) -> [a] -> [b]
    map Requirement a -> RequirementDetails
    forall {a}. Requirement a -> RequirementDetails
    reqDetailsF [Requirement a]
    reqList
                reqDetailsF Requirement a
    x  =
                  FilePath -> FilePath -> Bool -> Bool -> RequirementDetails
    RequirementDetails
                    (Requirement a -> FilePath
    forall a. Requirement a -> FilePath
    requirementName Requirement a
    x)
                    (Requirement a -> FilePath
    forall a. Requirement a -> FilePath
    requirementDescription Requirement a
    x)
                    (FilePath -> FilePath
    requirementNameAsProp (Requirement a -> FilePath
    forall a. Requirement a -> FilePath
    requirementName Requirement a
    x) FilePath -> [FilePath] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [FilePath]
    trueReqs)
                    (FilePath -> FilePath
    requirementNameAsProp (Requirement a -> FilePath
    forall a. Requirement a -> FilePath
    requirementName Requirement a
    x) FilePath -> [FilePath] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [FilePath]
    falseReqs)

                numTrues   = AnalysisResult -> ErrorCode
    SpecAnalysis.numAlwaysTrue  AnalysisResult
    specFormalAnalysis
                numFalses  = AnalysisResult -> ErrorCode
    SpecAnalysis.numAlwaysFalse AnalysisResult
    specFormalAnalysis
                trueReqs   = AnalysisResult -> [FilePath]
    SpecAnalysis.alwaysTrueReq  AnalysisResult
    specFormalAnalysis
                falseReqs  = AnalysisResult -> [FilePath]
    SpecAnalysis.alwaysFalseReq AnalysisResult
    specFormalAnalysis
                consistent = AnalysisResult -> Bool
    SpecAnalysis.consistent     AnalysisResult
    specFormalAnalysis

            pure $ CommandSummary
                     { commandExternalVariables      = numExterns
                     , commandInternalVariables      = numInternal
                     , commandRequirementsAny        = numReqs > 0
                     , commandRequirements           = numReqs
                     , commandRequirementsTrue       = numTrues
                     , commandRequirementsFalse      = numFalses
                     , commandRequirementsConsistent = consistent
                     , commandRequirementList        = reqListDetails
                     , commandDiagramsAny            = False
                     , commandDiagrams               = 0
                     , commandDiagramList            = []
                     }

      where

        fp :: FilePath
    fp             = CommandOptions -> FilePath
    commandInputFile 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

        ExprPairT FilePath -> Either FilePath a
    _parse [(FilePath, FilePath)] -> a -> a
    replace a -> FilePath
    printExpr a -> [FilePath]
    ids a
    _def = ExprPairT a
    exprT

    -- | Options used to customize the interpretation of input specifications and
    -- the resulting report.
    data CommandOptions = CommandOptions
      { CommandOptions -> FilePath
    commandTargetDir   :: String
      , CommandOptions -> Maybe FilePath
    commandTemplateDir :: Maybe String
      , CommandOptions -> FilePath
    commandInputFile   :: String
      , CommandOptions -> FilePath
    commandFormat      :: String
      , CommandOptions -> FilePath
    commandPropFormat  :: String
      , CommandOptions -> Maybe FilePath
    commandPropVia     :: Maybe String
      }

    -- | Summary of the files read.
    data CommandSummary = CommandSummary
        { CommandSummary -> ErrorCode
    commandExternalVariables      :: Int
        , CommandSummary -> ErrorCode
    commandInternalVariables      :: Int
        , CommandSummary -> Bool
    commandRequirementsAny        :: Bool
        , CommandSummary -> ErrorCode
    commandRequirements           :: Int
        , CommandSummary -> ErrorCode
    commandRequirementsTrue       :: Int
        , CommandSummary -> ErrorCode
    commandRequirementsFalse      :: Int
        , CommandSummary -> Bool
    commandRequirementsConsistent :: Bool
        , CommandSummary -> [RequirementDetails]
    commandRequirementList        :: [RequirementDetails]
        , CommandSummary -> Bool
    commandDiagramsAny            :: Bool
        , CommandSummary -> ErrorCode
    commandDiagrams               :: Int
        , CommandSummary -> [DiagramDetails]
    commandDiagramList            :: [DiagramDetails]
        }
      deriving ((forall x. CommandSummary -> Rep CommandSummary x)
    -> (forall x. Rep CommandSummary x -> CommandSummary)
    -> Generic CommandSummary
    forall x. Rep CommandSummary x -> CommandSummary
    forall x. CommandSummary -> Rep CommandSummary x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. CommandSummary -> Rep CommandSummary x
    from :: forall x. CommandSummary -> Rep CommandSummary x
    $cto :: forall x. Rep CommandSummary x -> CommandSummary
    to :: forall x. Rep CommandSummary x -> CommandSummary
    Generic, ErrorCode -> CommandSummary -> FilePath -> FilePath
    [CommandSummary] -> FilePath -> FilePath
    CommandSummary -> FilePath
    (ErrorCode -> CommandSummary -> FilePath -> FilePath)
    -> (CommandSummary -> FilePath)
    -> ([CommandSummary] -> FilePath -> FilePath)
    -> Show CommandSummary
    forall a.
    (ErrorCode -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    $cshowsPrec :: ErrorCode -> CommandSummary -> FilePath -> FilePath
    showsPrec :: ErrorCode -> CommandSummary -> FilePath -> FilePath
    $cshow :: CommandSummary -> FilePath
    show :: CommandSummary -> FilePath
    $cshowList :: [CommandSummary] -> FilePath -> FilePath
    showList :: [CommandSummary] -> FilePath -> FilePath
    Show)

    instance ToJSON CommandSummary

    -- | Information to include in a report about a requirement.
    data RequirementDetails = RequirementDetails
        { RequirementDetails -> FilePath
    summaryRequirementName  :: String
        , RequirementDetails -> FilePath
    summaryRequirementDesc  :: String
        , RequirementDetails -> Bool
    summaryRequirementTrue  :: Bool
        , RequirementDetails -> Bool
    summaryRequirementFalse :: Bool
        }
      deriving ((forall x. RequirementDetails -> Rep RequirementDetails x)
    -> (forall x. Rep RequirementDetails x -> RequirementDetails)
    -> Generic RequirementDetails
    forall x. Rep RequirementDetails x -> RequirementDetails
    forall x. RequirementDetails -> Rep RequirementDetails x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. RequirementDetails -> Rep RequirementDetails x
    from :: forall x. RequirementDetails -> Rep RequirementDetails x
    $cto :: forall x. Rep RequirementDetails x -> RequirementDetails
    to :: forall x. Rep RequirementDetails x -> RequirementDetails
    Generic, ErrorCode -> RequirementDetails -> FilePath -> FilePath
    [RequirementDetails] -> FilePath -> FilePath
    RequirementDetails -> FilePath
    (ErrorCode -> RequirementDetails -> FilePath -> FilePath)
    -> (RequirementDetails -> FilePath)
    -> ([RequirementDetails] -> FilePath -> FilePath)
    -> Show RequirementDetails
    forall a.
    (ErrorCode -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    $cshowsPrec :: ErrorCode -> RequirementDetails -> FilePath -> FilePath
    showsPrec :: ErrorCode -> RequirementDetails -> FilePath -> FilePath
    $cshow :: RequirementDetails -> FilePath
    show :: RequirementDetails -> FilePath
    $cshowList :: [RequirementDetails] -> FilePath -> FilePath
    showList :: [RequirementDetails] -> FilePath -> FilePath
    Show)

    instance ToJSON RequirementDetails

    -- | Information to include in a report about a diagram.
    data DiagramDetails = DiagramDetails
        { DiagramDetails -> ErrorCode
    summaryDiagramNumStates     :: Int
        , DiagramDetails -> Bool
    summaryDiagramDeterministic :: Bool
        }
      deriving ((forall x. DiagramDetails -> Rep DiagramDetails x)
    -> (forall x. Rep DiagramDetails x -> DiagramDetails)
    -> Generic DiagramDetails
    forall x. Rep DiagramDetails x -> DiagramDetails
    forall x. DiagramDetails -> Rep DiagramDetails x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DiagramDetails -> Rep DiagramDetails x
    from :: forall x. DiagramDetails -> Rep DiagramDetails x
    $cto :: forall x. Rep DiagramDetails x -> DiagramDetails
    to :: forall x. Rep DiagramDetails x -> DiagramDetails
    Generic, ErrorCode -> DiagramDetails -> FilePath -> FilePath
    [DiagramDetails] -> FilePath -> FilePath
    DiagramDetails -> FilePath
    (ErrorCode -> DiagramDetails -> FilePath -> FilePath)
    -> (DiagramDetails -> FilePath)
    -> ([DiagramDetails] -> FilePath -> FilePath)
    -> Show DiagramDetails
    forall a.
    (ErrorCode -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    $cshowsPrec :: ErrorCode -> DiagramDetails -> FilePath -> FilePath
    showsPrec :: ErrorCode -> DiagramDetails -> FilePath -> FilePath
    $cshow :: DiagramDetails -> FilePath
    show :: DiagramDetails -> FilePath
    $cshowList :: [DiagramDetails] -> FilePath -> FilePath
    showList :: [DiagramDetails] -> FilePath -> FilePath
    Show)

    instance ToJSON DiagramDetails

    -- * Errors

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

    -- ** Error codes

    -- | Error: the input file cannot be analyzed.
    ecCannotAnalyzeError :: ErrorCode
    ecCannotAnalyzeError :: ErrorCode
    ecCannotAnalyzeError = ErrorCode
    1

    -- * Auxiliary functions

    -- | Name of a requirement when used as a property or handler in a
    -- Copilot specification.
    requirementNameAsProp :: String -> String
    requirementNameAsProp :: FilePath -> FilePath
    requirementNameAsProp FilePath
    x = FilePath
    "prop" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    sanitizeUCIdentifier FilePath
    x