-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Ogma: Helper tool to interoperate between Copilot and other languages.
--   
--   Ogma is a tool to facilitate the integration of safe runtime monitors
--   into other systems. Ogma extends Copilot, a high-level runtime
--   verification framework that generates hard real-time C99 code.
--   
--   This package implements the internal commands of ogma.
@package ogma-core
@version 1.10.0

-- | Locations where conditions take place (within a file, or outside).
module Data.Location

-- | Locations where conditions take place (within a file, or outside).
data Location

-- | No location info.
LocationNothing :: Location

-- | Within a file.
LocationFile :: String -> Location

-- | On a line within a file.
LocationFileLine :: String -> Int -> Location

-- | On a line and column within a file.
LocationFileLC :: String -> Int -> Int -> Location

-- | A datatype representing the type of the results of processing input
--   files.
module Command.Result

-- | Result of the global process
data Result a
Success :: Result a
Error :: a -> String -> Location -> Result a

-- | True if the result is a success, False otherwise.
isSuccess :: Result a -> Bool

-- | True if the result is an error, False otherwise.
isError :: Result a -> Bool

-- | Copilot's struct representation of C Structs and creation from C's
--   AST.
module Language.Trans.CStruct2CopilotStruct

-- | Convert a top-level struct declaration into a CStruct
mkCStruct :: ExternalDeclaration -> Either String CStruct

-- | Convert a String to camel case, also eliminating the
--   _t at the end if present.
camelCaseTypeName :: String -> String

-- | Generate Copilot struct definitions and instances from structs defined
--   in a C header file.
--   
--   Working with Copilot structs requires three definitions: the datatype,
--   a Struct instance, and a Typed instance.
--   
--   This module converts the C structs into CStructs, and then
--   converts those CStructs into Copilot (i.e., Haskell) data type
--   declarations and instance declarations represented as strings.
module Language.Trans.CStructs2Copilot

-- | Convert all the CStructs in a header file into the declarations
--   needed in Copilot to use it.
cstructs2CopilotDecls :: TranslationUnit -> Either String [String]

-- | Convert a CStruct into the declarations needed in Copilot to
--   use it.
cstruct2CopilotDecls :: CStruct -> [String]

-- | Convert a CStruct definition into a Copilot Struct declaration.
--   
--   For example, given the struct generated by the following definition:
--   
--   
--   struct {
--     uint8_t f1;
--   } a_struct_t;
--   
--   
--   the corresponding Haskell definition would be:
--   
--   
--   data AStruct = AStruct
--       { aSF1 :: Word8 }
--     deriving Generic
--   
cStructToCopilotStruct :: CStruct -> String

-- | Convert a CStruct definition into a Copilot Struct
--   instance declaration. For example, for the struct:
--   
--   
--   struct {
--     uint8_t f1;
--   } a_struct_t;
--   
--   
--   the corresponding Struct instance would be:
--   
--   
--   instance Struct AStruct where
--     typeName = typeNameDefault
--     toValues = toValuesDefault
--   
structInstance :: CStruct -> String

-- | Convert a CStruct definition to Copilot Typed instance
--   declaration. For example, for the struct:
--   
--   
--   struct {
--     uint8_t f1;
--   } a_struct_t;
--   
--   
--   the corresponding Typed instance could be:
--   
--   
--   instance Typed AStruct where
--     typeOf = typeOfDefault
--   
typedInstance :: CStruct -> String

-- | Provide a suitable field name for a record field of a CStruct
--   in Haskell.
--   
--   For example, given the struct:
--   
--   
--   struct {
--     uint8_t f1;
--   } a_struct_t;
--   
--   
--   the field name in the Haskell record would be aSF1, where the
--   aS and comes from a_struct_t and the final
--   F1 comes from f1.
fieldName :: CStruct -> String -> String

-- | Convert a C struct name (e.g., some_type_t) to a Haskell type
--   name (e.g., SomeType).
cStructName2Haskell :: String -> String

