Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Trans.Spec2Copilot

Contents

Auxiliary

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

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 #

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.