20111219:OCaml:MiniProj:Quadrologic

Un article de WikiProg.

Le rendu est ouvert à l'adresse [1] et ce jusqu'au lundi 9 janvier 2012 à 23h42.

Introduction

Ce mini-projet est à réaliser seul et en OCaml. Les règles de rendu, le format de l'archive et son contenu seront décrits avec le pallier 0.

L'objectif est de réaliser un petit interpréteur pour des expressions utilisant une logique quadri-valuée (logique à quatre valeurs.) Le petit langage dispose de constantes globales et de fonctions pures. L'analyse lexico-syntaxique est fournie, ainsi que la description de l'arbre de syntaxe abstraite.

Logique quadri-valuée

Comme son nom l'indique la logique quadri-valuée travaille avec quatre valeurs au lieu de deux. Ces valeurs correspondent au treillis de Gallois utilisé pour l'interprétation abstraite des expressions booléennes, elle corresponde également à ce qu'on appelle la logique de Belnap (mais ne vous embêtez pas avec ça … )

Les quatre valeurs sont:

• none
• true
• false
• both

Elle reflète l'idée qu'une variable booléenne peut avoir une valeur inconnue (none), vraie (true), fausse (false) ou les deux (both). L'évaluation des expressions logiques (tables de véritée) devient donc:

MAJ (2011-12-20) Légère correction, maintenant la matrice est bien symétrique

Les autres opérateurs (équivalence = et implication =>) garde leur sémantique usuelle:

Le langage

Les différents éléments de notre langage sont:

• Des expressions logiques avec les opérateurs vues précédemment, des constantes (identifiant commençant par une lettre minuscule), des appels de fonctions ou l'une des quatre valeurs et enfin les parenthèses.
• Des définitions de fonctions et de constantes sous la forme:
  • fun nom(x1, ..., xn) = expression ; pour les fonctions
  • def x = expression ; pour les constantes
• Une expression principale (qui donne le résultat final) délimité par les mots clefs begin et end

Comme dans la plus part des langages les espaces et les sauts de lignes sont des séparateurs et leur nombre n'a pas d'importance. Les commentaires sont marqués par un # et s'étendent jusqu'à la fin de la ligne.

Voici un petit exemple de programme complet:

# Un exemple

# une fonction
fun f(x,y) =
  x => y;     # on peut fair un peu de mise en forme


def a = true;
def b = none;

fun g(z) = z = z;

def c = both;

# L'expression principale
begin
  f(a,b) & g(c)
end

La sémantique des expressions suit la descriptions de la section précédente. Les définitions (fonctions et constantes) obéisse aux règles suivantes:

• le corps d'une fonction ne contient comme symbole que les noms des paramètres de la fonction, aucune constante
• les noms de fonctions (et de constantes sauf pour les corps des fonctions) peuvent être utilisées après leur définition
• il ne peut y avoir deux entités (fonctions ou constantes) portant le même nom.

Dans l'expression principale tous les symboles sont définis (ils le sont avant) et donc utilisable. De plus, toutes les constantes non définies explicitement sont considérées comme existantes et fixées à la valeur none.

Vous n'aurez pas à gérer les erreurs, les programmes soumis à votre projet respecteront toujours les règles.

Rendu

Code founi

L'archive media:base-mpoc2011.tar.bz2 contient les fichiers du parser/lexer et la description de l'AST.

Le module Ast n'a qu'un fichier d'interface ast.mli, c'est normal, il n'y a qu'une définition de type et aucun code, il n'est donc pas nécessaire d'avoir un fichier ast.ml.

Utiliser le parser vous pouvez vous inspirez de bloc de code suivant:

