synth_tagged - pire implémentation ever

This commit is contained in:
Mylloon 2023-12-05 13:51:59 +01:00
parent 9e7de664e7
commit a90e8176e6
Signed by: Anri
GPG key ID: A82D63DFF8D1317F

View file

@ -117,7 +117,41 @@ and synth_tagged
: HopixTypes.typing_environment -> constructor Position.located : HopixTypes.typing_environment -> constructor Position.located
-> ty Position.located list option -> expression Position.located list -> HopixTypes.aty -> 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 and synth_apply
: HopixTypes.typing_environment -> expression Position.located : HopixTypes.typing_environment -> expression Position.located