diff --git a/README.md b/README.md index 61dd5b1..52c1c9e 100644 --- a/README.md +++ b/README.md @@ -34,6 +34,18 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ./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` les fichiers pour le parser `ocamlyacc` +- `main.ml` contient le code gérant la ligne de commande, le prompt et l'appel à la librairie. +- `pieuvre.ml` contient toutes les fonctions de manipulation de λ-termes. +- `structs.ml` contient l'ensemble des structures de données, genre λ-terme, environnements, types. +- `tactic.ml` contient la structure de définition des tactiques. + ## Répartition du travail ### Adrien