From a01eba04e3138f1581724a634f4d440bfaffc3cb Mon Sep 17 00:00:00 2001 From: Mylloon Date: Mon, 4 Dec 2023 17:47:16 +0100 Subject: [PATCH 1/3] 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 1edd925ed580bd5fe4d42052933cb0575dc0bf37 Mon Sep 17 00:00:00 2001 From: Mylloon Date: Mon, 4 Dec 2023 18:33:56 +0100 Subject: [PATCH 2/3] 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 Date: Mon, 4 Dec 2023 18:38:57 +0100 Subject: [PATCH 3/3] 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