Tom Planet

Tom 2.5 is finally out ! Here is the official announce: Tom 2.5 announcement -------------------- It is our great privilege and pleasure to announce the availability of Tom version 2.5. This release continues our work on the integration of pattern matching and rule based programming facilities into C and Java. Tom is a pattern matching compiler developed at INRIA. It is particularly well-suited for programming various transformations on trees/terms and XML based documents. Its design follows our research on the semantics and the efficient compilation of rule based languages (e.g. ELAN, developed at INRIA-Loria). Many applications have been developed in Tom. Among them, let us mention: - the Tom compiler itself - languages semantics, interpreters and program transformation tools - a generator of canonical abstract syntax trees (Gom) - a Just In Time strategy compiler using dynamic Java bytecode transformation - a proof assistant for supernatural deduction - a compiler algorithm for anti-pattern matching and disunification Tom is a complex compiler which adds powerful constructs to C and Java: rewrite rules, strategies, non linear syntactic matching, associative matching with neutral element (a.k.a. list-matching), XML based pattern matching, string matching, and equational rewriting. This offers the possibility to analyze and transform any kind of data-structure. Tom can be used for large scale developments and applications. It comes with documentation, as well as with programming and debugging support. This new release contains many improvements and new features: - a new compiler based on constraint propagation. This makes the code simpler and ready for combinations of theories. - a new strategy library, simpler to use, more efficient, and ready for graph traversal. - a new "rule" construct to specify conditional rewrite rules that are always applied (the data-structure is in normal form by construction). - a full support of list-operators whose domain is equal to the codomain. This corresponds to associative matching with neutral element (AU). An interesting variant for flattened lists (FL) has also been developed. - the data-structure can be normalized wrt. to associative-commutative (AC) or AC with neutral element (ACU). - any combination of patterns, anti-patterns, and list-operators is fully supported. - the possibility to define terms with pointers. This is very useful to represent, analyze, and transform term-graphs like CFG for example. Tom is available, in open source (GPL/BSD License), from the web page: http://tom.loria.fr/ Best regards, Tom development team

Tom 2.5 is finally out !

We tagged the release today, and prepared all the stuff for the release. thanks to Radu, we now even have an automatic installer for Windows. Now, we need to announce it to the whole world, before starting to refactor/break/enhance everything for tom 2.6, and integrate all the new ideas.

The release notes are at there.

The second release candidate for tom-2.5 was packed today. Please do report any bug or problems you get with this pre-release. Windows installer and Eclipse plugin will be added to the RC soon.

The first pre-release for tom-2.5 was released today. Please do report any bug or problems you get with this pre-release

An experimental windows installer is available for tom version 2.5 alpha. Please, contact us if you encounter any problem.

We are preparing a new release of Tom. This version will include a completely new strategy library, still very efficient, but able to traverse a graphs. The second major improvement comes from a completely new compiler based on constraint solving. The generated code is as good as before (and sometime better). This new technology will offer much more flexibility and possibility to extend the expressiveness of patterns. This version will also contains many improvements. In particular, Associative matching with neutral element is now fully supported.

