{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiWayIf                #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ScopedTypeVariables       #-}
-- Copyright 2022 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
--
-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
-- IT "AS IS."
--
-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
-- AGREEMENT.
--
-- | Shared functions across multiple backends.
module Command.Common
    ( parseInputFile
    , parseVariablesFile
    , parseRequirementsListFile
    , openVarDBFiles
    , openVarDBFilesWithDefault
    , parseTemplateVarsFile
    , checkArguments
    , specExtractExternalVariables
    , specExtractHandlers
    , ExprPair(..)
    , ExprPairT(..)
    , exprPair
    , processResult
    , cannotCopyTemplate
    , makeLeftE
    , mergeObjects
    , locateTemplateDir
    )
  where

-- External imports
import qualified Control.Exception      as E
import           Control.Monad.Except   (ExceptT (..), runExceptT, throwError)
import           Control.Monad.IO.Class (liftIO)
import           Data.Aeson             (Value (Null, Object), eitherDecode,
                                         eitherDecodeFileStrict, object)
import           Data.Aeson.KeyMap      (union)
import qualified Data.ByteString.Lazy   as L
import           Data.List              (isInfixOf, isPrefixOf)
import           System.Directory       (doesFileExist)
import           System.FilePath        ((</>))
import           System.Process         (readProcess)

-- External imports: auxiliary
import Data.ByteString.Extra as B (safeReadFile)
import Data.String.Extra     (sanitizeLCIdentifier, sanitizeUCIdentifier)

-- External imports: ogma
import Data.OgmaSpec            (Spec, externalVariableName, externalVariables,
                                 requirementName, requirementResultType,
                                 requirements)
import Language.CSVSpec.Parser  (parseCSVSpec)
import Language.JSONSpec.Parser (parseJSONSpec)
import Language.XLSXSpec.Parser (parseXLSXSpec)
import Language.XMLSpec.Parser  (parseXMLSpec)

-- External imports: language ASTs, transformers
import qualified Language.Lustre.AbsLustre as Lustre
import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec)

import qualified Language.SMV.AbsSMV       as SMV
import qualified Language.SMV.ParSMV       as SMV (myLexer, pBoolSpec)
import           Language.SMV.Substitution (substituteBoolExpr)

import qualified Language.Trans.Lustre2Copilot as Lustre (boolSpec2Copilot,
                                                          boolSpecNames)
import           Language.Trans.SMV2Copilot    as SMV (boolSpec2Copilot,
                                                       boolSpecNames)

-- Internal imports: VariableDBs
import Command.VariableDB (VariableDB, emptyVariableDB, mergeVariableDB)

-- Internal imports: auxiliary
import Command.Errors  (ErrorTriplet(..), ErrorCode)
import Command.Result  (Result (..))
import Data.Location   (Location (..))
import Paths_ogma_core (getDataDir)

-- | Process input specification, if available, and return its abstract
-- representation.
parseInputFile :: FilePath
               -> String
               -> String
               -> Maybe String
               -> ExprPairT a
               -> ExceptT ErrorTriplet IO (Spec a)
parseInputFile :: forall a.
String
-> String
-> String
-> Maybe String
-> ExprPairT a
-> ExceptT ErrorTriplet IO (Spec a)
parseInputFile String
fp String
formatName String
propFormatName Maybe String
propVia ExprPairT a
exprT =
  IO (Either ErrorTriplet (Spec a))
-> ExceptT ErrorTriplet IO (Spec a)
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either ErrorTriplet (Spec a))
 -> ExceptT ErrorTriplet IO (Spec a))
-> IO (Either ErrorTriplet (Spec a))
-> ExceptT ErrorTriplet IO (Spec a)
forall a b. (a -> b) -> a -> b
$ do
    let ExprPairT String -> Either String a
parse [(String, String)] -> a -> a
replace a -> String
print a -> [String]
ids a
def = ExprPairT a
exprT

    let wrapper :: String -> IO (Either String a)
wrapper = Maybe String
-> (String -> Either String a) -> String -> IO (Either String a)
forall a.
Maybe String
-> (String -> Either String a) -> String -> IO (Either String a)
wrapVia Maybe String
propVia String -> Either String a
parse
    -- Obtain format file.
    --
    -- A format name that exists as a file in the disk always takes preference
    -- over a file format included with Ogma. A file format with a forward
    -- slash in the name is always assumed to be a user-provided filename.
    -- Regardless of whether the file is user-provided or known to Ogma, we
    -- check (again) whether the file exists, and print an error message if
    -- not.
    Bool
exists  <- String -> IO Bool
doesFileExist String
formatName
    String
dataDir <- IO String
getDataDir
    let formatFile :: String
