ProB's Prolog Datastructures: Difference between revisions

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 Here is an overview of the set representations:

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

The empty set is encoded as the empty list.

[]

This represents a set containing at least the value Val and the rest:

[Val|Set]

Note that Set can in principle be any other form (e.g., avl_set(.)). The predicate expand_custom_set_to_list can be used to transform a set into a form using only the empty list and the [.|.] functor.

The next are called custom explicit sets, they always represent a fully known set.

A set can be represented by a non-empty AVL tree:

avl_set(AVL)

Given a list of parameter identifiers, a list of types and a predicate AST B, we can represent the set {P| P:T & B} as follows:

closure(P,T,B)

There are custom representations for complete types, these may be phased out in the future and replaced by the closure(.,.,.) representation:

global_set(GS)
freetype(T)

Freetype values

freeval(Id,Case,Value)

Constructor for denoting special values (undefined values, experimental support for reals,..)

term(Term)

term(undefined) is used for uninitialised variables (e.g., when using the B VAR construct). term(floating(Nr) is currently used for floating numbers, but this will probably change in the future.

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
real
boolean
string
global(G)
couple(Type1,Type2)
record(FieldTypes)
set(Type)
seq(Type)
freetype(F)

where FieldTypes is a list containing:

field(Name,Type)

The real type has been added in version 1.10 of ProB.

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)

...