From 61bcf5809682e00d7d4eef834eaea179478faad0 Mon Sep 17 00:00:00 2001 From: Nicolas PENELOUX Date: Wed, 6 Dec 2023 14:46:18 +0100 Subject: [PATCH] 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