Ajout des types et des fonctions à implémenter.

.gitignore

@@ -1,3 +1,5 @@
 _build
 pieuvre
 main.native
+
+*.kate-swp

main.ml

@@ -0,0 +1,2 @@
+open Struct
+open Pieuvre

pieuvre.ml

@@ -0,0 +1,28 @@
+open Structs
+
+exception TODOException;;
+
+(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
+let affiche_lam (l: lam) : unit =
+    raise TODOException
+;;
+
+(* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
+let alpha (l1: lam) (l2: lam) : bool =
+    raise TODOException
+;;
+
+(* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
+let betastep (l: lam) : lam option =
+    raise TODOException
+;;
+
+(* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
+let reduce (l:lam) : unit =
+    raise TODOException
+;;
+
+(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
+let typecheck (env: gam) (l: lam) (t: ty) : bool =
+    raise TODOException
+;;

structs.ml

@@ -0,0 +1,16 @@
+(* Variables des λ-termes *)
+type var = string;;
+(* Variable des types simples *)
+type tvar = string;;
+
+(* Type complexe *)
+type ty = TSimple of tvar | TImpl of ty * ty | TFalse;;
+
+(* λ-terme *)
+type lam = LFun of var * ty * lam | LApp of lam * lam | LVar of var | LExf of lam * ty;;
+
+(* Environnement de typage *)
+type gam = (tvar * ty) list;;
+
+(* λ-terme avec des trous *)
+type lho = (lam list) -> lam;;