{-# 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