{-# 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(..)
    , ReportFile(..)
    , CommandSummary(..)
    , ErrorCode
    )
  where

-- External imports
import qualified Control.Exception      as E
import           Control.Monad          (foldM)
import           Control.Monad.Except   (ExceptT (..), liftEither, runExceptT,
                                         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"

    reportData <- foldM
                    processFile
                    emptyCommandSummary
                    (commandInputFiles options)

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

    processFile :: CommandSummary
                -> ReportFile
                -> ExceptT ErrorTriplet IO CommandSummary
    processFile :: CommandSummary
-> ReportFile -> ExceptT ErrorTriplet IO CommandSummary
processFile CommandSummary
acc ReportFile
file = do
      let functions :: ExprPair
functions = FilePath -> ExprPair
exprPair (ReportFile -> FilePath
reportFilePropFormat ReportFile
file)
      s <- CommandOptions
-> ExprPair -> ReportFile -> ExceptT ErrorTriplet IO CommandSummary
command' CommandOptions
options ExprPair
functions ReportFile
file
      return $ mergeCommandSummary acc s

-- | 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
         -> ReportFile
         -> ExceptT ErrorTriplet IO CommandSummary
command' :: CommandOptions
-> ExprPair -> ReportFile -> ExceptT ErrorTriplet IO CommandSummary
command' CommandOptions
options (ExprPair ExprPairT a
exprT) ReportFile
file = 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 = FilePath -> ErrorCode -> Bool -> CommandSummaryDiagram
CommandSummaryDiagram
                               FilePath
fp
                               (AnalysisResult -> ErrorCode
numStates AnalysisResult
analysisResult)
                               (AnalysisResult -> Bool
deterministic AnalysisResult
analysisResult)

        pure $ CommandSummary
                 { commandRequirementsAny = False
                 , commandRequirementList = []
                 , commandDiagramsList    = [ diagramDetails ]
                 , commandDiagramsAny     = True
                 }

      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

            fileReqs   = CommandSummaryRequirements
                           { summaryRequirementsFile :: FilePath
summaryRequirementsFile       = FilePath
fp
                           , summaryExternalVariables :: ErrorCode
summaryExternalVariables      = ErrorCode
numExterns
                           , summaryInternalVariables :: ErrorCode
summaryInternalVariables      = ErrorCode
numInternal
                           , summaryRequirements :: ErrorCode
summaryRequirements           = ErrorCode
numReqs
                           , summaryRequirementsTrue :: ErrorCode
summaryRequirementsTrue       = ErrorCode
numTrues
                           , summaryRequirementsFalse :: ErrorCode
summaryRequirementsFalse      = ErrorCode
numFalses
                           , summaryRequirementsConsistent :: Bool
summaryRequirementsConsistent = Bool
consistent
                           , summaryRequirementsDetails :: [RequirementDetails]
summaryRequirementsDetails    = [RequirementDetails]
reqListDetails
                           }

        pure $ CommandSummary
                 { commandRequirementsAny = length reqListDetails > 0
                 , commandRequirementList = [fileReqs]
                 , commandDiagramsAny     = False
                 , commandDiagramsList    = []
                 }

  where

    fp :: FilePath
fp             = ReportFile -> FilePath
reportFilePath ReportFile
file
    formatName :: FilePath
formatName     = ReportFile -> FilePath
reportFileFormat ReportFile
file
    propFormatName :: FilePath
propFormatName = ReportFile -> FilePath
reportFilePropFormat ReportFile
file
    propVia :: Maybe FilePath
propVia        = ReportFile -> Maybe FilePath
reportFilePropVia ReportFile
file

    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 -> [ReportFile]
commandInputFiles  :: [ ReportFile ]
  }

-- | Information about one file in the command options.
data ReportFile = ReportFile
  { ReportFile -> FilePath
reportFilePath       :: FilePath
  , ReportFile -> FilePath
reportFileFormat     :: String
  , ReportFile -> FilePath
reportFilePropFormat :: String
  , ReportFile -> Maybe FilePath
reportFilePropVia    :: Maybe String
  }

-- | Summary of the files read.
data CommandSummary = CommandSummary
    { CommandSummary -> Bool
commandRequirementsAny :: Bool
    , CommandSummary -> [CommandSummaryRequirements]
commandRequirementList :: [CommandSummaryRequirements]
    , CommandSummary -> Bool
commandDiagramsAny     :: Bool
    , CommandSummary -> [CommandSummaryDiagram]
commandDiagramsList    :: [CommandSummaryDiagram]
    }
  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

-- | Summary with empty data.
emptyCommandSummary :: CommandSummary
emptyCommandSummary :: CommandSummary
emptyCommandSummary = Bool
-> [CommandSummaryRequirements]
-> Bool
-> [CommandSummaryDiagram]
-> CommandSummary
CommandSummary Bool
False [] Bool
False []

