Safe Haskell | None |
---|---|
Language | Haskell2010 |
Top-level interface to the Clafer compiler
Normal usage:
t :: InputModel -> InputModel -> Either [ClaferErr] [String] t a b = runClafer defaultClaferArgs $ do addModuleFragment a addModuleFragment b parse iModule <- desugar "" compile iModule generate
Example of compiling a model consisting of one fragment:
compileOneFragment :: ClaferArgs -> InputModel -> Either ClaferErr CompilerResult compileOneFragment args model = runClafer args $ do addModuleFragment model parse iModule <- desugar "http://mydomain.org/mymodel.cfr" compile iModule generate
compileTwoFragments :: ClaferArgs -> InputModel -> InputModel -> Either ClaferErr [String] compileTwoFragments args frag1 frag2 = runClafer args $ do addModuleFragment frag1 addModuleFragment frag2 parse iModule <- desugar "" compile iModule generate
Use "throwErr" to halt execution:
runClafer args $ when (notValid args) $ throwErr (ClaferErr "Invalid arguments.")
Use "catchErrs" to catch the errors.
- runCompiler :: Maybe URL -> ClaferArgs -> InputModel -> IO ()
- addModuleFragment :: Monad m => InputModel -> ClaferT m ()
- compile :: Monad m => IModule -> ClaferT m ()
- parse :: Monad m => ClaferT m ()
- desugar :: Monad m => Maybe URL -> ClaferT m IModule
- generate :: Monad m => ClaferT m (Map ClaferMode CompilerResult)
- generateHtml :: ClaferEnv -> String
- runClaferT :: Monad m => ClaferArgs -> ClaferT m a -> m (Either [ClaferErr] a)
- runClafer :: ClaferArgs -> ClaferM a -> Either [ClaferErr] a
- type ClaferErr = CErr ErrPos
- getEnv :: Monad m => ClaferT m ClaferEnv
- putEnv :: Monad m => ClaferEnv -> ClaferT m ()
- data CompilerResult
- = CompilerResult {
- extension :: String
- outputCode :: String
- statistics :: String
- claferEnv :: ClaferEnv
- mappingToAlloy :: [(Span, IrTrace)]
- stringMap :: Map Int String
- scopesList :: [(UID, Integer)]
- | NoCompilerResult { }
- = CompilerResult {
- type InputModel = String
- data Token
- data Module
- data GEnv
- data IModule
- data ClaferEnv = ClaferEnv {
- args :: ClaferArgs
- modelFrags :: [String]
- cAst :: Maybe Module
- cIr :: Maybe (IModule, GEnv, Bool)
- frags :: [Pos]
- astModuleTrace :: Map Span [Ast]
- otherTokens :: [Token]
- getIr :: Monad m => ClaferT m (IModule, GEnv, Bool)
- getAst :: Monad m => ClaferT m Module
- makeEnv :: ClaferArgs -> ClaferEnv
- data Pos = Pos Integer Integer
- data IrTrace
- module Language.Clafer.ClaferArgs
- module Language.Clafer.Front.ErrM
Documentation
runCompiler :: Maybe URL -> ClaferArgs -> InputModel -> IO () Source #
Run the Clafer compiler. mURL = Nothing means compile the top-level module mURL = Just url means compile an imported module from the given url
addModuleFragment :: Monad m => InputModel -> ClaferT m () Source #
Add a new fragment to the model. Fragments should be added in order.
parse :: Monad m => ClaferT m () Source #
Parses the model into AST. Adding more fragments beyond this point will have no effect.
generate :: Monad m => ClaferT m (Map ClaferMode CompilerResult) Source #
Generates outputs for the given IR.
generateHtml :: ClaferEnv -> String Source #
Splits the AST into their fragments, and generates the output for each fragment.
runClaferT :: Monad m => ClaferArgs -> ClaferT m a -> m (Either [ClaferErr] a) Source #
Uses the ErrorT convention: | Left is for error (a string containing the error message) | Right is for success (with the result)
putEnv :: Monad m => ClaferEnv -> ClaferT m () Source #
Set the ClaferEnv. Remember to set the env after every change.
data CompilerResult Source #
Result of generation for a given mode
CompilerResult | |
| |
NoCompilerResult | |
type InputModel = String Source #
each file contains exactly one mode. A module is a list of declarations
makeEnv :: ClaferArgs -> ClaferEnv Source #
module Language.Clafer.ClaferArgs
module Language.Clafer.Front.ErrM