ProB's Prolog Datastructures

Data Values

Integer value:

int(Nr)

where Nr is an integer

Booleans:

pred_true
pred_false

Enumerated or deferred set elements:

fd(Nr,Type)

where Nr is an integer >= 1 and Type is an atom representing the type of enumerated/deferred set

Strings

string(S)

where S is an atom

Pairs/couples

(Val1,Val2)

where Val1 and Val2 are values

Records

rec(Fields)

where Fields is a list of terms:

field(Name,Val)

where Name is atom representing the field name and Val is a value.

The fields are sorted by name!

Sets

[]
[Val|Set]
avl_set(AVL)
closure(P,T,B)
global_set(GS)
freetype(T)

Freetype values

freeval(Id,Case,Value)

AST (Abstract Syntax Tree)

An AST node has the form:

b(Expr,Type,Infos)

Expr generally has the form Functor(AST1,...,ASTk). Below we list possible cases. The predicate syntaxelement in bsyntaxtree.pl lists all allowed forms of Expr. Type is either pred for predicates, subst for substitutions or the value type for expressions, see below. Infos contains information about the AST node and is explained next.

Information list

Infos should be a ground list of informations. Some important information fields are:

contains_wd_condition
used_ids(Ids)
nodeid(PositionInfo)
refers_to_old_state(References)

AST types

Possible types are:

pred
subst
integer
boolean
string
global(G)
couple(T1,T2)
record(FieldTypes)
set(Type)
seq(Type)
freetype(F)

where FieldTypes is a list containing:

field(Name,Type)

Operators without arguments

boolean_false
boolean_true
bool_set

...

Unary operators

card(AST)
domain(AST)
front(AST)

...

Binary operators

cartesian_product(AST1,AST2)
composition(AST1,AST2)
concat(AST1,AST2)
conjunct(AST1,AST2).

...

Special operators

general_sum(Ids,AST,AST)
general_product(Ids,AST,AST)
lambda(Ids,AST,AST)
quantified_union(Ids,AST,AST)
quantified_intersection(Ids,AST,AST)
set_extension(ListOfASTs)
sequence_extension(ListOfASTs)

...