formatFile
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
"/" String
formatName Bool -> Bool -> Bool
|| Bool
exists
          = String
formatName
          | Bool
otherwise
          = String
dataDir String -> String -> String
</> String
"data" String -> String -> String
</> String
"formats" String -> String -> String
</>
               (String
formatName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
propFormatName)
    Bool
formatMissing <- Bool -> Bool
not (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO Bool
doesFileExist String
formatFile

    if Bool
formatMissing
      then Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a)))
-> Either ErrorTriplet (Spec a)
-> IO (Either ErrorTriplet (Spec a))
forall a b. (a -> b) -> a -> b
$ ErrorTriplet -> Either ErrorTriplet (Spec a)
forall a b. a -> Either a b
Left (ErrorTriplet -> Either ErrorTriplet (Spec a))
-> ErrorTriplet -> Either ErrorTriplet (Spec a)
forall a b. (a -> b) -> a -> b
$ String -> ErrorTriplet
commandIncorrectFormatSpec String
formatFile
      else do
        Either String (Spec a)
res <- do
          String
format <- String -> IO String
readFile String
formatFile

          -- All of the following operations use Either to return error
          -- messages.  The use of the monadic bind to pass arguments from one
          -- function to the next will cause the program to stop at the
          -- earliest error.
          if | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"XMLFormat" String
format
             -> do let xmlFormat :: XMLFormat
xmlFormat = String -> XMLFormat
forall a. Read a => String -> a
read String
format
                   String
content <- String -> IO String
readFile String
fp
                   (String -> IO (Either String a))
-> a -> XMLFormat -> String -> IO (Either String (Spec a))
forall a.
(String -> IO (Either String a))
-> a -> XMLFormat -> String -> IO (Either String (Spec a))
parseXMLSpec
                     (String -> IO (Either String a)
wrapper) (a
def) XMLFormat
xmlFormat String
content
                     -- (fmap (fmap print) . wrapper) (print def) xmlFormat content
             | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"CSVFormat" String
format
             -> do let csvFormat :: CSVFormat
csvFormat = String -> CSVFormat
forall a. Read a => String -> a
read String
format
                   String
content <- String -> IO String
readFile String
fp
                   (String -> IO (Either String a))
-> a -> CSVFormat -> String -> IO (Either String (Spec a))
forall a.
(String -> IO (Either String a))
-> a -> CSVFormat -> String -> IO (Either String (Spec a))
parseCSVSpec String -> IO (Either String a)
wrapper a
def CSVFormat
csvFormat String
content
             | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"XLSXFormat" String
format
             -> do let xlsxFormat :: XLSXFormat
xlsxFormat = String -> XLSXFormat
forall a. Read a => String -> a
read String
format
                   ByteString
content <- String -> IO ByteString
L.readFile String
fp
                   (String -> IO (Either String a))
-> a -> XLSXFormat -> ByteString -> IO (Either String (Spec a))
forall a.
(String -> IO (Either String a))
-> a -> XLSXFormat -> ByteString -> IO (Either String (Spec a))
parseXLSXSpec String -> IO (Either String a)
wrapper a
def XLSXFormat
xlsxFormat ByteString
content
             | Bool
otherwise
             -> do let jsonFormat :: JSONFormat
jsonFormat = String -> JSONFormat
forall a. Read a => String -> a
read String
format
                   Either String ByteString
content <- String -> IO (Either String ByteString)
B.safeReadFile String
fp
                   case Either String ByteString
content of
                     Left String
e  -> Either String (Spec a) -> IO (Either String (Spec a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Spec a) -> IO (Either String (Spec a)))
-> Either String (Spec a) -> IO (Either String (Spec a))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Spec a)
forall a b. a -> Either a b
Left String
e
                     Right ByteString
b -> do case ByteString -> Either String Value
forall a. FromJSON a => ByteString -> Either String a
eitherDecode ByteString
b of
                                     Left String
e  -> Either String (Spec a) -> IO (Either String (Spec a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Spec a) -> IO (Either String (Spec a)))
-> Either String (Spec a) -> IO (Either String (Spec a))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Spec a)
forall a b. a -> Either a b
Left String
e
                                     Right Value
v ->
                                       (String -> IO (Either String a))
-> JSONFormat -> Value -> IO (Either String (Spec a))
forall a.
(String -> IO (Either String a))
-> JSONFormat -> Value -> IO (Either String (Spec a))
parseJSONSpec
                                         (String -> IO (Either String a)
wrapper)
                                         JSONFormat
jsonFormat
                                         Value
v
        case Either String (Spec a)
res of
          Left String
