From 1d760b1565a8d5a833e5fe6066afc69dcb28b0b0 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Tue, 3 May 2022 12:00:36 +0200
Subject: [PATCH] =?UTF-8?q?Ajout=20des=20types=20et=20des=20fonctions=20?=
 =?UTF-8?q?=C3=A0=20impl=C3=A9menter.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .gitignore |  2 ++
 main.ml    |  2 ++
 pieuvre.ml | 28 ++++++++++++++++++++++++++++
 struct.ml  |  0
 structs.ml | 16 ++++++++++++++++
 5 files changed, 48 insertions(+)
 delete mode 100644 struct.ml
 create mode 100644 structs.ml

diff --git a/.gitignore b/.gitignore
index 74d3949..93424b3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 _build
 pieuvre
 main.native
+
+*.kate-swp
diff --git a/main.ml b/main.ml
index e69de29..8ff999d 100644
--- a/main.ml
+++ b/main.ml
@@ -0,0 +1,2 @@
+open Struct
+open Pieuvre
diff --git a/pieuvre.ml b/pieuvre.ml
index e69de29..7b887dc 100644
--- a/pieuvre.ml
+++ b/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
+;;
diff --git a/struct.ml b/struct.ml
deleted file mode 100644
index e69de29..0000000
diff --git a/structs.ml b/structs.ml
new file mode 100644
index 0000000..5884272
--- /dev/null
+++ b/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;;