New release of moca

New release of moca

[Pierre Weis]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 5018 bytes --]


             Relational types in Caml

I am pleased to announce the 0.3.0 version of Moca, a general construction
functions generator for relational types in Objective Caml.

In short:
=========
  Moca allows the high-level definition and automatic management of
complex invariants for data types; Moca also supports the automatic generation
of maximally shared values, independantly or in conjunction with the 
declared invariants.

Moca's home page is http://moca.inria.fr/
Moca's source files can be found at
       ftp://ftp.inria.fr/INRIA/caml-light/bazar-ocaml/moca-0.3.0.tgz

Moca is developped by Pierre Weis and Frédéric Blanqui.

In long:
========
  A relational type is a concrete type that declares invariants or relations
that are verified by its constructors. For each relational type definition,
Moca compiles a set of Caml construction functions that implements the declared
relations.

Moca supports two kinds of relations:
- algebraic relations (such as associativity or commutativity of a binary
  constructor),
- general rewrite rules that map some pattern of constructors and variables to
  some arbitrary user's define expression.

Algebraic relations are primitive, so that Moca ensures the correctness of
their treatment. By contrast, the general rewrite rules are under the
programmer's responsability, so that the desired properties must be verified by
a programmer's proof before compilation (including for completeness,
termination, and confluence of the resulting term rewriting system).

What's new in this release ?
============================
* mocac now compiles and installs under Windows + Cygwin,
* polymorphic data type definitions are fully supported,
* documentation has been completed,
* a paper has been published at ESOP'07: On the implementation of construction
  functions for non-free concrete data types.
  http://hal.inria.fr/docs/00/09/51/10/PS/main.ps
* keywords ``inverse'' and ``opposite'' have been made synonymous,
* addition of new algebraic invariants:
  - absorbing has been distinguished from absorbent,
  - unary distributive has been generalized with two operators.
* sharing has been generalized to polymorphic data type.
* non linear patterns are now accepted in user's defined rules.

An example
==========
The Moca compiler (named mocac) takes as input a file with extension .mlm that
contains the definition of a relational type (a type with ``private''
constructors, each constructor possibly decorated with a set of invariants or
algebraic relations).

For instance, consider peano.mlm, that defines the type peano with a binary
constructor Plus that is associative, treats the nullary constructor Zero as
its neutral element, and such that the rewrite rule Plus (Succ n, p) -> Succ
(Plus (n, p)) should be used whenever an instance of its left hand side appears
in a peano value:

     type peano = private
        | Zero
        | Succ of peano
        | Plus of peano * peano
        begin
          associative
          neutral (Zero)
          rule Plus (Succ n, p) -> Succ (Plus (n, p))
        end;;

>From this relational type definition, mocac will generate a regular Objective
Caml data type implementation, as a usual two files module.

>From peano.mlm, mocac produces the following peano.mli interface file:

     type peano = private
        | Zero
        | Succ of peano
        | Plus of peano * peano
     val plus : peano * peano -> peano
     val zero : peano
     val succ : peano -> peano

mocac also writes the following peano.ml file that implements this interface:

     type peano =
       | Zero
       | Succ of peano
       | Plus of peano * peano

     let rec plus z =
       match z with
       | Succ n, p -> succ (plus (n, p))
       | Zero, y -> y
       | x, Zero -> x
       | Plus (x, y), z -> plus (x, plus (y, z))
       | x, y -> insert_in_plus x y
     and insert_in_plus x u =
       match x, u with
       | _ -> Plus (x, u)
     and zero = Zero
     and succ x1 = Succ x1

To prove these construction functions to be correct, you would prove that
  - no Plus (Zero, x) nor Plus (x, Zero) can be a value in type peano,
  - for any x, y, z in peano. plus (plus (x, y), z) = plus (x, plus (y, z))
  - etc
  Hopefully, this is useless if mocac is correct: the construction functions
  respect all the declared invariants and relations.

To prove these construction functions to be incorrect, you would have to
  - find an example that violates the relations.
Hopefully, this is not possible (or please, report it!)

And, if you needed maximum sharing for peano values, you just have to compile
peano.mlm with the "--sharing" option of the mocac compiler:

$ mocac --sharing peano.mlm

would do the trick !

Conclusion:
===========
Moca is still evolving and a lot of proofs has still to be done about the
compiler and its algorithms.

Anyhow, we think Moca to be already usable and worth to give it a try.
Don't hesitate to send your constructive remarks and contributions !

Pierre Weis & Frédéric Blanqui.

Re: [Caml-list] New release of moca

[skaller]

On Fri, 2007-04-27 at 15:08 +0200, Pierre Weis wrote:
> Relational types in Caml
> 
> I am pleased to announce the 0.3.0 version of Moca, a general construction
> functions generator for relational types in Objective Caml.
> 
> In short:

It is quite nice!

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] New release of moca

[Jacques Carette]

Pierre Weis wrote:
>              Relational types in Caml
>   
Very nice indeed.  As a matter of fact, I was just reading (and 
enjoying) the ESOP paper in the plane yesterday!

My question is: why is this done as a pre-processor instead of as an 
extension of metaocaml?  Certainly some of the features of Moca can be 
implemented in metaocaml (I have done this myself for rings and 
monoids).  The added advantage of using metaocaml is, of course, the 
types.  As a (syntactic) pre-processor, getting good error messages out 
of Moca will be rather challenging, no?

Jacques

PS: Genuine question, not criticism.

Re: [Caml-list] New release of moca

[skaller]

