From 19a4354c66b386f0dfe40022f552729b87e60206 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Tue, 3 May 2022 15:13:58 +0200
Subject: [PATCH] =?UTF-8?q?Ajout=20de=20l'=CE=B1-conversion=20et=20des=20f?=
 =?UTF-8?q?onctions=20d'affichage=20des=20=CE=BB-termes=20et=20des=20types?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Makefile   |  2 +-
 main.ml    |  4 +++-
 pieuvre.ml | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++----
 structs.ml | 13 ++++++++--
 4 files changed, 81 insertions(+), 8 deletions(-)

diff --git a/Makefile b/Makefile
index d7c8313..cc44640 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 all: pieuvre
 
 pieuvre: *.ml *.mll *.mly
-	ocamlbuild -yaccflag -v -lib unix main.native
+	ocamlbuild -yaccflag -v -lib unix -lib str main.native
 	ln -f -s main.native pieuvre
 	chmod +x pieuvre
 
diff --git a/main.ml b/main.ml
index 8ff999d..02fd18b 100644
--- a/main.ml
+++ b/main.ml
@@ -1,2 +1,4 @@
-open Struct
+open Structs
 open Pieuvre
+
+let _ = print_string (string_of_ty (TImpl(TSimple("A"),TFalse)));;
diff --git a/pieuvre.ml b/pieuvre.ml
index 7b887dc..ff3b1cb 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -1,15 +1,77 @@
 open Structs
+open Str
 
 exception TODOException;;
+exception IllegalVarNameException of var
 
 (* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
-let affiche_lam (l: lam) : unit =
-    raise TODOException
+let rec string_of_ty (t: ty) : string =
+    match t with
+        | TSimple(tn) -> tn
+        | TImpl(t1,t2) -> (string_of_ty t1) ^ " -> " ^ (string_of_ty t2)
+        | TFalse -> "⊥"
 ;;
 
+(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
+let rec string_of_lam (l: lam) : string = match l with
+    | LFun(v,t,l') -> "λ"^v^":"^(string_of_ty t)^" . "^(string_of_lam l')
+    | LApp(l1, l2) -> (string_of_lam l1)^" "^(string_of_lam l2)
+    | LVar(v) -> v
+    | LExf(l',t) -> "exf("^(string_of_lam l')^" : "^(string_of_ty t)^")"
+;;
+
+let split (x:var) : string * int =
+    if string_match varRegex x 0
+    then
+        let xStr = matched_group 1 x in
+        let xInt = matched_group 2 x in
+        (xStr, int_of_string xInt)
+        
+    else raise (IllegalVarNameException(x))
+;;
+
+(* Renvoie un nom non utilisé dans la formule l qui commence par x *)
+let findFreeName (l: lam) (x: var) =
+    let xStr = fst (split x) in
+    let maxi = ref 0 in
+    let rec finder l = match l with
+        | LFun(v,t,l') -> (finder (LVar(v));finder l')
+        | LApp(l1, l2) -> (finder l1;finder l2)
+        | LVar(v) -> let (vS,vI) = split v in
+            if xStr=vS then maxi := max !maxi vI
+        | LExf(l',t) -> finder l'
+    in
+    finder l;
+    xStr ^ (string_of_int (!maxi+1))
+    
+        
+;;
+
+(* Renvoie l[s/x] *)
+let rec replace (l: lam) (x: var) (s: lam) = match l with
+    | LFun(v,t,l') -> 
+        if(v=x)
+        then let y=findFreeName l' v in
+            LFun(v,t,replace l' v (LVar(y)))
+            (* Pas besoin replace les x, ils ont tous été déjà remplacés *)
+        else LFun(v,t,replace l' x s)
+    | LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s)
+    | LVar(v) -> if v=x then s else LVar(v)
+    | LExf(l',t) -> LExf(replace l' x s, t)
+;;    
+
 (* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
-let alpha (l1: lam) (l2: lam) : bool =
-    raise TODOException
+let rec alpha (l1: lam) (l2: lam) : bool =
+    match (l1,l2) with
+        | (LFun(v1,t1,l1'),LFun(v2,t2,l2')) -> 
+            (t1 = t2) &&
+            (* On trouve un nom libre dans les deux sous-termes *)
+            let v' = findFreeName (LApp(l1', l2')) v1 in
+            alpha (replace l1 v1 (LVar(v'))) (replace l2 v2 (LVar(v')))
+        | (LApp(lf1,lx1),LApp(lf2,lx2)) -> (alpha lf1 lf2) && (alpha lx1 lx2)
+        | (LVar(x1),LVar(x2)) -> x1 = x2
+        | (LExf(l1', t1),LExf(l2', t2)) -> t1=t2 && (alpha l1' l2')
+        | _ -> false (* Les deux formules n'ont pas la même structure *)
 ;;
 
 (* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
diff --git a/structs.ml b/structs.ml
index 5884272..687b131 100644
--- a/structs.ml
+++ b/structs.ml
@@ -1,13 +1,22 @@
 (* Variables des λ-termes *)
 type var = string;;
+let varRegex = Str.regexp "^([a-z]+)([0-9]*)$";;
 (* Variable des types simples *)
 type tvar = string;;
+let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)$";;
 
 (* Type complexe *)
-type ty = TSimple of tvar | TImpl of ty * ty | TFalse;;
+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;;
+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;;