clafer-0.4.3: Compiles Clafer models to other formats: Alloy, JavaScript, JSON, HTML, Dot.

Safe HaskellNone
LanguageHaskell2010

Language.Clafer

Description

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.

Synopsis

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.

compile :: Monad m => IModule -> ClaferT m () Source

Compiles the AST into IR.

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)

getEnv :: Monad m => ClaferT m ClaferEnv Source

Get the ClaferEnv

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

Constructors

CompilerResult 

Fields

extension :: String

output file extension

outputCode :: String

output text

statistics :: String

the final environment of the compiler

claferEnv :: ClaferEnv

Maps source constraint spans in Alloy to the spans in the IR

mappingToAlloy :: [(Span, IrTrace)]

Map back from Ints used to represent Strings

stringMap :: Map Int String

scopes generated by scope inference

scopesList :: [(UID, Integer)]
 
NoCompilerResult 

Fields

reason :: String
 

data IModule Source

each file contains exactly one mode. A module is a list of declarations

data IrTrace Source

Constructors

IrPExp 

Fields

pUid :: String
 
LowerCard 

Fields

pUid :: String
 
isGroup :: Bool
 
UpperCard 

Fields

pUid :: String
 
isGroup :: Bool
 
ExactCard 

Fields

pUid :: String
 
isGroup :: Bool
 
NoTrace