-- | Merge two summaries.
mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary CommandSummary
c1 CommandSummary
c2 = CommandSummary
  { commandRequirementsAny :: Bool
commandRequirementsAny =
      CommandSummary -> Bool
commandRequirementsAny CommandSummary
c1 Bool -> Bool -> Bool
|| CommandSummary -> Bool
commandRequirementsAny CommandSummary
c2
  , commandRequirementList :: [CommandSummaryRequirements]
commandRequirementList =
      CommandSummary -> [CommandSummaryRequirements]
commandRequirementList CommandSummary
c1 [CommandSummaryRequirements]
-> [CommandSummaryRequirements] -> [CommandSummaryRequirements]
forall a. [a] -> [a] -> [a]
++ CommandSummary -> [CommandSummaryRequirements]
commandRequirementList CommandSummary
c2
  , commandDiagramsAny :: Bool
commandDiagramsAny =
      CommandSummary -> Bool
commandDiagramsAny CommandSummary
c1 Bool -> Bool -> Bool
|| CommandSummary -> Bool
commandDiagramsAny CommandSummary
c2
  , commandDiagramsList :: [CommandSummaryDiagram]
commandDiagramsList =
      CommandSummary -> [CommandSummaryDiagram]
commandDiagramsList CommandSummary
c1 [CommandSummaryDiagram]
-> [CommandSummaryDiagram] -> [CommandSummaryDiagram]
forall a. [a] -> [a] -> [a]
++ CommandSummary -> [CommandSummaryDiagram]
commandDiagramsList CommandSummary
c2
  }

-- | Requirement data for inclusion in the summary.
data CommandSummaryRequirements = CommandSummaryRequirements
    { CommandSummaryRequirements -> FilePath
summaryRequirementsFile       :: FilePath
    , CommandSummaryRequirements -> ErrorCode
summaryExternalVariables      :: Int
    , CommandSummaryRequirements -> ErrorCode
summaryInternalVariables      :: Int
    , CommandSummaryRequirements -> ErrorCode
summaryRequirements           :: Int
    , CommandSummaryRequirements -> ErrorCode
summaryRequirementsTrue       :: Int
    , CommandSummaryRequirements -> ErrorCode
summaryRequirementsFalse      :: Int
    , CommandSummaryRequirements -> Bool
summaryRequirementsConsistent :: Bool
    , CommandSummaryRequirements -> [RequirementDetails]
summaryRequirementsDetails    :: [RequirementDetails]
    }
  deriving ((forall x.
 CommandSummaryRequirements -> Rep CommandSummaryRequirements x)
-> (forall x.
    Rep CommandSummaryRequirements x -> CommandSummaryRequirements)
-> Generic CommandSummaryRequirements
forall x.
Rep CommandSummaryRequirements x -> CommandSummaryRequirements
forall x.
CommandSummaryRequirements -> Rep CommandSummaryRequirements x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x.
CommandSummaryRequirements -> Rep CommandSummaryRequirements x
from :: forall x.
CommandSummaryRequirements -> Rep CommandSummaryRequirements x
$cto :: forall x.
Rep CommandSummaryRequirements x -> CommandSummaryRequirements
to :: forall x.
Rep CommandSummaryRequirements x -> CommandSummaryRequirements
Generic, ErrorCode -> CommandSummaryRequirements -> FilePath -> FilePath
[CommandSummaryRequirements] -> FilePath -> FilePath
CommandSummaryRequirements -> FilePath
(ErrorCode -> CommandSummaryRequirements -> FilePath -> FilePath)
-> (CommandSummaryRequirements -> FilePath)
-> ([CommandSummaryRequirements] -> FilePath -> FilePath)
-> Show CommandSummaryRequirements
forall a.
(ErrorCode -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
$cshowsPrec :: ErrorCode -> CommandSummaryRequirements -> FilePath -> FilePath
showsPrec :: ErrorCode -> CommandSummaryRequirements -> FilePath -> FilePath
$cshow :: CommandSummaryRequirements -> FilePath
show :: CommandSummaryRequirements -> FilePath
$cshowList :: [CommandSummaryRequirements] -> FilePath -> FilePath
showList :: [CommandSummaryRequirements] -> FilePath -> FilePath
Show)

instance ToJSON CommandSummaryRequirements

-- | 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 CommandSummaryDiagram = CommandSummaryDiagram
    { CommandSummaryDiagram -> FilePath
summaryDiagramFile          :: FilePath
    , CommandSummaryDiagram -> ErrorCode
summaryDiagramNumStates     :: Int
    , CommandSummaryDiagram -> Bool
summaryDiagramDeterministic :: Bool
    }
  deriving ((forall x. CommandSummaryDiagram -> Rep CommandSummaryDiagram x)
-> (forall x. Rep CommandSummaryDiagram x -> CommandSummaryDiagram)
-> Generic CommandSummaryDiagram
forall x. Rep CommandSummaryDiagram x -> CommandSummaryDiagram
forall x. CommandSummaryDiagram -> Rep CommandSummaryDiagram x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommandSummaryDiagram -> Rep CommandSummaryDiagram x
from :: forall x. CommandSummaryDiagram -> Rep CommandSummaryDiagram x
$cto :: forall x. Rep CommandSummaryDiagram x -> CommandSummaryDiagram
to :: forall x. Rep CommandSummaryDiagram x -> CommandSummaryDiagram
Generic, ErrorCode -> CommandSummaryDiagram -> FilePath -> FilePath
[CommandSummaryDiagram] -> FilePath -> FilePath
CommandSummaryDiagram -> FilePath
(ErrorCode -> CommandSummaryDiagram -> FilePath -> FilePath)
-> (CommandSummaryDiagram -> FilePath)
-> ([CommandSummaryDiagram] -> FilePath -> FilePath)
-> Show CommandSummaryDiagram
forall a.
(ErrorCode -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
$cshowsPrec :: ErrorCode -> CommandSummaryDiagram -> FilePath -> FilePath
showsPrec :: ErrorCode -> CommandSummaryDiagram -> FilePath -> FilePath
$cshow :: CommandSummaryDiagram -> FilePath
show :: CommandSummaryDiagram -> FilePath
$cshowList :: [CommandSummaryDiagram] -> FilePath -> FilePath
showList :: [CommandSummaryDiagram] -> FilePath -> FilePath
Show)

instance ToJSON CommandSummaryDiagram

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