Caml masquotte Mocac : a module generator for relational types

Version 0.7.0

Where is it ?

Moca's source files are here.

The generated source documentation is available from here.

How to install it?

See the INSTALL file in the source directory.
For Windows: see the INSTALL.win file in the source directory.

What is it ?

Moca is a general construction functions generator for Caml data types with invariants.

Moca allows the high-level definition and automatic management of complex invariants for data types. In addition, Moca provides the automatic generation of maximally shared values, independantly or in conjunction with the declared invariants.

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

Moca supports two kinds of relations:

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).

Algebraic invariants are specified by using keywords denoting equational theories like commutativity and associativity. Moca generates construction functions that allow each equivalence class to be uniquely represented by their canonical value.

How does it work ?

The mocac compiler parses a special .mlm or .mlms file and produces a regular Caml module (i.e. a pair of an interface file and an implementation file).
The .mlm(s) file is similar to a Caml .mli file: it must declare a (private) data type with the possible addition of special annotations to specify the relations that the constructors verify.
Then the mocac compiler generates construction functions for the constructors, such that all the specified relations indeed hold for the values of the type defined.

Type definitions for Moca have the same syntax as those for Objective Caml with the addition of the invariants and/or algebraic relations associated to the constructors defined in the type.

As an additional benefit, you can obtain maximal sharing between the values built by the construction functions, if you use the special --sharing option of the mocac compiler.
This option is also automatically activated with a .mlms file input.

How can one use it ?

Simply call mocac with your .mlm(s) file as argument.
For Windows: call sh mocac with your .mlm(s) file as argument.

Examples

Here is the suitable definition for the data type representing the values of an additive group with one binary operation Add, a neutral element Zero, an opposite unary operator Opp, and a generator One:

type t = private
   | Zero
   | One
   | Opp of t
   | Add of t * t
     begin
       associative
       commutative
       neutral (Zero)
       opposite (Opp)
     end
;;

The algebraic properties of all the operators of the group operators are simply specified for the Add operation. The keywords associative, commutative, neutral, and opposite are Moca specific and set the expected properties of the constructor Add.

If we suppose this code to be in the file group.mlm, then the call mocac group.mlm generates the module Group as the two files group.mli and group.ml.

The interface file group.mli declares the t private type that is the support for the values of the group, and declares the signature of the construction functions for the constructors. It contains the following declarations:

type t = private
   | Zero
   | One
   | Opp of t
   | Add of t * t
   (* begin
        associative
        commutative
        neutral (Zero)
        inverse (Opp)
      end *)
;;
val zero : t
;;

val one : t
;;

val opp : t -> t
;;

val add : t * t -> t
;;

val eq_t : t -> t -> bool
;;


Now the file group.ml defines the type t and the corresponding construction functions. It is equivalent to:

type t =
   | Zero
   | One
   | Opp of t
   | Add of t * t
   (* begin
        associative
        commutative
        neutral (Zero)
        inverse (Opp)
      end *)
;;
let rec compare_add moca_x moca_y =
  match (moca_x, moca_y) with
  | (Opp moca_x, Opp moca_y) -> compare_add moca_x moca_y
  | (Opp moca_x, moca_y) -> compare_add moca_x moca_y
  | (moca_x, Opp moca_y) -> compare_add moca_x moca_y
  | (moca_x, moca_y) -> Pervasives.compare moca_x moca_y

and add moca_z =
  match moca_z with
  | (moca_x, Zero) -> moca_x
  | (Zero, moca_x) -> moca_x
  | (moca_x, Opp moca_y) when Pervasives.compare moca_x moca_y = 0 -> zero
  | (Opp moca_x, moca_y) when Pervasives.compare moca_x moca_y = 0 -> zero
  | (moca_x, Add ((Opp moca_y), moca_z))
      when
      Pervasives.compare moca_x moca_y = 0 ->
    moca_z
  | (Opp moca_x, Add (moca_y, moca_z))
      when
      Pervasives.compare moca_x moca_y = 0 ->
    moca_z
  | (Add (moca_x, moca_y), moca_z) -> add (moca_x, (add (moca_y, moca_z)))
  | (moca_x, Add (moca_y, moca_z)) ->
    if compare_add moca_x moca_y > 0
    then add (moca_y, (add (moca_x, moca_z)))
    else Add (moca_x, (Add (moca_y, moca_z)))
  | (moca_x, moca_y) when compare_add moca_x moca_y > 0 ->
    add (moca_y, moca_x)
  | (moca_x, moca_y) -> Add (moca_x, moca_y)

and zero = Zero

and one = One

and opp moca_x =
  match moca_x with
  | Opp moca_x -> moca_x
  | Add (moca_x1, moca_x2) -> add ((opp moca_x2), (opp moca_x1))
  | Zero -> zero
  | _ -> Opp moca_x
;;

external eq_t : t -> t -> bool = "%equal"
;;


All the values of the type t are now normalized with respect to the group's rules (put it another way: there is no value of type t that is not normalized). For instance:

# add (one, add (zero, opp one));;
- : t = Zero

The directory examples in the distribution contains many other examples of data structures with their corresponding modules generated by mocac.

Syntax

Moca extends the Caml syntax for type definitions as follows:

