Merge branch 'jalon3'

flap/src/hopix/hopixTypechecker.ml

@@ -5,98 +5,618 @@ open HopixAST
 (** Error messages *)
 
 let invalid_instantiation pos given expected =
-  HopixTypes.type_error pos (
+  HopixTypes.type_error
-      Printf.sprintf
+    pos
-        "Invalid number of types in instantiation: \
+    (Printf.sprintf
-         %d given while %d were expected." given expected
+       "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
+    HopixTypes.(
-                  Printf.(sprintf
+      type_error
-                            "Type mismatch.\nExpected:\n  %s\nGiven:\n  %s"
+        pos
-                            (string_of_aty expected)
+        Printf.(
-                            (string_of_aty given)))
+          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
+  : identifier list -> pattern Position.located -> identifier list
-  = fun vars Position.{ value; position; } ->
+  =
-  failwith "Students! This is your job!"
+  fun vars Position.{ value; position = _ } ->
+  match value with
+  | PWildcard -> vars
+  | PLiteral _ -> vars
+  | PVariable v -> linearity_variable v vars
+  | 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.
+
+       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 (
+    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 =
+  List.fold_left (fun vars pat -> check_pattern_linearity vars pat) vars plist
+
+and linearity_precord_list plist vars =
+  List.fold_left (fun vars (_, pat) -> check_pattern_linearity vars pat) vars plist
+;;
 
 (** Type-checking code *)
 
-let check_type_scheme :
+let check_type_scheme
-      HopixTypes.typing_environment ->
+  :  HopixTypes.typing_environment -> Position.t -> HopixAST.type_scheme
-      Position.t ->
+  -> HopixTypes.aty_scheme * HopixTypes.typing_environment
-      HopixAST.type_scheme ->
+  =
-      HopixTypes.aty_scheme * HopixTypes.typing_environment
+  fun env pos (ForallTy (ts, ty)) ->
-  = fun env pos (ForallTy (ts, ty)) ->
+  let ts = List.map Position.value ts in
-  failwith "Students! This is your job!"
+  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 =
+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 ->
-  failwith "Students! This is your job!"
+  match l with
+  | LInt _ -> HopixTypes.hint
+  | LChar _ -> HopixTypes.hchar
+  | LString _ -> HopixTypes.hstring
 
-let rec check_pattern :
+and synth_pattern
-          HopixTypes.typing_environment ->
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
-          HopixAST.pattern Position.located ->
+  -> HopixTypes.aty * HopixTypes.typing_environment
-          HopixTypes.aty ->
+  =
-          HopixTypes.typing_environment
+  fun env Position.{ value = p; position = pos } ->
-  = fun env Position.({ value = p; position = pos; } as pat) expected ->
+  match p with
-  failwith "Students! This is your job!"
+  | 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 synth_pattern :
+and pattern_wildcard : Position.t -> HopixTypes.aty * HopixTypes.typing_environment =
-      HopixTypes.typing_environment ->
+  fun pos -> HopixTypes.type_error pos "No types found."
-      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 :
+and pattern_literal
-      HopixTypes.typing_environment ->
+  :  HopixTypes.typing_environment -> HopixAST.literal Position.located
-      HopixAST.expression Position.located ->
+  -> HopixTypes.aty * HopixTypes.typing_environment
-      HopixTypes.aty
+  =
-  = fun env Position.{ value = e; position = pos; } ->
+  fun tenv l -> synth_literal l.value, tenv
-  failwith "Students! This is your job!"
 
-and check_expression :
+and pattern_variable : Position.t -> HopixTypes.aty * HopixTypes.typing_environment =
-      HopixTypes.typing_environment ->
+  fun pos -> HopixTypes.type_error pos "No types found."
-      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 :
+and pattern_tannot
-      HopixTypes.typing_environment ->
+  :  HopixTypes.typing_environment -> HopixAST.pattern Position.located
-      HopixAST.value_definition ->
+  -> HopixAST.ty Position.located -> HopixTypes.aty * HopixTypes.typing_environment
-      HopixTypes.typing_environment
+  =
-  = fun env def ->
+  fun tenv p ty ->
-  failwith "Students! This is your job!"
+  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
+  -> 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
+
+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 ->
+        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 ->
+  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
+  -> HopixAST.ty Position.located list option -> HopixAST.pattern Position.located list
+  -> 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)) ->
+      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
+  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
+  -> (HopixAST.label Position.located * HopixAST.pattern Position.located) list
+  -> 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
+    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)
+  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
+
+and synth_variable
+  :  HopixTypes.typing_environment -> identifier Position.located
+  -> ty Position.located list option -> HopixTypes.aty
+  =
+  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 "Unbound identifier `%s'." i)
+  in
+  match tlist with
+  | None -> HopixTypes.instantiate_type_scheme ty []
+  | 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
+  -> ty Position.located list option -> expression Position.located list -> HopixTypes.aty
+  =
+  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 found.")
+  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
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv f x ->
+  let f_type = synth_expression tenv f in
+  match f_type with
+  | HopixTypes.ATyArrow (expected, droit) ->
+    (*  a' -> b' *)
+    let given = synth_expression tenv x in
+    check_equal_types x.position ~expected ~given;
+    droit
+  | _ -> HopixTypes.type_error f.position "Can't 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 ->
+  (* Translate the types *)
+  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 found."
+  in
+  (* 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
+  :  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)
+
+and synth_tannot
+  :  HopixTypes.typing_environment -> expression Position.located -> ty Position.located
+  -> HopixTypes.aty
+  =
+  fun tenv expr ty ->
+  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'
+
+and synth_field
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> label Position.located -> ty Position.located list option -> HopixTypes.aty
+  =
+  fun tenv expr lbl _tlist ->
+  let expr_type = synth_expression tenv expr in
+  match expr_type with
+  | 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
+    (* 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
+
+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
+
+and synth_sequence
+  : HopixTypes.typing_environment -> expression Position.located list -> HopixTypes.aty
+  =
+  fun tenv elist ->
+  match elist with
+  | [] -> HopixTypes.type_error Position.dummy "Invalid sequence."
+  | [ x ] -> synth_expression tenv x
+  | x :: l ->
+    let given = synth_expression tenv x in
+    check_equal_types x.position ~expected:HopixTypes.hunit ~given;
+    synth_sequence tenv l
+
+and synth_define
+  :  HopixTypes.typing_environment -> value_definition -> expression Position.located
+  -> HopixTypes.aty
+  =
+  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
+  =
+  fun tenv expr -> HopixTypes.href (synth_expression tenv expr)
+
+and synth_assign
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  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
+  =
+  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
+  -> 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
+  =
+  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_ifthenelse
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ecase eif eelse ->
+  (* Pas testé !! *)
+  let ecasety = synth_expression tenv ecase in
+  check_equal_types ecase.position ~expected:HopixTypes.hbool ~given:ecasety;
+  let eifty = synth_expression tenv eif in
+  check_equal_types eif.position ~expected:HopixTypes.hunit ~given:eifty;
+  let eelsety = synth_expression tenv eelse in
+  check_equal_types eelse.position ~expected:HopixTypes.hunit ~given:eelsety;
+  HopixTypes.hunit
+
+and synth_while
+  :  HopixTypes.typing_environment -> expression Position.located
+  -> expression Position.located -> HopixTypes.aty
+  =
+  fun tenv ecase c ->
+  let ecasety = synth_expression tenv ecase in
+  check_equal_types ecase.position ~expected:HopixTypes.hbool ~given:ecasety;
+  let exprty = synth_expression tenv c in
+  check_equal_types c.position ~expected:HopixTypes.hunit ~given:exprty;
+  HopixTypes.hunit
+
+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 ->
+  let estart_ty = synth_expression tenv estart in
+  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:HopixTypes.hint ~given:eend_ty;
+  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:HopixTypes.hunit ~given:e_ty;
+  HopixTypes.hunit
+
+and check_expression
+  :  HopixTypes.typing_environment -> HopixAST.expression Position.located
+  -> HopixTypes.aty -> unit
+  =
+  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
+  -> HopixTypes.typing_environment
+  =
+  fun env -> function
+  | SimpleValue (id, ty, ex) ->
+    (match ty with
+     | 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 []);
+       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 *)
+    failwith "Students! This is your job! (check_value_definition | RecFunctions)"
+;;
 
 let check_definition env = function
-  | DefineValue vdef ->
+  | DefineValue vdef -> check_value_definition env vdef
-     check_value_definition env vdef
-
   | DefineType (t, ts, tdef) ->
-     let ts = List.map Position.value ts in
+    let ts = List.map Position.value ts in
-     HopixTypes.bind_type_definition (Position.value t) ts tdef env
+    HopixTypes.bind_type_definition (Position.value t) ts tdef env
-
   | DeclareExtern (x, tys) ->
-     let tys, _ = Position.located_pos (check_type_scheme env) tys in
+    let tys, _ = Position.located_pos (check_type_scheme env) tys in
-     HopixTypes.bind_value (Position.value x) tys env
+    HopixTypes.bind_value (Position.value x) tys env
+;;
 
 let typecheck env program =
-  List.fold_left
+  List.fold_left (fun env d -> Position.located (check_definition env) d) env program
-    (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