From 195139e05827bd90f89aa73bf854f6fba76fb08b Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 20 Nov 2023 04:43:27 +0100
Subject: [PATCH 01/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 134 ++++++++++++++---------------
 1 file changed, 66 insertions(+), 68 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index b1b324f..df5a494 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -5,98 +5,96 @@ open HopixAST
 (** Error messages *)
 
 let invalid_instantiation pos given expected =
-  HopixTypes.type_error pos (
-      Printf.sprintf
-        "Invalid number of types in instantiation: \
-         %d given while %d were expected." given expected
-    )
+  HopixTypes.type_error
+    pos
+    (Printf.sprintf
+       "Invalid number of types in instantiation: %d given while %d were expected."
+       given
+       expected)
+;;
 
 let check_equal_types pos ~expected ~given =
   if expected <> given
   then
-    HopixTypes.(type_error pos
-                  Printf.(sprintf
-                            "Type mismatch.\nExpected:\n  %s\nGiven:\n  %s"
-                            (string_of_aty expected)
-                            (string_of_aty given)))
+    HopixTypes.(
+      type_error
+        pos
+        Printf.(
+          sprintf
+            "Type mismatch.\nExpected:\n  %s\nGiven:\n  %s"
+            (string_of_aty expected)
+            (string_of_aty given)))
+;;
 
 (** Linearity-checking code for patterns *)
-
 let rec check_pattern_linearity
-        : identifier list -> pattern Position.located -> identifier list
-  = fun vars Position.{ value; position; } ->
-  failwith "Students! This is your job!"
+  : identifier list -> pattern Position.located -> identifier list
+  =
+  fun vars Position.{ value; position } -> failwith "Students! This is your job!"
+;;
 
 (** Type-checking code *)
 
-let check_type_scheme :
-      HopixTypes.typing_environment ->
-      Position.t ->
-      HopixAST.type_scheme ->
-      HopixTypes.aty_scheme * HopixTypes.typing_environment
-  = fun env pos (ForallTy (ts, ty)) ->
-  failwith "Students! This is your job!"
+let check_type_scheme
+  :  HopixTypes.typing_environment -> Position.t -> HopixAST.type_scheme
+  -> HopixTypes.aty_scheme * HopixTypes.typing_environment
+  =
+  fun env pos (ForallTy (ts, ty)) -> failwith "Students! This is your job!"
+;;
 
 let synth_literal : HopixAST.literal -> HopixTypes.aty =
-  fun l ->
+  fun l -> failwith "Students! This is your job!"
+;;
+
+let rec check_pattern
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located -> HopixTypes.aty
+  -> HopixTypes.typing_environment
+  =
+  fun env Position.({ value = p; position = pos } as pat) expected ->
   failwith "Students! This is your job!"
 
-let rec check_pattern :
-          HopixTypes.typing_environment ->
-          HopixAST.pattern Position.located ->
-          HopixTypes.aty ->
-          HopixTypes.typing_environment
-  = fun env Position.({ value = p; position = pos; } as pat) expected ->
+and synth_pattern
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun env Position.{ value = p; position = pos } -> failwith "Students! This is your job!"
+;;
+
+let rec synth_expression
+  :  HopixTypes.typing_environment -> HopixAST.expression Position.located
+  -> HopixTypes.aty
+  =
+  fun env Position.{ value = e; position = pos } -> failwith "Students! This is your job!"
+
+and check_expression
+  :  HopixTypes.typing_environment -> HopixAST.expression Position.located
+  -> HopixTypes.aty -> unit
+  =
+  fun env (Position.{ value = e; position = pos } as exp) expected ->
   failwith "Students! This is your job!"
 
-and synth_pattern :
-      HopixTypes.typing_environment ->
-      HopixAST.pattern Position.located ->
-      HopixTypes.aty * HopixTypes.typing_environment
-  = fun env Position.{ value = p; position = pos; } ->
-  failwith "Students! This is your job!"
-
-let rec synth_expression :
-      HopixTypes.typing_environment ->
-      HopixAST.expression Position.located ->
-      HopixTypes.aty
-  = fun env Position.{ value = e; position = pos; } ->
-  failwith "Students! This is your job!"
-
-and check_expression :
-      HopixTypes.typing_environment ->
-      HopixAST.expression Position.located ->
-      HopixTypes.aty ->
-      unit
-  = fun env (Position.{ value = e; position = pos; } as exp) expected ->
-  failwith "Students! This is your job!"
-
-and check_value_definition :
-      HopixTypes.typing_environment ->
-      HopixAST.value_definition ->
-      HopixTypes.typing_environment
-  = fun env def ->
-  failwith "Students! This is your job!"
+and check_value_definition
+  :  HopixTypes.typing_environment -> HopixAST.value_definition
+  -> HopixTypes.typing_environment
+  =
+  fun env def -> failwith "Students! This is your job!"
+;;
 
 let check_definition env = function
-  | DefineValue vdef ->
-     check_value_definition env vdef
-
+  | DefineValue vdef -> check_value_definition env vdef
   | DefineType (t, ts, tdef) ->
-     let ts = List.map Position.value ts in
-     HopixTypes.bind_type_definition (Position.value t) ts tdef env
-
+    let ts = List.map Position.value ts in
+    HopixTypes.bind_type_definition (Position.value t) ts tdef env
   | DeclareExtern (x, tys) ->
-     let tys, _ = Position.located_pos (check_type_scheme env) tys in
-     HopixTypes.bind_value (Position.value x) tys env
+    let tys, _ = Position.located_pos (check_type_scheme env) tys in
+    HopixTypes.bind_value (Position.value x) tys env
+;;
 
 let typecheck env program =
-  List.fold_left
-    (fun env d -> Position.located (check_definition env) d)
-    env program
+  List.fold_left (fun env d -> Position.located (check_definition env) d) env program
+;;
 
 type typing_environment = HopixTypes.typing_environment
 
 let initial_typing_environment = HopixTypes.initial_typing_environment
-
 let print_typing_environment = HopixTypes.string_of_typing_environment

From da6e4547a85ff8dbf4847d65d809a3d2176db9fb Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 20 Nov 2023 04:54:40 +0100
Subject: [PATCH 02/58] debug

---
 flap/src/hopix/hopixTypechecker.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index df5a494..31b7489 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -30,7 +30,8 @@ let check_equal_types pos ~expected ~given =
 let rec check_pattern_linearity
   : identifier list -> pattern Position.located -> identifier list
   =
-  fun vars Position.{ value; position } -> failwith "Students! This is your job!"
+  fun vars Position.{ value; position } ->
+  failwith "Students! This is your job! (check_pattern_linearity)"
 ;;
 
 (** Type-checking code *)
@@ -39,11 +40,12 @@ let check_type_scheme
   :  HopixTypes.typing_environment -> Position.t -> HopixAST.type_scheme
   -> HopixTypes.aty_scheme * HopixTypes.typing_environment
   =
-  fun env pos (ForallTy (ts, ty)) -> failwith "Students! This is your job!"
+  fun env pos (ForallTy (ts, ty)) ->
+  failwith "Students! This is your job! (check_type_scheme)"
 ;;
 
 let synth_literal : HopixAST.literal -> HopixTypes.aty =
-  fun l -> failwith "Students! This is your job!"
+  fun l -> failwith "Students! This is your job! (synth_literal)"
 ;;
 
 let rec check_pattern
@@ -51,33 +53,35 @@ let rec check_pattern
   -> HopixTypes.typing_environment
   =
   fun env Position.({ value = p; position = pos } as pat) expected ->
-  failwith "Students! This is your job!"
+  failwith "Students! This is your job! (check_pattern)"
 
 and synth_pattern
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun env Position.{ value = p; position = pos } -> failwith "Students! This is your job!"
+  fun env Position.{ value = p; position = pos } ->
+  failwith "Students! This is your job! (synth_pattern)"
 ;;
 
 let rec synth_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty
   =
-  fun env Position.{ value = e; position = pos } -> failwith "Students! This is your job!"
+  fun env Position.{ value = e; position = pos } ->
+  failwith "Students! This is your job! (synth_expression)"
 
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
   =
   fun env (Position.{ value = e; position = pos } as exp) expected ->
-  failwith "Students! This is your job!"
+  failwith "Students! This is your job! (check_expression)"
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
   -> HopixTypes.typing_environment
   =
-  fun env def -> failwith "Students! This is your job!"
+  fun env def -> failwith "Students! This is your job! (check_value_definition)"
 ;;
 
 let check_definition env = function

From e091ae9860bf50fd8915e5534429815aea61201b Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 21 Nov 2023 17:17:43 +0100
Subject: [PATCH 03/58] =?UTF-8?q?coup=C3=A9=20en=202?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 flap/src/hopix/hopixTypechecker.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 31b7489..4d53376 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -81,7 +81,11 @@ and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
   -> HopixTypes.typing_environment
   =
-  fun env def -> failwith "Students! This is your job! (check_value_definition)"
+  fun env -> function
+  | SimpleValue _ ->
+    failwith "Students! This is your job! (check_value_definition | SimpleValue)"
+  | RecFunctions _ ->
+    failwith "Students! This is your job! (check_value_definition | RecFunctions)"
 ;;
 
 let check_definition env = function

From acd881c0dd51529a11929a7e8abb27d101b9297f Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 21 Nov 2023 17:33:12 +0100
Subject: [PATCH 04/58] mm

---
 flap/src/hopix/hopixTypechecker.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 4d53376..e3b5f71 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -82,10 +82,13 @@ and check_value_definition
   -> HopixTypes.typing_environment
   =
   fun env -> function
-  | SimpleValue _ ->
+  | SimpleValue (id, Some ty, ex) ->
     failwith "Students! This is your job! (check_value_definition | SimpleValue)"
   | RecFunctions _ ->
+    (* Je crois que c'est galère et donc c'est pas grave si on arrive pas
+       à faire les fonctions récursives *)
     failwith "Students! This is your job! (check_value_definition | RecFunctions)"
+  | _ -> failwith "Students! This is your job!"
 ;;
 
 let check_definition env = function

From 79029a186e81f42665c3c4a866f64b897aee675e Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Sat, 25 Nov 2023 14:33:03 +0100
Subject: [PATCH 05/58] ?

---
 flap/src/hopix/hopixTypechecker.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 31b7489..d596cee 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -67,21 +67,18 @@ let rec synth_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty
   =
-  fun env Position.{ value = e; position = pos } ->
-  failwith "Students! This is your job! (synth_expression)"
-
+  fun env Position.{ value = e; position = pos } -> 
+    
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
   =
   fun env (Position.{ value = e; position = pos } as exp) expected ->
-  failwith "Students! This is your job! (check_expression)"
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
   -> HopixTypes.typing_environment
   =
-  fun env def -> failwith "Students! This is your job! (check_value_definition)"
 ;;
 
 let check_definition env = function

From ae2b764821eff7a0e171547fcb8038dd6d9f456f Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Sat, 25 Nov 2023 16:44:12 +0100
Subject: [PATCH 06/58] =?UTF-8?q?tentative=20de=20compr=C3=A9hension?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 flap/src/hopix/hopixTypechecker.ml | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 875cdbb..e12389b 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -67,21 +67,36 @@ let rec synth_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty
   =
-  fun env Position.{ value = e; position = pos } -> 
+  fun env Position.{ value = e; position = pos } -> function 
+    | Literal l -> type_of_literal l.value
+    | Variable(id,tlist) ->  failwith "Students! This is your job! Variable"
+    | Tagged(cons,_,[]) -> HopixTypes.hbool (*Pas sûr, j'ai regardé comme dans hopixInterpreter au début*)
+    | Apply(a,b) -> failwith "Students! This is your job! Apply"
+    | Record(field,tliste) -> failwith "Students! This is your job! Record"
+    | Fun(_) -> failwith "Students! This is your job! Fun synth" (* TODO : ici on ne peut pas synthesisé. cf Cours*)
+    | TypeAnnotation(expr,t) -> failwith "Students! This is your job! TypeAnnotation"
+
     
+and type_of_literal l =
+  match l with 
+  | LInt _ -> HopixTypes.hint
+  | LChar _ -> HopixTypes.hchar
+  | LString _ -> HopixTypes.hstring
+
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
   =
-  fun env (Position.{ value = e; position = pos } as exp) expected ->
+  fun env (Position.{ value = e; position = pos } as exp) expected -> function
+  |  Fun df -> failwith "Students! This is your job! Fun check"
+
+   
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
   -> HopixTypes.typing_environment
-  =
-<<<<<<< HEAD
-=======
-  fun env -> function
+  = 
+fun env -> function
   | SimpleValue (id, Some ty, ex) ->
     failwith "Students! This is your job! (check_value_definition | SimpleValue)"
   | RecFunctions _ ->
@@ -89,7 +104,6 @@ and check_value_definition
        à faire les fonctions récursives *)
     failwith "Students! This is your job! (check_value_definition | RecFunctions)"
   | _ -> failwith "Students! This is your job!"
->>>>>>> acd881c0dd51529a11929a7e8abb27d101b9297f
 ;;
 
 let check_definition env = function

From 3ee85d77663fce5e6a29efa50f63983456e447cf Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 28 Nov 2023 01:59:55 +0100
Subject: [PATCH 07/58] fix

---
 flap/src/hopix/hopixTypechecker.ml | 35 ++++++++++++++++--------------
 1 file changed, 19 insertions(+), 16 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index e12389b..bec91ab 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -67,18 +67,21 @@ let rec synth_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty
   =
-  fun env Position.{ value = e; position = pos } -> function 
-    | Literal l -> type_of_literal l.value
-    | Variable(id,tlist) ->  failwith "Students! This is your job! Variable"
-    | Tagged(cons,_,[]) -> HopixTypes.hbool (*Pas sûr, j'ai regardé comme dans hopixInterpreter au début*)
-    | Apply(a,b) -> failwith "Students! This is your job! Apply"
-    | Record(field,tliste) -> failwith "Students! This is your job! Record"
-    | Fun(_) -> failwith "Students! This is your job! Fun synth" (* TODO : ici on ne peut pas synthesisé. cf Cours*)
-    | TypeAnnotation(expr,t) -> failwith "Students! This is your job! TypeAnnotation"
+  fun env Position.{ value = e; position = pos } ->
+  match e with
+  | Literal l -> type_of_literal l.value
+  | Variable (id, tlist) -> failwith "Students! This is your job! Variable"
+  | Tagged (cons, _, []) ->
+    HopixTypes.hbool (*Pas sûr, j'ai regardé comme dans hopixInterpreter au début*)
+  | Apply (a, b) -> failwith "Students! This is your job! Apply"
+  | Record (field, tliste) -> failwith "Students! This is your job! Record"
+  | Fun _ ->
+    failwith "Students! This is your job! Fun synth"
+    (* TODO : ici on ne peut pas synthesisé. cf Cours*)
+  | TypeAnnotation (expr, t) -> failwith "Students! This is your job! TypeAnnotation"
 
-    
 and type_of_literal l =
-  match l with 
+  match l with
   | LInt _ -> HopixTypes.hint
   | LChar _ -> HopixTypes.hchar
   | LString _ -> HopixTypes.hstring
@@ -87,16 +90,16 @@ and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
   =
-  fun env (Position.{ value = e; position = pos } as exp) expected -> function
-  |  Fun df -> failwith "Students! This is your job! Fun check"
-
-   
+  fun env (Position.{ value = e; position = pos } as exp) expected ->
+  match e with
+  | Fun df -> failwith "Students! This is your job! Fun check"
+  | _ -> failwith "Students! This is your job! check_expression wildcard"
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
   -> HopixTypes.typing_environment
-  = 
-fun env -> function
+  =
+  fun env -> function
   | SimpleValue (id, Some ty, ex) ->
     failwith "Students! This is your job! (check_value_definition | SimpleValue)"
   | RecFunctions _ ->

From 9700dddcacfed9a8952ff30c775826c30ba943f4 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 28 Nov 2023 03:17:03 +0100
Subject: [PATCH 08/58] =?UTF-8?q?s=C3=A9pare=20les=20probl=C3=A8mes=20pour?=
 =?UTF-8?q?=20mieux=20comprendre=20parce=20que=20l=C3=A0=20c'est=20un=20ca?=
 =?UTF-8?q?lvere?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

les types des fonctions sont pas là pour avoir un truc par défaut mais sont probablement pas définitif
---
 flap/src/hopix/hopixTypechecker.ml | 158 ++++++++++++++++++++++++-----
 1 file changed, 133 insertions(+), 25 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index bec91ab..adb8c2b 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -45,7 +45,120 @@ let check_type_scheme
 ;;
 
 let synth_literal : HopixAST.literal -> HopixTypes.aty =
-  fun l -> failwith "Students! This is your job! (synth_literal)"
+  fun l ->
+  match l with
+  | LInt _ -> HopixTypes.hint
+  | LChar _ -> HopixTypes.hchar
+  | LString _ -> HopixTypes.hstring
+
+and synth_pattern
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun env Position.{ value = p; position = pos } ->
+  failwith "Students! This is your job! (synth_pattern)"
+
+and synth_variable
+  :  HopixTypes.typing_environment -> identifier Position.located
+  -> ty Position.located list option -> HopixTypes.aty
+  =
+  fun tenv i tx -> failwith "Students! This is your job! (synth_variable)"
+
+and synth_tagged
+  :  HopixTypes.typing_environment -> constructor Position.located
+  -> ty Position.located list option -> expression Position.located list -> HopixTypes.aty
+  =
+  fun tenv cons tlist e_args_list -> failwith "Students! This is your job! (synth_tagged)"
+
+and synth_apply
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv f x -> failwith "Students! This is your job! (synth_apply)"
+
+and synth_record
+  :  HopixTypes.typing_environment
+  -> (label Position.located * expression Position.located) list
+  -> ty Position.located list option -> HopixTypes.aty
+  =
+  fun tenv field tlist -> failwith "Students! This is your job! (synth_record)"
+
+and synth_fun
+  :  HopixTypes.typing_environment -> pattern Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv pat expr -> failwith "Students! This is your job! (synth_fun)"
+
+and synth_tannot
+  :  HopixTypes.typing_environment -> expression Position.located -> ty Position.located
+  -> HopixTypes.aty
+  =
+  fun tenv expr t ->
+  (* TODO : ici on ne peut pas synthesisé. cf Cours*)
+  failwith "Students! This is your job! (synth_tannot)"
+
+and synth_field
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> label Position.located -> ty Position.located list option -> HopixTypes.aty
+  =
+  fun tenv expr lbl tlist -> failwith "Students! This is your job! (synth_field)"
+
+and synth_tuple
+  : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
+  =
+  fun tenv elist -> failwith "Students! This is your job! (synth_tuple)"
+
+and synth_sequence
+  : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
+  =
+  fun tenv elist -> failwith "Students! This is your job! (synth_sequence)"
+
+and synth_define
+  :  HopixTypes.typing_environment -> value_definition -> expression Position.located
+  -> HopixTypes.aty
+  =
+  fun tenv vdef expr -> failwith "Students! This is your job! (synth_define)"
+
+and synth_ref
+  : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv expr -> failwith "Students! This is your job! (synth_ref)"
+
+and synth_assign
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ref expr -> failwith "Students! This is your job! (synth_assign)"
+
+and synth_read
+  : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ref -> failwith "Students! This is your job! (synth_read)"
+
+and synth_case
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> branch Position.located list -> HopixTypes.aty
+  =
+  fun tenv expr branches -> failwith "Students! This is your job! (synth_case)"
+
+and synth_ifthenelse
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ecase eif eelse -> failwith "Students! This is your job! (synth_ifthenelse)"
+
+and synth_while
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ecase expr -> failwith "Students! This is your job! (synth_while)"
+
+and synth_for
+  :  HopixTypes.typing_environment -> identifier Position.located
+  -> expression Position.located -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv id estart eend expr -> failwith "Students! This is your job! (synth_for)"
 ;;
 
 let rec check_pattern
@@ -54,37 +167,32 @@ let rec check_pattern
   =
   fun env Position.({ value = p; position = pos } as pat) expected ->
   failwith "Students! This is your job! (check_pattern)"
-
-and synth_pattern
-  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
-  -> HopixTypes.aty * HopixTypes.typing_environment
-  =
-  fun env Position.{ value = p; position = pos } ->
-  failwith "Students! This is your job! (synth_pattern)"
 ;;
 
 let rec synth_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty
   =
-  fun env Position.{ value = e; position = pos } ->
+  fun env Position.{ value = e; position = _ } ->
   match e with
-  | Literal l -> type_of_literal l.value
-  | Variable (id, tlist) -> failwith "Students! This is your job! Variable"
-  | Tagged (cons, _, []) ->
-    HopixTypes.hbool (*Pas sûr, j'ai regardé comme dans hopixInterpreter au début*)
-  | Apply (a, b) -> failwith "Students! This is your job! Apply"
-  | Record (field, tliste) -> failwith "Students! This is your job! Record"
-  | Fun _ ->
-    failwith "Students! This is your job! Fun synth"
-    (* TODO : ici on ne peut pas synthesisé. cf Cours*)
-  | TypeAnnotation (expr, t) -> failwith "Students! This is your job! TypeAnnotation"
-
-and type_of_literal l =
-  match l with
-  | LInt _ -> HopixTypes.hint
-  | LChar _ -> HopixTypes.hchar
-  | LString _ -> HopixTypes.hstring
+  | Literal l -> synth_literal l.value
+  | Variable (id, tlist) -> synth_variable env id tlist
+  | Tagged (cons, tlist, elist) -> synth_tagged env cons tlist elist
+  | Apply (elist1, elist2) -> synth_apply env elist1 elist2
+  | Record (field, tlist) -> synth_record env field tlist
+  | Fun (FunctionDefinition (def, expr)) -> synth_fun env def expr
+  | TypeAnnotation (expr, t) -> synth_tannot env expr t
+  | Field (expr, lbl, tlist) -> synth_field env expr lbl tlist
+  | Tuple elist -> synth_tuple env elist
+  | Sequence elist -> synth_sequence env elist
+  | Define (vdef, expr) -> synth_define env vdef expr
+  | Ref expr -> synth_ref env expr
+  | Assign (expr1, expr2) -> synth_assign env expr1 expr2
+  | Read expr -> synth_read env expr
+  | Case (expr, branches) -> synth_case env expr branches
+  | IfThenElse (ecase, eif, eelse) -> synth_ifthenelse env ecase eif eelse
+  | While (ecase, expr) -> synth_while env ecase expr
+  | For (id, ecase, expr1, expr2) -> synth_for env id ecase expr1 expr2
 
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located

From c41d137715760e40bf918a63d4c5513ada563449 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 28 Nov 2023 03:29:02 +0100
Subject: [PATCH 09/58] no type = fail

---
 flap/src/hopix/hopixTypechecker.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index adb8c2b..d315d1c 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -208,13 +208,15 @@ and check_value_definition
   -> HopixTypes.typing_environment
   =
   fun env -> function
-  | SimpleValue (id, Some ty, ex) ->
-    failwith "Students! This is your job! (check_value_definition | SimpleValue)"
+  | SimpleValue (id, ty, ex) ->
+    (match ty with
+     | None -> failwith "Type missing."
+     | Some ty' ->
+       failwith "Students! This is your job! (check_value_definition | SimpleValue)")
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas
        à faire les fonctions récursives *)
     failwith "Students! This is your job! (check_value_definition | RecFunctions)"
-  | _ -> failwith "Students! This is your job!"
 ;;
 
 let check_definition env = function

From 32374064305f0b2ac927086e44fc6bbf6d086446 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 28 Nov 2023 21:32:54 +0100
Subject: [PATCH 10/58] 40/111 ???

---
 flap/src/hopix/hopixTypechecker.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d315d1c..7f6a001 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -41,7 +41,9 @@ let check_type_scheme
   -> HopixTypes.aty_scheme * HopixTypes.typing_environment
   =
   fun env pos (ForallTy (ts, ty)) ->
-  failwith "Students! This is your job! (check_type_scheme)"
+    let ts = List.map Position.value ts in
+    let env = HopixTypes.bind_type_variables pos env ts in
+    (HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env)
 ;;
 
 let synth_literal : HopixAST.literal -> HopixTypes.aty =
@@ -212,7 +214,9 @@ and check_value_definition
     (match ty with
      | None -> failwith "Type missing."
      | Some ty' ->
-       failwith "Students! This is your job! (check_value_definition | SimpleValue)")
+       (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
+       let tys,_ = Position.located_pos (check_type_scheme env) ty' in
+       HopixTypes.bind_value (Position.value id) tys env)
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas
        à faire les fonctions récursives *)

From a01eba04e3138f1581724a634f4d440bfaffc3cb Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 17:47:16 +0100
Subject: [PATCH 11/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7f6a001..0699559 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -41,9 +41,9 @@ let check_type_scheme
   -> HopixTypes.aty_scheme * HopixTypes.typing_environment
   =
   fun env pos (ForallTy (ts, ty)) ->
-    let ts = List.map Position.value ts in
-    let env = HopixTypes.bind_type_variables pos env ts in
-    (HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env)
+  let ts = List.map Position.value ts in
+  let env = HopixTypes.bind_type_variables pos env ts in
+  HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env
 ;;
 
 let synth_literal : HopixAST.literal -> HopixTypes.aty =
@@ -215,7 +215,7 @@ and check_value_definition
      | None -> failwith "Type missing."
      | Some ty' ->
        (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
-       let tys,_ = Position.located_pos (check_type_scheme env) ty' in
+       let tys, _ = Position.located_pos (check_type_scheme env) ty' in
        HopixTypes.bind_value (Position.value id) tys env)
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas

From 4805abe9046f6f72fc52aaa35577461ac05c7c3c Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Mon, 4 Dec 2023 18:05:51 +0100
Subject: [PATCH 12/58] Apply ?

---
 flap/src/hopix/hopixTypechecker.ml | 81 +++++++++++++++++-------------
 1 file changed, 46 insertions(+), 35 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7f6a001..5f0c30d 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -46,7 +46,42 @@ let check_type_scheme
     (HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env)
 ;;
 
-let synth_literal : HopixAST.literal -> HopixTypes.aty =
+
+
+let rec check_pattern
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located -> HopixTypes.aty
+  -> HopixTypes.typing_environment
+  =
+  fun env Position.({ value = p; position = pos } as pat) expected ->
+  failwith "Students! This is your job! (check_pattern)"
+;;
+
+let rec synth_expression
+  :  HopixTypes.typing_environment -> HopixAST.expression Position.located
+  -> HopixTypes.aty
+  =
+  fun env Position.{ value = e; position = _ } ->
+  match e with
+  | Literal l -> synth_literal l.value
+  | Variable (id, tlist) -> synth_variable env id tlist
+  | Tagged (cons, tlist, elist) -> synth_tagged env cons tlist elist
+  | Apply (elist1, elist2) -> synth_apply env elist1 elist2
+  | Record (field, tlist) -> synth_record env field tlist
+  | Fun (FunctionDefinition (def, expr)) -> synth_fun env def expr
+  | TypeAnnotation (expr, t) -> synth_tannot env expr t
+  | Field (expr, lbl, tlist) -> synth_field env expr lbl tlist
+  | Tuple elist -> synth_tuple env elist
+  | Sequence elist -> synth_sequence env elist
+  | Define (vdef, expr) -> synth_define env vdef expr
+  | Ref expr -> synth_ref env expr
+  | Assign (expr1, expr2) -> synth_assign env expr1 expr2
+  | Read expr -> synth_read env expr
+  | Case (expr, branches) -> synth_case env expr branches
+  | IfThenElse (ecase, eif, eelse) -> synth_ifthenelse env ecase eif eelse
+  | While (ecase, expr) -> synth_while env ecase expr
+  | For (id, ecase, expr1, expr2) -> synth_for env id ecase expr1 expr2
+
+and  synth_literal : HopixAST.literal -> HopixTypes.aty =
   fun l ->
   match l with
   | LInt _ -> HopixTypes.hint
@@ -76,7 +111,16 @@ and synth_apply
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv f x -> failwith "Students! This is your job! (synth_apply)"
+  fun tenv f x -> (*failwith "Students! This is your job! (synth_apply)"*)
+  let f_type = synth_expression tenv f in
+  match f_type with 
+  | HopixTypes.ATyArrow (gauche,droit) -> (*  a' -> b' *)
+  (
+    let x_type = synth_expression tenv x in
+    check_equal_types x.position  gauche x_type; droit
+  )
+  | _ -> failwith ""
+    
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -161,40 +205,7 @@ and synth_for
   -> expression Position.located -> HopixTypes.aty
   =
   fun tenv id estart eend expr -> failwith "Students! This is your job! (synth_for)"
-;;
 
-let rec check_pattern
-  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located -> HopixTypes.aty
-  -> HopixTypes.typing_environment
-  =
-  fun env Position.({ value = p; position = pos } as pat) expected ->
-  failwith "Students! This is your job! (check_pattern)"
-;;
-
-let rec synth_expression
-  :  HopixTypes.typing_environment -> HopixAST.expression Position.located
-  -> HopixTypes.aty
-  =
-  fun env Position.{ value = e; position = _ } ->
-  match e with
-  | Literal l -> synth_literal l.value
-  | Variable (id, tlist) -> synth_variable env id tlist
-  | Tagged (cons, tlist, elist) -> synth_tagged env cons tlist elist
-  | Apply (elist1, elist2) -> synth_apply env elist1 elist2
-  | Record (field, tlist) -> synth_record env field tlist
-  | Fun (FunctionDefinition (def, expr)) -> synth_fun env def expr
-  | TypeAnnotation (expr, t) -> synth_tannot env expr t
-  | Field (expr, lbl, tlist) -> synth_field env expr lbl tlist
-  | Tuple elist -> synth_tuple env elist
-  | Sequence elist -> synth_sequence env elist
-  | Define (vdef, expr) -> synth_define env vdef expr
-  | Ref expr -> synth_ref env expr
-  | Assign (expr1, expr2) -> synth_assign env expr1 expr2
-  | Read expr -> synth_read env expr
-  | Case (expr, branches) -> synth_case env expr branches
-  | IfThenElse (ecase, eif, eelse) -> synth_ifthenelse env ecase eif eelse
-  | While (ecase, expr) -> synth_while env ecase expr
-  | For (id, ecase, expr1, expr2) -> synth_for env id ecase expr1 expr2
 
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located

From 1edd925ed580bd5fe4d42052933cb0575dc0bf37 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 18:33:56 +0100
Subject: [PATCH 13/58] type checking

---
 flap/src/hopix/hopixTypechecker.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 0699559..036af21 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -2,6 +2,8 @@
 
 open HopixAST
 
+let get_aty (HopixTypes.Scheme (_, aty_value)) : HopixTypes.aty = aty_value
+
 (** Error messages *)
 
 let invalid_instantiation pos given expected =
@@ -203,7 +205,9 @@ and check_expression
   fun env (Position.{ value = e; position = pos } as exp) expected ->
   match e with
   | Fun df -> failwith "Students! This is your job! Fun check"
-  | _ -> failwith "Students! This is your job! check_expression wildcard"
+  | _ ->
+    let given = synth_expression env exp in
+    check_equal_types pos ~expected ~given
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
@@ -212,10 +216,11 @@ and check_value_definition
   fun env -> function
   | SimpleValue (id, ty, ex) ->
     (match ty with
-     | None -> failwith "Type missing."
+     | None -> failwith "A type is missing."
      | Some ty' ->
        (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
-       let tys, _ = Position.located_pos (check_type_scheme env) ty' in
+       let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
+       check_expression tenv ex (get_aty tys);
        HopixTypes.bind_value (Position.value id) tys env)
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas

From 72c323b2c839dffd788f6bc1ce3539b9e05693b6 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 18:38:57 +0100
Subject: [PATCH 14/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index ee89423..b7fd253 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -48,8 +48,6 @@ let check_type_scheme
   HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env
 ;;
 
-
-
 let rec check_pattern
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located -> HopixTypes.aty
   -> HopixTypes.typing_environment
@@ -83,7 +81,7 @@ let rec synth_expression
   | While (ecase, expr) -> synth_while env ecase expr
   | For (id, ecase, expr1, expr2) -> synth_for env id ecase expr1 expr2
 
-and  synth_literal : HopixAST.literal -> HopixTypes.aty =
+and synth_literal : HopixAST.literal -> HopixTypes.aty =
   fun l ->
   match l with
   | LInt _ -> HopixTypes.hint
@@ -113,16 +111,16 @@ and synth_apply
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv f x -> (*failwith "Students! This is your job! (synth_apply)"*)
+  fun tenv f x ->
+  (*failwith "Students! This is your job! (synth_apply)"*)
   let f_type = synth_expression tenv f in
-  match f_type with 
-  | HopixTypes.ATyArrow (gauche,droit) -> (*  a' -> b' *)
-  (
+  match f_type with
+  | HopixTypes.ATyArrow (gauche, droit) ->
+    (*  a' -> b' *)
     let x_type = synth_expression tenv x in
-    check_equal_types x.position  gauche x_type; droit
-  )
+    check_equal_types x.position gauche x_type;
+    droit
   | _ -> failwith ""
-    
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -208,7 +206,6 @@ and synth_for
   =
   fun tenv id estart eend expr -> failwith "Students! This is your job! (synth_for)"
 
-
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit

From 07230fc0ed80148e4e85128c6b6e6d106bc24873 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Mon, 4 Dec 2023 18:40:31 +0100
Subject: [PATCH 15/58] sequence

---
 flap/src/hopix/hopixTypechecker.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 5f0c30d..3a91703 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -157,7 +157,16 @@ and synth_tuple
 and synth_sequence
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv elist -> failwith "Students! This is your job! (synth_sequence)"
+  fun tenv elist ->
+    match elist with
+    | [] -> failwith "erreur sequence"
+    | [x] -> synth_expression tenv x 
+    | x::l ->
+      (
+      let x_type = synth_expression tenv x in
+      check_equal_types x.position HopixTypes.hunit x_type
+      ; synth_sequence tenv l)
+
 
 and synth_define
   :  HopixTypes.typing_environment -> value_definition -> expression Position.located

From a4910af26df56be5421c82c370bfcb6cdafae1fd Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 18:50:55 +0100
Subject: [PATCH 16/58] sequence

Co-authored-by: Nicolas PENELOUX <nicolas.peneloux@free.fr>
---
 flap/src/hopix/hopixTypechecker.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index b7fd253..061ab25 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -157,7 +157,14 @@ and synth_tuple
 and synth_sequence
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv elist -> failwith "Students! This is your job! (synth_sequence)"
+  fun tenv elist ->
+  match elist with
+  | [] -> failwith "erreur sequence"
+  | [ x ] -> synth_expression tenv x
+  | x :: l ->
+    let x_type = synth_expression tenv x in
+    check_equal_types x.position HopixTypes.hunit x_type;
+    synth_sequence tenv l
 
 and synth_define
   :  HopixTypes.typing_environment -> value_definition -> expression Position.located

From ee1baae4202d2540e891925efb17db6a964cb476 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 22:58:47 +0100
Subject: [PATCH 17/58] typo

---
 flap/src/hopix/hopixTypechecker.ml | 22 +++++-----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index dc25c7a..2dc3989 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -115,10 +115,10 @@ and synth_apply
   (*failwith "Students! This is your job! (synth_apply)"*)
   let f_type = synth_expression tenv f in
   match f_type with
-  | HopixTypes.ATyArrow (gauche, droit) ->
+  | HopixTypes.ATyArrow (expected, droit) ->
     (*  a' -> b' *)
-    let x_type = synth_expression tenv x in
-    check_equal_types x.position gauche x_type;
+    let given = synth_expression tenv x in
+    check_equal_types x.position ~expected ~given;
     droit
   | _ -> failwith ""
 
@@ -158,25 +158,13 @@ and synth_sequence
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
   =
   fun tenv elist ->
-<<<<<<< HEAD
-    match elist with
-    | [] -> failwith "erreur sequence"
-    | [x] -> synth_expression tenv x 
-    | x::l ->
-      (
-      let x_type = synth_expression tenv x in
-      check_equal_types x.position HopixTypes.hunit x_type
-      ; synth_sequence tenv l)
-
-=======
   match elist with
   | [] -> failwith "erreur sequence"
   | [ x ] -> synth_expression tenv x
   | x :: l ->
-    let x_type = synth_expression tenv x in
-    check_equal_types x.position HopixTypes.hunit x_type;
+    let given = synth_expression tenv x in
+    check_equal_types x.position ~expected:HopixTypes.hunit ~given;
     synth_sequence tenv l
->>>>>>> a4910af26df56be5421c82c370bfcb6cdafae1fd
 
 and synth_define
   :  HopixTypes.typing_environment -> value_definition -> expression Position.located

From 1af819d86d12cc49eecf0d74c19676f55db53f63 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 23:36:04 +0100
Subject: [PATCH 18/58] ah! javais pas vu mdr

---
 flap/src/hopix/hopixTypechecker.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 2dc3989..cb2028b 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -2,8 +2,6 @@
 
 open HopixAST
 
-let get_aty (HopixTypes.Scheme (_, aty_value)) : HopixTypes.aty = aty_value
-
 (** Error messages *)
 
 let invalid_instantiation pos given expected =
@@ -235,7 +233,7 @@ and check_value_definition
      | Some ty' ->
        (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
        let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
-       check_expression tenv ex (get_aty tys);
+       check_expression tenv ex (HopixTypes.instantiate_type_scheme tys []);
        HopixTypes.bind_value (Position.value id) tys env)
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas

From 6338b05d39e5f89e5b1b02957bb1d181102e67fd Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 23:36:08 +0100
Subject: [PATCH 19/58] synth_variable

---
 flap/src/hopix/hopixTypechecker.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index cb2028b..2d7918a 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -97,7 +97,16 @@ and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located
   -> ty Position.located list option -> HopixTypes.aty
   =
-  fun tenv i tx -> failwith "Students! This is your job! (synth_variable)"
+  fun tenv id tlist ->
+  (* Get variable type *)
+  let ty =
+    try HopixTypes.lookup_type_scheme_of_identifier id.position id.value tenv with
+    | HopixTypes.Unbound (pos, Identifier (Id i)) ->
+      HopixTypes.type_error pos (Printf.sprintf "%s unbound" i)
+  in
+  match tlist with
+  | None -> HopixTypes.instantiate_type_scheme ty []
+  | Some _ -> failwith "Students! This is your job! (synth_variable tlist not None)"
 
 and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located

From 3c30abe0ac7e85f3867e7353d77e0a79feff0152 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 23:50:20 +0100
Subject: [PATCH 20/58] correct error msg

---
 flap/src/hopix/hopixTypechecker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 2d7918a..5abe051 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -102,7 +102,7 @@ and synth_variable
   let ty =
     try HopixTypes.lookup_type_scheme_of_identifier id.position id.value tenv with
     | HopixTypes.Unbound (pos, Identifier (Id i)) ->
-      HopixTypes.type_error pos (Printf.sprintf "%s unbound" i)
+      HopixTypes.type_error pos (Printf.sprintf "Unbound identifier `%s'." i)
   in
   match tlist with
   | None -> HopixTypes.instantiate_type_scheme ty []

From a4ea0f62d285d045a8557aac6c016dba591c226c Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Mon, 4 Dec 2023 23:50:29 +0100
Subject: [PATCH 21/58] synth_define

---
 flap/src/hopix/hopixTypechecker.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 5abe051..bf4ccde 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -177,7 +177,9 @@ and synth_define
   :  HopixTypes.typing_environment -> value_definition -> expression Position.located
   -> HopixTypes.aty
   =
-  fun tenv vdef expr -> failwith "Students! This is your job! (synth_define)"
+  fun tenv vdef expr ->
+  let tenv = check_value_definition tenv vdef in
+  synth_expression tenv expr
 
 and synth_ref
   : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty

From 28f303ee5130c11705d0c22e30e3f3ed01869e74 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 00:06:30 +0100
Subject: [PATCH 22/58] failwith

---
 flap/src/hopix/hopixTypechecker.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index bf4ccde..6d64811 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -106,7 +106,7 @@ and synth_variable
   in
   match tlist with
   | None -> HopixTypes.instantiate_type_scheme ty []
-  | Some _ -> failwith "Students! This is your job! (synth_variable tlist not None)"
+  | Some _ -> failwith "Students! This is your job! (synth_variable | tlist | None)"
 
 and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located
@@ -119,7 +119,6 @@ and synth_apply
   -> expression Position.located -> HopixTypes.aty
   =
   fun tenv f x ->
-  (*failwith "Students! This is your job! (synth_apply)"*)
   let f_type = synth_expression tenv f in
   match f_type with
   | HopixTypes.ATyArrow (expected, droit) ->
@@ -228,7 +227,7 @@ and check_expression
   =
   fun env (Position.{ value = e; position = pos } as exp) expected ->
   match e with
-  | Fun df -> failwith "Students! This is your job! Fun check"
+  | Fun df -> failwith "Students! This is your job! (check_expression | Fun)"
   | _ ->
     let given = synth_expression env exp in
     check_equal_types pos ~expected ~given
@@ -242,7 +241,6 @@ and check_value_definition
     (match ty with
      | None -> failwith "A type is missing."
      | Some ty' ->
-       (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
        let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
        check_expression tenv ex (HopixTypes.instantiate_type_scheme tys []);
        HopixTypes.bind_value (Position.value id) tys env)

From 11b86b509a7645409c71369a391e2a11a367cbc8 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 00:06:34 +0100
Subject: [PATCH 23/58] synth_ref

---
 flap/src/hopix/hopixTypechecker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 6d64811..c17f29e 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -183,7 +183,7 @@ and synth_define
 and synth_ref
   : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv expr -> failwith "Students! This is your job! (synth_ref)"
+  fun tenv expr -> HopixTypes.href (synth_expression tenv expr)
 
 and synth_assign
   :  HopixTypes.typing_environment -> expression Position.located

From 7e4a6b91bd33349eb429bb0430c95a39b478cfbf Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 03:59:04 +0100
Subject: [PATCH 24/58] essay at synth_tannot

---
 flap/src/hopix/hopixTypechecker.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index c17f29e..57cd879 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -145,9 +145,11 @@ and synth_tannot
   :  HopixTypes.typing_environment -> expression Position.located -> ty Position.located
   -> HopixTypes.aty
   =
-  fun tenv expr t ->
-  (* TODO : ici on ne peut pas synthesisé. cf Cours*)
-  failwith "Students! This is your job! (synth_tannot)"
+  fun tenv expr ty ->
+  (* Pas sûr de ça *)
+  let ty' = synth_expression tenv expr in
+  check_equal_types expr.position ~expected:(HopixTypes.internalize_ty tenv ty) ~given:ty';
+  ty'
 
 and synth_field
   :  HopixTypes.typing_environment -> expression Position.located

From 0fb9b8603b8e61c0ecbf86795417ca20020a69a0 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 03:59:26 +0100
Subject: [PATCH 25/58] .

---
 flap/src/hopix/hopixTypechecker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 57cd879..017134e 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -146,8 +146,8 @@ and synth_tannot
   -> HopixTypes.aty
   =
   fun tenv expr ty ->
-  (* Pas sûr de ça *)
   let ty' = synth_expression tenv expr in
+  (* Pas sûr de ça *)
   check_equal_types expr.position ~expected:(HopixTypes.internalize_ty tenv ty) ~given:ty';
   ty'
 

From f82e28cd8ba8c1c5ceca19a299b0304e2efd1baf Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:08:51 +0100
Subject: [PATCH 26/58] synth_assign

---
 flap/src/hopix/hopixTypechecker.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 017134e..c07e501 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -191,7 +191,13 @@ and synth_assign
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv ref expr -> failwith "Students! This is your job! (synth_assign)"
+  fun tenv ref expr ->
+  let refty = synth_expression tenv ref in
+  match HopixTypes.destruct_reference_type expr.position refty with
+  | expected ->
+    let given = synth_expression tenv expr in
+    check_equal_types expr.position ~expected ~given;
+    HopixTypes.hunit
 
 and synth_read
   : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty

From 9d077bcbc1687e99fb782f72181ec4f5d85a7d42 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:10:33 +0100
Subject: [PATCH 27/58] synth_read

---
 flap/src/hopix/hopixTypechecker.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index c07e501..6cd68ff 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -202,7 +202,9 @@ and synth_assign
 and synth_read
   : HopixTypes.typing_environment -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv ref -> failwith "Students! This is your job! (synth_read)"
+  fun tenv ref ->
+  let refty = synth_expression tenv ref in
+  HopixTypes.destruct_reference_type ref.position refty
 
 and synth_case
   :  HopixTypes.typing_environment -> expression Position.located

From 45bbd6a0dd891b992ba2dbe37a5d5a4c80825271 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:17:53 +0100
Subject: [PATCH 28/58] synth_ifthenelse

---
 flap/src/hopix/hopixTypechecker.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 6cd68ff..694c74f 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -216,7 +216,15 @@ and synth_ifthenelse
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv ecase eif eelse -> failwith "Students! This is your job! (synth_ifthenelse)"
+  fun tenv ecase eif eelse ->
+  (* Pas testé !! *)
+  let ecasety = synth_expression tenv ecase in
+  check_equal_types ecase.position ~expected:ecasety ~given:HopixTypes.hbool;
+  let eifty = synth_expression tenv eif in
+  check_equal_types eif.position ~expected:eifty ~given:HopixTypes.hunit;
+  let eelsety = synth_expression tenv eelse in
+  check_equal_types eelse.position ~expected:eelsety ~given:HopixTypes.hunit;
+  HopixTypes.hunit
 
 and synth_while
   :  HopixTypes.typing_environment -> expression Position.located

From 419e3e962ec0b9d5bc1b5d8b45d987cbc348865a Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:17:56 +0100
Subject: [PATCH 29/58] synth_while

---
 flap/src/hopix/hopixTypechecker.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 694c74f..594ace2 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -230,7 +230,12 @@ and synth_while
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv ecase expr -> failwith "Students! This is your job! (synth_while)"
+  fun tenv ecase c ->
+  let ecasety = synth_expression tenv ecase in
+  check_equal_types ecase.position ~expected:ecasety ~given:HopixTypes.hbool;
+  let exprty = synth_expression tenv c in
+  check_equal_types c.position ~expected:exprty ~given:HopixTypes.hunit;
+  HopixTypes.hunit
 
 and synth_for
   :  HopixTypes.typing_environment -> identifier Position.located

From 52eabc26972d203f2d29553018402c2a987da1fa Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:29:42 +0100
Subject: [PATCH 30/58] synth_for

---
 flap/src/hopix/hopixTypechecker.ml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 594ace2..0046e84 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -242,7 +242,20 @@ and synth_for
   -> expression Position.located -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv id estart eend expr -> failwith "Students! This is your job! (synth_for)"
+  fun tenv id estart eend expr ->
+  let estart_ty = synth_expression tenv estart in
+  check_equal_types estart.position ~expected:estart_ty ~given:HopixTypes.hint;
+  let eend_ty = synth_expression tenv eend in
+  check_equal_types eend.position ~expected:eend_ty ~given:HopixTypes.hint;
+  let tenv' =
+    HopixTypes.bind_value
+      id.value
+      (HopixTypes.monomorphic_type_scheme HopixTypes.hint)
+      tenv
+  in
+  let e_ty = synth_expression tenv' expr in
+  check_equal_types expr.position ~expected:e_ty ~given:HopixTypes.hunit;
+  HopixTypes.hunit
 
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located

From d2db0dfc4fe449ee48f9fc0fe6b6488e1ee1621c Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 04:32:24 +0100
Subject: [PATCH 31/58] typos

---
 flap/src/hopix/hopixTypechecker.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 0046e84..b2c399c 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -106,7 +106,7 @@ and synth_variable
   in
   match tlist with
   | None -> HopixTypes.instantiate_type_scheme ty []
-  | Some _ -> failwith "Students! This is your job! (synth_variable | tlist | None)"
+  | Some _ -> failwith "Students! This is your job! (synth_variable | tlist | Some)"
 
 and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located
@@ -126,7 +126,7 @@ and synth_apply
     let given = synth_expression tenv x in
     check_equal_types x.position ~expected ~given;
     droit
-  | _ -> failwith ""
+  | _ -> failwith "Error: apply"
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -167,7 +167,7 @@ and synth_sequence
   =
   fun tenv elist ->
   match elist with
-  | [] -> failwith "erreur sequence"
+  | [] -> failwith "Error: sequence"
   | [ x ] -> synth_expression tenv x
   | x :: l ->
     let given = synth_expression tenv x in

From b37962dee2ad980ec38acc8bbb7871cf06fd6a1b Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 11:38:31 +0100
Subject: [PATCH 32/58] oops

---
 flap/src/hopix/hopixTypechecker.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index b2c399c..d4cd9d9 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -219,11 +219,11 @@ and synth_ifthenelse
   fun tenv ecase eif eelse ->
   (* Pas testé !! *)
   let ecasety = synth_expression tenv ecase in
-  check_equal_types ecase.position ~expected:ecasety ~given:HopixTypes.hbool;
+  check_equal_types ecase.position ~expected:HopixTypes.hbool ~given:ecasety;
   let eifty = synth_expression tenv eif in
-  check_equal_types eif.position ~expected:eifty ~given:HopixTypes.hunit;
+  check_equal_types eif.position ~expected:HopixTypes.hunit ~given:eifty;
   let eelsety = synth_expression tenv eelse in
-  check_equal_types eelse.position ~expected:eelsety ~given:HopixTypes.hunit;
+  check_equal_types eelse.position ~expected:HopixTypes.hunit ~given:eelsety;
   HopixTypes.hunit
 
 and synth_while
@@ -232,9 +232,9 @@ and synth_while
   =
   fun tenv ecase c ->
   let ecasety = synth_expression tenv ecase in
-  check_equal_types ecase.position ~expected:ecasety ~given:HopixTypes.hbool;
+  check_equal_types ecase.position ~expected:HopixTypes.hbool ~given:ecasety;
   let exprty = synth_expression tenv c in
-  check_equal_types c.position ~expected:exprty ~given:HopixTypes.hunit;
+  check_equal_types c.position ~expected:HopixTypes.hunit ~given:exprty;
   HopixTypes.hunit
 
 and synth_for
@@ -244,9 +244,9 @@ and synth_for
   =
   fun tenv id estart eend expr ->
   let estart_ty = synth_expression tenv estart in
-  check_equal_types estart.position ~expected:estart_ty ~given:HopixTypes.hint;
+  check_equal_types estart.position ~expected:HopixTypes.hint ~given:estart_ty;
   let eend_ty = synth_expression tenv eend in
-  check_equal_types eend.position ~expected:eend_ty ~given:HopixTypes.hint;
+  check_equal_types eend.position ~expected:HopixTypes.hint ~given:eend_ty;
   let tenv' =
     HopixTypes.bind_value
       id.value
@@ -254,7 +254,7 @@ and synth_for
       tenv
   in
   let e_ty = synth_expression tenv' expr in
-  check_equal_types expr.position ~expected:e_ty ~given:HopixTypes.hunit;
+  check_equal_types expr.position ~expected:HopixTypes.hunit ~given:e_ty;
   HopixTypes.hunit
 
 and check_expression

From 4492c9b3ea164f844174142e5a65cfd6c9b9af35 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 11:47:52 +0100
Subject: [PATCH 33/58] better errors

---
 flap/src/hopix/hopixTypechecker.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d4cd9d9..debc113 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -126,7 +126,7 @@ and synth_apply
     let given = synth_expression tenv x in
     check_equal_types x.position ~expected ~given;
     droit
-  | _ -> failwith "Error: apply"
+  | _ -> HopixTypes.type_error f.position "Can't apply"
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -167,7 +167,7 @@ and synth_sequence
   =
   fun tenv elist ->
   match elist with
-  | [] -> failwith "Error: sequence"
+  | [] -> HopixTypes.type_error Position.dummy "Invalid sequence"
   | [ x ] -> synth_expression tenv x
   | x :: l ->
     let given = synth_expression tenv x in
@@ -261,12 +261,9 @@ and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
   =
-  fun env (Position.{ value = e; position = pos } as exp) expected ->
-  match e with
-  | Fun df -> failwith "Students! This is your job! (check_expression | Fun)"
-  | _ ->
-    let given = synth_expression env exp in
-    check_equal_types pos ~expected ~given
+  fun env (Position.{ position = pos } as exp) expected ->
+  let given = synth_expression env exp in
+  check_equal_types pos ~expected ~given
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
@@ -275,7 +272,7 @@ and check_value_definition
   fun env -> function
   | SimpleValue (id, ty, ex) ->
     (match ty with
-     | None -> failwith "A type is missing."
+     | None -> HopixTypes.type_error ex.position "Type is missing"
      | Some ty' ->
        let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
        check_expression tenv ex (HopixTypes.instantiate_type_scheme tys []);

From f44b7a585ee382e3bdc0cf538f68a402c1a5b807 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 12:10:00 +0100
Subject: [PATCH 34/58] synth_variable Some case

---
 flap/src/hopix/hopixTypechecker.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index debc113..9b5e0e5 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -106,7 +106,12 @@ and synth_variable
   in
   match tlist with
   | None -> HopixTypes.instantiate_type_scheme ty []
-  | Some _ -> failwith "Students! This is your job! (synth_variable | tlist | Some)"
+  | Some tlist' ->
+    (* Pas testé *)
+    let atlist = List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist' in
+    (try HopixTypes.instantiate_type_scheme ty atlist with
+     | HopixTypes.InvalidInstantiation { expected; given } ->
+       invalid_instantiation id.position expected given)
 
 and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located

From 4266ff51113d4506edf0524f918112e88555d9d4 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 12:30:16 +0100
Subject: [PATCH 35/58] wip: record

---
 flap/src/hopix/hopixTypechecker.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 9b5e0e5..a32f3aa 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -138,7 +138,18 @@ and synth_record
   -> (label Position.located * expression Position.located) list
   -> ty Position.located list option -> HopixTypes.aty
   =
-  fun tenv field tlist -> failwith "Students! This is your job! (synth_record)"
+  fun tenv field tlist ->
+  let fl = fst (List.hd field) in
+  let cons, _, _ =
+    HopixTypes.lookup_type_constructor_of_label fl.position fl.value tenv
+  in
+  let tlist' =
+    match tlist with
+    | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
+    | None -> HopixTypes.type_error fl.position "No types ??"
+  in
+  (* TODO: Typecheck *)
+  ATyCon (cons, tlist')
 
 and synth_fun
   :  HopixTypes.typing_environment -> pattern Position.located

From 9e7de664e7186d3d8e480bdb3c7b4bb2a8293208 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:05:21 +0100
Subject: [PATCH 36/58] synth_record : 35/111

---
 flap/src/hopix/hopixTypechecker.ml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index a32f3aa..d09e2b5 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -139,6 +139,7 @@ and synth_record
   -> ty Position.located list option -> HopixTypes.aty
   =
   fun tenv field tlist ->
+  (* Translate the types *)
   let fl = fst (List.hd field) in
   let cons, _, _ =
     HopixTypes.lookup_type_constructor_of_label fl.position fl.value tenv
@@ -148,7 +149,23 @@ and synth_record
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
     | None -> HopixTypes.type_error fl.position "No types ??"
   in
-  (* TODO: Typecheck *)
+  (* Type checking *)
+  List.iter
+    (fun (Position.{ position = label_pos; value = label_val }, expr) ->
+      let label_scheme =
+        try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
+        | HopixTypes.Unbound (pos, Label (LId i)) ->
+          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+      in
+      let arrow =
+        try HopixTypes.instantiate_type_scheme label_scheme tlist' with
+        | HopixTypes.InvalidInstantiation { expected; given } ->
+          invalid_instantiation (Position.position expr) expected given
+      in
+      let _, expected = HopixTypes.destruct_function_type label_pos arrow in
+      let given = synth_expression tenv expr in
+      check_equal_types label_pos ~expected ~given)
+    field;
   ATyCon (cons, tlist')
 
 and synth_fun

From a90e8176e6498cb86d6c2e29cc32490874df9761 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:51:59 +0100
Subject: [PATCH 37/58] =?UTF-8?q?synth=5Ftagged=20-=20pire=20impl=C3=A9men?=
 =?UTF-8?q?tation=20ever?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 flap/src/hopix/hopixTypechecker.ml | 36 +++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d09e2b5..6982529 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -117,7 +117,41 @@ and synth_tagged
   :  HopixTypes.typing_environment -> constructor Position.located
   -> ty Position.located list option -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv cons tlist e_args_list -> failwith "Students! This is your job! (synth_tagged)"
+  fun tenv cons tlist e_args_list ->
+  let cons_scheme =
+    try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
+    | HopixTypes.Unbound (pos, Constructor (KId c)) ->
+      HopixTypes.type_error pos (Printf.sprintf "Unbound constructor `%s'." c)
+  in
+  let tys =
+    List.map
+      (fun x -> HopixTypes.internalize_ty tenv x)
+      (match tlist with
+       | Some t -> t
+       | None -> HopixTypes.type_error cons.position "No types ??")
+  in
+  let tcons =
+    try HopixTypes.instantiate_type_scheme cons_scheme tys with
+    | HopixTypes.InvalidInstantiation { expected; given } ->
+      invalid_instantiation cons.position expected given
+  in
+  let targs = List.map (fun x -> synth_expression tenv x) e_args_list in
+  let expected_args, result =
+    HopixTypes.destruct_function_type_maximally cons.position tcons
+  in
+  (try
+     List.iter2
+       (fun expected given -> check_equal_types cons.position ~expected ~given)
+       expected_args
+       targs
+   with
+   | Invalid_argument _ ->
+     (* 35-bad *)
+     check_equal_types
+       cons.position
+       ~expected:result
+       ~given:(HopixTypes.ATyArrow (result, result)));
+  result
 
 and synth_apply
   :  HopixTypes.typing_environment -> expression Position.located

From 756ede6179943f4c56cf0a6cc2a1c552452c362d Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:52:18 +0100
Subject: [PATCH 38/58] mieux?

---
 flap/src/hopix/hopixTypechecker.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 6982529..37177bc 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -128,7 +128,7 @@ and synth_tagged
       (fun x -> HopixTypes.internalize_ty tenv x)
       (match tlist with
        | Some t -> t
-       | None -> HopixTypes.type_error cons.position "No types ??")
+       | None -> HopixTypes.type_error cons.position "No types found")
   in
   let tcons =
     try HopixTypes.instantiate_type_scheme cons_scheme tys with
@@ -181,7 +181,7 @@ and synth_record
   let tlist' =
     match tlist with
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
-    | None -> HopixTypes.type_error fl.position "No types ??"
+    | None -> HopixTypes.type_error fl.position "No types found"
   in
   (* Type checking *)
   List.iter

From ab4f67523923acb7a85171c3e565f358b1e11a3c Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 13:52:52 +0100
Subject: [PATCH 39/58] .

---
 flap/src/hopix/hopixTypechecker.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 37177bc..7114d34 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -128,7 +128,7 @@ and synth_tagged
       (fun x -> HopixTypes.internalize_ty tenv x)
       (match tlist with
        | Some t -> t
-       | None -> HopixTypes.type_error cons.position "No types found")
+       | None -> HopixTypes.type_error cons.position "No types found.")
   in
   let tcons =
     try HopixTypes.instantiate_type_scheme cons_scheme tys with
@@ -165,7 +165,7 @@ and synth_apply
     let given = synth_expression tenv x in
     check_equal_types x.position ~expected ~given;
     droit
-  | _ -> HopixTypes.type_error f.position "Can't apply"
+  | _ -> HopixTypes.type_error f.position "Can't apply."
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -181,7 +181,7 @@ and synth_record
   let tlist' =
     match tlist with
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
-    | None -> HopixTypes.type_error fl.position "No types found"
+    | None -> HopixTypes.type_error fl.position "No types found."
   in
   (* Type checking *)
   List.iter
@@ -234,7 +234,7 @@ and synth_sequence
   =
   fun tenv elist ->
   match elist with
-  | [] -> HopixTypes.type_error Position.dummy "Invalid sequence"
+  | [] -> HopixTypes.type_error Position.dummy "Invalid sequence."
   | [ x ] -> synth_expression tenv x
   | x :: l ->
     let given = synth_expression tenv x in
@@ -339,7 +339,7 @@ and check_value_definition
   fun env -> function
   | SimpleValue (id, ty, ex) ->
     (match ty with
-     | None -> HopixTypes.type_error ex.position "Type is missing"
+     | None -> HopixTypes.type_error ex.position "Type is missing."
      | Some ty' ->
        let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
        check_expression tenv ex (HopixTypes.instantiate_type_scheme tys []);

From 0ec66864fbc5ce4cf5c628602be813b60dab3bd7 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 5 Dec 2023 19:16:35 +0100
Subject: [PATCH 40/58] =?UTF-8?q?Fields=20(marche=20pas),=20d=C3=A9but=20p?=
 =?UTF-8?q?attern,=20Tuple=20et=20Fun?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 flap/src/hopix/hopixTypechecker.ml | 46 ++++++++++++++++++++++++++----
 1 file changed, 40 insertions(+), 6 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7114d34..7bcb070 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -90,8 +90,16 @@ and synth_pattern
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun env Position.{ value = p; position = pos } ->
-  failwith "Students! This is your job! (synth_pattern)"
+  fun env Position.{ value = p; position = pos } -> match p with
+    | PWildcard -> failwith "PWildcard"
+    | PLiteral l-> failwith "Pliteral"
+    | PVariable pv -> failwith "PVariable"
+    | PTypeAnnotation(p,ty) -> failwith "PTypeAnnot"
+    | PTuple(plist) -> failwith "PTuple"
+    | POr(plist) ->  failwith "POr"
+    | PAnd (plist) -> failwith "PAnd"
+    | PTaggedValue(cons,tlist,plist) -> failwith "PTagged"
+    | PRecord(plist,tlist) -> failwith "PRecord"
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located
@@ -206,7 +214,10 @@ and synth_fun
   :  HopixTypes.typing_environment -> pattern Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv pat expr -> failwith "Students! This is your job! (synth_fun)"
+  fun tenv pat expr -> 
+    let pat_type, tenv = synth_pattern tenv pat in
+    let expr_type = synth_expression tenv expr in 
+    ATyArrow(pat_type,expr_type) 
 
 and synth_tannot
   :  HopixTypes.typing_environment -> expression Position.located -> ty Position.located
@@ -222,12 +233,35 @@ and synth_field
   :  HopixTypes.typing_environment -> expression Position.located
   -> label Position.located -> ty Position.located list option -> HopixTypes.aty
   =
-  fun tenv expr lbl tlist -> failwith "Students! This is your job! (synth_field)"
-
+  fun tenv expr lbl tlist -> failwith "synth_field" (*let expr_type = synth_expression tenv expr in 
+  match expr_type with 
+  | ATyCon(cons,atlist) ->
+    (
+      (* Impossible car n'est pas dans le mli*)
+    let lbllist =  HopixTypes.lookup_information_of_type_constructor lbl.position cons tenv in 
+      match lbllist with 
+      | Record r ->
+        if List.mem lbl.value r 
+          then
+            let label_scheme =
+              try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
+        | HopixTypes.Unbound (pos, Label (LId i)) ->
+          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+      in
+        try HopixTypes.instantiate_type_scheme label_scheme atlist with
+        | HopixTypes.InvalidInstantiation { expected; given } ->
+          invalid_instantiation (Position.position expr) expected given
+        else 
+          failwith "Erreur de label"
+    )
+    | _ -> failwith "Ceci n'est pas un label"
+*)
 and synth_tuple
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv elist -> failwith "Students! This is your job! (synth_tuple)"
+  fun tenv elist -> let list_type = List.map(
+    fun x -> synth_expression tenv x
+  ) elist in HopixTypes.ATyTuple(list_type)
 
 and synth_sequence
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty

From 6bbb1f0996fb28d322fe31f3f8c4a73728df9aa2 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 19:45:57 +0100
Subject: [PATCH 41/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 51 ++++++++++++++++--------------
 1 file changed, 28 insertions(+), 23 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7bcb070..7a54b9f 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -90,16 +90,17 @@ and synth_pattern
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun env Position.{ value = p; position = pos } -> match p with
-    | PWildcard -> failwith "PWildcard"
-    | PLiteral l-> failwith "Pliteral"
-    | PVariable pv -> failwith "PVariable"
-    | PTypeAnnotation(p,ty) -> failwith "PTypeAnnot"
-    | PTuple(plist) -> failwith "PTuple"
-    | POr(plist) ->  failwith "POr"
-    | PAnd (plist) -> failwith "PAnd"
-    | PTaggedValue(cons,tlist,plist) -> failwith "PTagged"
-    | PRecord(plist,tlist) -> failwith "PRecord"
+  fun env Position.{ value = p; position = pos } ->
+  match p with
+  | PWildcard -> failwith "synth_pattern | PWildcard"
+  | PLiteral l -> failwith "synth_pattern | Pliteral"
+  | PVariable pv -> failwith "synth_pattern | PVariable"
+  | PTypeAnnotation (p, ty) -> failwith "synth_pattern | PTypeAnnot"
+  | PTuple plist -> failwith "synth_pattern | PTuple"
+  | POr plist -> failwith "synth_pattern | POr"
+  | PAnd plist -> failwith "synth_pattern | PAnd"
+  | PTaggedValue (cons, tlist, plist) -> failwith "synth_pattern | PTagged"
+  | PRecord (plist, tlist) -> failwith "synth_pattern | PRecord"
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located
@@ -214,10 +215,10 @@ and synth_fun
   :  HopixTypes.typing_environment -> pattern Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv pat expr -> 
-    let pat_type, tenv = synth_pattern tenv pat in
-    let expr_type = synth_expression tenv expr in 
-    ATyArrow(pat_type,expr_type) 
+  fun tenv pat expr ->
+  let pat_type, tenv = synth_pattern tenv pat in
+  let expr_type = synth_expression tenv expr in
+  ATyArrow (pat_type, expr_type)
 
 and synth_tannot
   :  HopixTypes.typing_environment -> expression Position.located -> ty Position.located
@@ -233,15 +234,18 @@ and synth_field
   :  HopixTypes.typing_environment -> expression Position.located
   -> label Position.located -> ty Position.located list option -> HopixTypes.aty
   =
-  fun tenv expr lbl tlist -> failwith "synth_field" (*let expr_type = synth_expression tenv expr in 
-  match expr_type with 
+  fun tenv expr lbl tlist ->
+  (* TODO *)
+  failwith "synth_field"
+(*let expr_type = synth_expression tenv expr in
+  match expr_type with
   | ATyCon(cons,atlist) ->
     (
       (* Impossible car n'est pas dans le mli*)
-    let lbllist =  HopixTypes.lookup_information_of_type_constructor lbl.position cons tenv in 
-      match lbllist with 
+    let lbllist =  HopixTypes.lookup_information_of_type_constructor lbl.position cons tenv in
+      match lbllist with
       | Record r ->
-        if List.mem lbl.value r 
+        if List.mem lbl.value r
           then
             let label_scheme =
               try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
@@ -251,17 +255,18 @@ and synth_field
         try HopixTypes.instantiate_type_scheme label_scheme atlist with
         | HopixTypes.InvalidInstantiation { expected; given } ->
           invalid_instantiation (Position.position expr) expected given
-        else 
+        else
           failwith "Erreur de label"
     )
     | _ -> failwith "Ceci n'est pas un label"
 *)
+
 and synth_tuple
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
   =
-  fun tenv elist -> let list_type = List.map(
-    fun x -> synth_expression tenv x
-  ) elist in HopixTypes.ATyTuple(list_type)
+  fun tenv elist ->
+  let list_type = List.map (fun x -> synth_expression tenv x) elist in
+  HopixTypes.ATyTuple list_type
 
 and synth_sequence
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty

From 624590e8492d1f8a3fc92bc2f85bc363552cb24c Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 20:27:51 +0100
Subject: [PATCH 42/58] wip: synth_field

---
 flap/src/hopix/hopixTypechecker.ml | 39 ++++++++++++------------------
 1 file changed, 15 insertions(+), 24 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7a54b9f..62f45b7 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -235,31 +235,22 @@ and synth_field
   -> label Position.located -> ty Position.located list option -> HopixTypes.aty
   =
   fun tenv expr lbl tlist ->
-  (* TODO *)
-  failwith "synth_field"
-(*let expr_type = synth_expression tenv expr in
+  let expr_type = synth_expression tenv expr in
   match expr_type with
-  | ATyCon(cons,atlist) ->
-    (
-      (* Impossible car n'est pas dans le mli*)
-    let lbllist =  HopixTypes.lookup_information_of_type_constructor lbl.position cons tenv in
-      match lbllist with
-      | Record r ->
-        if List.mem lbl.value r
-          then
-            let label_scheme =
-              try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
-        | HopixTypes.Unbound (pos, Label (LId i)) ->
-          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
-      in
-        try HopixTypes.instantiate_type_scheme label_scheme atlist with
-        | HopixTypes.InvalidInstantiation { expected; given } ->
-          invalid_instantiation (Position.position expr) expected given
-        else
-          failwith "Erreur de label"
-    )
-    | _ -> failwith "Ceci n'est pas un label"
-*)
+  | ATyCon (cons, atlist) ->
+    let label_scheme =
+      try HopixTypes.lookup_type_scheme_of_label lbl.position lbl.value tenv with
+      | HopixTypes.Unbound (pos, Label (LId i)) ->
+        HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+    in
+    let arrow =
+      try HopixTypes.instantiate_type_scheme label_scheme atlist with
+      | HopixTypes.InvalidInstantiation { expected; given } ->
+        invalid_instantiation (Position.position expr) expected given
+    in
+    (* TODO: On doit utiliser cons et tlist aussi *)
+    snd (HopixTypes.destruct_function_type lbl.position arrow)
+  | _ as x -> x
 
 and synth_tuple
   : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty

From a6f8ea69d0721a9dd4886acd5923d63f2600d2ea Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 20:39:55 +0100
Subject: [PATCH 43/58] ? j'en sais rien

---
 flap/src/hopix/hopixTypechecker.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 62f45b7..663e942 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -234,7 +234,7 @@ and synth_field
   :  HopixTypes.typing_environment -> expression Position.located
   -> label Position.located -> ty Position.located list option -> HopixTypes.aty
   =
-  fun tenv expr lbl tlist ->
+  fun tenv expr lbl _tlist ->
   let expr_type = synth_expression tenv expr in
   match expr_type with
   | ATyCon (cons, atlist) ->
@@ -248,7 +248,8 @@ and synth_field
       | HopixTypes.InvalidInstantiation { expected; given } ->
         invalid_instantiation (Position.position expr) expected given
     in
-    (* TODO: On doit utiliser cons et tlist aussi *)
+    (* Peut être inutile ? *)
+    let _ = HopixTypes.lookup_fields_of_type_constructor lbl.position cons tenv in
     snd (HopixTypes.destruct_function_type lbl.position arrow)
   | _ as x -> x
 

From ff8a7f9a31163a5fb6736d199cb1f72cebbb15e6 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 5 Dec 2023 20:48:26 +0100
Subject: [PATCH 44/58] ajout check_pattern_linearity

---
 flap/src/hopix/hopixTypechecker.ml | 34 +++++++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 5 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 7a54b9f..ff3dfb2 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -30,8 +30,32 @@ let check_equal_types pos ~expected ~given =
 let rec check_pattern_linearity
   : identifier list -> pattern Position.located -> identifier list
   =
-  fun vars Position.{ value; position } ->
-  failwith "Students! This is your job! (check_pattern_linearity)"
+  fun vars Position.{ value; position } -> match value with
+  | PWildcard -> vars
+  | PLiteral _ -> vars
+  | PVariable v -> linearity_variable v vars
+  | PTypeAnnotation(p,_) -> check_pattern_linearity vars p
+
+  (* Pour les deux matchs qui suivent, on fait la même chose : On regarde récursivement chaque pattern 
+     de chaque liste, et on effectue le check de linéarité pour chaque pattern. Seulement, pour PRecord qui est
+     un (label located * pattern located), on doit séparer en deux matchs distinct pour "ouvrir" la paire de PRecord *)
+  | PTaggedValue(_,_,plist) | PTuple(plist) | POr (plist) | PAnd (plist)
+  -> linearity_pattern_list plist vars
+  | PRecord(plist,_)
+  -> linearity_precord_list plist vars
+
+and linearity_variable v vars = 
+  if List.mem v.value vars then 
+    failwith "Il y a déjà une occurence de la variable dans le pattern"
+  else v.value::vars
+
+and linearity_pattern_list plist vars =
+  List.fold_left (fun vars pat -> check_pattern_linearity vars pat) vars plist
+
+and linearity_precord_list plist vars =
+  List.fold_left (fun vars (label,pat) -> check_pattern_linearity vars pat) vars plist
+  
+
 ;;
 
 (** Type-checking code *)
@@ -92,9 +116,9 @@ and synth_pattern
   =
   fun env Position.{ value = p; position = pos } ->
   match p with
-  | PWildcard -> failwith "synth_pattern | PWildcard"
-  | PLiteral l -> failwith "synth_pattern | Pliteral"
-  | PVariable pv -> failwith "synth_pattern | PVariable"
+  | PWildcard -> assert false
+  | PLiteral l -> synth_literal l.value, env
+  | PVariable pv -> assert false
   | PTypeAnnotation (p, ty) -> failwith "synth_pattern | PTypeAnnot"
   | PTuple plist -> failwith "synth_pattern | PTuple"
   | POr plist -> failwith "synth_pattern | POr"

From 1eab8ed491425b58b8d3d912b6ca2f4d056e75da Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 20:51:23 +0100
Subject: [PATCH 45/58] explicit types

---
 flap/src/hopix/hopixTypechecker.ml | 69 ++++++++++++++++++++++++++----
 1 file changed, 60 insertions(+), 9 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 663e942..1fa1029 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -92,15 +92,66 @@ and synth_pattern
   =
   fun env Position.{ value = p; position = pos } ->
   match p with
-  | PWildcard -> failwith "synth_pattern | PWildcard"
-  | PLiteral l -> failwith "synth_pattern | Pliteral"
-  | PVariable pv -> failwith "synth_pattern | PVariable"
-  | PTypeAnnotation (p, ty) -> failwith "synth_pattern | PTypeAnnot"
-  | PTuple plist -> failwith "synth_pattern | PTuple"
-  | POr plist -> failwith "synth_pattern | POr"
-  | PAnd plist -> failwith "synth_pattern | PAnd"
-  | PTaggedValue (cons, tlist, plist) -> failwith "synth_pattern | PTagged"
-  | PRecord (plist, tlist) -> failwith "synth_pattern | PRecord"
+  | PWildcard -> pattern_wildcard pos
+  | PLiteral l -> pattern_literal env l
+  | PVariable _ -> pattern_variable pos
+  | PTypeAnnotation (p, ty) -> pattern_tannot env p ty
+  | PTuple plist -> pattern_tuple env plist
+  | POr plist -> pattern_or env plist
+  | PAnd plist -> pattern_and env plist
+  | PTaggedValue (cons, tlist, plist) -> pattern_tagval env cons tlist plist
+  | PRecord (plist, tlist) -> pattern_record env plist tlist
+
+and pattern_wildcard : Position.t -> HopixTypes.aty * HopixTypes.typing_environment =
+  fun pos -> HopixTypes.type_error pos "No types found."
+
+and pattern_literal
+  :  HopixTypes.typing_environment -> HopixAST.literal Position.located
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv l -> failwith "synth_pattern | Pliteral"
+
+and pattern_variable : Position.t -> HopixTypes.aty * HopixTypes.typing_environment =
+  fun pos -> HopixTypes.type_error pos "No types found."
+
+and pattern_tannot
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
+  -> HopixAST.ty Position.located -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv p ty -> failwith "synth_pattern | PTypeAnnot"
+
+and pattern_tuple
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv plist -> failwith "synth_pattern | PTuple"
+
+and pattern_or
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv plist -> failwith "synth_pattern | POr"
+
+and pattern_and
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv plist -> failwith "synth_pattern | PAnd"
+
+and pattern_tagval
+  :  HopixTypes.typing_environment -> HopixAST.constructor Position.located
+  -> HopixAST.ty Position.located list option -> HopixAST.pattern Position.located list
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv cons tlist plist -> failwith "synth_pattern | PTagged"
+
+and pattern_record
+  :  HopixTypes.typing_environment
+  -> (HopixAST.label Position.located * HopixAST.pattern Position.located) list
+  -> HopixAST.ty Position.located list option
+  -> HopixTypes.aty * HopixTypes.typing_environment
+  =
+  fun tenv plist tlist -> failwith "synth_pattern | PRecord"
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located

From 4990e18caf5ee4af376b7d13ba4f165fbfaffe7f Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 5 Dec 2023 20:53:12 +0100
Subject: [PATCH 46/58] real conflict

---
 flap/src/hopix/hopixTypechecker.ml | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index b4c22d1..d4e2d71 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -116,17 +116,6 @@ and synth_pattern
   =
   fun env Position.{ value = p; position = pos } ->
   match p with
-<<<<<<< HEAD
-  | PWildcard -> assert false
-  | PLiteral l -> synth_literal l.value, env
-  | PVariable pv -> assert false
-  | PTypeAnnotation (p, ty) -> failwith "synth_pattern | PTypeAnnot"
-  | PTuple plist -> failwith "synth_pattern | PTuple"
-  | POr plist -> failwith "synth_pattern | POr"
-  | PAnd plist -> failwith "synth_pattern | PAnd"
-  | PTaggedValue (cons, tlist, plist) -> failwith "synth_pattern | PTagged"
-  | PRecord (plist, tlist) -> failwith "synth_pattern | PRecord"
-=======
   | PWildcard -> pattern_wildcard pos
   | PLiteral l -> pattern_literal env l
   | PVariable _ -> pattern_variable pos
@@ -187,7 +176,6 @@ and pattern_record
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
   fun tenv plist tlist -> failwith "synth_pattern | PRecord"
->>>>>>> 1eab8ed491425b58b8d3d912b6ca2f4d056e75da
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located

From cfbaa90ed9eff471eed4864831f1812cfb6cd5d3 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 20:58:36 +0100
Subject: [PATCH 47/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 36 +++++++++++++++++-------------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d4e2d71..74b98c8 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -30,32 +30,36 @@ let check_equal_types pos ~expected ~given =
 let rec check_pattern_linearity
   : identifier list -> pattern Position.located -> identifier list
   =
-  fun vars Position.{ value; position } -> match value with
+  fun vars Position.{ value; position = _ } ->
+  match value with
   | PWildcard -> vars
   | PLiteral _ -> vars
   | PVariable v -> linearity_variable v vars
-  | PTypeAnnotation(p,_) -> check_pattern_linearity vars p
+  | PTypeAnnotation (p, _) ->
+    (* Pour les deux matchs qui suivent, on fait la même chose :
+       On regarde récursivement chaque pattern de chaque liste, et on effectue le
+       check de linéarité pour chaque pattern.
 
-  (* Pour les deux matchs qui suivent, on fait la même chose : On regarde récursivement chaque pattern 
-     de chaque liste, et on effectue le check de linéarité pour chaque pattern. Seulement, pour PRecord qui est
-     un (label located * pattern located), on doit séparer en deux matchs distinct pour "ouvrir" la paire de PRecord *)
-  | PTaggedValue(_,_,plist) | PTuple(plist) | POr (plist) | PAnd (plist)
-  -> linearity_pattern_list plist vars
-  | PRecord(plist,_)
-  -> linearity_precord_list plist vars
+       Seulement, pour PRecord qui est un (label located * pattern located),
+       on doit séparer en deux matchs distinct pour "ouvrir" la paire de PRecord *)
+    check_pattern_linearity vars p
+  | PTaggedValue (_, _, plist) | PTuple plist | POr plist | PAnd plist ->
+    linearity_pattern_list plist vars
+  | PRecord (plist, _) -> linearity_precord_list plist vars
 
-and linearity_variable v vars = 
-  if List.mem v.value vars then 
-    failwith "Il y a déjà une occurence de la variable dans le pattern"
-  else v.value::vars
+and linearity_variable v vars =
+  if List.mem v.value vars
+  then
+    HopixTypes.type_error
+      v.position
+      "Il y a déjà une occurence de la variable dans le pattern"
+  else v.value :: vars
 
 and linearity_pattern_list plist vars =
   List.fold_left (fun vars pat -> check_pattern_linearity vars pat) vars plist
 
 and linearity_precord_list plist vars =
-  List.fold_left (fun vars (label,pat) -> check_pattern_linearity vars pat) vars plist
-  
-
+  List.fold_left (fun vars (_, pat) -> check_pattern_linearity vars pat) vars plist
 ;;
 
 (** Type-checking code *)

From fbd63b1c5db139f67b66bd519e400dcc39328260 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 5 Dec 2023 22:07:53 +0100
Subject: [PATCH 48/58] TypeAnnot

---
 flap/src/hopix/hopixTypechecker.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 74b98c8..38c7437 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -137,7 +137,7 @@ and pattern_literal
   :  HopixTypes.typing_environment -> HopixAST.literal Position.located
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv l -> failwith "synth_pattern | Pliteral"
+  fun tenv l -> synth_literal l.value, tenv
 
 and pattern_variable : Position.t -> HopixTypes.aty * HopixTypes.typing_environment =
   fun pos -> HopixTypes.type_error pos "No types found."
@@ -146,7 +146,13 @@ and pattern_tannot
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
   -> HopixAST.ty Position.located -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv p ty -> failwith "synth_pattern | PTypeAnnot"
+  fun tenv p ty -> 
+    let aty_of_ty = HopixTypes.internalize_ty tenv ty in 
+  match p.value with 
+  | PWildcard -> aty_of_ty, tenv
+  | PVariable i -> aty_of_ty,HopixTypes.bind_value i.value (HopixTypes.monomorphic_type_scheme aty_of_ty) tenv
+  | _ -> let pattern_type, tenv = synth_pattern tenv p in 
+  check_equal_types p.position ~expected:aty_of_ty ~given:pattern_type; pattern_type, tenv
 
 and pattern_tuple
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list

From 026805bd1250ca59d052bd80ed44fd6bb6264ed9 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Tue, 5 Dec 2023 23:03:03 +0100
Subject: [PATCH 49/58] =?UTF-8?q?ajout=20POr=20PAnd=20PTuple=20et=20d?=
 =?UTF-8?q?=C3=A9but=20PTagged?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 flap/src/hopix/hopixTypechecker.ml | 47 ++++++++++++++++++++++++++++--
 1 file changed, 44 insertions(+), 3 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 38c7437..1d4bd98 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -158,19 +158,40 @@ and pattern_tuple
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> failwith "synth_pattern | PTuple"
+  fun tenv plist -> let tys, tenv =
+  List.fold_left(
+    fun(tys,tenv) pat ->
+      let (ty,tenv) = synth_pattern tenv pat in
+      (ty::tys,tenv)
+  ) ([],tenv) plist in
+  HopixTypes.ATyTuple(List.rev tys), tenv
 
 and pattern_or
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> failwith "synth_pattern | POr"
+  fun tenv plist -> 
+    let ty', tenv' = synth_pattern tenv (List.hd (plist)) in 
+    let tenv = List.fold_left (
+      fun tenv pat ->
+        let pattern_type, tenv = synth_pattern tenv pat in
+        check_equal_types pat.position ~expected:pattern_type ~given:ty';tenv 
+    ) tenv' plist
+      in ty', tenv
 
+      (* TODO : Même code que pattern_or, à revoir ?*)
 and pattern_and
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> failwith "synth_pattern | PAnd"
+  fun tenv plist -> 
+    let ty', tenv' = synth_pattern tenv (List.hd (plist)) in 
+    let tenv = List.fold_left (
+      fun tenv pat ->
+        let pattern_type, tenv = synth_pattern tenv pat in
+        check_equal_types pat.position ~expected:pattern_type ~given:ty';tenv 
+    ) tenv' plist
+      in ty', tenv
 
 and pattern_tagval
   :  HopixTypes.typing_environment -> HopixAST.constructor Position.located
@@ -178,6 +199,25 @@ and pattern_tagval
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
   fun tenv cons tlist plist -> failwith "synth_pattern | PTagged"
+    (* TODO : à finir (trop fatigué sah): s'inspirer de ce qui a déjà été fait pour lex expressions.
+    let cons_scheme =
+    try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
+    | HopixTypes.Unbound (pos, Constructor (KId c)) ->
+      HopixTypes.type_error pos (Printf.sprintf "Unbound constructor `%s'." c)
+  in
+  let tys =
+    List.map
+      (fun x -> HopixTypes.internalize_ty tenv x)
+      (match tlist with
+       | Some t -> t
+       | None -> HopixTypes.type_error cons.position "No types found.")
+  in
+  let tcons =
+    try HopixTypes.instantiate_type_scheme cons_scheme tys with
+    | HopixTypes.InvalidInstantiation { expected; given } ->
+      invalid_instantiation cons.position expected given
+  in
+ *)
 
 and pattern_record
   :  HopixTypes.typing_environment
@@ -187,6 +227,7 @@ and pattern_record
   =
   fun tenv plist tlist -> failwith "synth_pattern | PRecord"
 
+
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located
   -> ty Position.located list option -> HopixTypes.aty

From e8c6f8da9b89d219b9426ef683b2bb58254797aa Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Tue, 5 Dec 2023 23:55:40 +0100
Subject: [PATCH 50/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 80 ++++++++++++++++++------------
 1 file changed, 47 insertions(+), 33 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 1d4bd98..0976d74 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -146,52 +146,67 @@ and pattern_tannot
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
   -> HopixAST.ty Position.located -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv p ty -> 
-    let aty_of_ty = HopixTypes.internalize_ty tenv ty in 
-  match p.value with 
+  fun tenv p ty ->
+  let aty_of_ty = HopixTypes.internalize_ty tenv ty in
+  match p.value with
   | PWildcard -> aty_of_ty, tenv
-  | PVariable i -> aty_of_ty,HopixTypes.bind_value i.value (HopixTypes.monomorphic_type_scheme aty_of_ty) tenv
-  | _ -> let pattern_type, tenv = synth_pattern tenv p in 
-  check_equal_types p.position ~expected:aty_of_ty ~given:pattern_type; pattern_type, tenv
+  | PVariable i ->
+    ( aty_of_ty
+    , HopixTypes.bind_value i.value (HopixTypes.monomorphic_type_scheme aty_of_ty) tenv )
+  | _ ->
+    let pattern_type, tenv = synth_pattern tenv p in
+    check_equal_types p.position ~expected:aty_of_ty ~given:pattern_type;
+    pattern_type, tenv
 
 and pattern_tuple
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> let tys, tenv =
-  List.fold_left(
-    fun(tys,tenv) pat ->
-      let (ty,tenv) = synth_pattern tenv pat in
-      (ty::tys,tenv)
-  ) ([],tenv) plist in
-  HopixTypes.ATyTuple(List.rev tys), tenv
+  fun tenv plist ->
+  let tys, tenv =
+    List.fold_left
+      (fun (tys, tenv) pat ->
+        let ty, tenv = synth_pattern tenv pat in
+        ty :: tys, tenv)
+      ([], tenv)
+      plist
+  in
+  HopixTypes.ATyTuple (List.rev tys), tenv
 
 and pattern_or
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> 
-    let ty', tenv' = synth_pattern tenv (List.hd (plist)) in 
-    let tenv = List.fold_left (
-      fun tenv pat ->
+  fun tenv plist ->
+  let ty', tenv' = synth_pattern tenv (List.hd plist) in
+  let tenv =
+    List.fold_left
+      (fun tenv pat ->
         let pattern_type, tenv = synth_pattern tenv pat in
-        check_equal_types pat.position ~expected:pattern_type ~given:ty';tenv 
-    ) tenv' plist
-      in ty', tenv
+        check_equal_types pat.position ~expected:pattern_type ~given:ty';
+        tenv)
+      tenv'
+      plist
+  in
+  ty', tenv
 
-      (* TODO : Même code que pattern_or, à revoir ?*)
+(* TODO : Même code que pattern_or, à revoir ? *)
 and pattern_and
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist -> 
-    let ty', tenv' = synth_pattern tenv (List.hd (plist)) in 
-    let tenv = List.fold_left (
-      fun tenv pat ->
+  fun tenv plist ->
+  let ty', tenv' = synth_pattern tenv (List.hd plist) in
+  let tenv =
+    List.fold_left
+      (fun tenv pat ->
         let pattern_type, tenv = synth_pattern tenv pat in
-        check_equal_types pat.position ~expected:pattern_type ~given:ty';tenv 
-    ) tenv' plist
-      in ty', tenv
+        check_equal_types pat.position ~expected:pattern_type ~given:ty';
+        tenv)
+      tenv'
+      plist
+  in
+  ty', tenv
 
 and pattern_tagval
   :  HopixTypes.typing_environment -> HopixAST.constructor Position.located
@@ -199,8 +214,9 @@ and pattern_tagval
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
   fun tenv cons tlist plist -> failwith "synth_pattern | PTagged"
-    (* TODO : à finir (trop fatigué sah): s'inspirer de ce qui a déjà été fait pour lex expressions.
-    let cons_scheme =
+(* (* TODO : à finir (trop fatigué sah):
+     s'inspirer de ce qui a déjà été fait pour lex expressions. *)
+  let cons_scheme =
     try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
     | HopixTypes.Unbound (pos, Constructor (KId c)) ->
       HopixTypes.type_error pos (Printf.sprintf "Unbound constructor `%s'." c)
@@ -216,8 +232,7 @@ and pattern_tagval
     try HopixTypes.instantiate_type_scheme cons_scheme tys with
     | HopixTypes.InvalidInstantiation { expected; given } ->
       invalid_instantiation cons.position expected given
-  in
- *)
+  in *)
 
 and pattern_record
   :  HopixTypes.typing_environment
@@ -227,7 +242,6 @@ and pattern_record
   =
   fun tenv plist tlist -> failwith "synth_pattern | PRecord"
 
-
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located
   -> ty Position.located list option -> HopixTypes.aty

From f9c8d3e2f9eaeb767edbb480b44a1aa8b49fa006 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Wed, 6 Dec 2023 09:51:18 +0100
Subject: [PATCH 51/58] synth_case

---
 flap/src/hopix/hopixTypechecker.ml | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 0976d74..b55c267 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -444,11 +444,30 @@ and synth_read
   let refty = synth_expression tenv ref in
   HopixTypes.destruct_reference_type ref.position refty
 
+and synth_branch
+  :  HopixTypes.typing_environment -> HopixTypes.aty -> branch Position.located
+  -> HopixTypes.aty option -> HopixTypes.aty option
+  =
+  fun tenv casety branch branchty ->
+  let (Branch (p, e)) = branch.value in
+  let given_case, tenv' = synth_pattern tenv p in
+  check_equal_types p.position ~expected:casety ~given:given_case;
+  let given_branch = synth_expression tenv' e in
+  (match branchty with
+   | None -> ()
+   | Some ty' -> check_equal_types e.position ~expected:ty' ~given:given_branch);
+  Some given_branch
+
 and synth_case
   :  HopixTypes.typing_environment -> expression Position.located
   -> branch Position.located list -> HopixTypes.aty
   =
-  fun tenv expr branches -> failwith "Students! This is your job! (synth_case)"
+  fun tenv expr branches ->
+  let casety = synth_expression tenv expr in
+  (* Test les branches *)
+  match List.fold_right (synth_branch tenv casety) branches None with
+  | Some branchesty -> branchesty
+  | None -> HopixTypes.type_error expr.position "No types found."
 
 and synth_ifthenelse
   :  HopixTypes.typing_environment -> expression Position.located

From c98eb70a06e7b48fd343953308a5a0ad5b81e1f0 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Wed, 6 Dec 2023 09:53:01 +0100
Subject: [PATCH 52/58] move synth_branch

---
 flap/src/hopix/hopixTypechecker.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index b55c267..d4037f4 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -444,6 +444,17 @@ and synth_read
   let refty = synth_expression tenv ref in
   HopixTypes.destruct_reference_type ref.position refty
 
+and synth_case
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> branch Position.located list -> HopixTypes.aty
+  =
+  fun tenv expr branches ->
+  let casety = synth_expression tenv expr in
+  (* Test les branches *)
+  match List.fold_right (synth_branch tenv casety) branches None with
+  | Some branchesty -> branchesty
+  | None -> HopixTypes.type_error expr.position "No types found."
+
 and synth_branch
   :  HopixTypes.typing_environment -> HopixTypes.aty -> branch Position.located
   -> HopixTypes.aty option -> HopixTypes.aty option
@@ -458,17 +469,6 @@ and synth_branch
    | Some ty' -> check_equal_types e.position ~expected:ty' ~given:given_branch);
   Some given_branch
 
-and synth_case
-  :  HopixTypes.typing_environment -> expression Position.located
-  -> branch Position.located list -> HopixTypes.aty
-  =
-  fun tenv expr branches ->
-  let casety = synth_expression tenv expr in
-  (* Test les branches *)
-  match List.fold_right (synth_branch tenv casety) branches None with
-  | Some branchesty -> branchesty
-  | None -> HopixTypes.type_error expr.position "No types found."
-
 and synth_ifthenelse
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> expression Position.located -> HopixTypes.aty

From 61bcf5809682e00d7d4eef834eaea179478faad0 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Wed, 6 Dec 2023 14:46:18 +0100
Subject: [PATCH 53/58] PTagged 72/111

---
 flap/src/hopix/hopixTypechecker.ml | 33 ++++++++++++++++++++++++++----
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d4037f4..fe5a885 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -213,9 +213,8 @@ and pattern_tagval
   -> HopixAST.ty Position.located list option -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv cons tlist plist -> failwith "synth_pattern | PTagged"
-(* (* TODO : à finir (trop fatigué sah):
-     s'inspirer de ce qui a déjà été fait pour lex expressions. *)
+  fun tenv cons tlist plist -> (*failwith "synth_pattern | PTagged"*)
+
   let cons_scheme =
     try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
     | HopixTypes.Unbound (pos, Constructor (KId c)) ->
@@ -232,7 +231,33 @@ and pattern_tagval
     try HopixTypes.instantiate_type_scheme cons_scheme tys with
     | HopixTypes.InvalidInstantiation { expected; given } ->
       invalid_instantiation cons.position expected given
-  in *)
+  in
+  let p_args, tenv = synth_list_pattern tenv plist in
+  (
+  let expected_args, result =
+    HopixTypes.destruct_function_type_maximally cons.position tcons
+  in
+  (try
+     List.iter2
+       (fun expected given -> check_equal_types cons.position ~expected ~given)
+       expected_args
+       p_args
+   with
+   | Invalid_argument _ ->
+     (* 35-bad *)
+     check_equal_types
+       cons.position
+       ~expected:result
+       ~given:(HopixTypes.ATyArrow (result, result)));
+  result
+  ),tenv
+
+and synth_list_pattern tenv = function
+| [] -> [], tenv
+| p :: plist ->
+  let ty, tenv = synth_pattern tenv p in 
+  let tys, tenv = synth_list_pattern tenv plist in
+  ty::tys, tenv
 
 and pattern_record
   :  HopixTypes.typing_environment

From 9168e114c003b0069258a0d60c12e8b175bbbd82 Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Wed, 6 Dec 2023 16:56:42 +0100
Subject: [PATCH 54/58] PRecord (marche pas)

---
 flap/src/hopix/hopixTypechecker.ml | 35 ++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index fe5a885..409bee1 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -213,7 +213,7 @@ and pattern_tagval
   -> HopixAST.ty Position.located list option -> HopixAST.pattern Position.located list
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv cons tlist plist -> (*failwith "synth_pattern | PTagged"*)
+  fun tenv cons tlist plist ->
 
   let cons_scheme =
     try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
@@ -265,7 +265,38 @@ and pattern_record
   -> HopixAST.ty Position.located list option
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist tlist -> failwith "synth_pattern | PRecord"
+  fun tenv plist tlist -> 
+    let label = fst(List.hd plist) in
+    let type_cons,_,labels = 
+    let LId label_name = label.value in
+    HopixTypes.lookup_type_constructor_of_label label.position label.value tenv
+   (* Printf.sprintf "erreur message ici"*)
+  
+  in
+  let tlist' =
+    match tlist with
+    | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
+    | None -> HopixTypes.type_error label.position "No types found."
+  in
+  List.iter
+    (fun (Position.{ position = label_pos; value = label_val }, pat) ->
+      let label_scheme =
+        try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
+        | HopixTypes.Unbound (pos, Label (LId i)) ->
+          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+      in
+      let arrow =
+        try HopixTypes.instantiate_type_scheme label_scheme tlist' with
+        | HopixTypes.InvalidInstantiation { expected; given } ->
+          invalid_instantiation (Position.position pat) expected given
+      in
+      let expected,_ = HopixTypes.destruct_function_type label_pos arrow in
+      let given,_ = synth_pattern tenv pat in
+      check_equal_types label_pos ~expected ~given)
+    plist;
+  ATyCon (type_cons, tlist'),tenv
+
+
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located

From e0bb403e111d203e0624977c0df44791597d09de Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Wed, 6 Dec 2023 17:23:45 +0100
Subject: [PATCH 55/58] correction Unbound PRecord

---
 flap/src/hopix/hopixTypechecker.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 409bee1..afab0d9 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -269,7 +269,10 @@ and pattern_record
     let label = fst(List.hd plist) in
     let type_cons,_,labels = 
     let LId label_name = label.value in
-    HopixTypes.lookup_type_constructor_of_label label.position label.value tenv
+    try HopixTypes.lookup_type_constructor_of_label label.position label.value tenv with
+    | HopixTypes.Unbound (pos, Label (LId i)) ->
+      HopixTypes.type_error pos (Printf.sprintf "There is no type definition for label `%s'." label_name )
+
    (* Printf.sprintf "erreur message ici"*)
   
   in

From 8b3a34ba2df1572a64ad43984ec5252fdecfaa4a Mon Sep 17 00:00:00 2001
From: Nicolas PENELOUX <nicolas.peneloux@free.fr>
Date: Wed, 6 Dec 2023 18:05:43 +0100
Subject: [PATCH 56/58] correction d'un bug

---
 flap/src/hopix/hopixTypechecker.ml | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index afab0d9..d5956e5 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -271,33 +271,32 @@ and pattern_record
     let LId label_name = label.value in
     try HopixTypes.lookup_type_constructor_of_label label.position label.value tenv with
     | HopixTypes.Unbound (pos, Label (LId i)) ->
-      HopixTypes.type_error pos (Printf.sprintf "There is no type definition for label `%s'." label_name )
-
-   (* Printf.sprintf "erreur message ici"*)
-  
+      HopixTypes.type_error pos (Printf.sprintf "There is no type definition for label `%s'." label_name )  
   in
   let tlist' =
     match tlist with
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
     | None -> HopixTypes.type_error label.position "No types found."
   in
-  List.iter
-    (fun (Position.{ position = label_pos; value = label_val }, pat) ->
+  let tenv = 
+  List.fold_left (
+    fun tenv (Position.{ position = label_pos; value = label_val }, pat) ->
       let label_scheme =
         try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
         | HopixTypes.Unbound (pos, Label (LId i)) ->
           HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
       in
-      let arrow =
+      let instance_type_scheme =
         try HopixTypes.instantiate_type_scheme label_scheme tlist' with
         | HopixTypes.InvalidInstantiation { expected; given } ->
           invalid_instantiation (Position.position pat) expected given
       in
-      let expected,_ = HopixTypes.destruct_function_type label_pos arrow in
-      let given,_ = synth_pattern tenv pat in
-      check_equal_types label_pos ~expected ~given)
-    plist;
-  ATyCon (type_cons, tlist'),tenv
+      let _,expected = HopixTypes.destruct_function_type label_pos instance_type_scheme in
+      let (given,tenv) = synth_pattern tenv pat in
+      check_equal_types label_pos ~expected ~given; tenv
+  ) tenv plist;
+    in 
+  ATyCon(type_cons, tlist'),tenv
 
 
 

From 1f1e58f84ff08dc0f80206ac12a2148bbaa3d291 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Wed, 6 Dec 2023 18:06:52 +0100
Subject: [PATCH 57/58] fmt

---
 flap/src/hopix/hopixTypechecker.ml | 102 +++++++++++++++--------------
 1 file changed, 52 insertions(+), 50 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index d5956e5..f4caabb 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -214,7 +214,6 @@ and pattern_tagval
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
   fun tenv cons tlist plist ->
-
   let cons_scheme =
     try HopixTypes.lookup_type_scheme_of_constructor cons.position cons.value tenv with
     | HopixTypes.Unbound (pos, Constructor (KId c)) ->
@@ -233,31 +232,30 @@ and pattern_tagval
       invalid_instantiation cons.position expected given
   in
   let p_args, tenv = synth_list_pattern tenv plist in
-  (
-  let expected_args, result =
-    HopixTypes.destruct_function_type_maximally cons.position tcons
-  in
-  (try
-     List.iter2
-       (fun expected given -> check_equal_types cons.position ~expected ~given)
-       expected_args
-       p_args
-   with
-   | Invalid_argument _ ->
-     (* 35-bad *)
-     check_equal_types
-       cons.position
-       ~expected:result
-       ~given:(HopixTypes.ATyArrow (result, result)));
-  result
-  ),tenv
+  ( (let expected_args, result =
+       HopixTypes.destruct_function_type_maximally cons.position tcons
+     in
+     (try
+        List.iter2
+          (fun expected given -> check_equal_types cons.position ~expected ~given)
+          expected_args
+          p_args
+      with
+      | Invalid_argument _ ->
+        (* 35-bad *)
+        check_equal_types
+          cons.position
+          ~expected:result
+          ~given:(HopixTypes.ATyArrow (result, result)));
+     result)
+  , tenv )
 
 and synth_list_pattern tenv = function
-| [] -> [], tenv
-| p :: plist ->
-  let ty, tenv = synth_pattern tenv p in 
-  let tys, tenv = synth_list_pattern tenv plist in
-  ty::tys, tenv
+  | [] -> [], tenv
+  | p :: plist ->
+    let ty, tenv = synth_pattern tenv p in
+    let tys, tenv = synth_list_pattern tenv plist in
+    ty :: tys, tenv
 
 and pattern_record
   :  HopixTypes.typing_environment
@@ -265,40 +263,44 @@ and pattern_record
   -> HopixAST.ty Position.located list option
   -> HopixTypes.aty * HopixTypes.typing_environment
   =
-  fun tenv plist tlist -> 
-    let label = fst(List.hd plist) in
-    let type_cons,_,labels = 
-    let LId label_name = label.value in
+  fun tenv plist tlist ->
+  let label = fst (List.hd plist) in
+  let type_cons, _, labels =
+    let (LId label_name) = label.value in
     try HopixTypes.lookup_type_constructor_of_label label.position label.value tenv with
     | HopixTypes.Unbound (pos, Label (LId i)) ->
-      HopixTypes.type_error pos (Printf.sprintf "There is no type definition for label `%s'." label_name )  
+      HopixTypes.type_error
+        pos
+        (Printf.sprintf "There is no type definition for label `%s'." label_name)
   in
   let tlist' =
     match tlist with
     | Some tlist -> List.map (fun t -> HopixTypes.internalize_ty tenv t) tlist
     | None -> HopixTypes.type_error label.position "No types found."
   in
-  let tenv = 
-  List.fold_left (
-    fun tenv (Position.{ position = label_pos; value = label_val }, pat) ->
-      let label_scheme =
-        try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
-        | HopixTypes.Unbound (pos, Label (LId i)) ->
-          HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
-      in
-      let instance_type_scheme =
-        try HopixTypes.instantiate_type_scheme label_scheme tlist' with
-        | HopixTypes.InvalidInstantiation { expected; given } ->
-          invalid_instantiation (Position.position pat) expected given
-      in
-      let _,expected = HopixTypes.destruct_function_type label_pos instance_type_scheme in
-      let (given,tenv) = synth_pattern tenv pat in
-      check_equal_types label_pos ~expected ~given; tenv
-  ) tenv plist;
-    in 
-  ATyCon(type_cons, tlist'),tenv
-
-
+  let tenv =
+    List.fold_left
+      (fun tenv (Position.{ position = label_pos; value = label_val }, pat) ->
+        let label_scheme =
+          try HopixTypes.lookup_type_scheme_of_label label_pos label_val tenv with
+          | HopixTypes.Unbound (pos, Label (LId i)) ->
+            HopixTypes.type_error pos (Printf.sprintf "Unbound label `%s'." i)
+        in
+        let instance_type_scheme =
+          try HopixTypes.instantiate_type_scheme label_scheme tlist' with
+          | HopixTypes.InvalidInstantiation { expected; given } ->
+            invalid_instantiation (Position.position pat) expected given
+        in
+        let _, expected =
+          HopixTypes.destruct_function_type label_pos instance_type_scheme
+        in
+        let given, tenv = synth_pattern tenv pat in
+        check_equal_types label_pos ~expected ~given;
+        tenv)
+      tenv
+      plist
+  in
+  ATyCon (type_cons, tlist'), tenv
 
 and synth_variable
   :  HopixTypes.typing_environment -> identifier Position.located

From bfb79a12ce2dd5d3630b5f2b0d1f0123c9cb4610 Mon Sep 17 00:00:00 2001
From: Mylloon <kennel.anri@tutanota.com>
Date: Wed, 6 Dec 2023 18:15:16 +0100
Subject: [PATCH 58/58] test-46

---
 flap/src/hopix/hopixTypechecker.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index f4caabb..d65a001 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -49,10 +49,12 @@ let rec check_pattern_linearity
 
 and linearity_variable v vars =
   if List.mem v.value vars
-  then
-    HopixTypes.type_error
-      v.position
-      "Il y a déjà une occurence de la variable dans le pattern"
+  then (
+    match v.value with
+    | Id i ->
+      HopixTypes.type_error
+        v.position
+        (Printf.sprintf "The variable %s has already appeared in this pattern." i))
   else v.value :: vars
 
 and linearity_pattern_list plist vars =