ogma-core: Use template expansion to generate standalone monitoring c…

…omponent. Refs nasa#189.

The standlone backend uses a fixed template to generate the Copilot
monitor. 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.

This commit modifies the ogma-core standalone command to use mustache to
generate the Copilot monitor via a template and variable expansion. We
introduce a new template that uses variables, and we modify the cabal
file to include the new files as data files that are copied over during
installation.

To be able to generate the files, we need to introduce a target
directory option for the standalone command.

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

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 (..))
@@ -84,15 +88,31 @@ 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
+    dataDir <- getDataDir
+    let templateDir = 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
+                    ]
+
+      let targetDir = standaloneTargetDir options
+
+      copyTemplate templateDir subst targetDir
+
+    return result
 
 -- | Print the contents of a Copilot module that implements the spec in an
 -- input file, using a subexpression handler.
@@ -104,7 +124,7 @@ standalone fp options = do
 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 +155,8 @@ 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
+  , standaloneFormat      :: String
   , standalonePropFormat  :: String
   , standaloneTypeMapping :: [(String, String)]
   , standaloneFilename    :: String
@@ -153,17 +174,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 =

ogma-core/src/Language/Trans/Spec2Copilot.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+-- Copyright 2024 United States Government as represented by the Administrator
 -- Copyright 2024 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -36,7 +38,7 @@
 module Language.Trans.Spec2Copilot where
 
 -- External imports
-import Data.List  ( intersect, lookup, union )
+import Data.List  ( intercalate, intersect, lookup, union )
 import Data.Maybe ( fromMaybe )
 
 -- External imports: auxiliary
@@ -56,46 +58,17 @@ spec2Copilot :: String                         -- Spec / target file name
              -> ([(String, String)] -> a -> a) -- Expr subsitution function
              -> (a -> String)                  -- Expr show function
              -> Spec a                         -- Specification
-             -> Either String String
+             -> Either String (String, String, String, String, String)
 spec2Copilot specName typeMaps exprTransform showExpr spec =
-    pure $ unlines $ concat
-      [ imports
-      , externs
-      , internals
-      , reqs
-      , clock
-      , ftp
-      , pre
-      , tpre
-      , notPreviousNot
-      , copilotSpec
-      , main'
-      ]
+    pure (externs, internals, reqs, triggers, specName)
 
   where
 
-    -- Import header block
-    imports :: [String]
-    imports =
-      [ "import           Copilot.Compile.C99"
-      , "import           Copilot.Language          hiding (prop)"
-      , "import           Copilot.Language.Prelude"
-      , "import           Copilot.Library.LTL       (next)"
-      , "import           Copilot.Library.MTL       hiding (since,"
-        ++ " alwaysBeen, trigger)"
-      , "import           Copilot.Library.PTLTL     (since, previous,"
-        ++ " alwaysBeen)"
-      , "import qualified Copilot.Library.PTLTL     as PTLTL"
-      , "import qualified Copilot.Library.MTL       as MTL"
-      , "import           Language.Copilot          (reify)"
-      , "import           Prelude                   hiding ((&&), (||), (++),"
-        ++ " (<=), (>=), (<), (>), (==), (/=), not)"
-      , ""
-      ]
-
     -- Extern streams
-    externs = concatMap externVarToDecl
-                        (externalVariables spec)
+    externs = unlines'
+            $ intercalate [""]
+            $ map externVarToDecl
+                  (externalVariables spec)
       where
         externVarToDecl i = [ propName
                                 ++ " :: Stream "
@@ -110,14 +83,15 @@ spec2Copilot specName typeMaps exprTransform showExpr spec =
                                 ++ show (externalVariableName i)
                                 ++ " "
                                 ++ "Nothing"
-                            , ""
                             ]
           where
             propName = safeMap nameSubstitutions (externalVariableName i)
 
     -- Internal stream definitions
