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

    -- External imports
    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 :: FilePath        -- ^ Path to a file containing a specification
            -> CommandOptions -- ^ Customization options
            -> IO (Maybe CommandSummary, Result ErrorCode)
    command :: FilePath
    -> CommandOptions -> IO (Maybe CommandSummary, Result ErrorCode)
    command FilePath
    fp CommandOptions
    options = do
      let functions :: ExprPair
    functions = FilePath -> ExprPair
    exprPair (CommandOptions -> FilePath
    commandPropFormat CommandOptions
    options)

      copilot <- FilePath
    -> CommandOptions
    -> ExprPair
    -> IO (Either FilePath CommandSummary)
    command' FilePath
    fp CommandOptions
    options ExprPair
    functions

      return $ commandResult options fp copilot

    -- | 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
              -> CommandOptions
              -> ExprPair
              -> IO (Either String CommandSummary)
    command' :: FilePath
    -> CommandOptions
    -> ExprPair
    -> IO (Either FilePath CommandSummary)
    command' FilePath
    fp CommandOptions
    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 $
              CommandSummaryDiagram
                (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 $
                CommandSummaryRequirement
                  numExterns numInternal numReqs numTrues numFalses consistent

      where

        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

    data CommandSummary
        = CommandSummaryRequirement
            { CommandSummary -> ErrorCode
    commandExternalVariables      :: Int
            , CommandSummary -> ErrorCode
    commandInternalVariables      :: Int
            , CommandSummary -> ErrorCode
    commandRequirements           :: Int
            , CommandSummary -> ErrorCode
    commandRequirementsTrue       :: Int
            , CommandSummary -> ErrorCode
    commandRequirementsFalse      :: Int
            , CommandSummary -> Bool
    commandRequirementsConsistent :: Bool
            }
        | CommandSummaryDiagram
            { CommandSummary -> ErrorCode
    commandNumStates     :: Int
            , CommandSummary -> Bool
    commandDeterministic :: Bool
            }
      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

    -- | Options used to customize the interpretation of input specifications.
    data CommandOptions = CommandOptions
      { CommandOptions -> FilePath
    commandFormat     :: String
      , CommandOptions -> FilePath
    commandPropFormat :: String
      , CommandOptions -> Maybe FilePath
    commandPropVia    :: 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
                  -> FilePath
                  -> Either String a
                  -> (Maybe a, Result ErrorCode)
    commandResult :: forall a.
    CommandOptions
    -> FilePath -> Either FilePath a -> (Maybe a, Result ErrorCode)
    commandResult CommandOptions
    _options FilePath
    fp Either FilePath a
    result = case Either FilePath a
    result of
      Left 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)