{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ScopedTypeVariables       #-}
-- 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 an overview of the input files.
module Command.Overview
    ( command
    , CommandOptions(..)
    , OverviewFile(..)
    , CommandSummary(..)
    , CommandSummaryRequirements(..)
    , CommandSummaryDiagram(..)
    , ErrorCode
    )
  where

-- External imports
import Control.Monad        (foldM)
import Control.Monad.Except (runExceptT)
import Data.Aeson           (ToJSON (..))
import GHC.Generics         (Generic)

-- External imports: Ogma
import Data.OgmaSpec (Spec (..))

-- Internal imports
import           Command.Common              (InputFile(..), parseInputFile)
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 overview of a spec 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@. All identifiers
-- used are valid C99 identifiers. The template, if provided, exists and uses
-- the variables needed by the overview application generator. The target
-- directory is writable and there's enough disk space to copy the files over.
command :: CommandOptions -- ^ Customization options
        -> IO (Maybe CommandSummary, Result ErrorCode)
command :: CommandOptions -> IO (Maybe CommandSummary, Result ErrorCode)
command CommandOptions
options = do
    fs <- (Either (FilePath, FilePath) CommandSummary
 -> OverviewFile -> IO (Either (FilePath, FilePath) CommandSummary))
-> Either (FilePath, FilePath) CommandSummary
-> [OverviewFile]
-> IO (Either (FilePath, FilePath) CommandSummary)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
            Either (FilePath, FilePath) CommandSummary
-> OverviewFile -> IO (Either (FilePath, FilePath) CommandSummary)
processFile
            (CommandSummary -> Either (FilePath, FilePath) CommandSummary
forall a b. b -> Either a b
Right CommandSummary
emptyCommandSummary)
            (CommandOptions -> [OverviewFile]
commandInputFiles CommandOptions
options)

    return $ commandResult options fs

  where

    processFile :: Either (FilePath, String) CommandSummary
                -> OverviewFile
                -> IO (Either (FilePath, String) CommandSummary)
    processFile :: Either (FilePath, FilePath) CommandSummary
-> OverviewFile -> IO (Either (FilePath, FilePath) CommandSummary)
processFile Either (FilePath, FilePath) CommandSummary
acc OverviewFile
file = case Either (FilePath, FilePath) CommandSummary
acc of
      Left (FilePath, FilePath)
_     -> Either (FilePath, FilePath) CommandSummary
-> IO (Either (FilePath, FilePath) CommandSummary)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Either (FilePath, FilePath) CommandSummary
acc
      Right CommandSummary
acc' -> do
        let functions :: ExprPair
functions = FilePath -> ExprPair
exprPair (OverviewFile -> FilePath
overviewFilePropFormat OverviewFile
file)
        c <- FilePath
-> OverviewFile -> ExprPair -> IO (Either FilePath CommandSummary)
command' (OverviewFile -> FilePath
overviewFilePath OverviewFile
file) OverviewFile
file ExprPair
functions
        case c of
          Left FilePath
msg -> Either (FilePath, FilePath) CommandSummary
-> IO (Either (FilePath, FilePath) CommandSummary)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (FilePath, FilePath) CommandSummary
 -> IO (Either (FilePath, FilePath) CommandSummary))
-> Either (FilePath, FilePath) CommandSummary
-> IO (Either (FilePath, FilePath) CommandSummary)
forall a b. (a -> b) -> a -> b
$ (FilePath, FilePath) -> Either (FilePath, FilePath) CommandSummary
forall a b. a -> Either a b
Left (OverviewFile -> FilePath
overviewFilePath OverviewFile
file, FilePath
msg)
          Right CommandSummary
s  -> Either (FilePath, FilePath) CommandSummary
-> IO (Either (FilePath, FilePath) CommandSummary)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (FilePath, FilePath) CommandSummary
 -> IO (Either (FilePath, FilePath) CommandSummary))
-> Either (FilePath, FilePath) CommandSummary
-> IO (Either (FilePath, FilePath) CommandSummary)
forall a b. (a -> b) -> a -> b
$ CommandSummary -> Either (FilePath, FilePath) CommandSummary
forall a b. b -> Either a b
Right (CommandSummary -> Either (FilePath, FilePath) CommandSummary)
-> CommandSummary -> Either (FilePath, FilePath) CommandSummary
forall a b. (a -> b) -> a -> b
$ CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary CommandSummary
acc' CommandSummary
s

-- | Generate overview of a spec 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@. All identifiers
-- used are valid C99 identifiers. The template, if provided, exists and uses
-- the variables needed by the overview application generator. The target
-- directory is writable and there's enough disk space to copy the files over.
command' :: FilePath
          -> OverviewFile
          -> ExprPair
          -> IO (Either String CommandSummary)
command' :: FilePath
-> OverviewFile -> ExprPair -> IO (Either FilePath CommandSummary)
command' FilePath
fp OverviewFile
options (ExprPair ExprPairT a
exprT) = do
    res <- ExceptT ErrorTriplet IO (InputFile a)
