Modalités de rendu (non contractuelles)
=======================================

Groupe de News:                 epita.comp.ocaml
Sujet de mail Yaka              [CAML]
Date de rendu:                  jeudi 16 juin 2003 - 12:00:00
Nom de l'exécutable:            ovide
Modalités:                      Ce mini-projet est à faire en monôme
Compilateur:                    ocamlc 3.04
Tools:                          ocamllex ocamlyacc camlp4

Sujet
=====

Le but de ce projet est de faire en Caml un transformateur de formules, qui
aura pour nom «ovide».

1) La grammaire des formules

Les formules que vous devrez parser devront répondre à la grammaire suivante.

symbole  ::= [a-z]'_'[0-9]+
prédicat ::= [A-Z]+
variable ::= [a-z][0-9]+

terme	::= variable
	| symbole
	| symbole '(' terme {',' terme} ')'

atome	::= prédicat
	| prédicat '(' terme {',' terme} ')'

formule	::= '0' | '1'
	| atom
	| '!' formule
	| formule '|' formule
	| formule '&' formule
	| formule '->' formule
	| '[' variable ']' formule	(* Universel *)
	| '{' variable '}' formule	(* Existentiel *)
	| '(' formule ')'


Les opérateurs auront la précédence suivante:
-> aura la priorité minimum. Il sera associatif à gauche.
| viendra ensuite, puis &. Il seront également associatif à gauche.
Enfin, [], (), {} et ! auront la priorité la plus haute.


2) Les modules

Votre programme devra comprendre trois modules correspondant tous à la
signature suivante:

module type FORMULA_TRANSFORM =
sig
	(* type for the formula *)
	type t

	(* creates the formula from a channel *)
	val of_channel : in_channel -> t

        (* converts a formula to a string, for printing *)
	val to_string : t -> string

	(* do the transformation *)
	val transform : t -> t

        (* check whether the transformation has been done *)
	var is_complete : t -> bool
end

Elle contient un type, qui est le type de formule sur lequel on travaillera
(l'utilisation d'un type somme est ici fortement conseillée), une fonction
permettant d'écrire nos formules, une fonction opérant la transformation sur
les formules et une fonction vérifiant que la formule passée en paramètre est
bien de la forme d'une formule transformée.

Par exemple, pour la skolemisation, le type t sera le type d'une formule,
'to_string' écrira la formule, 'transform' effectuera la skolemisation, et
'is_complete' vérifiera si la formule est bien sous la forme skolem.

Les trois modules devront être:
	- Un module qui mettra une formule sous forme prénexe
	- un module qui mettra une formule sous forme normale conjonctive
	- Un module qui mettra une formule sous forme de skolem

3) Le programme

Le programme s'intitulera «ovide» et prendra une formule sur son entrée
standard, suivie d'une fin de fichier. Les différents éléments d'une formule
pouront être séparés par un ou plusieurs espaces, retours à la ligne (\n ou
\r), ou tabulations.

Le programme sans option effectuera la skolemisation d'une formule si elle
n'est pas déjà sous forme skolem, et ne fera rien sinon.

Le programme avec l'option -n mettra la formule sous forme normale conjonctive
si elle n'y est pas déjà, et ne fera rien sinon.

Le programme avec l'option -p mettra la formule sous forme prénexe si elle n'y
est pas déjà, et ne fera rien sinon.

Dans tout les cas, le programme écrira le résultat sur sa sortie standard,
avec la même grammaire que la grammaire d'entrée. Il adoptera d'autre part les
valeurs de sortie suivantes:
  - 0 s'il a effectué une transformation,
  - 1 s'il n'a pas effectué de transformation,
  - 2 si une erreur d'analyse lexicale ou syntaxique est survenue.

Dans un tel cas d'erreur, rien ne sera affiché sur la sortie standard. Le
message sur la sortie d'erreur est laissé à votre discrétion.


4) Points divers

Une grande partie de la note sera fondée sur l'évaluation de l'effort passé à
tirer parti des particularités de Caml. À noter que le procédural est
proscrit. L'utilisation des while/for/array/references... et autres structures
imperatives est donc interdit.

La tarball de rendu s'intitulera «login_x-ovide.tar.bz2». Elle contiendra le
répertoire 'login_x-ovide'. Tout fichier rendu devra se trouver dans ce
répertoire.

La compilation de votre programme devra s'effectuer avec gmake. L'executable
sera créé à la racine du répertoire de rendu. Nous vous conseillons d'utiliser
l'outil OcamlMakefile présenté dans les exercices.

L'évaluation se fera par l'analyse à rebours de la sortie standard de votre
programme. Nous vous conseillons donc d'apporter un soin particulier à faire
que la sortie de votre programme soit bien analysable, sans quoi vos résultats
de moulinette seraient gravement pénalisant.

5) Exemple

$ echo "A(a1) & A(b1)" | ./ovide -n
A(a1) & A(b1)
$ echo $?
1
$ echo -n "[a1] {b1} (P(a1) & Q(b1))" | ./ovide
[a1] (P(a1) & Q(f_1(a1)))
$ echo $?
0