e  -> Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a)))
-> Either ErrorTriplet (Spec a)
-> IO (Either ErrorTriplet (Spec a))
forall a b. (a -> b) -> a -> b
$ ErrorTriplet -> Either ErrorTriplet (Spec a)
forall a b. a -> Either a b
Left (ErrorTriplet -> Either ErrorTriplet (Spec a))
-> ErrorTriplet -> Either ErrorTriplet (Spec a)
forall a b. (a -> b) -> a -> b
$ String -> ErrorTriplet
cannotOpenInputFile String
fp
          Right Spec a
x -> Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorTriplet (Spec a) -> IO (Either ErrorTriplet (Spec a)))
-> Either ErrorTriplet (Spec a)
-> IO (Either ErrorTriplet (Spec a))
forall a b. (a -> b) -> a -> b
$ Spec a -> Either ErrorTriplet (Spec a)
forall a b. b -> Either a b
Right Spec a
x

-- | Process a variable selection file, if available, and return the variable
-- names.
parseVariablesFile :: Maybe FilePath
                   -> ExceptT ErrorTriplet IO (Maybe [String])
parseVariablesFile :: Maybe String -> ExceptT ErrorTriplet IO (Maybe [String])
parseVariablesFile Maybe String
Nothing   = Maybe [String] -> ExceptT ErrorTriplet IO (Maybe [String])
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [String]
forall a. Maybe a
Nothing
parseVariablesFile (Just String
fp) = do
  -- Fail if the file cannot be opened.
  Either SomeException [String]
varNamesE <- IO (Either SomeException [String])
-> ExceptT ErrorTriplet IO (Either SomeException [String])
forall a. IO a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either SomeException [String])
 -> ExceptT ErrorTriplet IO (Either SomeException [String]))
-> IO (Either SomeException [String])
-> ExceptT ErrorTriplet IO (Either SomeException [String])
forall a b. (a -> b) -> a -> b
$ IO [String] -> IO (Either SomeException [String])
forall e a. Exception e => IO a -> IO (Either e a)
E.try (IO [String] -> IO (Either SomeException [String]))
-> IO [String] -> IO (Either SomeException [String])
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines (String -> [String]) -> IO String -> IO [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
fp
  case (Either SomeException [String]
varNamesE :: Either E.SomeException [String]) of
    Left SomeException
_         -> ErrorTriplet -> ExceptT ErrorTriplet IO (Maybe [String])
forall a. ErrorTriplet -> ExceptT ErrorTriplet IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ErrorTriplet -> ExceptT ErrorTriplet IO (Maybe [String]))
-> ErrorTriplet -> ExceptT ErrorTriplet IO (Maybe [String])
forall a b. (a -> b) -> a -> b
$ String -> ErrorTriplet
cannotOpenVarFile String
fp
    Right [String]
varNames -> Maybe [String] -> ExceptT ErrorTriplet IO (Maybe [String])
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String] -> ExceptT ErrorTriplet IO (Maybe [String]))
-> Maybe [String] -> ExceptT ErrorTriplet IO (Maybe [String])
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
varNames

-- | Process a requirements / handlers list file, if available, and return the
-- handler names.
parseRequirementsListFile :: Maybe FilePath
                          -> ExceptT ErrorTriplet IO (Maybe [String])
parseRequirementsListFile :: Maybe String -> ExceptT ErrorTriplet IO (Maybe [String])
parseRequirementsListFile Maybe String
Nothing   = Maybe [String] -> ExceptT ErrorTriplet IO (Maybe [String])
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [String]
forall a. Maybe a
Nothing
parseRequirementsListFile (Just String
fp) =
  IO (Either ErrorTriplet (Maybe [String]))
-> ExceptT ErrorTriplet IO (Maybe [String])
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either ErrorTriplet (Maybe [String]))
 -> ExceptT ErrorTriplet IO (Maybe [String]))
-> IO (Either ErrorTriplet (Maybe [String]))
-> ExceptT ErrorTriplet IO (Maybe [String])
forall a b. (a -> b) -> a -> b
$ ErrorTriplet
-> Either SomeException (Maybe [String])
-> Either ErrorTriplet (Maybe [String])
forall c b. c -> Either SomeException b -> Either c b
makeLeftE (String -> ErrorTriplet
cannotOpenHandlersFile String
fp) (Either SomeException (Maybe [String])
 -> Either ErrorTriplet (Maybe [String]))
