Merge branch 'develop-standalone-templates' into develop. Close #189.

**Description**

The standalone application generation backend uses a fixed template to
generate the standalone application. That template does not fit all use
cases, so we are finding users heavily modifying the output (which is
hard to keep up with when there are changes), and or not using ogma
altogether for that reason.

Allowing users to pick their own standalone template would make Ogma
more versatile.

**Type**

- Feature: Enable customizing output produced.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Ogma allows users to pick the custom standalone application template
they want to use instead of relying on the one provided by default.

The following dockerfile generates a standalone Copilot monitor using
the default template and using a copy and the default template and
checks that both are the same. It then adds a file to the copy of the
template and checks that the file is copied to the target directory when
the custom template is used, after which it prints the message
"Success". Compiling the produced component completes successfully:

```Dockerfile
FROM ubuntu:trusty

ENV DEBIAN_FRONTEND=noninteractive

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
RUN apt-get install --yes libz-dev

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN cabal v1-install alex happy
RUN apt-get install --yes git

CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cd .. \
    && cp -r $NAME/ogma-core/templates/standalone custom-template-standalone \
    && cabal v1-sandbox init \
    && cabal v1-install $NAME/$PAT**/ copilot-4.1 --constraint="aeson>=2.0.3.0" \
    && ./.cabal-sandbox/bin/ogma standalone --file-name $NAME/ogma-cli/examples/fret.json --input-format fcs --target-dir orig \
    && ./.cabal-sandbox/bin/ogma standalone --file-name $NAME/ogma-cli/examples/fret.json --input-format fcs --target-dir new --template-dir custom-template-standalone \
    && diff -rq orig new \
    && rm -rf new/ \
    && echo "Success" >> custom-template-standalone/README \
    && ./.cabal-sandbox/bin/ogma standalone --file-name $NAME/ogma-cli/examples/fret.json --input-format fcs --target-dir new --template-dir custom-template-standalone \
    && cabal v1-exec -- runhaskell -XPartialTypeSignatures -Wno-partial-type-signatures new/Copilot.hs \
    && cat new/README
```

Command (substitute variables based on new path after merge):

```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e "PAT=ogma"  -e "COMMIT=<HASH>" -it ogma-verify-189
```

**Solution implemented**

Modify `ogma-core` to use variable expansion based on mustache to create
the output files.

Modify `ogma-core`'s template to use the variables used by the
standalone application generation module.

Modify `ogma-core` to give users the ability to pick a target directory
via an input argument.

Modify `ogma-core` to give users the ability to pick a template
directory via an optional input argument.

Modify tests in `ogma-core` to provide the new arguments to the
standalone backend so that tests keep working.

Modify `ogma-cli` to give users the ability to pick a target directory
via an optional input argument (exposing the corresponding argument from
`ogma-core`).

Modify `ogma-cli` to give users the ability to pick a template directory
via an optional input argument (exposing the corresponding argument from
`ogma-core`).

**Further notes**

The `README` is not modified to demonstrate new capability, because
there is no entry in the `README` for the standalone backend.

ogma-cli/CHANGELOG.md

@@ -1,9 +1,10 @@
 # Revision history for ogma-cli
 
