Masquotte de Caml Moca: un générateur de modules pour les types à relations

Version 0.7.0

Où trouver le logiciel ?

Les sources de moca sont ici.

La documentation des sources se trouve ici.

Comment l'installer ?

Voir le fichier install dans le répertoire source.
Pour Windows : voir le fichier install.win dans le répertoire source.

De quoi s'agit-il ?

Moca est un générateur de modules pour les types de données relationnels.

Un type de données relationnel est un type de données concret dont les valeurs vérifient des relations qui sont déclarées lors de la définition du type.

Pour chaque définition de type relationnel, moca compile un ensemble de fonctions de construction qui implémente les relations déclarées en ne construisant que les valeurs vérifiant ces relations.

Moca permet ainsi la définition et le traitement automatique d'invariants complexes des structures de données.

De surcroît, moca est capable de générer des fonctions de constructions qui produisent des valeurs maximalement partagées.

Les relations de Moca

Moca admet deux espèces de relations:

Les relations algébriques sont primitives en moca et leur traitement est donc correct (sauf erreur à signaler d'urgence). Au contraire, les règles de réécriture générales sont sous la responsabilité pleine et entière du programmeur; en conséquence les propriétés attendues des règles doivent être soigneusement étudiées (ou mieux prouvées) avant la compilation (en particulier la terminaison, la complétude et la confluence du système de réécriture engendré).

Les invariants algébriques sont spécifiés à l'aide de mot-clés dénotant des théories équationnelles comme la commutativité et l'associativité. Les fonctions de construction générées par moca permettent alors de représenter chaque classe d'équivalence par une unique valeur, son représentant canonique.

Principe

Le compilateur mocac lit un fichier source .mlm (ou .mlms) et produit un module objective caml (fichier d'interface + fichier d'implementation).
Un fichier .mlm(s) est semblable à un fichier d'interface .mli habituel: il doit définir un type (privé), avec la possibilité supplémentaire de déclarer les relations algébriques qui sont associées aux constructeurs.
Mocac génère alors les fonctions de constructions pour les constructeurs, de telle sorte que les relations sont effectivement vérifiées pour toutes les valeurs du type défini.

Les définitions de type de moca ont exactement la même syntaxe que celles d'objective caml en dehors des annotations supplémentaires pour déclarer les relations algébriques associées aux constructeurs définis dans le type. Ces annotations apparaissent entre les mots clés begin et end dans le code de la définition de type.

Pour obtenir un partage maximal des données construites par les fonctions de construction, il suffit d'utiliser l'option spéciale --sharing du compilateur mocac.
Cette option est automatiquement utilisé lorsqu'un fichier .mlms est donné en argument.

Comment s'en servir ?

Il suffit d'écrire la définition d'un type à relations dans un fichier source avec l'extension .mlm (ou l'extension .mlms si vous désirez obtenir le partage maximal des valeurs construites).
Appelez ensuite mocac avec pour argument votre fichier source pour créer un module qui implémente le type à relations.
Sous windows : appeler sh mocac avec pour argument votre fichier .mlm(s).

Exemples

Voici une définition pour un type de données qui représente les valeurs d'un groupe additif. Le groupe comporte une opération binaire Add, un élément neutre Zero, un opérateur unaire pour l'opposé Opp, et un générateur One:

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

Les propriétés algébriques des opérateurs du groupe sont ici toutes portées par l'opération binaire Add. Les mots clés associative, commutative, neutral et opposite sont spécifiques à moca et confèrent les propriétés habituelles correspondantes au constructeur Add (plus exactement aux valeurs construites avec la fonction de construction de Add).

Si l'on suppose que le code précédent se trouve dans le fichier group.mlm, alors la commande

$ mocac group.mlm

génère le module Group sous la forme des deux fichiers group.mli et group.ml.

Le fichier d'interface du module Group, group.mli, déclare le type privé t qui est le support des valeurs du groupe et déclare la signature de toutes les fonctions de construction associées aux constructeurs de t:

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
;;


Le fichier d'implémentation du module Group, group.ml, définit le type t et les fonctions de construction correspondantes. Son contenu est équivalent à:

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"
;;