-> IO (Either SomeException (Maybe [String]))
-> IO (Either ErrorTriplet (Maybe [String]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (IO (Maybe [String]) -> IO (Either SomeException (Maybe [String]))
forall e a. Exception e => IO a -> IO (Either e a)
E.try (IO (Maybe [String]) -> IO (Either SomeException (Maybe [String])))
-> IO (Maybe [String])
-> IO (Either SomeException (Maybe [String]))
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String])
-> (String -> [String]) -> String -> Maybe [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> Maybe [String]) -> IO String -> IO (Maybe [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
fp)

-- | Read a list of variable DBs.
openVarDBFiles :: VariableDB
               -> [FilePath]
               -> ExceptT ErrorTriplet IO VariableDB
openVarDBFiles :: VariableDB -> [String] -> ExceptT ErrorTriplet IO VariableDB
openVarDBFiles VariableDB
acc []     = VariableDB -> ExceptT ErrorTriplet IO VariableDB
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return VariableDB
acc
openVarDBFiles VariableDB
acc (String
x:[String]
xs) = do
    VariableDB
file <- Maybe String -> ExceptT ErrorTriplet IO VariableDB
parseVarDBFile (String -> Maybe String
forall a. a -> Maybe a
Just String
x)
    VariableDB
acc' <- VariableDB -> VariableDB -> ExceptT ErrorTriplet IO VariableDB
forall (m :: * -> *).
Monad m =>
VariableDB -> VariableDB -> ExceptT ErrorTriplet m VariableDB
mergeVariableDB VariableDB
acc VariableDB
file
    VariableDB -> [String] -> ExceptT ErrorTriplet IO VariableDB
openVarDBFiles VariableDB
acc' [String]
xs

  where

    -- Process a variable database file, if available.
    parseVarDBFile :: Maybe FilePath
                   -> ExceptT ErrorTriplet IO VariableDB
    parseVarDBFile :: Maybe String -> ExceptT ErrorTriplet IO VariableDB
parseVarDBFile Maybe String
Nothing   = VariableDB -> ExceptT ErrorTriplet IO VariableDB
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return VariableDB
emptyVariableDB
    parseVarDBFile (Just String
fn) =
      IO (Either ErrorTriplet VariableDB)
-> ExceptT ErrorTriplet IO VariableDB
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either ErrorTriplet VariableDB)
 -> ExceptT ErrorTriplet IO VariableDB)
-> IO (Either ErrorTriplet VariableDB)
-> ExceptT ErrorTriplet IO VariableDB
forall a b. (a -> b) -> a -> b
$ ErrorTriplet
-> Either String VariableDB -> Either ErrorTriplet VariableDB
forall c a b. c -> Either a b -> Either c b
makeLeftE' (String -> ErrorTriplet
cannotOpenDB String
fn) (Either String VariableDB -> Either ErrorTriplet VariableDB)
-> IO (Either String VariableDB)
-> IO (Either ErrorTriplet VariableDB)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        String -> IO (Either String VariableDB)
forall a. FromJSON a => String -> IO (Either String a)
eitherDecodeFileStrict String
fn

-- | Read a list of variable DBs, as well as the default variable DB.
openVarDBFilesWithDefault :: [FilePath]
                          -> ExceptT ErrorTriplet IO VariableDB
openVarDBFilesWithDefault :: [String] -> ExceptT ErrorTriplet IO VariableDB
openVarDBFilesWithDefault [String]
files = do
  String
dataDir <- IO String -> ExceptT ErrorTriplet IO String
forall a. IO a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getDataDir
  let defaultDB :: String
defaultDB = String
dataDir String -> String -> String
</> String
"data" String -> String -> String
</> String
"variable-db.json"
  VariableDB -> [String] -> ExceptT ErrorTriplet IO VariableDB
openVarDBFiles VariableDB
emptyVariableDB ([String]
files [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
defaultDB])

-- | Process a JSON file with additional template variables to make available
-- during template expansion.
parseTemplateVarsFile :: Maybe FilePath
                      -> ExceptT ErrorTriplet IO Value
parseTemplateVarsFile :: Maybe String -> ExceptT ErrorTriplet IO Value
parseTemplateVarsFile Maybe String
Nothing   = Value -> ExceptT ErrorTriplet IO Value
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> ExceptT ErrorTriplet IO Value)
-> Value -> ExceptT ErrorTriplet IO Value
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
object []
parseTemplateVarsFile (Just String
fp) = do
  Either String ByteString
content <- IO (Either String ByteString)
-> ExceptT ErrorTriplet IO (Either String ByteString)
forall a. IO a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String ByteString)
 -> ExceptT ErrorTriplet IO (Either String ByteString))
-> IO (Either String ByteString)
-> ExceptT ErrorTriplet IO (Either String ByteString)
forall a b. (a -> b) -> a -> b
$ String -> IO (Either String ByteString)
B.safeReadFile String
fp
  let value :: Either String Value
value = ByteString -> Either String Value
forall a. FromJSON a => ByteString -> Either String a
eitherDecode (ByteString -> Either String Value)
-> Either String ByteString -> Either String Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Either String ByteString
content
  case Either String Value
