clafer-0.3.7: clafer compiles Clafer models to other formats, such as Alloy, XML, HTML, Dot.

Safe HaskellNone
LanguageHaskell2010

Language.Clafer.Intermediate.Intclafer

Description

Intermediate representation (IR) of a Clafer model

Synopsis

Documentation

type UID = String Source

unique identifier of a clafer

type CName = String Source

clafer name as declared in the source model

data IModule Source

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

Constructors

IModule 

Fields

_mName :: String

always empty for now because we don't have syntax for declaring modules

_mDecls :: [IElement]

List of top-level elements

data IClafer Source

Clafer has a list of fields that specify its properties. Some fields, marked as (o) are for generating optimized code

Constructors

IClafer 

Fields

_cinPos :: Span

the position of the syntax in source code

_isAbstract :: Bool

whether abstract or not (i.e., concrete)

_gcard :: Maybe IGCard

group cardinality

_ident :: CName

name declared in the model

_uid :: UID

a unique identifier

_super :: ISuper

superclafers

_card :: Maybe Interval

clafer cardinality

_glCard :: Interval

(o) global cardinality

_elements :: [IElement]

nested elements

data IElement Source

Clafer's subelement is either a clafer, a constraint, or a goal (objective) This is a wrapper type needed to have polymorphic lists of elements

Constructors

IEClafer 

Fields

_iClafer :: IClafer

the actual clafer

IEConstraint 

Fields

_isHard :: Bool

whether hard or not (soft)

_cpexp :: PExp

the container of the actual expression

IEGoal

Goal (optimization objective)

Fields

_isMaximize :: Bool

whether maximize or minimize

_cpexp :: PExp

the container of the actual expression

data ISuper Source

A list of superclafers. -> overlaping unique (set) ->> overlapping non-unique (bag) : non overlapping (disjoint)

Constructors

ISuper 

Fields

_isOverlapping :: Bool
 
_supers :: [PExp]
 

data IGCard Source

Group cardinality is specified as an interval. It may also be given by a keyword. xor 1..1 isKeyword = True 1..1 1..1 isKeyword = False

Constructors

IGCard 

type Interval = (Integer, Integer) Source

(Min, Max) integer interval. -1 denotes *

data PExp Source

This is expression container (parent). It has meta information about an actual expression exp

Constructors

PExp 

Fields

_iType :: Maybe IType

the inferred type

_pid :: String

non-empty unique id for expressions with span, "" for noSpan

_inPos :: Span

position in the input Clafer file

_exp :: IExp

the actual expression

data IExp Source

Constructors

IDeclPExp

quantified expression with declarations e.g., [ all x1; x2 : X | x1.ref != x2.ref ]

Fields

_quant :: IQuant
 
_oDecls :: [IDecl]
 
_bpexp :: PExp
 
IFunExp

expression with a unary function, e.g., -1 binary function, e.g., 2 + 3 ternary function, e.g., if x then 4 else 5

Fields

_op :: String
 
_exps :: [PExp]
 
IInt

integer number

Fields

_iint :: Integer
 
IDouble

real number

Fields

_idouble :: Double
 
IStr

string

Fields

_istr :: String
 
IClaferId

a reference to a clafer name

Fields

_modName :: String

module name - currently not used and empty since we have no module system

_sident :: CName

name of the clafer being referred to

_isTop :: Bool

identifier refers to a top-level definition

data IDecl Source

For IFunExp standard set of operators includes: 1. Unary operators: ! - not (logical) # - set counting operator - - negation (arithmetic) max - maximum (created for goals) min - minimum (created for goals) 2. Binary operators: <=> - equivalence => - implication || - disjunction xor - exclusive or && - conjunction < - less than > - greater than = - equality <= - less than or equal >= - greater than or equal != - inequality in - belonging to a set/being a subset nin - not belonging to a set/not being a subset + - addition/string concatenation - - substraction * - multiplication / - division ++ - set union -- - set difference & - set intersection <: - domain restriction :> - range restriction . - relational join 3. Ternary operators ifthenelse -- if then else

Local declaration disj x1; x2 : X ++ Y y1 : Y

Constructors

IDecl 

Fields

_isDisj :: Bool

is disjunct

_decls :: [CName]

a list of local names

_body :: PExp

set to which local names refer to

data IQuant Source

quantifier

Constructors

INo

does not exist

ILone

less than one

IOne

exactly one

ISome

at least one (i.e., exists)

IAll

for all

mapIR :: (Ir -> Ir) -> IModule -> IModule Source

map over IR

foldMapIR :: Monoid m => (Ir -> m) -> IModule -> m Source

foldMap over IR

foldIR :: (Ir -> a -> a) -> a -> IModule -> a Source

fold the IR

iMap :: (Ir -> Ir) -> Ir -> Ir Source

iFoldMap :: Monoid m => (Ir -> m) -> Ir -> m Source

iFold :: (Ir -> a -> a) -> a -> Ir -> a Source