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