-    internals = concatMap internalVarToDecl
-                      (internalVariables spec)
+    internals = unlines'
+              $ intercalate [""]
+              $ map internalVarToDecl
+                    (internalVariables spec)
       where
         internalVarToDecl i = (\implem ->
                                 [ propName
@@ -129,20 +103,19 @@ spec2Copilot specName typeMaps exprTransform showExpr spec =
                                 , propName
                                     ++ " = "
                                     ++ implem
-
-                                , ""
                                 ]) implementation
           where
             propName = safeMap nameSubstitutions (internalVariableName i)
             implementation = (internalVariableExpr i)
 
     -- Encoding of requirements as boolean streams
-    reqs :: [String]
-    reqs = concatMap reqToDecl (requirements spec)
+    reqs :: String
+    reqs = unlines' $ intercalate [""]
+         $ map reqToDecl (requirements spec)
       where
+        reqToDecl :: Requirement _ -> [String]
         reqToDecl i = [ reqComment, reqSignature
                       , reqBody nameSubstitutions
-                      , ""
                       ]
           where
             reqName = safeMap nameSubstitutions (requirementName i)
@@ -165,73 +138,17 @@ spec2Copilot specName typeMaps exprTransform showExpr spec =
                              (showExpr (exprTransform subs (requirementExpr i)))
 
 
-    -- Auxiliary streams: clock
-    clock :: [String]
-    clock = [ ""
-            , "-- | Clock that increases in one-unit steps."
-            , "clock :: Stream Int64"
-            , "clock = [0] ++ (clock + 1)"
-            , ""
-            ]
-
-    -- Auxiliary streams: first time point
-    ftp :: [String]
-    ftp = [ ""
-          , "-- | First Time Point"
-          , "ftp :: Stream Bool"
-          , "ftp = [True] ++ false"
-          , ""
-          ]
-
-    -- Auxiliary streams: pre
-    pre = [ ""
-          , "pre :: Stream Bool -> Stream Bool"
-          , "pre = ([False] ++)"
-          ]
-
-    -- Auxiliary streams: tpre
-    tpre = [ ""
-           , "tpre :: Stream Bool -> Stream Bool"
-           , "tpre = ([True] ++)"
-           ]
-
-    -- Auxiliary streams: notPreviousNot
-    notPreviousNot :: [String]
-    notPreviousNot = [ ""
-                     , "notPreviousNot :: Stream Bool -> Stream Bool"
-                     , "notPreviousNot = not . PTLTL.previous . not"
-                     ]
-
-    -- Main specification
-    copilotSpec :: [String]
-    copilotSpec = [ ""
-                  , "-- | Complete specification. Calls C handler functions"
-                    ++ " when"
-                  , "-- properties are violated."
-                  , "spec :: Spec"
-                  , "spec = do"
-                  ]
-                  ++ triggers
-                  ++ [ "" ]
+    -- Main specification triggers
+    triggers :: String
+    triggers = unlines' $ fmap reqTrigger (requirements spec)
       where
-        triggers :: [String]
-        triggers = fmap reqTrigger (requirements spec)
-
         reqTrigger :: Requirement a -> String
         reqTrigger r = "  trigger " ++ show handlerName ++ " (not "
                        ++ propName ++ ") " ++ "[]"
           where
             handlerName = "handler" ++ sanitizeUCIdentifier (requirementName r)
             propName    = safeMap nameSubstitutions (requirementName r)
 
-    -- Main program that compiles specification to C in two files (code and
-    -- header).
-    main' :: [String]
-    main' = [ ""
-            , "main :: IO ()"
-            , "main = reify spec >>= compile \"" ++ specName ++ "\""
-            ]
-
     -- Map from a variable name to its desired identifier in the code
     -- generated.
     internalVariableMap =
@@ -318,3 +235,9 @@ specAnalyze spec
 -- substitution table.
 safeMap :: [(String, String)] -> String -> String
 safeMap ls k = fromMaybe k $ lookup k ls
+
+-- | Create a string from a list of strings, inserting new line characters
+-- between them. Unlike 'Prelude.unlines', this function does not insert
+-- an end of line character at the end of the last string.
+unlines' :: [String] -> String
+unlines' = intercalate "\n"