    {-# 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 Data.List            (nub, (\\))
    import GHC.Generics         (Generic)

    -- External imports: Ogma
    import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
                          Requirement (..), Spec (..))

    -- Internal imports
    import Command.Common
    import Command.Errors              (ErrorCode, ErrorTriplet(..))
    import Command.Result              (Result (..))
    import Data.Location               (Location (..))
    import Language.Trans.Spec2Copilot (specAnalyze)

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

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

      (Maybe CommandSummary, Result ErrorCode)
    -> IO (Maybe CommandSummary, Result ErrorCode)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Maybe CommandSummary, Result ErrorCode)
     -> IO (Maybe CommandSummary, Result ErrorCode))
    -> (Maybe CommandSummary, Result ErrorCode)
    -> IO (Maybe CommandSummary, Result ErrorCode)
    forall a b. (a -> b) -> a -> b
    $ CommandOptions
    -> FilePath
    -> Either FilePath CommandSummary
    -> (Maybe CommandSummary, Result ErrorCode)
    forall a.
    CommandOptions
    -> FilePath -> Either FilePath a -> (Maybe a, Result ErrorCode)
    commandResult CommandOptions
    options FilePath
    fp Either FilePath CommandSummary
    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
        Either ErrorTriplet (Spec a)
    spec <- ExceptT ErrorTriplet IO (Spec a)
    -> IO (Either ErrorTriplet (Spec a))
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT ErrorTriplet IO (Spec a)
     -> IO (Either ErrorTriplet (Spec a)))
    -> ExceptT ErrorTriplet IO (Spec a)
    -> IO (Either ErrorTriplet (Spec a))
    forall a b. (a -> b) -> a -> b
    $ FilePath -> ExceptT ErrorTriplet IO (Spec a)
    parseInputFile' FilePath
    fp
        let spec' :: Either FilePath (Spec a)
    spec' = (ErrorTriplet -> Either FilePath (Spec a))
    -> (Spec a -> Either FilePath (Spec a))
    -> Either ErrorTriplet (Spec a)
    -> Either FilePath (Spec a)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (\(ErrorTriplet ErrorCode
    _ec FilePath
    msg Location
    _loc) -> FilePath -> Either FilePath (Spec a)
    forall a b. a -> Either a b
    Left FilePath
    msg) Spec a -> Either FilePath (Spec a)
    forall a b. b -> Either a b
    Right Either ErrorTriplet (Spec a)
    spec

        let summary :: Either FilePath CommandSummary
    summary = do
              Spec a
    spec1 <- Either FilePath (Spec a)
    spec'
              Spec a
    spec3 <- Spec a -> Either FilePath (Spec a)
    forall a. Spec a -> Either FilePath (Spec a)
    specAnalyze (Spec a -> Either FilePath (Spec a))
    -> Spec a -> Either FilePath (Spec a)
    forall a b. (a -> b) -> a -> b
    $ (a -> [FilePath]) -> Spec a -> Spec a
    forall a. (a -> [FilePath]) -> Spec a -> Spec a
    addMissingIdentifiers a -> [FilePath]
    ids Spec a
    spec1
              CommandSummary -> Either FilePath CommandSummary
    forall a. a -> Either FilePath a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CommandSummary -> Either FilePath CommandSummary)
    -> CommandSummary -> Either FilePath CommandSummary
    forall a b. (a -> b) -> a -> b
    $ ErrorCode -> ErrorCode -> ErrorCode -> CommandSummary
    CommandSummary ([ExternalVariableDef] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length (Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    spec3))
                                      ([InternalVariableDef] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length (Spec a -> [InternalVariableDef]
    forall a. Spec a -> [InternalVariableDef]
    internalVariables Spec a
    spec3))
                                      ([Requirement a] -> ErrorCode
    forall a. [a] -> ErrorCode
    forall (t :: * -> *) a. Foldable t => t a -> ErrorCode
    length (Spec a -> [Requirement a]
    forall a. Spec a -> [Requirement a]
    requirements Spec a
    spec3))
        Either FilePath CommandSummary
    -> IO (Either FilePath CommandSummary)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Either FilePath CommandSummary
    summary

      where

        parseInputFile' :: FilePath -> ExceptT ErrorTriplet IO (Spec a)
    parseInputFile' FilePath
    f = FilePath
    -> FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (Spec a)
    forall a.
    FilePath
    -> FilePath
    -> FilePath
    -> Maybe FilePath
    -> ExprPairT a
    -> ExceptT ErrorTriplet IO (Spec a)
    parseInputFile FilePath
    f FilePath
    formatName FilePath
    propFormatName Maybe FilePath
    propVia ExprPairT a
    exprT
        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
    _print a -> [FilePath]
    ids a
    _def = ExprPairT a
    exprT

    data CommandSummary = CommandSummary
      { CommandSummary -> ErrorCode
    commandExternalVariables :: Int
      , CommandSummary -> ErrorCode
    commandInternalVariables :: Int
      , CommandSummary -> ErrorCode
    commandRequirements      :: Int
      }
      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)

    -- | Add to a spec external variables for all identifiers mentioned in
    -- expressions that are not defined anywhere.
    addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a
    addMissingIdentifiers :: forall a. (a -> [FilePath]) -> Spec a -> Spec a
    addMissingIdentifiers a -> [FilePath]
    f Spec a
    s = Spec a
    s { externalVariables = vars' }
      where
        vars' :: [ExternalVariableDef]
    vars'   = Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    s [ExternalVariableDef]
    -> [ExternalVariableDef] -> [ExternalVariableDef]
    forall a. [a] -> [a] -> [a]
    ++ [ExternalVariableDef]
    newVars
        newVars :: [ExternalVariableDef]
    newVars = (FilePath -> ExternalVariableDef)
    -> [FilePath] -> [ExternalVariableDef]
    forall a b. (a -> b) -> [a] -> [b]
    map (\FilePath
    n -> FilePath -> FilePath -> ExternalVariableDef
    ExternalVariableDef FilePath
    n FilePath
    "") [FilePath]
    newVarNames

        -- Names that are not defined anywhere
        newVarNames :: [FilePath]
    newVarNames = [FilePath]
    identifiers [FilePath] -> [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ [FilePath]
    existingNames

        -- Identifiers being mentioned in the requirements.
        identifiers :: [FilePath]
    identifiers = [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a]
    nub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> a -> b
    $ (Requirement a -> [FilePath]) -> [Requirement a] -> [FilePath]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (a -> [FilePath]
    f (a -> [FilePath])
    -> (Requirement a -> a) -> Requirement a -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Requirement a -> a
    forall a. Requirement a -> a
    requirementExpr) (Spec a -> [Requirement a]
    forall a. Spec a -> [Requirement a]
    requirements Spec a
    s)

        -- Names that are defined in variables.
        existingNames :: [FilePath]
    existingNames = (ExternalVariableDef -> FilePath)
    -> [ExternalVariableDef] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map ExternalVariableDef -> FilePath
    externalVariableName (Spec a -> [ExternalVariableDef]
    forall a. Spec a -> [ExternalVariableDef]
    externalVariables Spec a
    s)
                     [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ (InternalVariableDef -> FilePath)
    -> [InternalVariableDef] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map InternalVariableDef -> FilePath
    internalVariableName (Spec a -> [InternalVariableDef]
    forall a. Spec a -> [InternalVariableDef]
    internalVariables Spec a
    s)