Skip to content

Commit

Permalink
Fix check of undeclared types in any operators
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
daniel-larraz committed Oct 4, 2024
1 parent 511202d commit e800fb4
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 1 deletion.
2 changes: 1 addition & 1 deletion src/lustre/typeCheckerContext.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)) ->
Expand Down
4 changes: 4 additions & 0 deletions tests/ounit/lustre/lustreTypeChecker/undeclared_type_06.lus
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
node N() returns (y: int);
let
y = any Foo;
tel
4 changes: 4 additions & 0 deletions tests/ounit/lustre/testLustreFrontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit e800fb4

Please sign in to comment.