From 4bfe9e9e6e1ef6f26f955422e7250063809c17f4 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Fri, 6 May 2022 01:29:00 +0200
Subject: [PATCH] =?UTF-8?q?Ajout=20du=20code=20de=20pieuvre=20qui=20manipu?=
 =?UTF-8?q?le=20les=20=CE=BB-expressions.}?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 pieuvre.ml | 77 +++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 62 insertions(+), 15 deletions(-)

diff --git a/pieuvre.ml b/pieuvre.ml
index ff3b1cb..55d8dca 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -20,15 +20,16 @@ let rec string_of_lam (l: lam) : string = match l with
     | 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)
+let split, tsplit =
+    let splitter regex x =
+    if string_match regex 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))
-;;
+    in (splitter varRegex, splitter tvarRegex);;
 
 (* Renvoie un nom non utilisé dans la formule l qui commence par x *)
 let findFreeName (l: lam) (x: var) =
@@ -43,8 +44,20 @@ let findFreeName (l: lam) (x: var) =
     in
     finder l;
     xStr ^ (string_of_int (!maxi+1))
-    
-        
+;;
+
+(* Renvoie un nom de type simple non utilisé dans le type t qui commence par x *)
+let findTFreeName (t: ty) (x: tvar) =
+    let xStr = fst (tsplit x) in
+    let maxi = ref 0 in
+    let rec finder t = match t with
+        | TImpl(t1, t2) -> (finder t1;finder t2)
+        | TSimple(y) -> let (yS,yI) = split y in
+            if xStr=yS then maxi := max !maxi yI
+        | TFalse -> () (* Le faux ne réserve pas de variables *)
+    in
+    finder t;
+    xStr ^ (string_of_int (!maxi+1))
 ;;
 
 (* Renvoie l[s/x] *)
@@ -75,16 +88,50 @@ let rec alpha (l1: lam) (l2: lam) : bool =
 ;;
 
 (* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
-let betastep (l: lam) : lam option =
-    raise TODOException
+let rec betastep (l: lam) : lam option = match l with
+    | LFun(v,t,l') -> betastep l'
+    | 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 -> 
+                match lf with
+                | LFun(x,_,corps) -> Some (replace corps x lx)
+                | _ -> None (* On ne peut pas β-réduire *)
+        end
+    | LVar(x) -> None
+    | LExf(l',_) -> betastep l'
 ;;
 
 (* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
-let reduce (l:lam) : unit =
-    raise TODOException
+let rec reduce (l:lam) : unit =
+    print_string (string_of_lam l);
+    print_newline ();
+    match (betastep l) with
+    | Some l' -> reduce l'
+    | None -> ()
 ;;
 
 (* 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
+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) -> 
+        let t' = (raise TODOException; TFalse) in
+        (typecheck env lf (TImpl(t',t))) && (typecheck env lx 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) -> 
+        if t=t'
+        then typecheck env l' t
+        else false (* Le ex falso a le mauvais type *)
 ;;