Safe Haskell	None

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
       compile
       generateFragments

Example of compiling a model consisting of one fragment:

 compileOneFragment :: ClaferArgs -> InputModel -> Either ClaferErr CompilerResult
 compileOneFragment args model =
   runClafer args $
     do
       addModuleFragment model
       parse
       compile
       generate

Use generateFragments instead to generate output based on their fragments.

 compileTwoFragments :: ClaferArgs -> InputModel -> InputModel -> Either ClaferErr [String]
 compileTwoFragments args frag1 frag2 =
   runClafer args $
    do
      addModuleFragment frag1
      addModuleFragment frag2
      parse
      compile
      generateFragments

Use throwErr to halt execution:

 runClafer args $
   when (notValid args) $ throwErr (ClaferErr "Invalid arguments.")

Use catchErrs to catch the errors.

Synopsis

Documentation

addModuleFragment :: Monad m => InputModel -> ClaferT m ()Source

Add a new fragment to the model. Fragments should be added in order.

compile :: Monad m => 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 -> Module -> StringSource

Splits the AST into their fragments, and generates the output for each fragment.

generateFragments :: Monad m => ClaferT m [String]Source

Splits the IR into their fragments, and generates the output for each fragment. | Might not generate the entire output (for example, Alloy scope and run commands) because | they do not belong in fragments.

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)

runClafer :: ClaferArgs -> ClaferM a -> Either [ClaferErr] aSource

Convenience

type ClaferErr = CErr ErrPos Source

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 claferEnv :: ClaferEnv the final environment of the compiler mappingToAlloy :: [(Span, IrTrace)] Maps source constraint spans in Alloy to the spans in the IR stringMap :: Map Int String Map back from Ints used to represent Strings scopesList :: [(UID, Integer)] scopes generated by scope inference
NoCompilerResult
Fields reason :: String

Instances

Show CompilerResult

claferIRXSD :: StringSource

The XML Schema of the IR

type VerbosityL = IntSource

type InputModel = StringSource

data Token Source

Instances

Eq Token
Ord Token
Show Token

data Module Source

Instances

Eq Module
Data Module
Ord Module
Read Module
Show Module
Typeable Module
Generic Module
Spannable Module
Print Module

data GEnv Source

Instances

Eq GEnv
Show GEnv

data IModule Source

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

Instances

Eq IModule
Data IModule
Ord IModule
Show IModule
Typeable IModule

voidf :: Monad m => m t -> m ()Source

data ClaferEnv Source

Constructors

ClaferEnv
Fields args :: ClaferArgs modelFrags :: [String] cAst :: Maybe Module cIr :: Maybe (IModule, GEnv, Bool) frags :: [Pos] irModuleTrace :: Map Span [Ir] astModuleTrace :: Map Span [Ast]

Instances

Show ClaferEnv

getIr :: Monad m => ClaferT m (IModule, GEnv, Bool)Source

getAst :: Monad m => ClaferT m Module Source

makeEnv :: ClaferArgs -> ClaferEnv Source

data Pos Source

Constructors

Pos Integer Integer

Instances

Eq Pos
Data Pos
Ord Pos
Read Pos
Show Pos
Typeable Pos
Generic Pos

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

Instances

Eq IrTrace
Show IrTrace

module Language.Clafer.ClaferArgs

module Language.Clafer.Front.ErrM