ogma-cli: Provide ability to preprocess properties via external command. Refs #197.

ogma-cli/CHANGELOG.md

@@ -1,13 +1,14 @@
 # Revision history for ogma-cli
 
-## [1.X.Y] - 2025-01-10
+## [1.X.Y] - 2025-01-14
 
 * Update contribution guidelines (#161).
 * Provide ability to customize template in fprime command (#185).
 * Provide ability to customize template in standalone command (#189).
 * Add repository information to cabal package (#148).
 * Add version bounds to all dependencies (#119).
 * Introduce new diagram command (#194).
+* Provide ability to preprocess properties via external command (#197).
 
 ## [1.5.0] - 2024-11-21
 

ogma-cli/src/CLI/CommandStandalone.hs

@@ -65,6 +65,7 @@ data CommandOpts = CommandOpts
   , standalonePropFormat  :: String
   , standaloneTypes       :: [String]
   , standaloneTarget      :: String
+  , standalonePropVia     :: Maybe String
   }
 
 -- | Transform an input specification into a Copilot specification.
@@ -79,6 +80,7 @@ command c = standalone (standaloneFileName c) internalCommandOpts
       , Command.Standalone.standalonePropFormat  = standalonePropFormat c
       , Command.Standalone.standaloneTypeMapping = types
       , Command.Standalone.standaloneFilename    = standaloneTarget c
+      , Command.Standalone.standalonePropVia     = standalonePropVia c
       }
 
     types :: [(String, String)]
@@ -150,6 +152,13 @@ commandOptsParser = CommandOpts
         <> showDefault
         <> value "monitor"
         )
+  <*> optional
+        ( strOption
+            (  long "parse-prop-via"
+            <> metavar "COMMAND"
+            <> help strStandalonePropViaDesc
+            )
+        )
 
 -- | Target dir flag description.
 strStandaloneTargetDirDesc :: String
@@ -180,6 +189,11 @@ strStandaloneTargetDesc :: String
 strStandaloneTargetDesc =
   "Filename prefix for monitoring files in target language"
 
+-- | External command to pre-process individual properties.
+strStandalonePropViaDesc :: String
+strStandalonePropViaDesc =
+  "Command to pre-process individual properties"
+
 -- * Error codes
 
 -- | Encoding of reasons why the command can fail.

ogma-core/CHANGELOG.md

@@ -1,13 +1,14 @@
 # Revision history for ogma-core
 
-## [1.X.Y] - 2025-01-10
+## [1.X.Y] - 2025-01-14
 
 * 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).
 * Add repository information to cabal package (#148).
 * Add version bounds to all dependencies (#119).
 * Add command to transform state diagrams into monitors (#194).
+* Extend standalone command to use external process to parse properties (#197).
 
 ## [1.5.0] - 2024-11-21
 

ogma-core/ogma-core.cabal

@@ -127,6 +127,7 @@ library
     , graphviz                >= 2999.20  && < 2999.21
     , megaparsec              >= 8.0.0    && < 9.10
     , mtl                     >= 2.2.2    && < 2.4
+    , process                 >= 1.6      && < 1.7
     , text                    >= 1.2.3.1  && < 2.1
 
     , ogma-extra              >= 1.5.0 && < 1.6

ogma-core/src/Command/FPrimeApp.hs

@@ -41,8 +41,8 @@ module Command.FPrimeApp
 
 -- External imports
 import qualified Control.Exception    as E
-import           Control.Monad.Except ( ExceptT, liftEither, liftIO, runExceptT,
-                                        throwError )
+import           Control.Monad.Except ( ExceptT(..), liftEither, liftIO,
+                                        runExceptT, throwError )
 import           Data.Aeson           ( eitherDecode, object, (.=) )
 import           Data.Char            ( toUpper )
 import           Data.List            ( find, intercalate, nub, sort )
@@ -167,12 +167,15 @@ parseOptionalFRETCS Nothing   = return Nothing
 parseOptionalFRETCS (Just fp) = do
   -- Throws an exception if the file cannot be read.
   content <- liftIO $ B.safeReadFile fp
-  let fretCS :: Either String (Spec String)
-      fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content
 
-  case fretCS of
-    Left e   -> throwError $ cannotOpenFRETFile fp e
-    Right cs -> return $ Just cs
+  fretCS <- case eitherDecode =<< content of
+              Left e  -> ExceptT $ return $ Left $ cannotOpenFRETFile fp e
+              Right v -> ExceptT $ do
+                           p <- parseJSONSpec (return . return) fretFormat v
+                           case p of
+                             Left e  -> return $ Left $ cannotOpenFRETFile fp e
+                             Right r -> return $ Right r
+  return $ Just fretCS
 
 -- | Process a variable selection file, if available, and return the variable
 -- names.

ogma-core/src/Command/ROSApp.hs

@@ -45,8 +45,8 @@ module Command.ROSApp
 
 -- External imports
 import qualified Control.Exception    as E
-import           Control.Monad.Except (ExceptT, liftEither, liftIO, runExceptT,
-                                       throwError)
+import           Control.Monad.Except (ExceptT(..), liftEither, liftIO,
+                                       runExceptT, throwError)
 import           Data.Aeson           (eitherDecode, object, (.=))
 import           Data.List            (find, intersperse)
 import           Data.Maybe           (fromMaybe)
@@ -176,12 +176,15 @@ parseOptionalFRETCS Nothing   = return Nothing
 parseOptionalFRETCS (Just fp) = do
   -- Throws an exception if the file cannot be read.
   content <- liftIO $ B.safeReadFile fp
-  let fretCS :: Either String (Spec String)
-      fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content
 
-  case fretCS of
-    Left e   -> throwError $ cannotOpenFRETFile fp e
-    Right cs -> return $ Just cs
+  fretCS <- case eitherDecode =<< content of
+              Left e  -> ExceptT $ return $ Left $ cannotOpenFRETFile fp e
+              Right v -> ExceptT $ do
+                           p <- parseJSONSpec (return . return) fretFormat v
+                           case p of
+                             Left e  -> return $ Left $ cannotOpenFRETFile fp e
+                             Right r -> return $ Right r
+  return $ Just fretCS
 
 -- | Process a variable selection file, if available, and return the variable
 -- names.

ogma-core/src/Command/Standalone.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE OverloadedStrings         #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
 -- Copyright 2020 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -45,6 +46,7 @@ import Data.ByteString.Lazy (fromStrict)
 import Data.Foldable        (for_)
 import Data.List            (nub, (\\))
 import Data.Maybe           (fromMaybe)
+import System.Process       (readProcess)
 import System.FilePath      ((</>))
 import Data.Text.Lazy       (pack)
 
@@ -144,13 +146,17 @@ standalone' fp options (ExprPair parse replace print ids) = do
 
   format <- read <$> readFile formatFile
 
+  let wrapper = wrapVia (standalonePropVia options) parse
+
   -- 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.
   content <- B.safeReadFile fp
   res <- case content of
            Left s  -> return $ Left s
-           Right b -> return $ parseJSONSpec parse format =<< eitherDecode b
+           Right b -> do case eitherDecode b of
+                           Left e  -> return $ Left e
+                           Right v -> parseJSONSpec wrapper format v
 
   -- Complement the specification with any missing/implicit definitions
   let res' = fmap (addMissingIdentifiers ids) res
@@ -159,6 +165,23 @@ standalone' fp options (ExprPair parse replace print ids) = do
 
   return copilot
 
+-- | 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 Nothing  parse s = return (parse s)
+wrapVia (Just f) parse s =
+  E.handle (\(e :: IOException) -> return $ Left $ show e) $ do
+    out <- readProcess f [] s
+    return $ parse out
+
 -- | Options used to customize the conversion of specifications to Copilot
 -- code.
 data StandaloneOptions = StandaloneOptions
@@ -168,6 +191,7 @@ data StandaloneOptions = StandaloneOptions
   , standalonePropFormat  :: String
   , standaloneTypeMapping :: [(String, String)]
   , standaloneFilename    :: String
+  , standalonePropVia     :: Maybe String
   }
 
 -- * Error codes

ogma-core/tests/Main.hs

@@ -110,6 +110,7 @@ testFretComponentSpec2Copilot file success = do
                  , standaloneFilename    = "fret"
                  , standaloneTargetDir   = targetDir
                  , standaloneTemplateDir = Nothing
+                 , standalonePropVia     = Nothing
                  }
     result <- standalone file opts
 
@@ -145,6 +146,7 @@ testFretReqsDBCoCoSpec2Copilot file success = do
                  , standaloneFilename    = "fret"
                  , standaloneTargetDir   = targetDir
                  , standaloneTemplateDir = Nothing
+                 , standalonePropVia     = Nothing
                  }
     result <- standalone file opts
 

ogma-language-jsonspec/CHANGELOG.md

@@ -1,9 +1,10 @@
 # Revision history for ogma-language-jsonspec
 
-## [1.X.Y] - 2024-12-24
+## [1.X.Y] - 2025-01-14
 
 * Add repository information to cabal package (#148).
 * Add version bounds to all dependencies (#119).
+* Extend JSON spec parser to use an IO action to parse properties (#197).
 
 ## [1.5.0] - 2024-11-21
 

ogma-language-jsonspec/ogma-language-jsonspec.cabal

@@ -74,6 +74,7 @@ library
     , jsonpath               >= 0.3      && < 0.4
     , text                   >= 1.2.3.1  && < 2.1
     , megaparsec             >= 8.0.0    && < 9.10
+    , mtl                    >= 2.2.2    && < 2.4
     , bytestring             >= 0.10.8.2 && < 0.13
 
     , ogma-spec              >= 1.5.0 && < 1.6

ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs

@@ -33,6 +33,7 @@
 module Language.JSONSpec.Parser where
 
 -- External imports
+import           Control.Monad.Except  (ExceptT (..), runExceptT)
 import           Data.Aeson            (FromJSON (..), Value (..), decode, (.:))
 import           Data.Aeson.Key        (toString)
 import qualified Data.Aeson.KeyMap     as M
@@ -107,9 +108,9 @@ parseJSONFormat jsonFormat = do
              , jfiRequirementExpr = jfi12
              }
 
-parseJSONSpec :: (String -> Either String a) -> JSONFormat -> Value -> Either String (Spec a)
-parseJSONSpec parseExpr jsonFormat value = do
-  jsonFormatInternal <- parseJSONFormat jsonFormat
+parseJSONSpec :: (String -> IO (Either String a)) -> JSONFormat -> Value -> IO (Either String (Spec a))
+parseJSONSpec parseExpr jsonFormat value = runExceptT $ do
+  jsonFormatInternal <- except $ parseJSONFormat jsonFormat
 
   let values :: [Value]
       values = maybe [] (`executeJSONPath` value) (jfiInternalVars jsonFormatInternal)
@@ -131,7 +132,7 @@ parseJSONSpec parseExpr jsonFormat value = do
                    , internalVariableExpr    = varExpr
                    }
 
-  internalVariableDefs <- mapM internalVarDef values
+  internalVariableDefs <- except $ mapM internalVarDef values
 
   let values :: [Value]
       values = maybe [] (`executeJSONPath` value) (jfiExternalVars jsonFormatInternal)
@@ -150,22 +151,22 @@ parseJSONSpec parseExpr jsonFormat value = do
                    , externalVariableType    = varType
                    }
 
-  externalVariableDefs <- mapM externalVarDef values
+  externalVariableDefs <- except $ mapM externalVarDef values
 
   let values :: [Value]
       values = executeJSONPath (jfiRequirements jsonFormatInternal) value
 
       -- requirementDef :: Value -> Either String (Requirement a)
       requirementDef value = do
         let msg = "Requirement name"
-        reqId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value))
+        reqId <- except $ valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value))
 
         let msg = "Requirement expression"
-        reqExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value))
-        reqExpr' <- parseExpr reqExpr
+        reqExpr <- except $ valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value))
+        reqExpr' <- ExceptT $ parseExpr reqExpr
 
         let msg = "Requirement description"
-        reqDesc <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (executeJSONPath e value))) (jfiRequirementDesc jsonFormatInternal)
+        reqDesc <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (executeJSONPath e value))) (jfiRequirementDesc jsonFormatInternal)
 
         return $ Requirement
                    { requirementName        = reqId
@@ -198,3 +199,7 @@ showErrorsM :: Show a => Maybe (Either a b) -> Either String (Maybe b)
 showErrorsM Nothing          = Right Nothing
 showErrorsM (Just (Left s))  = Left (show s)
 showErrorsM (Just (Right x)) = Right (Just x)
+
+-- | Wrap an 'Either' value in an @ExceptT m@ monad.
+except :: Monad m => Either e a -> ExceptT e m a
+except = ExceptT . return