ogma-core: Use generalized JSON parser for DB Spec. Refs #122.

The JSON parsing functions currently used by ogma-core to parse
requirement DBs are very specific to the formats supported.

This commit replaces the existing FRET DB parser and converter by one
that is based on the new generic JSON-based parsing library. The old
module implementing the adhoc converter, as well as the dependency on
the ad hoc parser, are removed.

ogma-core/.hlint.yaml

@@ -6,7 +6,5 @@
 
 # We use data instead of newtype for uniformity.
 - ignore: { name: Use newtype instead of data
-          , within: [ Command.FRETReqsDB2Copilot
-                    , Language.Trans.FRETReqsDB2Copilot
-                    ]
+          , within: [ Command.FRETReqsDB2Copilot ]
           }

ogma-core/ogma-core.cabal

@@ -92,7 +92,6 @@ library
     Language.Trans.CStruct2CopilotStruct
     Language.Trans.CStructs2Copilot
     Language.Trans.CStructs2MsgHandlers
-    Language.Trans.FRETReqsDB2Copilot
     Language.Trans.Spec2Copilot
     Language.Trans.SMV2Copilot
 
@@ -114,7 +113,6 @@ library
     , ogma-language-c         >= 1.2.0 && < 1.3
     , ogma-language-cocospec  >= 1.2.0 && < 1.3
     , ogma-language-copilot   >= 1.2.0 && < 1.3
-    , ogma-language-fret-reqs >= 1.2.0 && < 1.3
     , ogma-language-jsonspec  >= 1.2.0 && < 1.3
     , ogma-language-smv       >= 1.2.0 && < 1.3
     , ogma-spec               >= 1.2.0 && < 1.3

ogma-core/src/Command/FRETReqsDB2Copilot.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE ExistentialQuantification #-}
 -- Copyright 2020 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -30,9 +31,6 @@
 --
 -- | Transform a FRET requirements database containing a temporal logic
 -- specification into a Copilot specification.
---
--- This module makes use of
--- "Language.Trans.FRETReqsDB2Copilot", which does most of the work.
 module Command.FRETReqsDB2Copilot
     ( fretReqsDB2Copilot
     , FRETReqsDB2CopilotOptions(..)
@@ -42,22 +40,36 @@ module Command.FRETReqsDB2Copilot
 
 -- External imports
 import Control.Monad.IfElse ( awhen )
-import Data.Aeson           ( eitherDecode )
+import Data.Aeson           ( eitherDecode, decode )
+import Data.ByteString.Lazy ( fromStrict )
+import Data.List            ( nub, (\\) )
 
 -- External imports: auxiliary
 import Data.ByteString.Extra as B ( safeReadFile )
-import Data.List.Extra       ( headEither )
 
 -- Internal imports: auxiliary
 import Command.Result ( Result (..) )
 import Data.Location  ( Location (..) )
 
--- Internal imports: FRET files and conversion to Copilot
-import qualified Language.FRETReqsDB.AST           as FRET ( FRETReqsDB )
-import qualified Language.Trans.FRETReqsDB2Copilot as T
-  ( fret2CopilotModule
-  , FRETReqsDB2CopilotOptions(FRETReqsDB2CopilotOptions)
-  )
+-- Internal imports: language ASTs, transformers
+import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
+                      Requirement (..), Spec (..))
+
+import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec
+import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer,
+                                                             pBoolSpec )
+
+import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)
+
+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.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot,
+                                                              boolSpecNames)
+import           Language.Trans.SMV2Copilot      as SMV (boolSpec2Copilot,
+                                                         boolSpecNames)
+import           Language.Trans.Spec2Copilot     (spec2Copilot, specAnalyze)
 
 -- | Print the contents of a Copilot module that implements the Past-time TL
 -- formula in a FRET file.
@@ -71,42 +83,56 @@ fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET
                    -> FRETReqsDB2CopilotOptions
                                -- ^ Customization options formula
                    -> IO (Result ErrorCode)
-fretReqsDB2Copilot fp useCoCoSpec = do
+fretReqsDB2Copilot fp options = do
 
-  -- 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.
-  fret <- parseFret fp
+  let functions = fretExprPair (fretReqsDB2CopilotUseCoCoSpec options)
 
-  -- Extract internal command options from external command options
-  let internalOptions = fretReqsDB2CopilotOptions useCoCoSpec
-
-  let copilot = T.fret2CopilotModule internalOptions =<< headEither =<< fret
+  copilot <- fretReqsDB2Copilot' fp options functions
 
   let (mOutput, result) =
-        fretReqsDB2CopilotResult useCoCoSpec fp copilot
+        fretReqsDB2CopilotResult options fp copilot
 
   awhen mOutput putStrLn
   return result
 
