clafer-0.3.9: 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

type URL = String Source

file:/ ftp: or http:/ prefixed URL

data Ir Source

A "supertype" of all IR types

Constructors

IRIModule IModule 
IRIElement IElement 
IRIType IType 
IRClafer IClafer 
IRIExp IExp 
IRPExp PExp 
IRIReference (Maybe IReference) 
IRIQuant IQuant 
IRIDecl IDecl 
IRIGCard (Maybe IGCard) 

Instances

data IType Source

Constructors

TBoolean 
TString 
TInteger 
TReal 
TClafer [UID]

the type is an intersection of the listed clafers supports having paths in the inheritance hierarchy supports multiple inheritance

Instances

data IModule Source

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

Constructors

IModule 

Fields

_mName :: String

always empty (no syntax for declaring modules)

_mDecls :: [IElement]

List of top-level elements

Instances

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

_parentUID :: UID

"root" if top-level, "" if unresolved or for root clafer, otherwise UID of the parent clafer

_super :: Maybe PExp

superclafer - only allowed PExp is IClaferId. Nothing = default super "clafer"

_reference :: Maybe IReference

reference type, bag or set

_card :: Maybe Interval

clafer cardinality

_glCard :: Interval

(o) global cardinality

_elements :: [IElement]

nested elements

Instances

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 constraint or assertion

_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

Instances

data IReference Source

A type of reference. -> values unique (set) ->> values non-unique (bag)

Constructors

IReference 

Fields

_isSet :: Bool

whether set or bag

_ref :: PExp

the only allowed reference expressions are IClafer and set expr. (++, **, --s)

Instances

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 

Fields

_isKeyword :: Bool

whether given by keyword: or, xor, mux

_interval :: Interval
 

Instances

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

Instances

type ClaferBinding = Maybe UID Source

Embedes reference to a resolved Clafer

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

_binding :: ClaferBinding

the UID of the bound IClafer, if resolved

Instances

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

Instances

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

Instances

type LineNo = Integer Source

type ColNo = Integer Source

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

unWrapIModule :: Ir -> IModule Source

unWrapIElement :: Ir -> IElement Source

unWrapIType :: Ir -> IType Source

unWrapIClafer :: Ir -> IClafer Source

unWrapIExp :: Ir -> IExp Source

unWrapPExp :: Ir -> PExp Source

unWrapIReference :: Ir -> Maybe IReference Source

unWrapIQuant :: Ir -> IQuant Source

unWrapIDecl :: Ir -> IDecl Source

unWrapIGCard :: Ir -> Maybe IGCard Source

mName :: Lens' IModule String Source

mDecls :: Lens' IModule [IElement] Source

uid :: Lens' IClafer UID Source

super :: Lens' IClafer (Maybe PExp) Source

reference :: Lens' IClafer (Maybe IReference) Source

parentUID :: Lens' IClafer UID Source

isAbstract :: Lens' IClafer Bool Source

ident :: Lens' IClafer CName Source

glCard :: Lens' IClafer Interval Source

gcard :: Lens' IClafer (Maybe IGCard) Source

elements :: Lens' IClafer [IElement] Source

cinPos :: Lens' IClafer Span Source

card :: Lens' IClafer (Maybe Interval) Source

isMaximize :: Traversal' IElement Bool Source

isHard :: Traversal' IElement Bool Source

iClafer :: Traversal' IElement IClafer Source

cpexp :: Traversal' IElement PExp Source

ref :: Lens' IReference PExp Source

isSet :: Lens' IReference Bool Source

isKeyword :: Lens' IGCard Bool Source

interval :: Lens' IGCard Interval Source

pid :: Lens' PExp String Source

inPos :: Lens' PExp Span Source

iType :: Lens' PExp (Maybe IType) Source

exp :: Lens' PExp IExp Source

sident :: Traversal' IExp CName Source

quant :: Traversal' IExp IQuant Source

op :: Traversal' IExp String Source

oDecls :: Traversal' IExp [IDecl] Source

modName :: Traversal' IExp String Source

istr :: Traversal' IExp String Source

isTop :: Traversal' IExp Bool Source

iint :: Traversal' IExp Integer Source

idouble :: Traversal' IExp Double Source

exps :: Traversal' IExp [PExp] Source

bpexp :: Traversal' IExp PExp Source

binding :: Traversal' IExp ClaferBinding Source

isDisj :: Lens' IDecl Bool Source

decls :: Lens' IDecl [CName] Source

body :: Lens' IDecl PExp Source