value of
    Right x :: Value
x@(Object Object
_) -> Value -> ExceptT ErrorTriplet IO Value
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
x
    Right x :: Value
x@Value
Null       -> Value -> ExceptT ErrorTriplet IO Value
forall a. a -> ExceptT ErrorTriplet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
x
    Right Value
_            -> ErrorTriplet -> ExceptT ErrorTriplet IO Value
forall a. ErrorTriplet -> ExceptT ErrorTriplet IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ErrorTriplet
cannotReadObjectTemplateVars String
fp)
    Either String Value
_                  -> ErrorTriplet -> ExceptT ErrorTriplet IO Value
forall a. ErrorTriplet -> ExceptT ErrorTriplet IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ErrorTriplet
cannotOpenTemplateVars String
fp)

-- | Check that the arguments provided are sufficient to operate.
--
-- The backend provides several modes of operation, which are selected
-- by providing different arguments to the `ros` command.
--
-- When an input specification file is provided, the variables and requirements
-- defined in it are used unless variables or handlers files are provided, in
-- which case the latter take priority.
--
-- If an input file is not provided, then the user must provide BOTH a variable
-- list, and a list of handlers.
checkArguments :: Maybe (Spec a)
               -> Maybe [String]
               -> Maybe [String]
               -> Either ErrorTriplet ()
checkArguments :: forall a.
Maybe (Spec a)
-> Maybe [String] -> Maybe [String] -> Either ErrorTriplet ()
checkArguments Maybe (Spec a)
Nothing Maybe [String]
Nothing   Maybe [String]
Nothing   = ErrorTriplet -> Either ErrorTriplet ()
forall a b. a -> Either a b
Left ErrorTriplet
wrongArguments
checkArguments Maybe (Spec a)
Nothing Maybe [String]
Nothing   Maybe [String]
_         = ErrorTriplet -> Either ErrorTriplet ()
forall a b. a -> Either a b
Left ErrorTriplet
wrongArguments
checkArguments Maybe (Spec a)
Nothing Maybe [String]
_         Maybe [String]
Nothing   = ErrorTriplet -> Either ErrorTriplet ()
forall a b. a -> Either a b
Left ErrorTriplet
wrongArguments
checkArguments Maybe (Spec a)
_       (Just []) Maybe [String]
_         = ErrorTriplet -> Either ErrorTriplet ()
forall a b. a -> Either a b
Left ErrorTriplet
wrongArguments
checkArguments Maybe (Spec a)
_       Maybe [String]
_         (Just []) = ErrorTriplet -> Either ErrorTriplet ()
forall a b. a -> Either a b
Left ErrorTriplet
wrongArguments
checkArguments Maybe (Spec a)
_       Maybe [String]
_         Maybe [String]
_         = () -> Either ErrorTriplet ()
forall a b. b -> Either a b
Right ()

-- | Extract the variables from a specification, and sanitize them.
specExtractExternalVariables :: Maybe (Spec a) -> [String]
specExtractExternalVariables :: forall a. Maybe (Spec a) -> [String]
specExtractExternalVariables Maybe (Spec a)
Nothing   = []
specExtractExternalVariables (Just Spec a
cs) = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
sanitizeLCIdentifier
                                       ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (ExternalVariableDef -> String)
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ExternalVariableDef -> String
externalVariableName
                                       ([ExternalVariableDef] -> [String])
-> [ExternalVariableDef] -> [String]
forall a b. (a -> b) -> a -> b
$ Spec a -> [ExternalVariableDef]
forall a. Spec a -> [ExternalVariableDef]
externalVariables Spec a
cs

-- | Extract the requirements from a specification, and sanitize them to match
-- the names of the handlers used by Copilot.
specExtractHandlers :: Maybe (Spec a) -> [(String, Maybe String)]
specExtractHandlers :: forall a. Maybe (Spec a) -> [(String, Maybe String)]
specExtractHandlers Maybe (Spec a)
Nothing   = []
specExtractHandlers (Just Spec a
cs) = (Requirement a -> (String, Maybe String))
-> [Requirement a] -> [(String, Maybe String)]
forall a b. (a -> b) -> [a] -> [b]
map Requirement a -> (String, Maybe String)
forall {a}. Requirement a -> (String, Maybe String)
extractReqData
                              ([Requirement a] -> [(String, Maybe String)])
-> [Requirement a] -> [(String, Maybe String)]
forall a b. (a -> b) -> a -> b
$ Spec a -> [Requirement a]
forall a. Spec a -> [Requirement a]
requirements Spec a
cs
  where
    extractReqData :: Requirement a -> (String, Maybe String)
