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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Language.Trans.Lustre2Copilot

Description

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.

Synopsis

- boolSpec2Copilot :: BoolSpec -> String
- boolSpecNames :: BoolSpec -> [String]

# Documentation

boolSpec2Copilot :: BoolSpec -> String Source #

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.

boolSpecNames :: BoolSpec -> [String] Source #

Return all identifiers used in a BoolSpec that are not reserved keywords.