-- | Return the corresponding type in Copilot/Haskell for a given type.
cTypeName2HaskellType :: String -> String

-- | Generate Copilot struct definitions and instances from structs defined
--   in a C header file.
--   
--   Working with Copilot structs requires three definitions: the datatype,
--   a Struct instance, and a Typed instance.
--   
--   This module converts the C structs into CStructs, and then
--   converts those CStructs into Copilot (i.e., Haskell) data type
--   declarations and instance declarations. The result is then printed to
--   a file. This module makes use of
--   Language.Trans.CStructs2Copilot, which does most of the work.
module Command.CStructs2Copilot

-- | Generate Copilot struct definitions and instances from structs defined
--   in a C header file.
cstructs2Copilot :: FilePath -> IO (Result ErrorCode)

-- | Encoding of reasons why the command can fail.
--   
--   The error code used is 1 for user error.
type ErrorCode = Int

-- | Generate C methods that process message dealing with the structs
--   defined in a header file.
--   
--   This module contains the pure conversion from CStructs into C code.
--   Normally, this module would be implemented as a conversion between C
--   ASTs, but we want to add comments to the generated code, which are not
--   representable in the abstract syntax tree.
module Language.Trans.CStructs2MsgHandlers

-- | Generate a C methods that process message dealing with the structs
--   defined in a header file.
cstructs2MsgHandlers :: TranslationUnit -> Either String String

-- | Generate a C method that processes one message dealing with one kind
--   of struct.
cstruct2MsgHandler :: CStruct -> String

-- | Generate C methods that process NASA Core Flight System messages
--   dealing with the structs defined in a header file.
--   
--   This module makes use of Language.Trans.CStructs2MsgHandlers,
--   which does most of the work.
module Command.CStructs2MsgHandlers

-- | Print message handlers that copy data and make it available to
--   Copilot.
cstructs2MsgHandlers :: FilePath -> IO (Result ErrorCode)

-- | Encoding of reasons why the command can fail.
--   
--   The error code used is 1 for user error.
type ErrorCode = Int

-- | Transform a Lustre specification, extended with temporal logic
--   operators, into a Copilot specification.
--   
--   Normally, this module would be implemented as a conversion between
--   ASTs, but we want to add comments to the generated code, which are not
--   representable in the abstract syntax tree.
module Language.Trans.Lustre2Copilot

-- | Return the Copilot representation of a Lustre BoolSpec.
--   
--   This function returns the temporal property only. The string does not
--   contain any top-level names, any imports, or auxiliary definitions
--   that may be required.
boolSpec2Copilot :: BoolSpec -> String

-- | Return all identifiers used in a BoolSpec that are not reserved
--   keywords.
boolSpecNames :: BoolSpec -> [String]

-- | Transform an SMV TL specification into a Copilot specification.
--   
--   Normally, this module would be implemented as a conversion between
--   ASTs, but we want to add comments to the generated code, which are not
--   representable in the abstract syntax tree.
module Language.Trans.SMV2Copilot

-- | Return the Copilot representation of an SMV BoolSpec.
--   
--   This function returns the temporal property only. The string does not
--   contain any top-level names, any imports, or auxiliary definitions
--   that may be required.
boolSpec2Copilot :: BoolSpec -> String

-- | Return the Copilot representation of an SMV boolean constant.
const2Copilot :: BoolConst -> String

-- | Return the Copilot representation of a numeric expression.
numExpr2Copilot :: NumExpr -> String

-- | Return the Copilot representation of an SMV additive operator.
additiveOp2Copilot :: AdditiveOp -> String

-- | Return the Copilot representation of an SMV multiplicative operator.
multOp2Copilot :: MultOp -> String

-- | Return the Copilot representation of an SMV comparison operator.
ordOp2Copilot :: OrdOp -> String

-- | Return the Copilot representation of a unary logical SMV operator.
opOne2Copilot :: OpOne -> String

