The Pieuvre™ Proof Assistant
============================

Ne vous êtes jamais vous dit que votre quotidien était morose ? Que tout ce que vous pourriez prouver dans votre vie ne serait que vain ? C'est que vous avez besoin du réconfort de Pieuvre™ !

Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, que vous êtes effrayés par l'incurable finitude de votre esprit, l'ineffable efficacité de Pieuvre™ saura vous réconforter en vous assurant des preuves complètes et sans accroc.

Bien plus efficace que d'autres gallinacés, l'interface CLI de Pieuvre™ saura convenir à petits et grands. Son design entre post-modernisme et romantisme baroque néo-mérovingien rappellera aux utilisateur·ices les plus avertis les plus grandes heures de l'humanité.

Allez, tous à vos pieuvres !

*L'équipe de Pieuvre™ n'est pas responsable des dommages occasionnés par les réalisations philosophiques causées aux utilisateur·ices de par l'utilisation du programme*

# Utilisation
`Pieuvre` génère automatiquement un fichier `log.8pus` contenant la preuve venant d'être faite. Attention, le fichier `log.8pus` ne doit jamais être donné en entrée de Pieuvre™ !

## Option `typecheck`
L'option `typecheck` vérifie si un lambda-terme est bien typé. Elle s'utilise de la manière suivante :
```
./pieuvre -typecheck tests/typecheck/right-type
./pieuvre -typecheck tests/typecheck/wrong-type
```

## Option `alpha`
L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :
```
./pieuvre -alpha tests/lambda-terms/alpha-eq.lams
./pieuvre -alpha tests/lambda-terms/alpha-not-eq.lams
```

## Option `reduce`
L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :
```
./pieuvre -reduce tests/lambda-terms/lambda.lam
```

## Notes d'implémentation

- Les λ-termes à trous sont représentés par leurs fonctions de remplissage. À la liste des λ-termes à mettre dans les trous, on associe le λ-terme complété.

### Découpage des fichiers

- `lexer.mll` et `parser.mly` sont les fichiers pour le parser `ocamlyacc`
- `main.ml` contient le code gérant la ligne de commande, la construction du lambda-terme en appelant les fonctions de `pieuvre.ml`
- `pieuvre.ml` contient toutes les fonctions de manipulation de λ-termes.
- `structs.ml` contient l'ensemble des structures de données : λ-terme, environnements, types
- `tactic.ml` contient la structure de définition des tactiques.

## Répartition du travail

### Adrien
- Interface interactive (avec le parsage des formules, des tactiques, ...), lecture des fichiers
- Construction d'un lambda-terme à partir de la preuve (sans et / ou )
- Tactiques élémentaires (`intro`, `intros`, `assumption`, `apply`, `elim`)
- Options `alpha`, `reduce`, `typecheck`, ... : partie interactive appelant les fonctions écrites par Samy
- Écriture de tests (irréfutabilité du tiers exclus, de la formule de Peirce, ...)

### Samy
- Introduction du README
- Fonctions de manipulation des λ-termes (`pieuvre.ml`)
- Typecheck
- Erreurs lors des tactiques.
- `\/` et `/\`
- Parsing des λ-termes
- `True` et `exact`
- Option `-computetype`
- Écriture de tests