constr-decl ::= constr-name [ annotation ]
| constr-name of typeexpr [ annotation ]
annotation ::= begin { relation | completion_hint }+ end
side ::= left
| right
invopp ::= inverse
| opposite
rpo_status ::= lexicographic
| multiset
completion_hint ::= completion precedence int
| completion status rpo_status
relation ::= commutative [ ( comp ) ]
| associative
| involutive
| idempotent [side]
| nilpotent [side]
| neutral [side] ( constr-name )
| absorbent [side] ( constr-name )
| absorbing [side] ( constr-name )
| distributive [invopp] [side] ( constr-name [,constr-name] )
| rule pattern -> expression
| completion completion_hint

Semantics

This section briefly describes the equational theory corresponding to every keyword and the properties of representatives generated by Moca. More detailed specifications for each algebraic relation is available from the source documentation .

Commutative

commutative
behaves like commutative (Pervasives.compare).
If C is commutative (comp),
then C (x, y) = C (y, x) and, for every value matching C (x, y), we have comp x y < 0.
comp is the identifier of a comparison function given by the user.
It must be a total order on the terms for the defined types.

Associative

If C is associative,
then C (C (x, y), z) = C (x, C (y, z)) and no value matches C (C (x, y), z).

Involutive

If C is involutive,
then C (C (x)) = x and no value matches C (C (x)).

Idempotent

idempotent
is the conjunction of idempotent left and idempotent right.
If C is idempotent left,
then C (x, C (x, y)) = C (x, y) and no value matches C (x, C (x, y)).
If C is idempotent right,
then C (C (x, y), y) = C (x, y) and no value matches C (C (x, y), y).

Neutral

neutral (D),
is the conjunction of neutral left (D) and neutral right (D).
If C is neutral left (D),
then C (D, x) = x and no value matches C (D, x).
If C is neutral right (D),
then C (x, D) = x and no value matches C (x, D).

Nilpotent

nilpotent(A)
is the conjunction of nilpotent left (A) and nilpotent right (A).
If C is nilpotent left (A),
then C (x, C (x, y)) = (A) and no value matches C (x, C (x, y)).
If C is nilpotent right (A),
then C (C (x, y), y) = (A) and no value matches C (C (x, y), y).

Inverse

inverse (I, E)
is the conjunction of inverse left (I, E) and inverse right (I, E).
If C is inverse left (I, E),
then C (I (x), x) = E and no value matches C (I (x), x).
If C is inverse right (I, E),
then C (x, I (x)) = E and no value matches C (x, I (x)).
If C is neutral [side] (E),
then inverse [side'] (I) is equivalent to inverse [side'] (I, E).
If C is inverse [side] (I, E) and absorbent [side'] (A),
then the construction function associated to C raises the exception (Failure "Division by Absorbent") when one of its arguments is A.

Distributive

distributive (D, E)
is the conjunction of distributive left (D, E) and distributive right (D, E).
distributive (D)
is the same as distributive (D, D)
If C is distributive left (D, E),
then C (D (x, y), z) = E (C (x, z), C (y, z)) and no value matches C (D (x, y), z).
If C is distributive right (D, E),
then C (z, D (x, y)) = E (C (z, x), C (z, y)) and no value matches C (z, D (x, y)).
If C is distributive inverse left (D, E),
then C (D (x, y), z) = E (C (y, z), C (x, z)) and no value matches C (D (x, y), z).

Absorbent

absorbent (A)
is the conjunction of absorbent left (A) and absorbent right (A).
If C is absorbent left (A),
then C (A, x) = A and no value matches C (A, x).
If C is absorbent right (A),
then C (x, A) = A and no value matches C (x, A).

Absorbing

absorbing (D)
is the conjunction of absorbing left (D) and absorbing right (D).
If C is absorbing left (D),
then C (D (x, y), y) = y and no value matches C (D (x, y), y).
If C is absorbing right (D),
then C (x, D (x, y)) = x and no value matches C (x, D (x, y)).
If C has rule l -> r,
then C (l) = r and no value matches C (l).
This annotation is provided for expert user, and should only be used when the previous predefined annotations are not sufficient. In the generated code, the constructors in r are replaced by calls to the corresponding construction functions; the simplifications induced by user's rules are applied first and as much as possible. When there is a user's defined rule annotation in the type specification, the code generated by Moca is not guaranteed to be correct or even to terminate anymore.

Completion hints

If trying out the experimental completion feature of Moca, some parameters may be specified using the following keywords in the source code:

If C has completion status s,
then the generator c will have status s, i.e. lexicographic (lex) or multiset (mul), for the RPO order during completion.
If C has completion precedence i,
then the integer i will represent C in the order on the integers which will induce a precedence on generator symbols.

Bibliography

On the implementation of construction functions for non-free concrete data types, F. Blanqui, T. Hardin and P. Weis, ESOP'07.
Download: [ps], [pdf], [dvi].

Go there to see the slides of Moca talks.

Contact

The first version of Moca has been developped by the ARC Quotient (more information on Quotient is given here).
Moca is currently developped by Frédéric Blanqui, Richard Bonichon, and Pierre Weis.

If you want to get in touch with implementors, contact Pierre Weis, Frédéric Blanqui, or Richard Bonichon (Richard dot Bonichon at gmail.com).

This file was created on the 11th of April 2005.


Last modification date: Monday, June 4th, 2012.
Copyright © 2005 - 2012 INRIA, all rights reserved.