On Sun, 2007-04-29 at 10:09 -0400, Jacques Carette wrote:
> Pierre Weis wrote:
> >              Relational types in Caml
> >   
> Very nice indeed.  As a matter of fact, I was just reading (and 
> enjoying) the ESOP paper in the plane yesterday!
> 
> My question is: why is this done as a pre-processor instead of as an 
> extension of metaocaml?  

So that ordinary Ocaml users have access to it?

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] New release of moca

[Jacques Carette]

skaller wrote:
>> My question is: why is this done as a pre-processor instead of as an 
>> extension of metaocaml?  
>>     
>
> So that ordinary Ocaml users have access to it

Sorry, my feeling is that, by now, the meta-programming core of 
metaocaml is stable enough to be merged into Objective Caml.  I guess I 
should have stated that.

To maintain Objective Caml's competitiveness with GHC, which has 
Template Haskell, this seems to be an obvious thing to do -- especially 
since I personally consider metaocaml to be superior to TH.

Jacques

New release of moca

[Pierre Weis]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 5349 bytes --]


             Relational types in Caml

We are pleased to announce the 0.5.0 version of Moca, a general construction
functions generator for relational types in Objective Caml.

In short:
=========
  Moca allows the high-level definition and automatic management of
complex invariants for data types; Moca also supports the automatic generation
of maximally shared values, independantly or in conjunction with the 
declared invariants.

Moca's home page is http://moca.inria.fr/
Moca's source files can be found at
       ftp://ftp.inria.fr/INRIA/caml-light/bazar-ocaml/moca-0.5.0.tgz

Moca is developped by Pierre Weis and Frédéric Blanqui, Richard Bonichon and
Laura Lowenthal (see the file AUTHORS in the main directory of the
distribution).

In long:
========

  A relational type is a concrete type that declares invariants or relations
that are verified by its constructors. For each relational type definition,
Moca compiles a set of Caml construction functions that implements the
declared relations.

Moca supports two kinds of relations:
- algebraic relations (such as associativity or commutativity of a binary
  constructor),
- general rewrite rules that map some pattern of constructors and variables to
  some arbitrary user's defined expression.

Algebraic relations are primitive, so that Moca ensures the correctness of
their treatment. By contrast, the general rewrite rules are under the
programmer's responsability, so that the desired properties must be verified
by a programmer's proof before compilation (including for completeness,
termination, and confluence of the resulting term rewriting system).

What's new in this release ?
============================

* Lot of work on the documentation: a research paper has been published to
  described the framework at ESOP'07, talks about relational types and the
  internal of the compiler are included in the distribution.

* An automatic test generation facility has been developped to test the
  specifications written in Moca.

* Arbitrary Caml code can be written in the .mlm files (any sequence of Caml
  signature items are allowed as extra algebraic properties of
  generators). This ``external'' code is included as is in the resulting module.

* Commutativity relation gets an extra argument which gives the order used to sort
  the combs (or lists in case of a vary-adic generator).

* Source code of the compiler has been documented.

* No more shell scripts: the compiler is entirely written in Caml.

* User's defined rules have been generalized from pattern -> pattern
  to pattern -> expr.

An example
==========

The Moca compiler (named mocac) takes as input a file with extension .mlm
that contains the definition of a relational type (a type with ``private''
constructors, each constructor possibly decorated with a set of invariants or
algebraic relations).

For instance, consider peano.mlm, that defines the type peano with a binary
constructor Plus that is associative, treats the nullary constructor Zero as
its neutral element, and such that the rewrite rule Plus (Succ n, p) -> Succ
(Plus (n, p)) should be used whenever an instance of its left hand side
appears in a peano value:

     type peano = private
        | Zero
        | Succ of peano
        | Plus of peano * peano
        begin
          associative
          neutral (Zero)
          rule Plus (Succ n, p) -> Succ (Plus (n, p))
        end;;

>From this relational type definition, mocac will generate a regular Objective
Caml data type implementation, as a usual two files module.

>From peano.mlm, mocac produces the following peano.mli interface file:

     type peano = private
        | Zero
        | Succ of peano
        | Plus of peano * peano
     val plus : peano * peano -> peano
     val zero : peano
     val succ : peano -> peano

mocac also writes the following peano.ml file that implements this interface:

     type peano =
       | Zero
       | Succ of peano
       | Plus of peano * peano

     let rec plus z =
       match z with
       | Succ n, p -> succ (plus (n, p))
       | Zero, y -> y
       | x, Zero -> x
       | Plus (x, y), z -> plus (x, plus (y, z))
       | x, y -> insert_in_plus x y
     and insert_in_plus x u =
       match x, u with
       | _ -> Plus (x, u)
     and zero = Zero
     and succ x1 = Succ x1

To prove these construction functions to be correct, you would prove that
  - no Plus (Zero, x) nor Plus (x, Zero) can be a value in type peano,
  - for any x, y, z in peano. plus (plus (x, y), z) = plus (x, plus (y, z))
  - etc
  Hopefully, this is useless if mocac is correct: the construction functions
  respect all the declared invariants and relations.

To prove these construction functions to be incorrect, you would have to
  - find an example that violates the relations.
Hopefully, this is not possible (or please, report it!)

And, if you needed maximum sharing for peano values, you just have to compile
peano.mlm with the "--sharing" option of the mocac compiler:

$ mocac --sharing peano.mlm

would do the trick !

Conclusion:
===========
Moca is still evolving and a lot of proofs has still to be done about the
compiler and its algorithms.

Anyhow, we think Moca to be already usable and worth to give it a try.
Don't hesitate to send your constructive remarks and contributions !

Pierre Weis & Frédéric Blanqui.