| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Language.Trans.Spec2Copilot
Contents
Description
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.
Synopsis
- spec2Copilot :: 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)
- safeMap :: [(String, String)] -> String -> String
- unlines' :: [String] -> String
- internalVariableMap :: Spec a -> [(String, String)]
- externalVariableMap :: Spec a -> [(String, String)]
- requirementNameMap :: Spec a -> [(String, String)]
- internalVariableNames :: Spec a -> [String]
- externalVariableNames :: Spec a -> [String]
- requirementNames :: Spec a -> [String]
Documentation
spec2Copilot :: String -> [(String, String)] -> ([(String, String)] -> a -> a) -> (a -> String) -> Spec a -> Either String (String, String, String, String, String) Source #
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.
specAnalyze :: Spec a -> Either String (Spec a) Source #
Check that a specification does not contain any name clashes between variables and/or requirements.
Auxiliary
safeMap :: [(String, String)] -> String -> String Source #
Substitute a string based on a given substitution table.
This function leaves the key unchanged if it cannot be found in the substitution table.
unlines' :: [String] -> String Source #
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.
internalVariableMap :: Spec a -> [(String, String)] Source #
Map from an internal variable name to its desired identifier in the code generated.
externalVariableMap :: Spec a -> [(String, String)] Source #
Map from an external variable name to its desired identifier in the code generated.