extractReqData Requirement a
r =
      (String -> String
handlerNameF (Requirement a -> String
forall a. Requirement a -> String
requirementName Requirement a
r), Requirement a -> Maybe String
forall a. Requirement a -> Maybe String
requirementResultType Requirement a
r)

    handlerNameF :: String -> String
handlerNameF = (String
"handler" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
sanitizeUCIdentifier

-- * Handler for boolean expressions

-- | Handler for boolean expressions that knows how to parse them, replace
-- variables in them, and convert them to Copilot.
--
-- It also contains a default value to be used whenever an expression cannot be
-- found in the input file.
data ExprPair = forall a . ExprPair
  { ()
exprTPair   :: ExprPairT a
  }

data ExprPairT a = ExprPairT
  { forall a. ExprPairT a -> String -> Either String a
exprTParse   :: String -> Either String a
  , forall a. ExprPairT a -> [(String, String)] -> a -> a
exprTReplace :: [(String, String)] -> a -> a
  , forall a. ExprPairT a -> a -> String
exprTPrint   :: a -> String
  , forall a. ExprPairT a -> a -> [String]
exprTIdents  :: a -> [String]
  , forall a. ExprPairT a -> a
exprTUnknown :: a
  }


-- | Return a handler depending on whether it should be for Lustre boolean
-- expressions or for SMV boolean expressions. We default to SMV if not format
-- is given.
exprPair :: String -> ExprPair
exprPair :: String -> ExprPair
exprPair String
"lustre" = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String BoolSpec)
-> ([(String, String)] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> String)
-> (BoolSpec -> [String])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either String BoolSpec
Lustre.pBoolSpec ([Token] -> Either String BoolSpec)
-> (String -> [Token]) -> String -> Either String BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
Lustre.myLexer)
    (\[(String, String)]
_ -> BoolSpec -> BoolSpec
forall a. a -> a
id)
    (BoolSpec -> String
Lustre.boolSpec2Copilot)
    (BoolSpec -> [String]
Lustre.boolSpecNames)
    (Ident -> BoolSpec
Lustre.BoolSpecSignal (String -> Ident
Lustre.Ident String
"undefined"))
exprPair String
"literal" = ExprPairT String -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT String -> ExprPair) -> ExprPairT String -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String String)
-> ([(String, String)] -> String -> String)
-> (String -> String)
-> (String -> [String])
-> String
-> ExprPairT String
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    String -> Either String String
forall a b. b -> Either a b
Right
    (\[(String, String)]
_ -> String -> String
forall a. a -> a
id)
    String -> String
forall a. a -> a
id
    ([String] -> String -> [String]
forall a b. a -> b -> a
const [])
    String
"undefined"
exprPair String
"cocospec" = String -> ExprPair
exprPair String
"lustre"
exprPair String
_ = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  (String -> Either String BoolSpec)
-> ([(String, String)] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> String)
-> (BoolSpec -> [String])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
(String -> Either String a)
-> ([(String, String)] -> a -> a)
-> (a -> String)
-> (a -> [String])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either String BoolSpec
SMV.pBoolSpec ([Token] -> Either String BoolSpec)
-> (String -> [Token]) -> String -> Either String BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
SMV.myLexer)
    ([(String, String)] -> BoolSpec -> BoolSpec
forall {t :: * -> *}.
Foldable t =>
t (String, String) -> BoolSpec -> BoolSpec
substituteBoolExpr)
    (BoolSpec -> String
SMV.boolSpec2Copilot)
    (BoolSpec -> [String]
SMV.boolSpecNames)
    (Ident -> BoolSpec
SMV.BoolSpecSignal (String -> Ident
SMV.Ident String
"undefined"))

-- * Errors

-- | Process a computation that can fail with an error code, and turn it into a
-- computation that returns a 'Result'.
processResult :: Monad m => ExceptT ErrorTriplet m a -> m (Result ErrorCode)
processResult :: forall (m :: * -> *) a.
Monad m =>
ExceptT ErrorTriplet m a -> m (Result ErrorCode)
processResult ExceptT ErrorTriplet m a
m = do
  Either ErrorTriplet a
r <- ExceptT ErrorTriplet m a -> m (Either ErrorTriplet a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT ErrorTriplet m a
m
  case Either ErrorTriplet a
r of
    Left (ErrorTriplet ErrorCode
errorCode String
msg Location
location)
      -> Result ErrorCode -> m (Result ErrorCode)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result ErrorCode -> m (Result ErrorCode))
-> Result ErrorCode -> m (Result ErrorCode)
forall a b. (a -> b) -> a -> b
$ ErrorCode -> String -> Location -> Result ErrorCode
forall a. a -> String -> Location -> Result a
Error ErrorCode
errorCode String
msg Location
location
    Either ErrorTriplet a
