Previous Up Next

Chapter 8  Advanced features (*)

8.1  Hand-written mappings

Up to now, we have considered examples where the implementation of data-types is either predefined (Xml case), or generated by a tool (Gom case). One interesting contribution of Tom 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.

8.1.1  Defining a simple mapping

In this section, we consider that we have a Java library for representing tree based data structures. On another side, to be able to use Tom, 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 Java 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.

8.1.2  Using backquote constructs

When using the backquote construct (‘suc(suc(zero)) for example), Tom 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, Tom 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;
  }

8.1.3  Advanced examples

Let us suppose that we have a Java class Person with two getters (getFirstname and getLastname). In order to illustrate the signature definition formalism, we try to redefine (without using Gom) the abstract data type for the sort Person.

The first thing to do consists in defining the Tom sort Person:

  %typeterm Person {
    implement { Person }
  }

To avoid any confusion, we use the same name twice: the Tom sort Person is implemented by the Java 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() }
    make(t0, t1) {  new Person(t0, t1) }
  }

In this example, we illustrate another possibility offered by Tom: 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 Java (by using Person.getClass() for example).

8.1.4  Using list-matching

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 Tom 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 Java 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.

Tom 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() }
  }

Previous Up Next