{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE MultiWayIf                #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ScopedTypeVariables       #-}
-- Copyright 2020 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.
--
-- | Transform a specification into a standalone Copilot specification.
module Command.Standalone
    ( command
    , commandLogic
    , AppData
    , CommandOptions(..)
    , ErrorCode
    )
  where

-- External imports
import Control.Applicative  ((<|>))
import Control.Exception    as E
import Control.Monad.Except (ExceptT (..), liftEither)
import Data.Aeson           (ToJSON (..))
import Data.Maybe           (fromMaybe)
import GHC.Generics         (Generic)

-- External imports: Ogma
import System.Directory.Extra (copyTemplate)

-- Internal imports
import Command.Common
import Command.Errors                 (ErrorCode, ErrorTriplet(..))
import Command.Result                 (Result (..))
import Data.Aeson.Extra               (mergeObjects)
import Data.Either.Extra              (mapLeft)
import Data.ExprPair                  (ExprPair(..), ExprPairT(..), exprPair)
import Data.Location                  (Location (..))
import Data.Spec.Extra                (addMissingIdentifiers)
import Data.Spec.Parser               (readInputExpr)
import Language.Trans.Diagram2Copilot (DiagramMode (..), diagram2CopilotSpec)
import Language.Trans.Spec2Copilot    (spec2Copilot, specAnalyze)

-- | Generate a new standalone Copilot monitor that implements the spec 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 standalone application generator. The target
-- directory is writable and there's enough disk space to copy the files over.
command :: CommandOptions -- ^ Customization options
        -> IO (Result ErrorCode)
command :: CommandOptions -> IO (Result ErrorCode)
command CommandOptions
options = ExceptT ErrorTriplet IO () -> IO (Result ErrorCode)
forall (m :: * -> *) a.
Monad m =>
ExceptT ErrorTriplet m a -> m (Result ErrorCode)
processResult (ExceptT ErrorTriplet IO () -> IO (Result ErrorCode))
-> ExceptT ErrorTriplet IO () -> IO (Result ErrorCode)
forall a b. (a -> b) -> a -> b
$ do
    -- Obtain template dir
    templateDir <- Maybe FilePath -> FilePath -> ExceptT ErrorTriplet IO FilePath
forall e. Maybe FilePath -> FilePath -> ExceptT e IO FilePath
locateTemplateDir Maybe FilePath
mTemplateDir FilePath
"standalone"

    templateVars <- parseTemplateVarsFile templateVarsF

    appData <- command' options functions

    let subst = Value -> Value -> Value
mergeObjects (AppData -> Value
forall a. ToJSON a => a -> Value
toJSON AppData
appData) Value
templateVars

    -- Expand template
    ExceptT $ fmap (makeLeftE cannotCopyTemplate) $ E.try $
      copyTemplate templateDir subst targetDir

  where

    targetDir :: FilePath
targetDir     = CommandOptions -> FilePath
commandTargetDir CommandOptions
options
    mTemplateDir :: Maybe FilePath
mTemplateDir  = CommandOptions -> Maybe FilePath
commandTemplateDir CommandOptions
options
    functions :: ExprPair
functions     = FilePath -> ExprPair
exprPair (CommandOptions -> FilePath
commandPropFormat CommandOptions
options)
    templateVarsF :: Maybe FilePath
templateVarsF = CommandOptions -> Maybe FilePath
commandExtraVars CommandOptions
options

-- | Generate a new standalone Copilot monitor that implements the spec in an
-- input file, using a subexpression handler.
--
-- 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 standalone application generator. The target
-- directory is writable and there's enough disk space to copy the files over.
command' :: CommandOptions
         -> ExprPair
         -> ExceptT ErrorTriplet IO AppData
command' :: CommandOptions -> ExprPair -> ExceptT ErrorTriplet IO AppData
command' CommandOptions
options (ExprPair ExprPairT a
exprT) = do

    -- Read spec and complement the specification with any missing/implicit
    -- definitions.
    specT <- ExceptT ErrorTriplet IO (Maybe (InputFile a))
-> (FilePath -> ExceptT ErrorTriplet IO (Maybe (InputFile a)))
-> Maybe FilePath
-> ExceptT ErrorTriplet IO (Maybe (InputFile a))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe (InputFile a)
-> ExceptT ErrorTriplet IO (Maybe (InputFile a))
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (InputFile a)
forall a. Maybe a
Nothing) (\FilePath
e -> InputFile a -> Maybe (InputFile a)
forall a. a -> Maybe a
Just (InputFile a -> Maybe (InputFile a))
-> (Spec a -> InputFile a) -> Spec a -> Maybe (InputFile a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec a -> InputFile a
forall a. Spec a -> InputFile a
InputFileSpec (Spec a -> Maybe (InputFile a))
-> ExceptT ErrorTriplet IO (Spec a)
-> ExceptT ErrorTriplet IO (Maybe (InputFile a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> ExceptT ErrorTriplet IO (Spec a)
readInputExpr' FilePath
e) Maybe FilePath
triggerExprM
    specF <- if null fpA
                  then return Nothing
                  else do
                    fpA' <- mapM readInputFile' fpA
                    let fpA'' = [InputFile a] -> [InputFile a]
forall a. [InputFile a] -> [InputFile a]
combineInputFiles [InputFile a]
fpA'
                    if length fpA'' > 1
                      then liftEither $ Left commandMultipleInputTypes
                      else pure $ Just $ head fpA''

    let spec = Maybe (InputFile a)
specT Maybe (InputFile a) -> Maybe (InputFile a) -> Maybe (InputFile a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (InputFile a)
specF

    case spec of
      Maybe (InputFile a)
Nothing    -> Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData)
-> Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
forall a b. (a -> b) -> a -> b
$ ErrorTriplet -> Either ErrorTriplet AppData
forall a b. a -> Either a b
Left (ErrorTriplet -> Either ErrorTriplet AppData)
-> ErrorTriplet -> Either ErrorTriplet AppData
forall a b. (a -> b) -> a -> b
$ ErrorTriplet
commandMissingSpec
      Just InputFile a
spec' -> Maybe FilePath
-> [FilePath]
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> InputFile a
-> ExceptT ErrorTriplet IO AppData
forall a.
Maybe FilePath
-> [FilePath]
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> InputFile a
-> ExceptT ErrorTriplet IO AppData
commandLogic Maybe FilePath
triggerExprM [FilePath]
fpA FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT InputFile a
spec'

  where
    triggerExprM :: Maybe FilePath
triggerExprM   = CommandOptions -> Maybe FilePath
commandConditionExpr CommandOptions
options
    fpA :: [FilePath]
fpA            = CommandOptions -> [FilePath]
commandInputFiles CommandOptions
options
    name :: FilePath
name           = CommandOptions -> FilePath
commandFilename CommandOptions
options
    typeMaps :: [(FilePath, FilePath)]
typeMaps       = [(FilePath, FilePath)] -> [(FilePath, FilePath)]
typeToCopilotTypeMapping (CommandOptions -> [(FilePath, FilePath)]
commandTypeMapping CommandOptions
options)
    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

    readInputExpr' :: FilePath -> ExceptT ErrorTriplet IO (Spec a)
readInputExpr' FilePath
e =
      FilePath
-> FilePath
-> Maybe FilePath
-> ExprPairT a
-> ExceptT ErrorTriplet IO (Spec a)
forall a.
FilePath
-> FilePath
-> Maybe FilePath
-> ExprPairT a
-> ExceptT ErrorTriplet IO (Spec a)
readInputExpr FilePath
e FilePath
propFormatName Maybe FilePath
propVia ExprPairT a
exprT

    readInputFile' :: FilePath -> ExceptT ErrorTriplet IO (InputFile a)
readInputFile' FilePath
f =
      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
f FilePath
formatName FilePath
propFormatName Maybe FilePath
propVia ExprPairT a
exprT


-- | Generate the data of a new standalone Copilot monitor that implements the
-- spec, using a subexpression handler.
commandLogic :: Maybe String
             -> [FilePath]
             -> String
             -> [(String, String)]
             -> ExprPairT a
             -> InputFile a
             -> ExceptT ErrorTriplet IO AppData
commandLogic :: forall a.
Maybe FilePath
-> [FilePath]
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> InputFile a
-> ExceptT ErrorTriplet IO AppData
commandLogic Maybe FilePath
expr [FilePath]
fps FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT (InputFileDiagram Diagram
d) =
    AppData -> ExceptT ErrorTriplet IO AppData
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppData -> ExceptT ErrorTriplet IO AppData)
-> AppData -> ExceptT ErrorTriplet IO AppData
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath -> FilePath -> AppData
AppData [] FilePath
int [] FilePath
trigs FilePath
name
  where
    (FilePath
int, FilePath
trigs) = Diagram -> DiagramMode -> (FilePath, FilePath)
diagram2CopilotSpec Diagram
d DiagramMode
ComputeState

commandLogic Maybe FilePath
expr [FilePath]
fps FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT (InputFileSpec Spec a
input) = do
    let spec :: Spec a
spec = (a -> [FilePath]) -> Spec a -> Spec a
forall a. (a -> [FilePath]) -> Spec a -> Spec a
addMissingIdentifiers a -> [FilePath]
ids Spec a
input
    -- Analyze the spec for incorrect identifiers and convert it to Copilot.
    -- If there is an error, we change the error to a message we control.
    let appData :: Either ErrorTriplet AppData
appData = (FilePath -> ErrorTriplet)
-> Either FilePath AppData -> Either ErrorTriplet AppData
forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft FilePath -> ErrorTriplet
commandIncorrectSpec' (Either FilePath AppData -> Either ErrorTriplet AppData)
-> Either FilePath AppData -> Either ErrorTriplet AppData
forall a b. (a -> b) -> a -> b
$ do
          spec' <- Spec a -> Either FilePath (Spec a)
forall a. Spec a -> Either FilePath (Spec a)
specAnalyze Spec a
spec
          res   <- spec2Copilot name typeMaps replace print spec'

          -- Pack the results
          let (ext, int, reqs, trigs, specN) = res

          return $ AppData ext int reqs trigs specN

    Either ErrorTriplet AppData -> ExceptT ErrorTriplet IO AppData
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither Either ErrorTriplet AppData
appData

  where

    commandIncorrectSpec' :: FilePath -> ErrorTriplet
commandIncorrectSpec' = case (Maybe FilePath
expr, [FilePath]
fps) of
      (Maybe FilePath
Nothing,    [])   -> FilePath -> FilePath -> ErrorTriplet
forall a. HasCallStack => FilePath -> a
error FilePath
"Both expression and file are missing"
      (Maybe FilePath
Nothing,    [FilePath]
fps') -> FilePath -> ErrorTriplet
commandIncorrectSpecF
      (Just FilePath
expr', [FilePath]
_)    -> FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpecE FilePath
expr'

    ExprPairT FilePath -> Either FilePath a
parse [(FilePath, FilePath)] -> a -> a
replace a -> FilePath
print a -> [FilePath]
ids a
def = ExprPairT a
exprT

-- ** Argument processing

-- | Options used to customize the conversion of specifications to Copilot
-- code.
data CommandOptions = CommandOptions
  { CommandOptions -> Maybe FilePath
commandConditionExpr :: Maybe String
  , CommandOptions -> [FilePath]
commandInputFiles  :: [FilePath]         -- ^ Input specification file(s).
  , CommandOptions -> FilePath
commandTargetDir   :: FilePath           -- ^ Target directory where the
                                             -- application should be created.
  , CommandOptions -> Maybe FilePath
commandTemplateDir :: Maybe FilePath     -- ^ Directory where the template
                                             -- is to be found.
  , CommandOptions -> FilePath
commandFormat      :: String             -- ^ Format of the input file.
  , CommandOptions -> FilePath
commandPropFormat  :: String             -- ^ Format used for input
                                             -- properties.
  , CommandOptions -> [(FilePath, FilePath)]
commandTypeMapping :: [(String, String)]
  , CommandOptions -> FilePath
commandFilename    :: String
  , CommandOptions -> Maybe FilePath
commandPropVia     :: Maybe String       -- ^ Use external command to
                                             -- pre-process system properties.
  , CommandOptions -> Maybe FilePath
commandExtraVars   :: Maybe FilePath -- ^ File containing additional
                                         -- variables to make available to the
                                         -- template.
  }

-- * Mapping of types from input format to Copilot
typeToCopilotTypeMapping :: [(String, String)] -> [(String, String)]
typeToCopilotTypeMapping :: [(FilePath, FilePath)] -> [(FilePath, FilePath)]
typeToCopilotTypeMapping [(FilePath, FilePath)]
types =
    [ (FilePath
"bool",    FilePath
"Bool")
    , (FilePath
"int",     FilePath
intType)
    , (FilePath
"integer", FilePath
intType)
    , (FilePath
"real",    FilePath
realType)
    , (FilePath
"string",  FilePath
"String")
    , (FilePath
"",        FilePath
"_")
    ]
  where
    intType :: FilePath
intType  = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"Int64" (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"int" [(FilePath, FilePath)]
types
    realType :: FilePath
realType = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"Float" (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"real" [(FilePath, FilePath)]
types

-- | Data that may be relevant to generate a ROS application.
data AppData = AppData
    { AppData -> FilePath
externs   :: String
    , AppData -> FilePath
internals :: String
    , AppData -> FilePath
reqs      :: String
    , AppData -> FilePath
triggers  :: String
    , AppData -> FilePath
specName  :: String
    }
  deriving ((forall x. AppData -> Rep AppData x)
-> (forall x. Rep AppData x -> AppData) -> Generic AppData
forall x. Rep AppData x -> AppData
forall x. AppData -> Rep AppData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AppData -> Rep AppData x
from :: forall x. AppData -> Rep AppData x
$cto :: forall x. Rep AppData x -> AppData
to :: forall x. Rep AppData x -> AppData
Generic)

instance ToJSON AppData

-- | Error message associated to not having a spec of any kind.
commandMissingSpec :: ErrorTriplet
commandMissingSpec :: ErrorTriplet
commandMissingSpec =
    ErrorCode -> FilePath -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecMissingSpec FilePath
msg Location
LocationNothing
  where
    msg :: FilePath
msg =
      FilePath
"No input specification has been provided."

-- | Error message associated to having multiple input files of incompatible
-- types.
commandMultipleInputTypes :: ErrorTriplet
commandMultipleInputTypes :: ErrorTriplet
commandMultipleInputTypes =
    ErrorCode -> FilePath -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecMultipleInputTypes FilePath
msg Location
LocationNothing
  where
    msg :: FilePath
msg =
      FilePath
"Too many inputs provided. Provide one diagram or multiple specs."

-- | Error message associated to not being able to formalize the input spec.
commandIncorrectSpecF :: String -> ErrorTriplet
commandIncorrectSpecF :: FilePath -> ErrorTriplet
commandIncorrectSpecF FilePath
e =
    ErrorCode -> FilePath -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecIncorrectSpec FilePath
msg Location
LocationNothing
  where
    msg :: FilePath
msg =
      FilePath
"The input specification(s) canbot be formalized: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
e

-- | Error message associated to not being able to formalize the input spec.
commandIncorrectSpecE :: String -> String -> ErrorTriplet
commandIncorrectSpecE :: FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpecE FilePath
expr FilePath
e =
    ErrorCode -> FilePath -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecIncorrectSpec FilePath
msg Location
LocationNothing
  where
    msg :: FilePath
msg =
      FilePath
"The input specification " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
expr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" cannot be formalized: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
e

-- ** Error codes

-- | Error: there is no input argument.
ecMissingSpec :: ErrorCode
ecMissingSpec :: ErrorCode
ecMissingSpec = ErrorCode
1

-- | Error: multiple inputs of incompatible types.
ecMultipleInputTypes :: ErrorCode
ecMultipleInputTypes :: ErrorCode
ecMultipleInputTypes = ErrorCode
1

-- | Error: the input specification cannot be formalized.
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec = ErrorCode
1