-- | Return the Copilot representation of a unary logical non-MTL SMV
--   operator.
opOneAlone2Copilot :: Op1Name -> String

-- | Return the Copilot representation of a unary logical MTL SMV operator.
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String

-- | Return the Copilot representation of a unary logical MTL SMV operator
--   that uses an explicit range.
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String

-- | Return the Copilot representation of a unary logical possibly MTL SMV
--   operator.
opOneMTL2Copilot' :: Op1Name -> String

-- | Return the Copilot representation of an SMV number.
number2Copilot :: Number -> String

-- | Return the Copilot representation of a binary logical non-MTL SMV
--   operator.
opTwo2Copilot :: OpTwo -> String

-- | Return the Copilot representation of an SMV identifier.
ident2Copilot :: Ident -> String

-- | Return all identifiers used in a BoolSpec that are not reserved
--   keywords.
boolSpecNames :: BoolSpec -> [String]

-- | Return all identifiers used in a numeric expression.
numExprNames :: NumExpr -> [String]

-- | Transform an Ogma specification into a standalone Copilot
--   specification.
--   
--   Normally, this module would be implemented as a conversion between
--   ASTs, but we want to add comments to the generated code, which are not
--   representable in the abstract syntax tree.
module Language.Trans.Spec2Copilot

-- | For a given spec, return the corresponding Copilot file, or an error
--   message if such file cannot be generated.
--   
--   PRE: there are no name clashes between the variables and names used in
--   the specification and any definitions in Haskell's Prelude or in
--   Copilot.
spec2Copilot :: forall a. String -> [(String, String)] -> ([(String, String)] -> a -> a) -> (a -> String) -> Spec a -> Either String (String, String, String, String, String)
specAnalyze :: Spec a -> Either String (Spec a)

-- | Substitute a string based on a given substitution table.
--   
--   This function leaves the key unchanged if it cannot be found in the
--   substitution table.
safeMap :: [(String, String)] -> String -> String

-- | Create a string from a list of strings, inserting new line characters
--   between them. Unlike unlines, this function does not insert an
--   end of line character at the end of the last string.
unlines' :: [String] -> String

-- | Transform a state diagram into a Copilot specification.
module Command.Diagram

-- | Generate a new Copilot monitor that implements a state machine
--   described in a diagram given as 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 stateMachine,
--   externalState, noneOf,
--   checkValidTransitions, main, spec,
--   stateMachine1, clock, ftp,
--   notPreviousNot. All identifiers used are valid C99
--   identifiers. The template, if provided, exists and uses the variables
--   needed by the diagram application generator. The target directory is
--   writable and there's enough disk space to copy the files over.
diagram :: FilePath -> DiagramOptions -> IO (Result ErrorCode)

-- | Options used to customize the conversion of diagrams to Copilot code.
data DiagramOptions
DiagramOptions :: FilePath -> Maybe FilePath -> DiagramFormat -> DiagramPropFormat -> String -> DiagramMode -> String -> String -> DiagramOptions
[diagramTargetDir] :: DiagramOptions -> FilePath
[diagramTemplateDir] :: DiagramOptions -> Maybe FilePath
[diagramFormat] :: DiagramOptions -> DiagramFormat
[diagramPropFormat] :: DiagramOptions -> DiagramPropFormat
[diagramFilename] :: DiagramOptions -> String
[diagramMode] :: DiagramOptions -> DiagramMode
[diagramStateVar] :: DiagramOptions -> String
[diagramInputVar] :: DiagramOptions -> String

-- | Diagram formats supported.
data DiagramFormat
Mermaid :: DiagramFormat
Dot :: DiagramFormat

-- | Modes of operation.
data DiagramMode

-- | Check if given state matches expectation
CheckState :: DiagramMode

-- | Compute expected state
ComputeState :: DiagramMode

-- | Check if transitioning to a state would be possible.
CheckMoves :: DiagramMode

