From 15afcecabe72d66ea52c5a6a8adacb8ede7572cb Mon Sep 17 00:00:00 2001
From: Adrien Vannson <adrien.vannson@protonmail.com>
Date: Sun, 8 May 2022 18:10:08 +0200
Subject: [PATCH] Correction d'un bug

---
 pieuvre.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/pieuvre.ml b/pieuvre.ml
index 55d8dca..56aeb13 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -8,7 +8,7 @@ exception IllegalVarNameException of var
 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)
+        | TImpl(t1,t2) -> "(" ^ (string_of_ty t1) ^ " -> " ^ (string_of_ty t2) ^ ")"
         | TFalse -> "⊥"
 ;;
 
@@ -27,7 +27,7 @@ let split, tsplit =
             let xStr = matched_group 1 x in
             let xInt = matched_group 2 x in
             (xStr, int_of_string xInt)
-        
+
     else raise (IllegalVarNameException(x))
     in (splitter varRegex, splitter tvarRegex);;
 
@@ -62,7 +62,7 @@ let findTFreeName (t: ty) (x: tvar) =
 
 (* Renvoie l[s/x] *)
 let rec replace (l: lam) (x: var) (s: lam) = match l with
-    | LFun(v,t,l') -> 
+    | LFun(v,t,l') ->
         if(v=x)
         then let y=findFreeName l' v in
             LFun(v,t,replace l' v (LVar(y)))
@@ -71,12 +71,12 @@ let rec replace (l: lam) (x: var) (s: lam) = match l with
     | 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 rec alpha (l1: lam) (l2: lam) : bool =
     match (l1,l2) with
-        | (LFun(v1,t1,l1'),LFun(v2,t2,l2')) -> 
+        | (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
@@ -90,14 +90,14 @@ let rec alpha (l1: lam) (l2: lam) : bool =
 (* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
 let rec betastep (l: lam) : lam option = match l with
     | LFun(v,t,l') -> betastep l'
-    | LApp(lf,lx) -> 
+    | LApp(lf,lx) ->
         begin
         match (betastep lf) with
         | Some lf' -> Some (LApp(lf',lx))
         | None ->
             match (betastep lx) with
             | Some lx' -> Some (LApp(lf, lx'))
-            | None -> 
+            | None ->
                 match lf with
                 | LFun(x,_,corps) -> Some (replace corps x lx)
                 | _ -> None (* On ne peut pas β-réduire *)
@@ -120,17 +120,17 @@ let rec typecheck (env: gam) (l: lam) (t: ty) : bool =
     match (l,t) with
     | (LFun(x,t,l'),TImpl(tx,ty)) -> typecheck ((x,tx)::env) l' ty
     | (LFun(_,_,_),_) -> false (* Une fonction est forcément une ... fonction *)
-    | (LApp(lf,lx),t) -> 
+    | (LApp(lf,lx),t) ->
         let t' = (raise TODOException; TFalse) in
         (typecheck env lf (TImpl(t',t))) && (typecheck env lx t')
-    | (LVar(x),t) -> 
+    | (LVar(x),t) ->
         begin
         match env with
         | (y,t')::env' -> if x=y then t=t'
             else typecheck env' l t
         | [] -> raise TODOException
         end
-    | (LExf(l',t'),t) -> 
+    | (LExf(l',t'),t) ->
         if t=t'
         then typecheck env l' t
         else false (* Le ex falso a le mauvais type *)