-> IO (Either ErrorTriplet (InputFile a))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT ErrorTriplet IO (InputFile a)
 -> IO (Either ErrorTriplet (InputFile a)))
-> ExceptT ErrorTriplet IO (InputFile a)
-> IO (Either ErrorTriplet (InputFile a))
forall a b. (a -> b) -> a -> b
$
             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
      Left (ErrorTriplet ErrorCode
_ FilePath
s Location
_) -> Either FilePath CommandSummary
-> IO (Either FilePath CommandSummary)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either FilePath CommandSummary
 -> IO (Either FilePath CommandSummary))
-> Either FilePath CommandSummary
-> IO (Either FilePath CommandSummary)
forall a b. (a -> b) -> a -> b
$ FilePath -> Either FilePath CommandSummary
forall a b. a -> Either a b
Left FilePath
s

      Right (InputFileDiagram Diagram
diagramR) -> do
        analysisResult <- Diagram -> IO AnalysisResult
analyzeDiagram Diagram
diagramR
        pure $ Right $ emptyCommandSummary
                         { commandSummaryDiagrams =
                             [ CommandSummaryDiagram
                                 fp
                                 (numStates analysisResult)
                                 (deterministic analysisResult)
                             ]
                         }

      Right (InputFileSpec Spec a
spec') -> 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)
specAnalyzed  = Spec a -> Either FilePath (Spec a)
forall a. Spec a -> Either FilePath (Spec a)
Spec2Copilot.specAnalyze Spec a
specCompleted

        specFormalAnalysis <-
          [(FilePath, FilePath)]
-> ([(FilePath, FilePath)] -> a -> a)
-> (a -> FilePath)
-> Spec a
-> IO (Either FilePath AnalysisResult)
forall a.
[(FilePath, FilePath)]
-> ([(FilePath, FilePath)] -> a -> a)
-> (a -> FilePath)
-> Spec a
-> IO (Either FilePath AnalysisResult)
SpecAnalysis.specAnalyze [] [(FilePath, FilePath)] -> a -> a
replace a -> FilePath
printExpr Spec a
specCompleted

        pure $ do
          numExterns  <- length . externalVariables <$> specAnalyzed
          numInternal <- length . internalVariables <$> specAnalyzed
          numReqs     <- length . requirements      <$> specAnalyzed
          numTrues    <- SpecAnalysis.numAlwaysTrue  <$> specFormalAnalysis
          numFalses   <- SpecAnalysis.numAlwaysFalse <$> specFormalAnalysis
          consistent  <- SpecAnalysis.consistent     <$> specFormalAnalysis

          pure $ emptyCommandSummary
                   { commandSummaryRequirements =
                       [ CommandSummaryRequirements
                           fp
                           numExterns
                           numInternal
                           numReqs
                           numTrues
                           numFalses
                           consistent
                      ]
                   }

  where

    formatName :: FilePath
formatName     = OverviewFile -> FilePath
overviewFileFormat OverviewFile
options
    propFormatName :: FilePath
propFormatName = OverviewFile -> FilePath
overviewFilePropFormat OverviewFile
options
    propVia :: Maybe FilePath
propVia        = OverviewFile -> Maybe FilePath
overviewFilePropVia OverviewFile
options

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

data CommandSummary = CommandSummary
    { CommandSummary -> [CommandSummaryRequirements]
commandSummaryRequirements :: [CommandSummaryRequirements]
    , CommandSummary -> [CommandSummaryDiagram]
commandSummaryDiagrams     :: [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 -> ShowS
[CommandSummary] -> ShowS
CommandSummary -> FilePath
(ErrorCode -> CommandSummary -> ShowS)
-> (CommandSummary -> FilePath)
-> ([CommandSummary] -> ShowS)
-> Show CommandSummary
forall a.
(ErrorCode -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: ErrorCode -> CommandSummary -> ShowS
showsPrec :: ErrorCode -> CommandSummary -> ShowS
$cshow :: CommandSummary -> FilePath
show :: CommandSummary -> FilePath
$cshowList :: [CommandSummary] -> ShowS
showList :: [CommandSummary] -> ShowS
Show)

instance ToJSON CommandSummary

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

-- | Merge two summaries.
mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary CommandSummary
c1 CommandSummary
c2 = CommandSummary
  { commandSummaryRequirements :: [CommandSummaryRequirements]
commandSummaryRequirements =
      CommandSummary -> [CommandSummaryRequirements]
commandSummaryRequirements CommandSummary
c1 [CommandSummaryRequirements]
-> [CommandSummaryRequirements] -> [CommandSummaryRequirements]
forall a. [a] -> [a] -> [a]
++ CommandSummary -> [CommandSummaryRequirements]
commandSummaryRequirements CommandSummary
c2
  , commandSummaryDiagrams :: [CommandSummaryDiagram]
commandSummaryDiagrams =
      CommandSummary -> [CommandSummaryDiagram]
commandSummaryDiagrams CommandSummary
c1 [CommandSummaryDiagram]
-> [CommandSummaryDiagram] -> [CommandSummaryDiagram]
forall a. [a] -> [a] -> [a]
++ CommandSummary -> [CommandSummaryDiagram]
commandSummaryDiagrams CommandSummary
c2
  }

instance Semigroup CommandSummary where
  <> :: CommandSummary -> CommandSummary -> CommandSummary
(<>) = CommandSummary -> CommandSummary -> CommandSummary
mergeCommandSummary

instance Monoid CommandSummary where
  mempty :: CommandSummary
mempty  = CommandSummary
emptyCommandSummary

-- | Requirement data for inclusion in the summary.
data CommandSummaryRequirements = CommandSummaryRequirements
    { CommandSummaryRequirements -> FilePath
commandRequirementsFile       :: FilePath
    , CommandSummaryRequirements -> ErrorCode
commandExternalVariables      :: Int
    , CommandSummaryRequirements -> ErrorCode
commandInternalVariables      :: Int
    , CommandSummaryRequirements -> ErrorCode
commandRequirements           :: Int
    , CommandSummaryRequirements -> ErrorCode
commandRequirementsTrue       :: Int
    , CommandSummaryRequirements -> ErrorCode
commandRequirementsFalse      :: Int
    , CommandSummaryRequirements -> Bool
commandRequirementsConsistent :: Bool
    }
  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 -> ShowS
[CommandSummaryRequirements] -> ShowS
CommandSummaryRequirements -> FilePath
(ErrorCode -> CommandSummaryRequirements -> ShowS)
-> (CommandSummaryRequirements -> FilePath)
-> ([CommandSummaryRequirements] -> ShowS)
-> Show CommandSummaryRequirements
forall a.
(ErrorCode -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: ErrorCode -> CommandSummaryRequirements -> ShowS
showsPrec :: ErrorCode -> CommandSummaryRequirements -> ShowS
$cshow :: CommandSummaryRequirements -> FilePath
show :: CommandSummaryRequirements -> FilePath
$cshowList :: [CommandSummaryRequirements] -> ShowS
showList :: [CommandSummaryRequirements] -> ShowS
Show)

instance ToJSON CommandSummaryRequirements

-- | Diagram Data for inclusion in the summary.
data CommandSummaryDiagram = CommandSummaryDiagram
    { CommandSummaryDiagram -> FilePath
commandDiagramFile          :: FilePath
    , CommandSummaryDiagram -> ErrorCode
commandDiagramNumStates     :: Int
    , CommandSummaryDiagram -> Bool
commandDiagramDeterministic :: 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 -> ShowS
[CommandSummaryDiagram] -> ShowS
CommandSummaryDiagram -> FilePath
(ErrorCode -> CommandSummaryDiagram -> ShowS)
-> (CommandSummaryDiagram -> FilePath)
-> ([CommandSummaryDiagram] -> ShowS)
-> Show CommandSummaryDiagram
forall a.
(ErrorCode -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: ErrorCode -> CommandSummaryDiagram -> ShowS
showsPrec :: ErrorCode -> CommandSummaryDiagram -> ShowS
$cshow :: CommandSummaryDiagram -> FilePath
show :: CommandSummaryDiagram -> FilePath
$cshowList :: [CommandSummaryDiagram] -> ShowS
showList :: [CommandSummaryDiagram] -> ShowS
Show)

instance ToJSON CommandSummaryDiagram

-- | Options used to customize the interpretation of input specifications.
data CommandOptions = CommandOptions
  { CommandOptions -> [OverviewFile]
commandInputFiles :: [ OverviewFile ]
  }

-- | Information about one file in the command options.
data OverviewFile = OverviewFile
  { OverviewFile -> FilePath
overviewFilePath       :: FilePath
  , OverviewFile -> FilePath
overviewFileFormat     :: String
  , OverviewFile -> FilePath
overviewFilePropFormat :: String
  , OverviewFile -> Maybe FilePath
overviewFilePropVia    :: Maybe String
  }

-- * Error codes

-- | Error: the input file cannot be read due to it being unreadable or the
-- format being incorrect.
ecOverviewError :: ErrorCode
ecOverviewError :: ErrorCode
ecOverviewError = ErrorCode
1

-- * Result

-- | Process the result of the transformation function.
commandResult :: CommandOptions
              -> Either (FilePath, String) a
              -> (Maybe a, Result ErrorCode)
commandResult :: forall a.
CommandOptions
-> Either (FilePath, FilePath) a -> (Maybe a, Result ErrorCode)
commandResult CommandOptions
_options Either (FilePath, FilePath) a
result = case Either (FilePath, FilePath) a
result of
  Left (FilePath
fp, FilePath
msg) -> (Maybe a
forall a. Maybe a
Nothing, ErrorCode -> FilePath -> Location -> Result ErrorCode
forall a. a -> FilePath -> Location -> Result a
Error ErrorCode
ecOverviewError FilePath
msg (FilePath -> Location
LocationFile FilePath
fp))
  Right a
t        -> (a -> Maybe a
forall a. a -> Maybe a
Just a
t,  Result ErrorCode
forall a. Result a
Success)