_ -> Result ErrorCode -> m (Result ErrorCode)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Result ErrorCode
forall a. Result a
Success

-- ** Error messages

-- | Exception handler to deal with the case in which the arguments
-- provided are incorrect.
wrongArguments :: ErrorTriplet
wrongArguments :: ErrorTriplet
wrongArguments =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecWrongArguments String
msg Location
LocationNothing
  where
    msg :: String
msg =
      String
"the arguments provided are insufficient: you must provide an input "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"specification, or both a variables and a handlers file."

-- | Exception handler to deal with the case in which the input file cannot be
-- opened.
cannotOpenInputFile :: FilePath -> ErrorTriplet
cannotOpenInputFile :: String -> ErrorTriplet
cannotOpenInputFile String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotOpenInputFile String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"cannot open input specification file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Exception handler to deal with the case in which the variable DB cannot be
-- opened.
cannotOpenDB :: FilePath -> ErrorTriplet
cannotOpenDB :: String -> ErrorTriplet
cannotOpenDB String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotOpenDBFile String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"cannot open variable DB file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Exception handler to deal with the case in which the variable file
-- provided by the user cannot be opened.
cannotOpenVarFile :: FilePath -> ErrorTriplet
cannotOpenVarFile :: String -> ErrorTriplet
cannotOpenVarFile String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotOpenVarFile  String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"cannot open variable list file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Exception handler to deal with the case in which the handlers file cannot
-- be opened.
cannotOpenHandlersFile :: FilePath -> ErrorTriplet
cannotOpenHandlersFile :: String -> ErrorTriplet
cannotOpenHandlersFile String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotOpenHandlersFile String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"cannot open handlers file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Error message associated to the format file not being found.
commandIncorrectFormatSpec :: FilePath -> ErrorTriplet
commandIncorrectFormatSpec :: String -> ErrorTriplet
commandIncorrectFormatSpec String
formatFile =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecIncorrectFormatFile String
msg (String -> Location
LocationFile String
formatFile)
  where
    msg :: String
msg =
      String
"The format specification " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
formatFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not exist or is not "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"readable"

-- | Exception handler to deal with the case in which the template vars file
-- cannot be opened.
cannotOpenTemplateVars :: FilePath -> ErrorTriplet
cannotOpenTemplateVars :: String -> ErrorTriplet
cannotOpenTemplateVars String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotOpenTemplateVarsFile String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"Cannot open file with additional template variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Exception handler to deal with the case in which the template vars file
-- cannot be opened.
cannotReadObjectTemplateVars :: FilePath -> ErrorTriplet
cannotReadObjectTemplateVars :: String -> ErrorTriplet
cannotReadObjectTemplateVars String
file =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotReadObjectTemplateVarsFile String
msg (String -> Location
LocationFile String
file)
  where
    msg :: String
msg =
      String
"Cannot open file with additional template variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | Exception handler to deal with the case of files that cannot be
-- copied/generated due lack of space or permissions or some I/O error.
cannotCopyTemplate :: ErrorTriplet
cannotCopyTemplate :: ErrorTriplet
cannotCopyTemplate =
    ErrorCode -> String -> Location -> ErrorTriplet
ErrorTriplet ErrorCode
ecCannotCopyTemplate String
msg Location
LocationNothing
  where
    msg :: String
msg =
      String
"Generation failed during copy/write operation. Check that"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" there's free space in the disk and that you have the necessary"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" permissions to write in the destination directory."

-- ** Error codes

-- | Error: wrong arguments provided.
ecWrongArguments :: ErrorCode
ecWrongArguments :: ErrorCode
ecWrongArguments = ErrorCode
1

-- | Error: the input specification provided by the user cannot be opened.
ecCannotOpenInputFile :: ErrorCode
ecCannotOpenInputFile :: ErrorCode
ecCannotOpenInputFile = ErrorCode
1

-- | Error: the variable DB provided by the user cannot be opened.
ecCannotOpenDBFile :: ErrorCode
ecCannotOpenDBFile :: ErrorCode
ecCannotOpenDBFile = ErrorCode
1

-- | Error: the variable file provided by the user cannot be opened.
ecCannotOpenVarFile :: ErrorCode
ecCannotOpenVarFile :: ErrorCode
ecCannotOpenVarFile = ErrorCode
1

-- | Error: the handlers file provided by the user cannot be opened.
ecCannotOpenHandlersFile :: ErrorCode
ecCannotOpenHandlersFile :: ErrorCode
ecCannotOpenHandlersFile = ErrorCode
1

-- | Error: the format file cannot be opened.
ecIncorrectFormatFile :: ErrorCode
ecIncorrectFormatFile :: ErrorCode
ecIncorrectFormatFile = ErrorCode
1