let main () =
  (* Appel du parser *)
  let tree = Parser.main Lexer.token (Lexing.from_channel stdin) in
  begin
    (* tree est notre AST, c'est ici que le travail commence *)
  end
 
let _ = main ()

Pour compiler les fichiers du parser (parser.mly) et du lexer (lexer.mll) il faut faire appel à ocamlyacc et ocamllex pour produire les fichier OCaml correspondant. Vous pouvez vous inspirez du bout de Makefile suivant:

MAJ(2011-12-20) Attention petite modification ligne 11, il faut remplacer mli par .mli, le fichier media:base-mpoc2011.tar.bz2 est à jour.

Mais vous pouvez aussi utiliser ocamlbuild, qui est beaucoup plus simple, il faut quand même un Makefile pour respecter le sujet, mais beaucoup plus simple:

Et voila …

Niveau 0 (2 points)

Le niveau 0 correspond à un rendu correct et dans les temps. Votre rendu respectera les règles suivantes:

• L'archive aura pour nom login-mpoc2011_quadro.tar.bz2 (suffixe de rendu mpoc2011_quadro)
• L'archive se décompressera dans le répertoire: login-mpoc2011_quadro
• Le répertoire login-mpoc2011_quadro devra contenir au moins les fichiers suivants:
  • AUTHORS (au format habituel)
  • ast.mli, lexer.mll, parser.mly (fournis)
  • Makefile
  • vos fichiers

L'évaluation du niveau est la suivante:

• Si l'archive ou le répertoire ne sont pas correct: aucun point et arrêt de l'évaluation
• Si Makefile manquant: aucun point et arrêt de l'évaluation
• Si make ne produit pas un binaire quadro dans le répertoire courant: aucun point et arrêt de l'évaluation
• Si AUTHORS ou fichiers fournis manquant: aucun point (mais l'évaluation continue.)

Attention, les fichiers fournis doivent être rendu en l'état, ils seront remplacés par leur version originale si ce n'est pas le cas et considérés comme absents.

En outre, pour que la suite soit possible, il faut que votre Makefile fournisse les règles suivantes:

• clean (nettoyage total)
• all, quadro et la règle par défaut (sans paramètre): production du binaire (natif) quadro correspondant au programme de votre projet.

Le binaire quadro acceptera des programmes de notre langage sur l'entrée standard. Sans paramètre, il effectuera un pretty-print de son entrée (niveau 1) et avec l'option -exec il évaluera le programme (niveaux suivants.) Tout autre option provoquera l'affichage de l'aide sur la sortie d'erreur (stderr) et un arrêt du programme (sans résultat donc.)

Niveau 1 (4 points)

L'objectif de ce niveau est de vous familiariser avec l'AST produit par mon parser.

Dans ce niveau vous devrez réécrire (pretty-print) le contenu du programme passé en entrée au même format. La sortie de votre programme doit être un programme valide sémantiquement identique (la mise en forme peut changer), seul les commentaires seront perdus.

Pour accéder à ce niveau, on lancera votre programme sans paramètre et le contenu à afficher sera lu sur l'entrée standard. Un moyen de vérifier votre niveau (au moins en partie) est de s'assurer que le résultat reste le même après plusieurs appel en cascade, par exemple:

shell> cat cat ex-sujet.qlo
# Un exemple

# une fonction
fun f(x,y) =
  x => y;     # on peut fair un peu de mise en forme


def a = true;
def b = none;

fun g(z) = z = z;

def c = both;

# L'expression principale
begin
  f(a,b) & g(c)
end
shell> ./quadro < ex-sujet.qlo > sortie1.qlo
shell> ./quadro < ex-sujet.qlo | ./quadro > sortie2.qlo
shell> diff sortie1.qlo sortie2.qlo
shell>

Normalement, la dernière ligne (diff) ne devrait rien afficher.

Évaluation

Pour les niveaux suivants (2, 3 et 4), votre programme devra (lorsque l'on lui passe l'option -exec) évaluer les expressions passées sur son entrée standard et afficher les résultats directement. Le statut d'exécution (paramètre de la fonction exit) de votre programme devra obligatoirement être 0.

Le résultat ne peut être que l'une des quatre valeurs de la logique: none, true, false et both.

shell>./quadro -exec
begin
  none
end^D
none
shell> ./quadro -exec < programme.qlo
none

dans l'exemple précédent, ^D correspond à la combinaison de touche control et D pour mettre fin à l'entrée standard.

Niveau 2 (4 points)

Dans ce niveau nous nous limiterons à l'évaluation de programme ne contenant qu'une expression principale et ni fonction, ni constantes.

shell> cat niveau2.qlo
begin
  (true | both) = true
end
shell> ./quadro < niveau2.qlo
true
shell>

Niveau 3 (5 points)

Dans ce niveau on ajoute la gestion de constantes (définies ou non).

shell> cat niveau3.qlo
def a = true;
def c = true;
begin
  (a | b) = c
end
shell> ./quadro < niveau3.qlo
true
shell>

b n'est pas défini et vaut donc none

Niveau 4 (5 points)

Dans ce niveau vous gérerez toutes les possibilités du langage (constantes et fonctions.)

On rappelle que dans les fonctions, seuls les noms de paramètres sont définis, les noms de constantes (définis ou non) ne sont pas acceptées (les tests seront toujours corrects de ce point de vue là.)

shell> cat niveau4.qlo
fun f(x,y) = x => y;
def a = true;
fun g(a) = f(a,a);
begin
  g(a)
end
shell> ./quadro -exec < niveau4.qlo
true
shell>

Conseils et autres

Où l'on reparle de correction automatique

Ce projet sera corrigé de manière complètement automatique, ce qui implique que:

• Un projet ne respectant pas les règles (répertoire, format … ), ne compilant pas ou ne respectant pas les spécifications demandées (affichages, options … ) ne vaudra pas plus de 2 ou 0.
• Les affichages non demandé sont considérés comme des erreurs
• Si votre programme ne rencontre pas d'erreur en cours d'exécution, il termine avec le statut 0 (exit 0), et bien sûr une valeur différente de 0 dans le cas contraire.
• La propreté et la mise en forme du code n'ont aucune importance
• Les exécutions de votre binaire par la moulinette se feront en temps limité (de 15 à 180 secondes en fonction des situations) par conséquent un programme (beaucoup) trop lent sera considéré comme un programme planté ou en boucle infinie.
• il n'y a pas d'intervention manuelle dans la correction, à aucun moment et sous aucune forme.
• la moulinette est juste et impartiale
• la moulinette ne se trompe pas (ou alors pour tout le monde et ce sera corrigé avant publication.)

À titre d'information, voici ce comment les tests pourraient commencer sur une archive de l'étudiant login_x:

tar xjf login_x-mpoc2011_quadro.tar.bz2 login_x-mpoc2011_quadro
cd login_x-mpoc2011_quadro
make clean
make || make quadro
...

Modules pratiques

Parmi les modules que je vous conseille, il y a:

• Hashtbl (les tables de hashage)
• Map (un peu pareil mais en fonctionnel basé sur des AVL)
• Arg (gestion des options, de l'affichage de l'aide … très pratique)
• Printf ou Format (affichage, le second est plus intelligent mais plus dure à prendre en main.)

Autres références sur le sujet

Il existe quelques liens plus ou moins facile à trouver sur les logiques à quatre valeurs. J'ai opté pour la sémantique de Belnap qui semble la plus répandue. Si vous chercher les tables de vérité de cette logique, j'ai pris comme référence l'article disponible à ici[2] (dispo en pdf gratuit.)

Il y a également un page sur le sujet sur wikipedia (en anglais) mais attention, j'ai vu au moins quelques erreurs dans les tables de vérité (pour la négation.) Je n'ai pas vérifier dans le détail, donc faites attention.