Les valeurs du type t sont maintenant toutes correctement construites par les fonctions de construction, donc normalisées selon les règles des groupes (autrement dit, il n'existe pas de valeur du type t qui ne soit pas normalisée). Par exemple:

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

Le répertoire examples de la distribution contient de nombreux autres exemples de structures de données traitées par moca.

Syntaxe

Moca étend la syntaxe des définitions de type de caml de la manière suivante:

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

Sémantique

Nous donnons la théorie équationnelle qui correspond à chaque mot-clé et les propriétés des représentants des classes d'équivalence générés par moca. Les spécifications détaillées de chacun des constructeurs algébriques sont disponible dans la documentation des sources.

Dans toute la suite, on suppose qu'on définit le type à relations t et que C est l'un des constructeurs de t dont la fonction de construction associée est c. Plus généralement, les identificateurs D, E et A, lorsqu'ils apparaissent dans les définitions, sont des constructeurs du type t dont les fonctions de construction respectives sont d, e et a.

Commutative

Si le constructeur C est déclaré commutative (compare), alors
pour tout x, y du type t,
c (x, y) = c (y, x)
pour tout x, y du type t,
si C (x, y) appartient au type t alors compare x y < 0.
Note: compare est le nom d'une fonction de comparaison donnée par l'utilisateur dans la définition du type t, au sein d'une définition de valeur (une définition Caml comprise entre les mots clés begin et end). La fonction compare doit être un ordre total pour les termes du type t. Si elle n'est pas définie avec le type à relation, la fonction compare vaut Pervasives.compare.
Si le constructeur C est déclaré commutative, alors
C est en fait déclaré commutative (Pervasives.compare).

Associative

Si le constructeur C est déclaré associative, alors
pour tout x, y, z du type t,
c (c (x, y), z) = c (x, c (y, z))
pour tout x, y, z du type t, C (C (x, y), z) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (C (x, y), z).)

Involutive

Si le constructeur C est déclaré involutive, alors
pour tout x du type t
c (c (x)) = x
pour tout x du type t, C (C (x)) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (C (x)).)

Idempotent

Si le constructeur C est déclaré idempotent, alors
C est déclaré à la fois idempotent left et idempotent right .
Si le constructeur C est déclaré idempotent left, alors
pour tout x, y du type t,
c (x, c (x, y)) = c (x, y)
pour tout x, y du type t, C (x, C (x, y)) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, C (x, y)).)
Si le constructeur C est déclaré idempotent right, alors
pour tout x, y du type t,
c (c (x, y), y) = c (x, y)
pour tout x, y du type t, C (C (x, y), y) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (C (x, y), y)).)

Neutral

Si le constructeur C est déclaré neutral (D), alors
C est déclaré à la fois neutral left (D) et neutral right (D).
Si le constructeur C est déclaré neutral left (D), alors
pour tout x du type t,
c (d, x) = x
pour tout x du type t, C (D, x) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (D, x).)
Si le constructeur C est déclaré neutral right (D), alors
pour tout x du type t,
c (x, d) = x
pour tout x du type t, C (x, D) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, D).)

Nilpotent

Si le constructeur C est déclaré nilpotent (A), alors
C est déclaré à la fois nilpotent left (A) et nilpotent right (A).
Si le constructeur C est déclaré nilpotent left(A), alors
pour tout x, y du type t,
c (x, c (x, y)) = a
pour tout x du type t, C (x, C (x, y) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, C (x, y)).)

Inverse

