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

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

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

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

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)

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
 

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

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

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