-- | Property formats supported.
data DiagramPropFormat
Lustre :: DiagramPropFormat
Inputs :: DiagramPropFormat
Literal :: DiagramPropFormat
SMV :: DiagramPropFormat

-- | Encoding of reasons why the command can fail.
--   
--   The error code used is 1 for user error.
type ErrorCode = Int
instance GHC.Show.Show Command.Diagram.DiagramMode
instance GHC.Classes.Eq Command.Diagram.DiagramMode
instance GHC.Show.Show Command.Diagram.DiagramFormat
instance GHC.Classes.Eq Command.Diagram.DiagramFormat
instance GHC.Show.Show Command.Diagram.DiagramPropFormat
instance GHC.Classes.Eq Command.Diagram.DiagramPropFormat
instance GHC.Classes.Eq Command.Diagram.Diagram
instance GHC.Show.Show Command.Diagram.Diagram

-- | Transform a specification into a standalone Copilot specification.
module Command.Standalone

-- | 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. 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.
command :: CommandOptions -> IO (Result ErrorCode)

-- | Generate the data of a new standalone Copilot monitor that implements
--   the spec, using a subexpression handler.
commandLogic :: Maybe String -> Maybe FilePath -> String -> [(String, String)] -> ExprPairT a -> Spec a -> ExceptT ErrorTriplet IO AppData

-- | Data that may be relevant to generate a ROS application.
data AppData

-- | Options used to customize the conversion of specifications to Copilot
--   code.
data CommandOptions
CommandOptions :: Maybe String -> Maybe FilePath -> FilePath -> Maybe FilePath -> String -> String -> [(String, String)] -> String -> Maybe String -> Maybe FilePath -> CommandOptions
[commandConditionExpr] :: CommandOptions -> Maybe String

-- | Input specification file.
[commandInputFile] :: CommandOptions -> Maybe FilePath

-- | Target directory where the application should be created.
[commandTargetDir] :: CommandOptions -> FilePath

-- | Directory where the template is to be found.
[commandTemplateDir] :: CommandOptions -> Maybe FilePath

-- | Format of the input file.
[commandFormat] :: CommandOptions -> String

-- | Format used for input properties.
[commandPropFormat] :: CommandOptions -> String
[commandTypeMapping] :: CommandOptions -> [(String, String)]
[commandFilename] :: CommandOptions -> String

-- | Use external command to pre-process system properties.
[commandPropVia] :: CommandOptions -> Maybe String

-- | File containing additional variables to make available to the
--   template.
[commandExtraVars] :: CommandOptions -> Maybe FilePath

-- | Encoding of reasons why the command can fail.
type ErrorCode = Int
instance GHC.Generics.Generic Command.Standalone.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.Standalone.AppData

-- | Create Robot Operating System (ROS) applications that subscribe
--   to obtain data and call Copilot when new values arrive.
--   
--   It is the user's responsibility to modify the generated
--   CopilotCC++ code to deal with the monitors they'd like to
--   implement, and the data they must manipulate.
module Command.ROSApp

-- | Generate a new ROS application connected to Copilot.
command :: CommandOptions -> IO (Result ErrorCode)

-- | Options used to customize the conversion of specifications to ROS
--   applications.
data CommandOptions
CommandOptions :: Maybe String -> Maybe FilePath -> FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> String -> String -> Maybe String -> Maybe FilePath -> [Node] -> [String] -> CommandOptions

-- | Trigger condition.
[commandConditionExpr] :: CommandOptions -> Maybe String

-- | Input specification file.
[commandInputFile] :: CommandOptions -> Maybe FilePath

-- | Target directory where the application should be created.
[commandTargetDir] :: CommandOptions -> FilePath

-- | Directory where the template is to be found.
[commandTemplateDir] :: CommandOptions -> Maybe FilePath

-- | File containing a list of variables to make available to Copilot.
[commandVariables] :: CommandOptions -> Maybe FilePath

-- | File containing a list of known variables with their types and the
--   message IDs they can be obtained from.
[commandVariableDB] :: CommandOptions -> Maybe FilePath

-- | File containing a list of handlers used in the Copilot specification.
--   The handlers are assumed to receive no arguments.
[commandHandlers] :: CommandOptions -> Maybe FilePath

-- | Format of the input file.
[commandFormat] :: CommandOptions -> String

-- | Format used for input properties.
[commandPropFormat] :: CommandOptions -> String

-- | Use external command to pre-process system properties.
[commandPropVia] :: CommandOptions -> Maybe String

-- | File containing additional variables to make available to the
--   template.
[commandExtraVars] :: CommandOptions -> Maybe FilePath

-- | Additional applications to turn on during testing.
[commandTestingApps] :: CommandOptions -> [Node]

-- | Limited list of variables to use for testing.
[commandTestingVars] :: CommandOptions -> [String]

-- | A package-qualified ROS 2 node name.
data Node
Node :: String -> String -> Node

-- | Encoding of reasons why the command can fail.
type ErrorCode = Int
instance GHC.Generics.Generic Command.ROSApp.VarDecl
instance GHC.Generics.Generic Command.ROSApp.Monitor
instance GHC.Generics.Generic Command.ROSApp.Node
instance GHC.Generics.Generic Command.ROSApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.ROSApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.ROSApp.Node
instance Data.Aeson.Types.ToJSON.ToJSON Command.ROSApp.Monitor
instance Data.Aeson.Types.ToJSON.ToJSON Command.ROSApp.VarDecl

-- | Produce an overview of the input files.
module Command.Overview

-- | Generate overview of a spec given 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. The template, if provided, exists and
--   uses the variables needed by the overview application generator. The
--   target directory is writable and there's enough disk space to copy the
--   files over.
command :: FilePath -> CommandOptions -> IO (Maybe CommandSummary, Result ErrorCode)

-- | Options used to customize the interpretation of input specifications.
data CommandOptions
CommandOptions :: String -> String -> Maybe String -> CommandOptions
[commandFormat] :: CommandOptions -> String
[commandPropFormat] :: CommandOptions -> String
[commandPropVia] :: CommandOptions -> Maybe String
data CommandSummary
CommandSummary :: Int -> Int -> Int -> CommandSummary
[commandExternalVariables] :: CommandSummary -> Int
[commandInternalVariables] :: CommandSummary -> Int
[commandRequirements] :: CommandSummary -> Int

-- | Encoding of reasons why the command can fail.
type ErrorCode = Int
instance GHC.Show.Show Command.Overview.CommandSummary
instance GHC.Generics.Generic Command.Overview.CommandSummary
instance Data.Aeson.Types.ToJSON.ToJSON Command.Overview.CommandSummary

-- | Create FPrime components that subscribe to obtain data and call
--   Copilot when new values arrive.
module Command.FPrimeApp

-- | Generate a new FPrime component connected to Copilot.
command :: CommandOptions -> IO (Result ErrorCode)

-- | Options used to customize the conversion of specifications to F'
--   applications.
data CommandOptions
CommandOptions :: Maybe String -> Maybe FilePath -> FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> String -> String -> Maybe String -> Maybe FilePath -> CommandOptions

-- | Trigger condition.
[commandConditionExpr] :: CommandOptions -> Maybe String

-- | Input specification file.
[commandInputFile] :: CommandOptions -> Maybe FilePath

-- | Target directory where the component should be created.
[commandTargetDir] :: CommandOptions -> FilePath

-- | Directory where the template is to be found.
[commandTemplateDir] :: CommandOptions -> Maybe FilePath

-- | File containing a list of variables to make available to Copilot.
[commandVariables] :: CommandOptions -> Maybe FilePath

-- | File containing a list of known variables with their types and the
--   message IDs they can be obtained from.
[commandVariableDB] :: CommandOptions -> Maybe FilePath

