Handle all user generated code errors in the type checker #885

Merged
ghallak merged 15 commits from ghallak/270 into master 2022-07-26 00:48:47 +09:00
5 changed files with 30 additions and 14 deletions
Showing only changes of commit a7602b1cae - Show all commits

View File

@ -1098,6 +1098,7 @@ check_typedef_sccs(Env, TypeMap, [{acyclic, Name} | SCCs], Acc) ->
case maps:get(Name, TypeMap, undefined) of case maps:get(Name, TypeMap, undefined) of
undefined -> check_typedef_sccs(Env, TypeMap, SCCs, Acc); %% Builtin type undefined -> check_typedef_sccs(Env, TypeMap, SCCs, Acc); %% Builtin type
{type_def, Ann, D, Xs, Def0} -> {type_def, Ann, D, Xs, Def0} ->
check_parameterizable(D, Xs),
Def = check_event(Env, Name, Ann, check_typedef(bind_tvars(Xs, Env), Def0)), Def = check_event(Env, Name, Ann, check_typedef(bind_tvars(Xs, Env), Def0)),
Acc1 = [{type_def, Ann, D, Xs, Def} | Acc], Acc1 = [{type_def, Ann, D, Xs, Def} | Acc],
Env1 = bind_type(Name, Ann, {Xs, Def}, Env), Env1 = bind_type(Name, Ann, {Xs, Def}, Env),
@ -1353,6 +1354,13 @@ check_fields(Env, TypeMap, RecTy, [{field_t, Ann, Id, Type} | Fields]) ->
Env1 = bind_field(name(Id), #field_info{ ann = Ann, kind = record, field_t = Type, record_t = RecTy }, Env), Env1 = bind_field(name(Id), #field_info{ ann = Ann, kind = record, field_t = Type, record_t = RecTy }, Env),
check_fields(Env1, TypeMap, RecTy, Fields). check_fields(Env1, TypeMap, RecTy, Fields).
check_parameterizable({id, Ann, "event"}, [_ | _]) ->
type_error({parameterized_event, Ann});
check_parameterizable({id, Ann, "state"}, [_ | _]) ->
type_error({parameterized_state, Ann});
check_parameterizable(_Name, _Xs) ->
ok.
check_event(Env, "event", Ann, Def) -> check_event(Env, "event", Ann, Def) ->
case Def of case Def of
{variant_t, Cons} -> {variant_t, Cons} ->
@ -3490,6 +3498,12 @@ mk_error({referencing_undefined_interface, InterfaceId}) ->
mk_error({missing_definition, Id}) -> mk_error({missing_definition, Id}) ->
Msg = io_lib:format("Missing definition of function `~s`", [name(Id)]), Msg = io_lib:format("Missing definition of function `~s`", [name(Id)]),
mk_t_err(pos(Id), Msg); mk_t_err(pos(Id), Msg);
mk_error({parameterized_state, Ann}) ->
Msg = "The state type cannot be parameterized",
mk_t_err(pos(Ann), Msg);
mk_error({parameterized_event, Ann}) ->
Msg = "The event type cannot be parameterized",
mk_t_err(pos(Ann), Msg);
mk_error(Err) -> mk_error(Err) ->
Msg = io_lib:format("Unknown error: ~p", [Err]), Msg = io_lib:format("Unknown error: ~p", [Err]),
mk_t_err(pos(0, 0), Msg). mk_t_err(pos(0, 0), Msg).

View File

@ -18,12 +18,6 @@ format({missing_init_function, Con}) ->
Msg = io_lib:format("Missing init function for the contract '~s'.", [pp_expr(Con)]), Msg = io_lib:format("Missing init function for the contract '~s'.", [pp_expr(Con)]),
Cxt = "The 'init' function can only be omitted if the state type is 'unit'.", Cxt = "The 'init' function can only be omitted if the state type is 'unit'.",
mk_err(pos(Con), Msg, Cxt); mk_err(pos(Con), Msg, Cxt);
format({parameterized_state, Decl}) ->
Msg = "The state type cannot be parameterized.",
mk_err(pos(Decl), Msg);
format({parameterized_event, Decl}) ->
Msg = "The event type cannot be parameterized.",
mk_err(pos(Decl), Msg);
format({invalid_entrypoint, Why, Ann, {id, _, Name}, Thing}) -> format({invalid_entrypoint, Why, Ann, {id, _, Name}, Thing}) ->
What = case Why of higher_order -> "higher-order (contains function types)"; What = case Why of higher_order -> "higher-order (contains function types)";
polymorphic -> "polymorphic (contains type variables)" end, polymorphic -> "polymorphic (contains type variables)" end,

View File

@ -973,7 +973,8 @@ failing_contracts() ->
"when checking the type of the pattern `r10 : rec_inv(Animal)` against the expected type `Main.rec_inv(Cat)`">>, "when checking the type of the pattern `r10 : rec_inv(Animal)` against the expected type `Main.rec_inv(Cat)`">>,
<<?Pos(41,13) <<?Pos(41,13)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the pattern `r11 : rec_inv(Cat)` against the expected type `Main.rec_inv(Animal)`">>]) "when checking the type of the pattern `r11 : rec_inv(Cat)` against the expected type `Main.rec_inv(Animal)`">>
])
, ?TYPE_ERROR(polymorphism_variance_switching_oracles, , ?TYPE_ERROR(polymorphism_variance_switching_oracles,
[<<?Pos(15,13) [<<?Pos(15,13)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
@ -1016,13 +1017,24 @@ failing_contracts() ->
"when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>, "when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>,
<<?Pos(44,13) <<?Pos(44,13)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the pattern `q15 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Cat, Animal)`">>]) "when checking the type of the pattern `q15 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Cat, Animal)`">>
])
, ?TYPE_ERROR(missing_definition, , ?TYPE_ERROR(missing_definition,
[<<?Pos(2,14) [<<?Pos(2,14)
"Missing definition of function `foo`">>]) "Missing definition of function `foo`">>
])
, ?TYPE_ERROR(child_with_decls, , ?TYPE_ERROR(child_with_decls,
[<<?Pos(2,14) [<<?Pos(2,14)
"Missing definition of function `f`">>]) "Missing definition of function `f`">>
])
, ?TYPE_ERROR(parameterised_state,
[<<?Pos(3,8)
"The state type cannot be parameterized">>
])
, ?TYPE_ERROR(parameterised_event,
[<<?Pos(3,12)
"The event type cannot be parameterized">>
])
]. ].
-define(Path(File), "code_errors/" ??File). -define(Path(File), "code_errors/" ??File).
@ -1042,10 +1054,6 @@ failing_code_gen_contracts() ->
, ?FATE_ERR(missing_init_function, 1, 10, , ?FATE_ERR(missing_init_function, 1, 10,
"Missing init function for the contract 'MissingInitFunction'.\n" "Missing init function for the contract 'MissingInitFunction'.\n"
"The 'init' function can only be omitted if the state type is 'unit'.") "The 'init' function can only be omitted if the state type is 'unit'.")
, ?FATE_ERR(parameterised_state, 3, 8,
"The state type cannot be parameterized.")
, ?FATE_ERR(parameterised_event, 3, 12,
"The event type cannot be parameterized.")
, ?FATE_ERR(polymorphic_aens_resolve, 4, 5, , ?FATE_ERR(polymorphic_aens_resolve, 4, 5,
"Invalid return type of AENS.resolve:\n" "Invalid return type of AENS.resolve:\n"
" 'a\n" " 'a\n"