ogma-core-1.14.0: Ogma: Helper tool to interoperate between Copilot and other languages.

Safe Haskell | None
Language | Haskell2010

Command.Standalone

Description

Transform a specification into a standalone Copilot specification.

Synopsis

- command :: CommandOptions -> IO (Result ErrorCode)
- commandLogic :: Maybe String -> [FilePath] -> String -> [(String, String)] -> ExprPairT a -> InputFile a -> ExceptT ErrorTriplet IO AppData
- data AppData
- data CommandOptions = CommandOptions {
  - commandConditionExpr :: Maybe String
  - commandInputFiles :: [FilePath]
  - commandTargetDir :: FilePath
  - commandTemplateDir :: Maybe FilePath
  - commandFormat :: String
  - commandPropFormat :: String
  - commandTypeMapping :: [(String, String)]
  - commandFilename :: String
  - commandPropVia :: Maybe String
  - commandExtraVars :: Maybe FilePath
  }
- type ErrorCode = Int

# Documentation

command Source #

Arguments

:: CommandOptions | Customization options
-> IO (Result ErrorCode) |

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.

commandLogic :: Maybe String -> [FilePath] -> String -> [(String, String)] -> ExprPairT a -> InputFile a -> ExceptT ErrorTriplet IO AppData Source #

Generate the data of a new standalone Copilot monitor that implements the spec, using a subexpression handler.

data AppData Source #

Data that may be relevant to generate a ROS application.

#### Instances

Instances details

ToJSON AppData Source # |
Instance details Defined in Command.Standalone Methods toJSON :: AppData -> Value Source # toEncoding :: AppData -> Encoding Source # toJSONList :: [AppData] -> Value Source # toEncodingList :: [AppData] -> Encoding Source # omitField :: AppData -> Bool Source #
Generic AppData Source # |

Instance details

Defined in Command.Standalone

Associated Types

type Rep AppData |

Instance details

Defined in Command.Standalone

type Rep AppData = D1 ('MetaData "AppData" "Command.Standalone" "ogma-core-1.14.0-Fq0eOcjOUbXAutdAdQvAxc" 'False) (C1 ('MetaCons "AppData" 'PrefixI 'True) ((S1 ('MetaSel ('Just "externs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "internals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :*: (S1 ('MetaSel ('Just "reqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "triggers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "specName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))

Methods

from :: AppData -> Rep AppData x Source #

to :: Rep AppData x -> AppData Source #

type Rep AppData Source # |

Instance details

Defined in Command.Standalone

type Rep AppData = D1 ('MetaData "AppData" "Command.Standalone" "ogma-core-1.14.0-Fq0eOcjOUbXAutdAdQvAxc" 'False) (C1 ('MetaCons "AppData" 'PrefixI 'True) ((S1 ('MetaSel ('Just "externs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "internals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :*: (S1 ('MetaSel ('Just "reqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "triggers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "specName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))

data CommandOptions Source #

Options used to customize the conversion of specifications to Copilot code.

Constructors

CommandOptions |

Fields

- commandConditionExpr :: Maybe String
- commandInputFiles :: [FilePath]

  Input specification file(s).

- commandTargetDir :: FilePath

  Target directory where the application should be created.

- commandTemplateDir :: Maybe FilePath

  Directory where the template is to be found.

- commandFormat :: String

  Format of the input file.

- commandPropFormat :: String

  Format used for input properties.

- commandTypeMapping :: [(String, String)]
- commandFilename :: String
- commandPropVia :: Maybe String

  Use external command to pre-process system properties.

- commandExtraVars :: Maybe FilePath

  File containing additional variables to make available to the template.

type ErrorCode = Int Source #

Encoding of reasons why the command can fail.