From 756dd13fece86697e0b170f864e35decccefea01 Mon Sep 17 00:00:00 2001 From: Thomas Wies Date: Thu, 21 Nov 2024 02:21:46 -0500 Subject: [PATCH] improve error message --- lib/ast/astDef.ml | 2 +- lib/frontend/typing.ml | 11 +++++++---- test/ci/front-end/fail/tuple.t | 5 ++++- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/lib/ast/astDef.ml b/lib/ast/astDef.ml index b8394aa..721e510 100644 --- a/lib/ast/astDef.ml +++ b/lib/ast/astDef.ml @@ -916,7 +916,7 @@ module Expr = struct let to_int expr = match expr with | App (Int i, _, _) -> Int.of_int64_exn i - | _ -> Error.error (to_loc expr) "Expected Int expression" + | _ -> Error.type_error (to_loc expr) "Expected Int constant" let unfold_tuple expr = match expr with diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml index 88f5818..fdcab5d 100644 --- a/lib/frontend/typing.ml +++ b/lib/frontend/typing.ml @@ -264,10 +264,13 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t (* backpropagate typ2 to expr1 if needed *) let expected_typ1 = let ty = match constr with - | TupleLookUp -> - let _lookup_type = Type.tuple_lookup typ1 (Expr.to_int expr2) in - (* above lookup checks well-formedness of typ1 *) - typ1 + | TupleLookUp -> + let idx = Expr.to_int expr2 in + begin match typ1 with + | App (Prod, ts, _) when idx < List.length ts && idx >= 0 -> typ1 + | App (Prod, _, _) -> Error.type_error (Expr.to_loc expr2) "Index out of bounds" + | App _ -> Error.type_error (Expr.to_loc expr1) "Expected product type" + end | MapLookUp -> Type.(map typ2 (Type.map_codom typ1)) | Diff | Union | Inter | Plus | Minus | Mult | Div | Mod | Subseteq | Eq | Gt | Lt | Geq | Leq -> diff --git a/test/ci/front-end/fail/tuple.t b/test/ci/front-end/fail/tuple.t index ea4c39a..974f20b 100644 --- a/test/ci/front-end/fail/tuple.t +++ b/test/ci/front-end/fail/tuple.t @@ -1,3 +1,6 @@ $ dune exec -- raven --shh ./tuple.rav - [Error] Index out of bounds + [Error] File "./tuple.rav", line 7, columns 20-22: + 7 | var zz: Int := x#2; + ^^ + Type Error: Index out of bounds. [1]