+-- | Print the contents of a Copilot module that implements the Past-time TL
+-- formula in a FRET file, using a subexpression handler.
+--
+-- PRE: The file given is readable, contains a valid FRET file with a PT
+-- formula in the @ptExpanded@ key, the formula does not use any identifiers
+-- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers
+-- used are valid C99 identifiers.
+fretReqsDB2Copilot' :: FilePath
+                           -> FRETReqsDB2CopilotOptions
+                           -> FRETExprPair
+                           -> IO (Either String String)
+fretReqsDB2Copilot' fp options (FRETExprPair parse replace print ids) = do
+  let name        = fretReqsDB2CopilotFilename options
+      useCoCoSpec = fretReqsDB2CopilotUseCoCoSpec options
+      typeMaps    = [("", "_")]
+
+  -- 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 (fretFormat useCoCoSpec) =<< eitherDecode b
+
+  -- Complement the specification with any missing/implicit definitions
+  let res' = fmap (addMissingIdentifiers ids) res
+
+  let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res'
+
+  return copilot
+
 -- | Options used to customize the conversion of FRET Requirements Database
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
   , fretReqsDB2CopilotFilename    :: String
   }
 
--- | Parse a JSON file containing a FRET requirement database.
---
--- Returns a 'Left' with an error message if the file does not have the correct
--- format.
---
--- Throws an exception if the file cannot be read.
-parseFret :: FilePath -> IO (Either String [FRET.FRETReqsDB])
-parseFret fp = do
-  content <- B.safeReadFile fp
-  return $ eitherDecode =<< content
-
 -- * Error codes
 
 -- | Encoding of reasons why the command can fail.
@@ -119,17 +145,6 @@ type ErrorCode = Int
 ecFretReqsDBError :: ErrorCode
 ecFretReqsDBError = 1
 
--- * Input arguments
-
--- | Convert command input argument options to internal transformation function
--- input arguments.
-fretReqsDB2CopilotOptions :: FRETReqsDB2CopilotOptions
-                          -> T.FRETReqsDB2CopilotOptions
-fretReqsDB2CopilotOptions options =
-  T.FRETReqsDB2CopilotOptions
-      (fretReqsDB2CopilotUseCoCoSpec options)
-      (fretReqsDB2CopilotFilename options)
-
 -- * Result
 
 -- | Process the result of the transformation function.
@@ -140,3 +155,62 @@ fretReqsDB2CopilotResult :: FRETReqsDB2CopilotOptions
 fretReqsDB2CopilotResult options fp result = case result of
   Left msg -> (Nothing, Error ecFretReqsDBError msg (LocationFile fp))
   Right t  -> (Just t, Success)
+
+-- * Parser
+
+-- | JSONPath selectors for a FRET file
+fretFormat :: Bool -> JSONFormat
+fretFormat useCoCoSpec = JSONFormat
+  { specInternalVars    = Nothing
+  , specInternalVarId   = ""
+  , specInternalVarExpr = ""
+  , specInternalVarType = Nothing
+  , specExternalVars    = Just ".semantics.variables..*.*"
+  , specExternalVarId   = ""
+  , specExternalVarType = Nothing
+  , specRequirements    = "$[:]"
+  , specRequirementId   = ".reqid"
+  , specRequirementDesc = Just ".fulltext"
+  , specRequirementExpr = if useCoCoSpec then ".semantics.CoCoSpecCode" else ".semantics.ptExpanded"
+  }
+
+-- * Handler for boolean expressions
+
+-- | Handler for boolean expressions that knows how to parse them, replace
+-- variables in them, and convert them to Copilot.
+data FRETExprPair = forall a . FRETExprPair
+  { exprParse   :: String -> Either String a
+  , exprReplace :: [(String, String)] -> a -> a
+  , exprPrint   :: a -> String
+  , exprIdents  :: a -> [String]
+  }
+
+-- | Return a handler depending on whether it should be for CoCoSpec boolean
+-- expressions or for SMV boolean expressions.
+fretExprPair :: Bool -> FRETExprPair
+fretExprPair True  = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)
+                                  (\_ -> id)
+                                  (CoCoSpec.boolSpec2Copilot)
+                                  (CoCoSpec.boolSpecNames)
+fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer)
+                                  (substituteBoolExpr)
+                                  (SMV.boolSpec2Copilot)
+                                  (SMV.boolSpecNames)
+
+-- | Add to a spec external variables for all identifiers mentioned in
+-- expressions that are not defined anywhere.
+addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a
+addMissingIdentifiers f s = s { externalVariables = vars' }
+  where
+    vars'   = externalVariables s ++ newVars
+    newVars = map (\n -> ExternalVariableDef n "") newVarNames
+
+    -- Names that are not defined anywhere
+    newVarNames = identifiers \\ existingNames
+
+    -- Identifiers being mentioned in the requirements.
+    identifiers = nub $ concatMap (f . requirementExpr) (requirements s)
+
+    -- Names that are defined in variables.
+    existingNames = map externalVariableName (externalVariables s)
+                 ++ map internalVariableName (internalVariables s)