-- | File containing a list of handlers used in the Copilot specification.
--   The handlers are assumed to receive no arguments.
[commandHandlers] :: CommandOptions -> Maybe FilePath

-- | Format of the input file.
[commandFormat] :: CommandOptions -> String

-- | Format used for input properties.
[commandPropFormat] :: CommandOptions -> String

-- | Use external command to pre-process system properties.
[commandPropVia] :: CommandOptions -> Maybe String

-- | File containing additional variables to make available to the
--   template.
[commandExtraVars] :: CommandOptions -> Maybe FilePath

-- | Encoding of reasons why the command can fail.
type ErrorCode = Int
instance GHC.Generics.Generic Command.FPrimeApp.VarDecl
instance GHC.Generics.Generic Command.FPrimeApp.Monitor
instance GHC.Generics.Generic Command.FPrimeApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.FPrimeApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.FPrimeApp.Monitor
instance Data.Aeson.Types.ToJSON.ToJSON Command.FPrimeApp.VarDecl

-- | Create NASA Core Flight System (CFS) applications that
--   subscribe to the communication bus and call Copilot when new messages
--   arrive.
--   
--   The applications are created ready to be extracted in the application
--   directory in CFS, and they subscribe to a generic monitor. It is the
--   user's responsibility to modify the generated Copilot and C code to
--   deal with the monitors they'd like to implement, and the data they
--   must manipulate.
module Command.CFSApp

-- | Generate a new CFS application connected to Copilot.
command :: CommandOptions -> IO (Result ErrorCode)

-- | Options used to customize the conversion of specifications to ROS
--   applications.
data CommandOptions
CommandOptions :: Maybe String -> Maybe FilePath -> FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> String -> String -> Maybe String -> Maybe FilePath -> CommandOptions

-- | Trigger condition.
[commandConditionExpr] :: CommandOptions -> Maybe String

-- | Input specification file.
[commandInputFile] :: CommandOptions -> Maybe FilePath

-- | Target directory where the application should be created.
[commandTargetDir] :: CommandOptions -> FilePath

-- | Directory where the template is to be found.
[commandTemplateDir] :: CommandOptions -> Maybe FilePath

-- | File containing a list of variables to make available to Copilot.
[commandVariables] :: CommandOptions -> Maybe FilePath

-- | File containing a list of known variables with their types and the
--   message IDs they can be obtained from.
[commandVariableDB] :: CommandOptions -> Maybe FilePath

-- | File containing a list of handlers used in the Copilot specification.
--   The handlers are assumed to receive no arguments.
[commandHandlers] :: CommandOptions -> Maybe FilePath

-- | Format of the input file.
[commandFormat] :: CommandOptions -> String

-- | Format used for input properties.
[commandPropFormat] :: CommandOptions -> String

-- | Use external command to pre-process system properties.
[commandPropVia] :: CommandOptions -> Maybe String

-- | File containing additional variables to make available to the
--   template.
[commandExtraVars] :: CommandOptions -> Maybe FilePath

-- | Encoding of reasons why the command can fail.
type ErrorCode = Int
instance GHC.Generics.Generic Command.CFSApp.VarDecl
instance GHC.Generics.Generic Command.CFSApp.MsgInfo
instance GHC.Generics.Generic Command.CFSApp.MsgData
instance GHC.Generics.Generic Command.CFSApp.Trigger
instance GHC.Generics.Generic Command.CFSApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.CFSApp.AppData
instance Data.Aeson.Types.ToJSON.ToJSON Command.CFSApp.Trigger
instance Data.Aeson.Types.ToJSON.ToJSON Command.CFSApp.MsgData
instance Data.Aeson.Types.ToJSON.ToJSON Command.CFSApp.MsgInfo
instance Data.Aeson.Types.ToJSON.ToJSON Command.CFSApp.VarDecl
