| title | permalink |
|---|---|
Documentation:Advanced features |
/Documentation:Advanced_features/ |
Up to now, we have considered examples where the implementation of data-types is either predefined ( case), or generated by a tool ( case). One interesting contribution of is to be customizable. By defining a mapping between the signature formalism (%typeterm, %op, etc.) and the concrete implementation, it becomes possible to perform pattern matching against any data-structure and consider subtyping.
In this section, we consider that we have a library for representing tree based data structures. On another side, to be able to use , we consider the following abstract data-type:
%typeterm Nat
%op Nat zero()
%op Nat suc(Nat)
By doing so, we have defined a sort (Nat), and two operators (zero and suc). When defining a mapping, the goal consists in explaining to Tom how the considered abstract data-type is implemented, and how a term (over this signature) can be de-constructed.
For expository reasons, the ATerm library is the library used to implement terms. However, any other tree/term based library could have been used instead.
In order to define a correct mapping, we have to describe how the algebraic sort (Nat in our example) is implemented (by the ATermAppl class). This is done via the implement construct:
%typeterm Nat {
implement { ATermAppl }
}
The second part of the mapping definition consists in defining how the symbols (zero and suc) are represented in memory. This is done via the is_fsym construct:
%op Nat zero() {
is_fsym(t) { t.getName().equals("zero") }
}
%op Nat suc(pred:Nat) {
is_fsym(t) { t.getName().equals("suc") }
get_slot(pred,t) { (ATermAppl)t.getArgument(0) }
}
In addition, get_slot describes how to retrieve a subterm of a term.
Given a term built over the ATerm library, it becomes possible to perform pattern matching as previously explained.
When using the backquote construct (‘suc(suc(zero)) for example), has to know how to build a term in memory. For this purpose, we consider an extension of the signature definition formalism: the make construct.
%op Nat zero() {
is_fsym(t) { t.getName().equals("zero") }
make { SingletonFactory.getInstance().makeAppl(
SingletonFactory.getInstance().makeAFun("zero",0,false)) }
}
%op Nat suc(pred:Nat) {
is_fsym(t) { t.getName().equals("suc") }
get_slot(pred,t) { (ATermAppl)t.getArgument(0) }
make(t) { SingletonFactory.getInstance().makeAppl(
SingletonFactory.getInstance().makeAFun("suc",1,false),t) }
}
The makeAFun function has three arguments: the function name, the number of arguments and a boolean that indicates if the quotes are included in the function name or not.
Given this mapping, can be used as previously: the following function implements the addition of two Peano integers:
public ATermAppl plus(ATermAppl t1, ATermAppl t2) {
%match(t2) {
zero() -> { return t1; }
suc(y) -> { return `suc(plus(t1,y)); }
}
return null;
}
Let us suppose that we have a class Person with two getters (getFirstname and getLastname). In order to illustrate the signature definition formalism, we try to redefine (without using ) the abstract data type for the sort Person.
The first thing to do consists in defining the sort Person:
%typeterm Person {
implement { Person }
is_sort(t) { t instanceof Person }
}
To avoid any confusion, we use the same name twice: the sort Person is implemented by the class Person. When declaring an operator, we defined the behavior as shown in the previous example:
%op Person person(firstname:String, lastname:String) {
is_fsym(t) { t instanceof Person }
get_slot(firstname,t) { t.getFirstname() }
get_slot(lastname,t) { t.getLastname() }
get_default(firstname) { "Bob" }
get_default(lastname) { "Doe" }
make(t0, t1) { new Person(t0, t1) }
}
In this example, we illustrate another possibility offered by : being able to know whether a term is rooted by a symbol without explicitly representing this symbol. The is_fsym(t) construct should return true when the term t is rooted by the algebraic operator we are currently defining. In this example, we say that the term t is rooted by the symbol person when the object t is implemented by an instance of the class Person. By doing so, we do not explicitly represent the symbol person, even if it could have been done via the reflective capabilities of (by using Person.getClass() for example).
We also introduce the get_default(t) optionnal construct in this example. It allows to set a default value to one or several fields of the operator. Then, those default values can be used as follow:
//use of lastname default value
//explicit notation
Person p1 = `person[firstname="John"];
//implicit notation
Person p2 = `person("John",_);
//use of firstname default value
Person p3 = `person[lastname="Dylan"];
//use of all default values
Person p4 = `person(_,_);
In this section, we show how to describe a type hierarchy between declared sorts.
Assuming the sort Person defined above and supposing that we have a class Woman with three getters (getFirstname, getLastname and getLastsinglename), we define the sort Woman:
%typeterm Woman extends Person {
implement { Woman }
is_sort(t) { t instanceof Woman }
}
Once more we use the same name twice: the sort Woman is implemented by the class Woman which extends the class Person. We propagate this subtype relation in by declaring that Woman is a subsort of (i.e. extends) Person. Note that, as in , multiple inheritance is not allowed in since a sort can not be defined twice. The supertypes of a sort are obtained by reflexive and transitive closure over the direct supertype relation.
When declaring the operator Woman, we define its behavior:
%op Woman woman(firstname:String, lastname:String, lastsinglename:String) {
is_fsym(t) { t instanceof Woman}
get_slot(firstname,t) { t.getFirstname() }
get_slot(lastname,t) { t.getLastname() }
get_slot(lastsinglename,t) { t.getLastsinglename() }
make(t0, t1, t2) { new Woman(t0, t1, t2) }
}
Given this mapping, when considering a subject of sort Person is able to match patterns having the same sort Person or a subsort as Woman:
public void print(Person p) {
%match(p) {
woman(first,last,lastsingle)-> {
if (`last != `lastsingle) {
System.out.println("woman"+ `last + " " + `first + " is married.");
}
}
person(first,last) -> {
System.out.println("person "+ `last + " " + `first);
}
}
}
In this section, we show how to describe a mapping for associative operators.
%typeterm TomList {
implement { ArrayList }
equals(l1,l2) { l1.equals(l2) }
}
Assuming that the sort Element is already defined, we can use the %oparray construct to define an associative operator. We also have to explain to how to compute the size of a list, and how to access a given element. This is done via get_size and get_element constructs:
%oparray TomList conc( Element* ) {
is_fsym(t) { t instanceof ArrayList }
get_element(l,n) { (ATermAppl)l.get(n) }
get_size(l) { l.size() }
make_empty(n) { myEmpty(n) }
make_append(e,l) { myAdd(e,(ArrayList)l) }
}
This construct is similar to %op except that additional information have to be given: how to build an empty list (make_empty), and how to add an element to a given list (make_append). The auxiliary functions are defined as follows:
private static ArrayList myAdd(Object e,ArrayList l) {
l.add(e);
return l;
}
private static ArrayList myEmpty(int n) {
ArrayList res = new ArrayList(n);
return res;
}
Usually, we use an associative operator to represent (in a abstract way) a list data structure. There are many ways to implement a list, but the two most well-known are the use of array based list, and the use of linked-list. The previously described mapping shows how to map an abstract list to an array based implementation.
offers another similar construct %oplist to map an associative operator to a linked-list based implementation. When using the ATerm library for example, a possible implementation could be:
%typeterm TomTerm {
implement { aterm.ATermAppl }
equals(t1, t2) { t1==t2 }
}
%typeterm TomList {
implement { ATermList }
equals(l1,l2) { l1==l2 }
}
%oplist TomList conc( TomTerm* ) {
is_fsym(t) { t instanceof aterm.ATermList }
make_empty() { aterm.pure.SingletonFactory.getInstance().makeList() }
make_insert(e,l) { l.insert(e) }
get_head(l) { (aterm.ATermAppl)l.getFirst() }
get_tail(l) { l.getNext() }
is_empty(l) { l.isEmpty() }
}