-## [1.X.Y] - 2024-11-26
+## [1.X.Y] - 2024-12-23
 
 * Update contribution guidelines (#161).
 * Provide ability to customize template in fprime command (#185).
+* Provide ability to customize template in standalone command (#189).
 
 ## [1.5.0] - 2024-11-21
 

ogma-cli/src/CLI/CommandStandalone.hs

@@ -43,7 +43,7 @@ module CLI.CommandStandalone
   where
 
 -- External imports
-import Options.Applicative (Parser, help, long, metavar, many, short,
+import Options.Applicative (Parser, help, long, many, metavar, optional, short,
                             showDefault, strOption, switch, value)
 
 -- External imports: command results
@@ -58,11 +58,13 @@ import qualified Command.Standalone
 
 -- | Options to generate Copilot from specification.
 data CommandOpts = CommandOpts
-  { standaloneFileName   :: FilePath
-  , standaloneFormat     :: String
-  , standalonePropFormat :: String
-  , standaloneTypes      :: [String]
-  , standaloneTarget     :: String
+  { standaloneTargetDir   :: FilePath
+  , standaloneTemplateDir :: Maybe FilePath
+  , standaloneFileName    :: FilePath
+  , standaloneFormat      :: String
+  , standalonePropFormat  :: String
+  , standaloneTypes       :: [String]
+  , standaloneTarget      :: String
   }
 
 -- | Transform an input specification into a Copilot specification.
@@ -71,7 +73,9 @@ command c = standalone (standaloneFileName c) internalCommandOpts
   where
     internalCommandOpts :: Command.Standalone.StandaloneOptions
     internalCommandOpts = Command.Standalone.StandaloneOptions
-      { Command.Standalone.standaloneFormat      = standaloneFormat c
+      { Command.Standalone.standaloneTargetDir   = standaloneTargetDir c
+      , Command.Standalone.standaloneTemplateDir = standaloneTemplateDir c
+      , Command.Standalone.standaloneFormat      = standaloneFormat c
       , Command.Standalone.standalonePropFormat  = standalonePropFormat c
       , Command.Standalone.standaloneTypeMapping = types
       , Command.Standalone.standaloneFilename    = standaloneTarget c
@@ -98,6 +102,20 @@ commandDesc =
 commandOptsParser :: Parser CommandOpts
 commandOptsParser = CommandOpts
   <$> strOption
+        (  long "target-dir"
+        <> metavar "DIR"
+        <> showDefault
+        <> value "copilot"
+        <> help strStandaloneTargetDirDesc
+        )
+  <*> optional
+        ( strOption
+            (  long "template-dir"
+            <> metavar "DIR"
+            <> help strStandaloneTemplateDirArgDesc
+            )
+        )
+  <*> strOption
         (  long "file-name"
         <> metavar "FILENAME"
         <> help strStandaloneFilenameDesc
@@ -133,6 +151,14 @@ commandOptsParser = CommandOpts
         <> value "monitor"
         )
 
+-- | Target dir flag description.
+strStandaloneTargetDirDesc :: String
+strStandaloneTargetDirDesc = "Target directory"
+
+-- | Template dir flag description.
+strStandaloneTemplateDirArgDesc :: String
+strStandaloneTemplateDirArgDesc = "Directory holding standalone source template"
+
 -- | Filename flag description.
 strStandaloneFilenameDesc :: String
 strStandaloneFilenameDesc = "File with properties or requirements"

ogma-core/CHANGELOG.md

@@ -1,9 +1,10 @@
 # Revision history for ogma-core
 
-## [1.X.Y] - 2024-12-04
+## [1.X.Y] - 2024-12-23
 
 * Replace queueSize with QUEUE_SIZE in FPP file (#186).
 * Use template expansion system to generate F' monitoring component (#185).
+* Use template expansion system to generate standalone Copilot monitor (#189).
 
 ## [1.5.0] - 2024-11-21
 

ogma-core/ogma-core.cabal

@@ -71,6 +71,7 @@ data-files:          templates/copilot-cfs/CMakeLists.txt
                      templates/fprime/Copilot.hpp
                      templates/fprime/Dockerfile
                      templates/fprime/instance-copilot
+                     templates/standalone/Copilot.hs
                      data/formats/fcs_smv
                      data/formats/fcs_cocospec
                      data/formats/fdb_smv
@@ -143,6 +144,7 @@ test-suite unit-tests
 
   build-depends:
       base
+    , directory
     , HUnit
     , QuickCheck
     , test-framework

ogma-core/src/Command/Standalone.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE OverloadedStrings         #-}
 -- Copyright 2020 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -38,15 +39,18 @@ module Command.Standalone
   where
 
 -- External imports
-import Data.Aeson           (decode, eitherDecode)
-import Data.ByteString.Lazy (fromStrict, pack)
+import Control.Exception    as E
+import Data.Aeson           (decode, eitherDecode, object, (.=))
+import Data.ByteString.Lazy (fromStrict)
 import Data.Foldable        (for_)
 import Data.List            (nub, (\\))
 import Data.Maybe           (fromMaybe)
 import System.FilePath      ((</>))
+import Data.Text.Lazy       (pack)
 
 -- External imports: auxiliary
-import Data.ByteString.Extra as B ( safeReadFile )
+import Data.ByteString.Extra  as B ( safeReadFile )
+import System.Directory.Extra ( copyTemplate )
 
 -- Internal imports: auxiliary
 import Command.Result  (Result (..))
@@ -73,38 +77,61 @@ import           Language.Trans.SMV2Copilot      as SMV (boolSpec2Copilot,
                                                          boolSpecNames)
 import           Language.Trans.Spec2Copilot     (spec2Copilot, specAnalyze)
 
--- | Print the contents of a Copilot module that implements the spec in an
+-- | 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.
+-- 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.
 standalone :: FilePath          -- ^ Path to a file containing a specification
            -> StandaloneOptions -- ^ Customization options
            -> IO (Result ErrorCode)
 standalone fp options = do
+  E.handle (return . standaloneTemplateError options fp) $ do
+    -- Obtain template dir
+    templateDir <- case standaloneTemplateDir options of
+                     Just x  -> return x
+                     Nothing -> do
+                       dataDir <- getDataDir
+                       return $ dataDir </> "templates" </> "standalone"
 
-  let functions = exprPair (standalonePropFormat options)
+    let functions = exprPair (standalonePropFormat options)
 
-  copilot <- standalone' fp options functions
+    copilot <- standalone' fp options functions
 
-  let (mOutput, result) = standaloneResult options fp copilot
+    let (mOutput, result) = standaloneResult options fp copilot
 
-  for_ mOutput putStrLn
-  return result
+    for_ mOutput $ \(externs, internals, reqs, triggers, specName) -> do
+      let subst = object $
+                    [ "externs"   .= pack externs
+                    , "internals" .= pack internals
+                    , "reqs"      .= pack reqs
+                    , "triggers"  .= pack triggers
+                    , "specName"  .= pack specName
+                    ]
 
--- | Print the contents of a Copilot module that implements the spec in an
+      let targetDir = standaloneTargetDir options
+
+      copyTemplate templateDir subst targetDir
+
+    return result
+
+-- | 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.
+-- 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.
 standalone' :: FilePath
             -> StandaloneOptions
             -> ExprPair
-            -> IO (Either String String)
+            -> IO (Either String (String, String, String, String, String))
 standalone' fp options (ExprPair parse replace print ids) = do
   let name     = standaloneFilename options
       typeMaps = typeToCopilotTypeMapping options
@@ -135,7 +162,9 @@ standalone' fp options (ExprPair parse replace print ids) = do
 -- | Options used to customize the conversion of specifications to Copilot
 -- code.
 data StandaloneOptions = StandaloneOptions
-  { standaloneFormat      :: String
+  { standaloneTargetDir   :: FilePath
+  , standaloneTemplateDir :: Maybe FilePath
+  , standaloneFormat      :: String
   , standalonePropFormat  :: String
   , standaloneTypeMapping :: [(String, String)]
   , standaloneFilename    :: String
@@ -153,17 +182,36 @@ type ErrorCode = Int
 ecStandaloneError :: ErrorCode
 ecStandaloneError = 1
 
+-- | Error: standalone component generation failed during the copy/write
+-- process.
+ecStandaloneTemplateError :: ErrorCode
+ecStandaloneTemplateError = 2
+
 -- * Result
 
 -- | Process the result of the transformation function.
 standaloneResult :: StandaloneOptions
                  -> FilePath
-                 -> Either String String
-                 -> (Maybe String, Result ErrorCode)
+                 -> Either String a
+                 -> (Maybe a, Result ErrorCode)
 standaloneResult options fp result = case result of
   Left msg -> (Nothing, Error ecStandaloneError msg (LocationFile fp))
   Right t  -> (Just t, Success)
 
+-- | Report an error when trying to open or copy the template
+standaloneTemplateError :: StandaloneOptions
+                        -> FilePath
+                        -> E.SomeException
+                        -> Result ErrorCode
+standaloneTemplateError options fp exception =
+    Error ecStandaloneTemplateError msg (LocationFile fp)
+  where
+    msg =
+      "Standlone monitor generation failed during copy/write operation. Check"
+      ++ " that there's free space in the disk and that you have the necessary"
+      ++ " permissions to write in the destination directory. "
+      ++ show exception
+
 -- * Mapping of types from input format to Copilot
 typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)]
 typeToCopilotTypeMapping options =