This week, Pierre-Etienne suggested that we should try Cenqua Clover (http://www.cenqua.com/clover/) for Tom.

Once integrated into our build system, this code coverage tool gives many useful advices.
I wasn't convinced that code coverage can be useful, but after testing it, now I am.
Running the Tom test suite and some examples build shows many things we do not really test at all, and spots areas of improvement.

This week-end, i decided (slightly influenced by Pierre-Étienne) to implement a new and shiny feature in Gom: the possiblility to specify packages in module names.

This feature in cool, as it removes the need to use a compilation option to integrate the Gom data structure in a project: you simply have to name your module accordingly to the package.

Previously, to place the module "Peano" in the "classical" package, we had to write the Peano module in a file, Peano.gom

module Peano
abstract syntax
Nat = zero() | suc(n:Nat)

and then to compile it with gom -p classical Peano.gom

Then, for each gom file in a project, the call was different ! That's not fun if you are used to javac.
Now, we simply write

module classical.Peano
abstract syntax
Nat = zero() | suc(n:Nat)

and compile it with gom Peano.gom

Once prepared to implement that, found what to change in the design, and all, i simply read the Changelog, and found the entry

2006-11-04 tonio
* src/tom/gom/parser/:
- add support for qualifier module names
the module "dir.mod" is similar to the declaration
of a module "mod" compiled with "--package dir" option

I'm not sure I should add a new entry simply because I thought about implementing that a second time.

Tom is hosted by FishEye! http://fisheye3.cenqua.com/browse/tom have fun!

The tom plugin is referenced by Eclipse Plugin Central: http://www.eclipseplugincentral.com/Web_Links-index-req-viewlink-cid-771.html

My work environment

And the most important: a great keyboard (thanks pem)

Source code analysis

I just saw an analysis of the different languages used in the Kaffe project, at http://supreetsethi.net/drupal/node/103



I wish we could have something like that for Tom. I guess it would show we have nearly no make files, very few ant scripts, and keep concentrate our efforts on Tom itself

I just added the post-commit hooks for cia to the svn repository of Tom.

That was pretty easy, except that it seems gforge does not support xml-rpc, and I had to let the cia-bot script fall back to hte old email technique.

Here is the stat page for tom: http://cia.navi.cx/stats/project/tom

/\_/ |. . |
( -/ )
`T/

A shrinked cat... add some spaces to see his cheeks

No Tom today, some minor bug prevents me to post my wonderful example It is the chance to play with other cool languages.

Since I left my old but well-working modem for the brand new livebox, i’m very unhappy. To illustrate this fact and to improve my ascii-art skills, figure 1 summarizes the story (yes, this a png, yes this is lame..but wordpress won’t let me insert spaces into code tags, nor verbatim ones).

One really annoying thing is the dhcp server that allocates a (apparently) random address to every new wireless connected computer. It means that I have to guess my brother’s ip address to establish an ssh/sftp connection. I thought I just had to do some broadcast ping on the network, but I didn’t find any command to do this.

/!\ Antoine, if you’re reading this : there surely is an os pre-built solution for this problem, please don’t make me feel like i am completely useless /!\

So i thought of ocaml as a scripting language. As a result i came out with a tiny script. Sorry again for the missing indentation. [edit: now working !]

open Thread
open Sys

let ping ip =
  let ret = Sys.command ("ping -c1 "^ip^" > /dev/null") in
    match ret with
      0 -> print_string (ip^"tokn"); flush stdout
     | _ -> ()
;;

let wait = List.iter Thread.join in
  let t = ref [] in
  let i = ref 1 in
    while !i < 255 do
      try
        t := Thread.create ping ("192.168.1."^(string_of_int !i))::!t ;
        i := !i+1
      with
        _ -> wait !t; t := []
    done;

  wait !t
;;

The only tricky part is the line _ -> wait !t; t := [] , which waits to the n first ping commands to end when the underlying os can’t create more processes anymore.Now let’s look at the profit of using caml here:

• The standard library provides portable threads.
• All type are infered, so it’s like writing it with a scripting language like python or perl.
• However, the program is typesafe and is more likely to run without errors out of the box.
• The program is compiled : huge gain here
• Writing ocaml scripts is much more cooler than shell ones !

Why not boost some dying project like NetBSD by replacing sh with ocaml ? This surely would make a slashdot entry

PS: For real and funny ascii art, take a look at nerdboy.

The Tom logo contest is open. Feel free to submit any idea.

Here are some possibilities:





Note that these logo may not be free. We have to check.

We now use the subversion facilities offered by Gforge. Please, update your source tree and keep us informed in case of problem.

One of my favourite way of wasting time is to take part to blind tests with my friends. This allow us to improve our knowledge of the great 80’s One problem with this game is that it requires a referee who can’t play, so no one wants to attend this role. That’s why, being good geeks, we decided to let the computer chose the tracks and decide who was right. To achieve this, my friend Paul (phd student in the led project) wrote a plugin for the great amarok music player, using the great python language. By the way, a python backend for tom is on the way … i’m just to lazy for the moment to handle indentation issues.

That’s cool, but the plugin was completly unsuable because of the accuracy of artists’ names required by the program. We then took a look at the existing algorithms which compute a sort of “sound equality”. The oldest and most famous of them seems to be the soundex one. The wikipedia description isn’t very precise but as you can see, it is mainly composed of rewrite rules :

1. Retain the first letter of the string
2. Remove all occurrences of the following letters, unless it is the first letter: a, e, h, i, o, u, w, y
3. Assign numbers to the remaining letters (after the first) as follows:
   • b, f, p, v = 1
   • c, g, j, k, q, s, x, z = 2
   • d, t = 3
   • l = 4
   • m, n = 5
   • r = 6
4. If two or more letters with the same number were adjacent in the original name (before step 1), or adjacent except for any intervening h and w (American census only), then omit all but the first.
5. Return the first four characters, right-padding with zeroes if there are fewer than four.

The translation into Tom rules is straightforward. For instance, rule 4 is translated as follows:

 public String removeDoubles(String s) {
  %match (String s) {
    (f,X*,x,x,Y*)     -> { return removeDoubles(`f+`X*+`x+`Y*); }
    (f,X*,x,'w',x,Y*) -> { return removeDoubles(`f+`X*+`x+`Y*); }
    (f,X*,x,'h',x,Y*) -> { return removeDoubles(`f+`X*+`x+`Y*); }
  }
  return s;
}

I missed a character disjunction to express things like (f,X*,x,'h'|'z',x,Y*). I don’t know if it is possible with Tom, if not we’ll have to look at it. The code is therefore somewhat long but it is ok to read.

Now let’s play :

polux@betty:~$ java Soundex "bill evans" "byle evannz"
true
polux@betty:~$ java Soundex "bill evans" "britney spears"
false

I hope so ! However, as indicated by the wikipedia, the algorithm is far from perfect :

polux@betty:~$ java Soundex "franz schubert" "frank zappa"
true

At least, it splits artists into bad and good ones

Bon, enfin, on arrive a avoir un dépot subversion qui fonctionne.

cvs2svn se plantait un peu sur les fichiers binaires, on a du refaire tous les imports en utilisant

cvs2svn --dump-only --keywords-off --no-default-eol ~/cvsroot

pour avoir un dépot correct

Donc maintenant, pour obtenir tom, on peut (et doit) faire:

svn co svn+ssh://login@scm.gforge.inria.fr/svn/tom/jtom/trunk jtom


Today we decided to switch tom from cvs to subversion.

The expected gain is the ability to easily move things around, and also use diff in disconnected mode.
As branchs are easy to use with subversion, i hope we will soon begin to use branches for our development

The switch was not as easy as we thought, to get a correct layout of the repository, but cvs2svn helped a lot.

The new repository should be available tonight !

During the ρ-calculus workshop in London, Clement and I wrote a proofchecker for Lemuridae (available in Tom cvs), our proof assistant for superdeduction. What is this about ? In many logical formalisms, proofs are mathematical objects represented by a tree :

A proof assistant is a program that helps to interactively build such trees (even if the tree representation isn’t always obvious for the user). Thus, checking a proof basically means checking that a tree is well-formed.
The smart idea behind proof checkers is that even if your proof assistant has been written by the worst programmer ever and is over bugged, the proof is still validated by a little piece of code in which you can trust. In particular, this principle is the keystone of the commonly trusted coq proof assistant.

Here comes Tom ! The deduction rules (nodes of the tree) we have to check have the following shape :

where Γ and Δ stand for a list of formulae, and A and B represent formulae. Lists and patterns ? This looks like a job for tom. The rule above is simply checked by the following pattern :

rule("implies L",
     (
       rule(_,_,sequent((g1*,g2*),(A,d*)),_), 
       rule(_,_,sequent((g1*,B,g2*),d),_)
     ),
     sequent((g1*,a,g2*),d),
     a@implies(A,B)  
    )

This is practically like reading the deduction rule ! The only difference is the last argument of rule which indicates the active formula. It is worth noticing the extensive use of non-linear and associative matching here. Given these patterns, our proof checker is 100 lines long and everybody can actually be conviced that it does what it is designed for. Compared to coq’s proof checker, which is 6568 lines long according to sloccount, and which looks like this :

(* since the head may be reducible, we might introduce lifts of 0 *)
let compact_stack head stk =
  let rec strip_rec depth = function
    | Zshift(k)::s -> strip_rec (depth+k) s
    | Zupdate(m)::s ->
      (* Be sure to create a new cell otherwise sharing would be
lost by the update operation *)
      let h' = lft_fconstr depth head in
      let _ = update m (h'.norm,h'.term) in
        strip_rec depth s
    | stk -> zshift depth stk in
       strip_rec 0 stk

this is really a big step forward in proof assistants trusting. (ok, construction calculus is far more complicated than sequent calculus but still, caml code for sequent calculus would look the same).

One issue remains : how can we trust tom’s generated code ? Easy answer : it has been certified … using Coq.

The build environment of tom now integrates the use of findbugs, to help spotting errors.

Yet, we are starting to fix the issues it shows.
The first ones were about an incorrect use of the Cloneable interface.

To me, this issue is weird: you should use "super.clone()" when defining the clone() method, instead of using "new", so that the class can be later extended. The problem is that I want the "clone()" method to be public, and not to throw "CloneNotSupportedException". Then, y have to "try{ } catch" this exception in the clone method, and send a RuntimeException in the catch part. But it will never happen, as I implement Cloneable.

Is Java's Cloneable interface simply poorly designed, or am I simply misusing it? Seems like Joshua Blosh favor the first solution.

Tom is a cool language which adds powerful (associative (on lists)) pattern matching and strategic programming to Java (as well as C and ocaml).

• You love functionnal programming but also digg on imperative languages ?
• You need the expressiveness of strategic programming on top of a J2EE, AJAX, web 2.0, [latest web techno] ?
• Your top notch [ocaml,haskell,scheme] application is cool, but …
• You’re looking for cool programming stuff like writing a one-liner sorting algorithm ?
• You like to experiment new ways of programming without learning a whole new language and abandon your libraries ?
• You need to write a DSL before tomorrow morning ?
• Your girlfriend dumped you and you wanna die except if you discover some wonderful new PL that will make you forget her for a couple of months ?

Tom was designed for you !

You can download it here, or install the eclipse plugin as explained here (compiler included) and start to practice the tutorial right now !

Voici mon environnement de travail

I will mainly use this blog to talk about Tom development, and uninteresting things.

toc toc toc... y-a-quelqu'un ?

findbugs (http://findbugs.sourceforge.net/) was integrated into tom's build system. It is not mandatory to install it for Tom development, ant it is necessary to install findbugs and set the "findbugs.home" property to use it. Currently, findbugs gives around 100 warnings. About 60% of them are probably false positives, but we should work on reducing the number of "real" problems

It is our great privilege and pleasure to announce the availability of Tom version 2.4. This release continues our work on the integration of pattern matching and rule based programming facilities into C and Java. Tom is a pattern matching compiler developed at INRIA. It is particularly well-suited for programming various transformations on trees/terms and XML based documents. Its design follows our research on the efficient compilation of rule based languages (e.g. ELAN, developed at INRIA-Loria). Many applications have been developed in Tom. Among them, let us mention: - the Tom compiler itself - languages semantics, interpreters and program transformation tools - a Just In Time strategy compiler using dynamic Java bytecode transformation - a generator of canonical abstract syntax trees (Gom) - a proof assistant for supernatural deduction - a compiler algorithm for anti-pattern matching and disunification Tom is a complex compiler which adds powerful constructs to C and Java: non linear syntactic matching, associative matching with neutral element (a.k.a. list-matching), XML based pattern matching, string matching, and equational rewriting. This offers the possibility to analyze and transform any kind of data-structure. Tom can be used for large scale developments and applications. It comes with documentation, programming, and debugging support. This new release contains many improvements and new features: - Anti-Patterns: Tom now supports not only pattern matching, but also anti-pattern matching. For example, the pattern (_*,!a(),_*) denotes a list which contains at least one element different from a(). In a similar way, !(_*,a(),_*) denotes a list which does not contain any a(). - Reflexive Strategies: A strategy is now a term that can be matched like any other term. This allows to dynamically build or transform a strategy at runtime. - Congruence Strategies: Gom generates new elementary congruence and constructions strategies. This allows for instance to define the Map operation in a easy way: map(s) = _conc(s) - Java Bytecode: A support for Java bytecode analysis and transformation is available in the runtime library. This allows class loading, bytecode analysis and transformation in an algebraic framework. Using the strategy language, the control flow graph can be explored and visualized using dot. - Eclipse Plugin: It is back for Eclipse version 3.2. It also supports Gom and all new functionalities. Tom is available, in open source (GPL/BSD License), from the web page: http://tom.loria.fr