Language.Clafer

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.

Documentation

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

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

compile :: Monad m => ClaferT m ()

Compiles the AST into IR.

parse :: Monad m => ClaferT m ()

Parses the model into AST. Adding more fragments beyond this point will have no effect.

generate :: Monad m => ClaferT m (Map ClaferMode CompilerResult)

Generates outputs for the given IR.

generateHtml :: ClaferEnv -> Module -> String

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

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

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)

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] a

Convenience

type ClaferErr = CErr ErrPos

getEnv :: Monad m => ClaferT m ClaferEnv

Get the ClaferEnv

putEnv :: Monad m => ClaferEnv -> ClaferT m ()

Set the ClaferEnv. Remember to set the env after every change.

data CompilerResult

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 :: String

The XML Schema of the IR

type VerbosityL = Int

type InputModel = String

data Token

Instances

Eq Token

Ord Token

Show Token

data Module

Instances

Eq Module

Data Module

Ord Module

Read Module

Show Module

Typeable Module

Generic Module

Spannable Module

Print Module

data GEnv

Instances

Eq GEnv

Show GEnv

data IModule

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 ()

data ClaferEnv

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)

getAst :: Monad m => ClaferT m Module

makeEnv :: ClaferArgs -> ClaferEnv

data Pos

Constructors

Pos Integer Integer

Instances

Eq Pos

Data Pos

Ord Pos

Read Pos

Show Pos

Typeable Pos

Generic Pos

data IrTrace

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