| Safe Haskell | None |
|---|---|
| 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.