From 9fd690dd5b7732df9da15a82265bb0f96490cd6d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 6 Dec 2024 22:28:59 +0000 Subject: [PATCH] TC: Fix missing location on generated guards --- src/lib/type_check.ml | 20 ++++++++++++++++--- src/lib/type_error.ml | 9 ++++++--- test/typecheck/pass/existential_ast/v1.expect | 2 +- test/typecheck/pass/existential_ast/v2.expect | 2 +- test/typecheck/pass/poly_vector/v1.expect | 2 +- test/typecheck/pass/reg_32_64/v3.expect | 2 +- 6 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index d36c3cec9..ac3c56ec1 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -2254,10 +2254,14 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au let inferred_exp = infer_funapp l env f [x; y] uannot (Some typ) in expect_subtype env inferred_exp typ | Some _ -> - let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in + let inferred_exp = + infer_funapp l env f [x; mk_exp ~loc:(exp_loc y) (E_typ (bool_typ, y))] uannot (Some typ) + in expect_subtype env inferred_exp typ | exception Type_error _ -> - let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in + let inferred_exp = + infer_funapp l env f [x; mk_exp ~loc:(exp_loc y) (E_typ (bool_typ, y))] uannot (Some typ) + in expect_subtype env inferred_exp typ end | E_app (f, xs), _ -> @@ -2550,12 +2554,22 @@ and check_case env pat_typ pexp typ = let env = bind_pattern_vector_subranges pat env in match bind_pat env pat pat_typ with | tpat, env, guards -> + let hint_loc l = + match guard with + | None -> Parse_ast.Hint ("guard created for this pattern", pat_loc pat, l) + | Some exp -> Parse_ast.Hint ("combining pattern with guard", exp_loc exp, l) + in let guard = match (guard, guards) with None, h :: t -> Some (h, t) | Some x, l -> Some (x, l) | None, [] -> None in let guard = match guard with - | Some (h, t) -> Some (List.fold_left (fun acc guard -> mk_exp (E_app_infix (acc, mk_id "&", guard))) h t) + | Some (h, t) -> + Some + (List.fold_left + (fun acc guard -> mk_exp ~loc:(hint_loc (exp_loc guard)) (E_app_infix (acc, mk_id "&", guard))) + h t + ) | None -> None in let checked_guard, env' = diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml index cb4a5438c..284fcb579 100644 --- a/src/lib/type_error.ml +++ b/src/lib/type_error.ml @@ -277,9 +277,12 @@ let message_of_type_error type_error = (Seq [msg; Line ""; Location (prefix, hint', l', msg')], hint) ) | Err_other str -> ((if str = "" then Seq [] else Line str), None) - | Err_function_arg (_, typ, err) -> - let msg, _ = to_message err in - (msg, Some ("checking function argument has type " ^ string_of_typ typ)) + | Err_function_arg (_, typ, err) -> ( + let msg, hint = to_message err in + match hint with + | None -> (msg, Some ("checking function argument has type " ^ string_of_typ typ)) + | Some _ -> (msg, hint) + ) | Err_unbound_id { id; locals; have_function } -> let name = string_of_id id in let closest = find_closest name (fun callback -> Bindings.iter (fun other_id _ -> callback other_id) locals) in diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect index aa05a8d3c..22c16ebe1 100644 --- a/test/typecheck/pass/existential_ast/v1.expect +++ b/test/typecheck/pass/existential_ast/v1.expect @@ -7,5 +7,5 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}. Type error: pass/existential_ast/v1.sail:46.7-21: 46 | Some(Ctor2(y, x, c)) -  | ^------------^ checking function argument has type ast +  | ^------------^ checking function argument has type (range(0, 31), int('ex192#), bitvector(4))  | range(0, 31) is not contained within range(0, 31) diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect index e768a5be3..1c6624ae4 100644 --- a/test/typecheck/pass/existential_ast/v2.expect +++ b/test/typecheck/pass/existential_ast/v2.expect @@ -7,5 +7,5 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}. Type error: pass/existential_ast/v2.sail:39.7-21: 39 | Some(Ctor2(y, x, c)) -  | ^------------^ checking function argument has type ast +  | ^------------^ checking function argument has type (range(0, 30), int('ex192#), bitvector(4))  | range(0, 30) is not contained within range(0, 30) diff --git a/test/typecheck/pass/poly_vector/v1.expect b/test/typecheck/pass/poly_vector/v1.expect index 835e1980f..1ee472b58 100644 --- a/test/typecheck/pass/poly_vector/v1.expect +++ b/test/typecheck/pass/poly_vector/v1.expect @@ -1,5 +1,5 @@ Type error: pass/poly_vector/v1.sail:17.5-24: 17 | if my_length(xs) == 32 then { -  | ^-----------------^ checking function argument has type int('n) +  | ^-----------------^ checking function argument has type vector('n, 'a)  | Type mismatch between vector('n, 'a) and bitvector(32) diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect index 1d143c412..66146793a 100644 --- a/test/typecheck/pass/reg_32_64/v3.expect +++ b/test/typecheck/pass/reg_32_64/v3.expect @@ -7,7 +7,7 @@ Explicit effect annotations are deprecated. They are no longer used and can be r Type error: pass/reg_32_64/v3.sail:29.2-27: 29 | reg_deref(R)['d - 1 .. 0] -  | ^-----------------------^ checking function argument has type int('m) +  | ^-----------------------^ (operator -)  | No overloading for (operator -), tried:  | * sub_atom  | pass/reg_32_64/v3.sail:29.15-17: