====== Mini projet CHR ======

Ce projet a pour objectif de construire un moteur d'unification typée pour des termes de logique du premier ordre dans le langage CHR au dessus de Prolog.

Il est à rendre pour le 28 février 2015 par mail à [[emmanuel.coquery@univ-lyon1.fr]].

==== Ressources ====


On rappelle qu'il est possible d'utiliser l'interpréteur CHR en ligne disponible [[http://dtai.cs.kuleuven.be/CHR/webchr.shtml|ici]], ressources disponibles [[http://dtai.cs.kuleuven.be/CHR/|ici]].

[[http://www.doc.gold.ac.uk/~mas02gw/prolog_tutorial/prologpages/|Tutoriel Prolog]]



===== Termes et types =====


Les termes de logique, ainsi que les types, seront représentés par des termes Prolog manipulés en CHR.

Un terme sera représenté comme suit (selon sa sorte):
  * une variable: ''var(//nom//)'' où ''//nom//'' sera le nom de la variable;
  * une constante ''const(//nom//)'' où nom sera le nom de la constante;
  * un symbole de fonction appliqué à des termes ''fonct(//symb//,//liste//)'' où ''//liste//'' = ''[//t<sub>1</sub>//, ... ,//t<sub>n</sub>//]'' est la liste Prolog des termes passés en arguments au symbole de fonction ''//symb//''.

Un type sera;
  * soit ''t(//nom//)'' (types de primitifs de base, où ''//nom//'' peut être //e.g.// int, string, float, ...);
  * soit ''fleche(//liste//,//res//)'' où ''//liste//'' est une liste Prolog de types et ''//res//'' est un type.

Les types primitifs seront ceux des variables, des constantes et des termes, alors que les types flèche seront ceux des symboles de fonction (''//liste//'' est la liste des types des arguments et ''//res//'' est le type résultat)

<note important>Attention à ne pas confondre la notion de terme et de variable en Prolog (e.g. ''X'' est une variable en Prolog) avec les termes et les variables définis ci-dessus où la variable de logique //x// est représentée par ''var('x')''</note>
===== Unification simple =====

On commencera par implémenter l'[[http://en.wikipedia.org/wiki/Unification_%28computer_science%29#A_unification_algorithm|algorithme de Martelli et Montanari]] expliqué en cours.

On pourra utiliser les contraintes CHR suivantes:
  * ''unif/2'' représentera une équation entre deux termes.
  * ''unif_list/2'' représentera deux listes de termes à unifier. On générera une contrainte ''unif/2'' pour chaque paire de termes à unifier. Par exemple unif_list([t1,t2,t3],[t4,t5,t6]) se simplifiera en 3 contraintes ''unif(t1,t4)'', ''unif(t2,t5)'' et ''unif(t3,t6)''.
  * ''eliminate/2'' représentera une substitution à appliquer sur les équations courantes. Remarque: cette contrainte est utilisée pour le codage de la règle //eliminate// de l'algorithme. La substitution ne doit pas s'appliquer sur l'équation d'où elle provient (dans la règle, la substitution est appliquée sur G et pas sur x=t)

Voici, à titre d'exemple, le codage de deux règles: swap et delete
<code prolog>

% delete
% supprime une équation si elle demande d'unifier les mêmes termes logiques

unif(T,T) <=> true.

% swap
% T est un terme, var(Y) est une variable
% la garde T \= var(Z) impose que T ne soit pas unifiable en Prolog avec var(Z), 
% ce qui impose que T ne soit pas une variable logique

unif(T,var(Y)) <=> T \= var(Z) | unif(var(Y),T).

</code>

<note tip>
**Exemple**

La contrainte suivante:
<code prolog>
unif(funct (plus , [ var(x), funct(plus, [var(x), const(b)]) ] ),
     funct(plus, [ funct(plus, [const(a), var(y)]), var(z) ] ) )
</code>
doit se transformer en:
<code prolog>
unif(var(x), funct(plus, [const(a), var(y)]) ),
unif(var(z), funct(plus, [funct(plus, [const(a), var(y)]), const(b) ] ) )
</code>
</note>
===== Typage =====

Pour procéder au typage des termes, on se donne les contraintes CHR suivantes:
  * ''type_constante/2'': associe un type à une constante. On supposera que le type associé à une constante est un type primitif.
  * ''type_symb_fonction/2'': associe un type (fleche) à un symbole de fonction.
  * ''type/2'': associe un type primitif à un terme.
  * ''type_check/1'': demande à trouver et vérifier le type du terme logique passé en argument

Définir des règles CHR pour le typage en vous appuyant sur les remarques suivantes:
  * un même terme logique ne peut pas avoir deux types différents
  * si un terme est une constante, son type est donné par la contrainte CHR ''type_constante''
  * si un terme est une application d'un symbole de fonction //''f''// à des arguments ''//t1, ... , tn//'', son type peut être déduit du type de ''//f//''. De même, les types de ''//t1, ... , tn//'' sont imposés par le type de ''//f//''
  * si un terme est une variable, son type est imposé par son utilisation

<note tip>
**Exemple**
Les contraintes suivantes:
<code prolog>
type_constante(a, t(int)), type_constante(b, t(int)), 
type_symb_fonction(plus, fleche([t(int),t(int)],t(int))),
check( fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]) )
</code>
Doivent se transformer en
<code prolog>
% contraintes inchangées
type_constante(a, t(int)), type_constante(b, t(int)), 
type_symb_fonction(plus, fleche([t(int),t(int)],t(int))),
% nouvelles contraintes
type(fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]), t(int)),
type(fonct(plus, [ const(a), const(b) ] ), t(int)),
type(const(a), t(int)),
type(const(b), t(int))
</code>
</note>

<note tip>
**Exemple**
Les contraintes suivantes:
<code prolog>
type_constante(a, t(string)), type_constante(b, t(int)), 
type_symb_fonction(plus, fleche([t(int),t(int)],t(int))),
check( fonct(plus, [ const(a), const(b) ] ) )
</code>
Doivent se transformer en ''false''
</note>


<note tip>
**Exemple**
Les contraintes suivantes:
<code prolog>
type_constante(a, t(int)), 
type_symb_fonction(plus, fleche([t(int),t(int)],t(int))),
check( fonct(plus, [ fonct(plus, [ const(a), var(b) ] ), var(b) ]) )
</code>
Doivent se transformer en
<code prolog>
% contraintes inchangées
type_constante(a, t(int)), 
type_symb_fonction(plus, fleche([t(int),t(int)],t(int))),
% nouvelles contraintes
type(fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]), t(int)),
type(fonct(plus, [ const(a), const(b) ] ), t(int)),
type(const(a), t(int)),
type(var(b), t(int))
</code>
</note>


<note tip>
**Exemple**
Les contraintes suivantes:
<code prolog>
type_symb_fonction(concat, fleche([t(string),t(string)],t(string))),
type_symb_fonction(i2s, fleche([t(int)],t(string))),
check( fonct(concat, [ var(x), fonct(i2s, [var(x)]) ] ) )
</code>
Doivent se transformer en ''false''
</note>

===== Unification typée =====

Combiner les deux solveurs précédents pour qu'une unification qui rend égaux deux termes de types différents échoue.