Ajout du typecheck des preuves finales.

main.ml

@@ -9,12 +9,12 @@ let filename = ref "" in
 
 let reduce = ref false in
 let alpha = ref false in
-let typecheck = ref false in
+let typecheck_option = ref false in
 
 Arg.parse
     [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
      ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
-     ("-typecheck", Arg.Set typecheck, "Check if a lambda term has a given type")]
+     ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")]
     (fun s -> filename := s)
     "The available options are:";
 
@@ -121,4 +121,17 @@ while !subgoals <> [] do
         )
 done;
 
-Printf.printf "Final proof :\n%s\n" (string_of_lam (!fill_holes []));;
+let finalLam = !fill_holes [] in
+    if (typecheck [] finalLam ty)
+    then 
+        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
+    else
+    (
+        Printf.printf "Invalid proof constructed !\n";
+        Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
+        Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
+    )
+;;
+    
+
+

pieuvre.ml

@@ -1,6 +1,7 @@
 open Structs
 open Str
 
+
 exception TODOException;;
 exception IllegalVarNameException of var
 
@@ -115,23 +116,31 @@ let rec reduce (l:lam) : unit =
     | None -> ()
 ;;
 
-(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
+(* Calcule le type du λ-terme l sous l'environnement env. 7
-let rec typecheck (env: gam) (l: lam) (t: ty) : bool =
+Renvoie None si la formule n'est pas typable ou si la formule n'est pas close (sous d'environnement)*)
-    match (l,t) with
+let rec computeType (env: gam) (l: lam) : ty option =
-    | (LFun(x,t,l'),TImpl(tx,ty)) -> typecheck ((x,tx)::env) l' ty
+    match l with
-    | (LFun(_,_,_),_) -> false (* Une fonction est forcément une ... fonction *)
+    | LFun(x,tx,l') -> Option.bind (computeType ((x,tx)::env) l') (fun ty -> Some (TImpl(tx,ty)))
-    | (LApp(lf,lx),t) ->
+    | LApp(lf,lx) ->
-        let t' = raise TODOException in
+        let tx = computeType env lx in
-        (typecheck env lf (TImpl(t',t))) && (typecheck env lx t')
+        let tf = computeType env lf in
-    | (LVar(x),t) ->
+        begin
+            match tf with
+            | Some TImpl(tx',ty') -> if Some tx'=tx then Some ty' else None
+            | _ -> None (* Si none, l'argument n'est pas typable, si Some _, on ne peut typer l'application *)
+        end
+    | LVar(x) ->
         begin
         match env with
-        | (y,t')::env' -> if x=y then t=t'
+        | (y,ty)::env' -> if x=y then Some ty
-            else typecheck env' l t
+            else computeType env' l
-        | [] -> raise TODOException
+        | [] -> None
         end
-    | (LExf(l',t'),t) ->
+    | LExf(l',t) ->
-        if t=t'
+        if (computeType env l')=Some t
-        then typecheck env l' t
+        then Some t
-        else false (* Le ex falso a le mauvais type *)
+        else None (* Le ex falso a le mauvais type *)
 ;;
+
+(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
+let typecheck (env: gam) (l: lam) (t: ty) : bool = (computeType env l = Some t);