-- | Error: the template vars file provided by the user cannot be opened.
ecCannotOpenTemplateVarsFile :: ErrorCode
ecCannotOpenTemplateVarsFile :: ErrorCode
ecCannotOpenTemplateVarsFile = ErrorCode
1

-- | Error: the template variables file passed does not contain a JSON object.
ecCannotReadObjectTemplateVarsFile :: ErrorCode
ecCannotReadObjectTemplateVarsFile :: ErrorCode
ecCannotReadObjectTemplateVarsFile = ErrorCode
1

-- | Error: the files cannot be copied/generated due lack of space or
-- permissions or some I/O error.
ecCannotCopyTemplate :: ErrorCode
ecCannotCopyTemplate :: ErrorCode
ecCannotCopyTemplate = ErrorCode
1

-- * Auxiliary Functions

-- | Return the path to the template directory.
locateTemplateDir :: Maybe FilePath
                  -> FilePath
                  -> ExceptT e IO FilePath
locateTemplateDir :: forall e. Maybe String -> String -> ExceptT e IO String
locateTemplateDir Maybe String
mTemplateDir String
name =
  case Maybe String
mTemplateDir of
    Just String
x  -> String -> ExceptT e IO String
forall a. a -> ExceptT e IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
x
    Maybe String
Nothing -> IO String -> ExceptT e IO String
forall a. IO a -> ExceptT e IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> ExceptT e IO String)
-> IO String -> ExceptT e IO String
forall a b. (a -> b) -> a -> b
$ do
      String
dataDir <- IO String
getDataDir
      String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
dataDir String -> String -> String
</> String
"templates" String -> String -> String
</> String
name

-- | Parse a property using an auxiliary program to first translate it, if
-- available.
--
-- If a program is given, it is first called on the property, and then the
-- result is parsed with the parser passed as an argument. If a program is not
-- given, then the parser is applied to the given string.
wrapVia :: Maybe String                -- ^ Auxiliary program to translate the
                                       -- property.
        -> (String -> Either String a) -- ^ Parser used on the result.
        -> String                      -- ^ Property to parse.
        -> IO (Either String a)
wrapVia :: forall a.
Maybe String
-> (String -> Either String a) -> String -> IO (Either String a)
wrapVia Maybe String
Nothing  String -> Either String a
parse String
s = Either String a -> IO (Either String a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String a
parse String
s)
wrapVia (Just String
f) String -> Either String a
parse String
s =
  (IOException -> IO (Either String a))
-> IO (Either String a) -> IO (Either String a)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
E.handle (\(IOException
e :: E.IOException) -> Either String a -> IO (Either String a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String a -> IO (Either String a))
-> Either String a -> IO (Either String a)
forall a b. (a -> b) -> a -> b
$ String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ IOException -> String
forall a. Show a => a -> String
show IOException
e) (IO (Either String a) -> IO (Either String a))
-> IO (Either String a) -> IO (Either String a)
forall a b. (a -> b) -> a -> b
$ do
    String
out <- String -> [String] -> String -> IO String
readProcess String
f [] String
s
    Either String a -> IO (Either String a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String a -> IO (Either String a))
-> Either String a -> IO (Either String a)
forall a b. (a -> b) -> a -> b
$ String -> Either String a
parse String
out

-- | Merge two JSON objects.
--
-- Fails if the values are not objects or null.
mergeObjects :: Value -> Value -> Value
mergeObjects :: Value -> Value -> Value
mergeObjects (Object Object
m1) (Object Object
m2) = Object -> Value
Object (Object -> Object -> Object
forall v. KeyMap v -> KeyMap v -> KeyMap v
union Object
m1 Object
m2)
mergeObjects Value
obj         Value
Null        = Value
obj
mergeObjects Value
Null        Value
obj         = Value
obj
mergeObjects Value
_           Value
_           = String -> Value
forall a. HasCallStack => String -> a
error String
"The values passed are not objects"

-- | Replace the left Exception in an Either.
makeLeftE :: c -> Either E.SomeException b -> Either c b
makeLeftE :: forall c b. c -> Either SomeException b -> Either c b
makeLeftE = c -> Either SomeException b -> Either c b
forall c a b. c -> Either a b -> Either c b
makeLeftE'

-- | Replace the left value in an @Either@.
makeLeftE' :: c -> Either a b -> Either c b
makeLeftE' :: forall c a b. c -> Either a b -> Either c b
makeLeftE' c
c (Left a
_)  = c -> Either c b
forall a b. a -> Either a b
Left c
c
makeLeftE' c
_ (Right b
x) = b -> Either c b
forall a b. b -> Either a b
Right b
x