From e800fb435de3ecf2e3d3e656d5d473d72ab622b2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 3 Oct 2024 22:07:36 -0500 Subject: [PATCH] Fix check of undeclared types in any operators Bug introduced in be290ed. Notice that desugaring of any operators occurs before type checking. Previous code, `SI.add id ty_vars`, does not work because it leads to incorrect positions being reported in error messages. --- src/lustre/typeCheckerContext.ml | 2 +- tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus | 4 ++++ tests/ounit/lustre/testLustreFrontend.ml | 4 ++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus diff --git a/src/lustre/typeCheckerContext.ml b/src/lustre/typeCheckerContext.ml index e5d34e2ea..e862b157b 100644 --- a/src/lustre/typeCheckerContext.ml +++ b/src/lustre/typeCheckerContext.ml @@ -807,7 +807,7 @@ and ty_vars_of_type ctx node_name ty = | UserType (_, ty_args, id) -> ( match lookup_ty_syn ctx id ty_args with | Some ty -> ty_vars_of_type ctx node_name ty - | None -> assert false + | None -> SI.empty ) | RefinementType (_, (_, _, ty), e) | ArrayType (_, (ty, e)) -> diff --git a/tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus b/tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus new file mode 100644 index 000000000..fe332fcec --- /dev/null +++ b/tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus @@ -0,0 +1,4 @@ +node N() returns (y: int); +let + y = any Foo; +tel \ No newline at end of file diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml index 13b34b1bc..66eda065c 100644 --- a/tests/ounit/lustre/testLustreFrontend.ml +++ b/tests/ounit/lustre/testLustreFrontend.ml @@ -599,6 +599,10 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [ match load_file "./lustreTypeChecker/undeclared_type_05.lus" with | Error (`LustreTypeCheckerError (_, UndeclaredType _)) -> true | _ -> false); + mk_test "test undeclared 6" (fun () -> + match load_file "./lustreTypeChecker/undeclared_type_06.lus" with + | Error (`LustreTypeCheckerError (_, UndeclaredType _)) -> true + | _ -> false); mk_test "test arity incorrect node call" (fun () -> match load_file "./lustreTypeChecker/arity_incorrect_node_call.lus" with | Error (`LustreTypeCheckerError (_, IlltypedCall _)) -> true