{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Command.Standalone
( command
, commandLogic
, AppData
, CommandOptions(..)
, ErrorCode
)
where
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)
import Data.OgmaSpec (ExternalVariableDef (..),
InternalVariableDef (..), Requirement (..),
Spec (..))
import System.Directory.Extra (copyTemplate)
import Command.Common
import Command.Errors (ErrorCode, ErrorTriplet(..))
import Command.Result (Result (..))
import Data.Location (Location (..))
import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze)
command :: CommandOptions
-> 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
FilePath
templateDir <- Maybe FilePath -> FilePath -> ExceptT ErrorTriplet IO FilePath
forall e. Maybe FilePath -> FilePath -> ExceptT e IO FilePath
locateTemplateDir Maybe FilePath
mTemplateDir FilePath
"standalone"
Value
templateVars <- Maybe FilePath -> ExceptT ErrorTriplet IO Value
parseTemplateVarsFile Maybe FilePath
templateVarsF
AppData
appData <- CommandOptions -> ExprPair -> ExceptT ErrorTriplet IO AppData
command' CommandOptions
options ExprPair
functions
let subst :: Value
subst = Value -> Value -> Value
mergeObjects (AppData -> Value
forall a. ToJSON a => a -> Value
toJSON AppData
appData) Value
templateVars
IO (Either ErrorTriplet ()) -> ExceptT ErrorTriplet IO ()
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either ErrorTriplet ()) -> ExceptT ErrorTriplet IO ())
-> IO (Either ErrorTriplet ()) -> ExceptT ErrorTriplet IO ()
forall a b. (a -> b) -> a -> b
$ (Either SomeException () -> Either ErrorTriplet ())
-> IO (Either SomeException ()) -> IO (Either ErrorTriplet ())
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ErrorTriplet -> Either SomeException () -> Either ErrorTriplet ()
forall c b. c -> Either SomeException b -> Either c b
makeLeftE ErrorTriplet
cannotCopyTemplate) (IO (Either SomeException ()) -> IO (Either ErrorTriplet ()))
-> IO (Either SomeException ()) -> IO (Either ErrorTriplet ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO (Either SomeException ())
forall e a. Exception e => IO a -> IO (Either e a)
E.try (IO () -> IO (Either SomeException ()))
-> IO () -> IO (Either SomeException ())
forall a b. (a -> b) -> a -> b
$
FilePath -> Value -> FilePath -> IO ()
copyTemplate FilePath
templateDir Value
subst FilePath
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
command' :: CommandOptions
-> ExprPair
-> ExceptT ErrorTriplet IO AppData
command' :: CommandOptions -> ExprPair -> ExceptT ErrorTriplet IO AppData
command' CommandOptions
options (ExprPair ExprPairT a
exprT) = do
Spec a
input <- 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
fp FilePath
formatName FilePath
propFormatName Maybe FilePath
propVia ExprPairT a
exprT
FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
forall a.
FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
commandLogic FilePath
fp FilePath
name [(FilePath, FilePath)]
typeMaps ExprPairT a
exprT Spec a
input
where
fp :: FilePath
fp = CommandOptions -> 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
commandLogic :: FilePath
-> String
-> [(String, String)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
commandLogic :: forall a.
FilePath
-> FilePath
-> [(FilePath, FilePath)]
-> ExprPairT a
-> Spec a
-> ExceptT ErrorTriplet IO AppData
commandLogic 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
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 -> FilePath -> ErrorTriplet
commandIncorrectSpec FilePath
fp) (Either FilePath AppData -> Either ErrorTriplet AppData)
-> Either FilePath AppData -> Either ErrorTriplet AppData
forall a b. (a -> b) -> a -> b
$ do
Spec a
spec' <- Spec a -> Either FilePath (Spec a)
forall a. Spec a -> Either FilePath (Spec a)
specAnalyze Spec a
spec
(FilePath, FilePath, FilePath, FilePath, FilePath)
res <- FilePath
-> [(FilePath, FilePath)]
-> ([(FilePath, FilePath)] -> a -> a)
-> (a -> FilePath)
-> Spec a
-> Either
FilePath (FilePath, FilePath, FilePath, FilePath, FilePath)
forall a.
FilePath
-> [(FilePath, FilePath)]
-> ([(FilePath, FilePath)] -> a -> a)
-> (a -> FilePath)
-> Spec a
-> Either
FilePath (FilePath, FilePath, FilePath, FilePath, FilePath)
spec2Copilot FilePath
name [(FilePath, FilePath)]
typeMaps [(FilePath, FilePath)] -> a -> a
replace a -> FilePath
print Spec a
spec'
let (FilePath
ext, FilePath
int, FilePath
reqs, FilePath
trigs, FilePath
specN) = (FilePath, FilePath, FilePath, FilePath, FilePath)
res
AppData -> Either FilePath AppData
forall a. a -> Either FilePath a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppData -> Either FilePath AppData)
-> AppData -> Either FilePath AppData
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath -> FilePath -> AppData
AppData FilePath
ext FilePath
int FilePath
reqs FilePath
trigs FilePath
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
ExprPairT FilePath -> Either FilePath a
parse [(FilePath, FilePath)] -> a -> a
replace a -> FilePath
print a -> [FilePath]
ids a
def = ExprPairT a
exprT
data CommandOptions = CommandOptions
{ CommandOptions -> FilePath
commandInputFile :: FilePath
, CommandOptions -> FilePath
commandTargetDir :: FilePath
, CommandOptions -> Maybe FilePath
commandTemplateDir :: Maybe FilePath
, CommandOptions -> FilePath
commandFormat :: String
, CommandOptions -> FilePath
commandPropFormat :: String
, CommandOptions -> [(FilePath, FilePath)]
commandTypeMapping :: [(String, String)]
, CommandOptions -> FilePath
commandFilename :: String
, CommandOptions -> Maybe FilePath
commandPropVia :: Maybe String
, CommandOptions -> Maybe FilePath
commandExtraVars :: Maybe FilePath
}
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 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
commandIncorrectSpec :: String -> String -> ErrorTriplet
commandIncorrectSpec :: FilePath -> FilePath -> ErrorTriplet
commandIncorrectSpec 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
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec :: ErrorCode
ecIncorrectSpec = ErrorCode
1
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
newVarNames :: [FilePath]
newVarNames = [FilePath]
identifiers [FilePath] -> [FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a] -> [a]
\\ [FilePath]
existingNames
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)
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