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