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

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

-- Internal imports
import Command.Common
import Command.Errors              (ErrorCode, ErrorTriplet(..))
import Command.Result              (Result (..))
import Data.Location               (Location (..))
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 (Spec a))
-> (FilePath -> ExceptT ErrorTriplet IO (Maybe (Spec a)))
-> Maybe FilePath
-> ExceptT ErrorTriplet IO (Maybe (Spec a))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe (Spec a) -> ExceptT ErrorTriplet IO (Maybe (Spec a))
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Spec a)
forall a. Maybe a
Nothing) (\FilePath
e -> Spec a -> Maybe (Spec a)
forall a. a -> Maybe a
Just (Spec a -> Maybe (Spec a))
-> ExceptT ErrorTriplet IO (Spec a)
-> ExceptT ErrorTriplet IO (Maybe (Spec a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> ExceptT ErrorTriplet IO (Spec a)
parseInputExpr' FilePath
e) Maybe FilePath
triggerExprM
    specF <- maybe (return Nothing) (\FilePath
f -> Spec a -> Maybe (Spec a)
forall a. a -> Maybe a
Just (Spec a -> Maybe (Spec a))
-> ExceptT ErrorTriplet IO (Spec a)
-> ExceptT ErrorTriplet IO (Maybe (Spec a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> ExceptT ErrorTriplet IO (Spec a)
parseInputFile' FilePath
f) fpM
    let spec = Maybe (Spec a)
specT Maybe (Spec a) -> Maybe (Spec a) -> Maybe (Spec a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (Spec a)
specF

    case spec of
      Maybe (Spec 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 Spec a
spec' -> Maybe FilePath
-> Maybe FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
forall a.
Maybe FilePath
-> Maybe FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
commandLogic Maybe FilePath
triggerExprM Maybe FilePath
fpM FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT Spec a
spec'

  where
    triggerExprM :: Maybe FilePath
triggerExprM   = CommandOptions -> Maybe FilePath
commandConditionExpr CommandOptions
options
    fpM :: Maybe FilePath
fpM            = CommandOptions -> Maybe FilePath
commandInputFile 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

    parseInputExpr' :: FilePath -> ExceptT ErrorTriplet IO (Spec a)
parseInputExpr' 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)
parseInputExpr FilePath
e FilePath
propFormatName Maybe FilePath
propVia ExprPairT a
exprT

    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


-- | Generate the data of a new standalone Copilot monitor that implements the
-- spec, using a subexpression handler.
commandLogic :: Maybe String
             -> Maybe FilePath
             -> String
             -> [(String, String)]
             -> ExprPairT a
             -> Spec a
             -> ExceptT ErrorTriplet IO AppData
commandLogic :: forall a.
Maybe FilePath
-> Maybe FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
commandLogic Maybe FilePath
expr Maybe FilePath
fp FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT 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, Maybe FilePath
fp) of
      (Maybe FilePath
Nothing,    Just FilePath
fp') -> FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpecF FilePath
fp'
      (Just FilePath
expr', Maybe FilePath
_)        -> FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpecE FilePath
expr'
      (Maybe FilePath
_, Maybe FilePath
_)                 -> FilePath -> FilePath -> ErrorTriplet
forall a. HasCallStack => FilePath -> a
error FilePath
"Both expression and file are missing"

    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 -> Maybe FilePath
commandInputFile   :: Maybe FilePath     -- ^ Input specification file.
  , 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 not being able to formalize the input spec.
commandIncorrectSpecF :: String -> String -> ErrorTriplet
commandIncorrectSpecF :: FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpecF FilePath
file FilePath
e =
    ErrorCode -> FilePath -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecIncorrectSpec FilePath
msg (FilePath -> Location
LocationFile FilePath
file)
  where
    msg :: FilePath
msg =
      FilePath
"The input specification " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" 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: the input specification cannot be formalized.
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec = ErrorCode
1

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

mapLeft :: (a -> c) -> Either a b -> Either c b
mapLeft :: forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft a -> c
f (Left a
x)  = c -> Either c b
forall a b. a -> Either a b
Left (a -> c
f a
x)
mapLeft a -> c
_ (Right b
x) = b -> Either c b
forall a b. b -> Either a b
Right b
x