Si le constructeur C est déclaré inverse (I, E), alors
C est déclaré à la fois inverse left (I, E) et inverse right (I, E).
Si le constructeur C est déclaré inverse left (I, E), alors
pour tout x, y du type t,
c (i (x), x) = e
pour tout x du type t, C (I (x), x) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (I (x), x).)
Si le constructeur C est déclaré inverse right (I, E), alors
pour tout x du type t, c (x, i (x)) = e
pour tout x du type t, C (x, I (x)) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, I (x)).)
Si le constructeur C est déclaré neutral [side] (E), alors
la déclaration inverse [side'] (I) est équivalente à inverse [side'] (I, E).
Si le constructeur C est déclaré inverse [side](i, e) et absorbent[side'](A), alors
la fonction de construction associée à C lève l'exception Failure "Division by Absorbent" quand un des arguments est A.

Distributive

Si le constructeur C est déclaré distributive (D, E), alors
le constructeur C est déclaré à la fois distributive left (D, E), distributive right (D, E).
Si le constructeur C est déclaré distributive (D), alors
le constructeur C est déclaré distributive (D, D).
Si le constructeur C est déclaré distributive left (D, E), alors
pour tout x, y, z du type t,
c (d (x, y), z) = e (c (x, z), c (y, z))
pour tout x, y, z du type t, C (D (x, y), z) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (D (x, y), z).)
Si le constructeur C est déclaré distributive right (D, E), alors
pour tout x, y, z du type t, c (z, d (x, y)) = e (c (z, x), c (z, y))
pour tout x, y, z du type t, C (z, D (x, y)) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (z, D (x, y)).)
Si le constructeur C est déclaré distributive inverse left (D, E), alors
pour tout x, y, z du type t, c (d (x, y), z) = e (c (y, z), c (x, z))
pour tout x, y, z du type t, C (D (x, y), z) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (D (x, y), z).)

Absorbent

Si le constructeur C est déclaré absorbent (A), alors
le constructeur C est déclaré absorbent left (A) et absorbent right (A) .
Si le constructeur C est déclaré absorbent left (A), alors
pour tout x du type t, c (a, x) = a
pour tout x du type t, C (A, x) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (A, x).)
Si le constructeur C est déclaré absorbent right (A), alors
pour tout x du type t, c (x, a) = a
pour tout x du type t, C (x, A) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, A).)

Absorbing

Si le constructeur C est déclaré absorbing (D), alors
C est déclaré absorbing left (D), et absorbing right (D) .
Si le constructeur C est déclaré absorbing left (D), alors
pour tout x, y du type t, c (d (x, y), y) = y
pour tout x, y du type t, C (D (x, y), y) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (D (x, y), y).)
Si le constructeur C est déclaré absorbing right (D), alors
pour tout x, y du type t, c (x, d (x, y)) = x
pour tout x, y du type t, C (x, D (x, y)) n'est pas élément du type t.
(Autrement dit: aucune valeur du type t n'est filtrée par le filtre C (x, D (x, y)).)

Rule

Si le constructeur C est déclaré rule l -> r, alors
pour toute valeur x du type t qui est filtrée par le filtre l (i.e. il existe une substitution sigma des variables libres de l telle que sigma (l) = x), on a
c (x) = r où les variables liées dans l qui apparaissent dans r sont substituées aux sous-termes correspondants de x (i.e. c (x) = sigma (r)).
pour toute valeur x du type t qui est filtrée par le filtre l, C (x) n'est pas élément de t.
Cette annotation définit une règle de l'utilisateur. Elle est fournie pour les utilisateurs experts seulement quand les annotations prédéfinies sont insuffisantes.

Aide à la complétion

Lors de l'utilisation de la complétion (expérimentale) dans Moca, certains paramètres peuvent être spécifiés dans le code source par les mots-clés suivants:

Si le constructeur C est déclaré completion status s, alors
le générateur C aura le statut s, c'est-à-dire lexicographique (pour le statut lexicographic) ou multi-ensemble (pour le statut multiset), pour l'ordre RPO (ordre récursif des chemins ou Recursive Path Ordering) pendant la complétion.
Si le constructeur C est déclaré completion precedence i, alors
C sera représenté par l'entier i dans l'ordre sur les entiers qui induira l'ordre de précédence sur les symboles pendant la complétion.

Bibliographie

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

Cliquez ici pour voir les transparents des présentations sur Moca.

Contact

La première version de Moca a été développée dans le cadre de l'arc quotient (pour plus d'information, voir le site de l'ARC).

Moca est actuellement développé par Frédéric Blanqui, Richard Bonichon, and Pierre Weis.

Si vous voulez contacter les implémenteurs, écrivez à Pierre Weis ou Frédéric Blanqui, ou Richard Bonichon (Richard dot Bonichon at gmail.com).

Fichier créé le 11 avril 2005.


Dernière modification le lundi 4 juin 2012.
Copyright © 2005 - 2012 INRIA, tous droits réservés.