From 8475b024dff98b40b709225ededb46e883cec61b Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sat, 6 May 2023 14:07:14 +0300 Subject: [PATCH] Break the dependecy between constraints and env --- src/aeso_ast_infer_types.erl | 65 ++++++++++++++++++++- src/aeso_tc_constraints.erl | 56 ++++++++++++++++-- src/aeso_tc_env.erl | 110 ----------------------------------- 3 files changed, 113 insertions(+), 118 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index e9a5971..b203593 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -73,6 +73,9 @@ potential_unused_variables(A, B, C) -> aeso_tc_warnings:potential_unused_variabl potential_unused_function(A, B, C, D) -> aeso_tc_warnings:potential_unused_function(A, B, C, D). mk_warning(A) -> aeso_tc_warnings:mk_warning(A). used_stateful(A) -> aeso_tc_warnings:used_stateful(A). +used_variable(A, B, C) -> aeso_tc_warnings:used_variable(A, B, C). +register_function_call(A, B) -> aeso_tc_warnings:register_function_call(A, B). +used_constant(A, B) -> aeso_tc_warnings:used_constant(A, B). warn_potential_negative_spend(A, B, C) -> aeso_tc_warnings:warn_potential_negative_spend(A, B, C). warn_potential_division_by_zero(A, B, C) -> aeso_tc_warnings:warn_potential_division_by_zero(A, B, C). potential_unused_return_value(A) -> aeso_tc_warnings:potential_unused_return_value(A). @@ -1060,10 +1063,10 @@ infer_expr(_Env, Body={id, As, "???"}) -> type_error({hole_found, As, T}), {typed, As, Body, T}; infer_expr(Env, Id = {Tag, As, _}) when Tag == id; Tag == qid -> - {QName, Type} = aeso_tc_env:lookup_name(Env, As, Id), + {QName, Type} = lookup_name(Env, As, Id), {typed, As, QName, Type}; infer_expr(Env, Id = {Tag, As, _}) when Tag == con; Tag == qcon -> - {QName, Type} = aeso_tc_env:lookup_name(Env, As, Id, [freshen]), + {QName, Type} = lookup_name(Env, As, Id, [freshen]), {typed, As, QName, Type}; infer_expr(Env, {tuple, As, Cpts}) -> NewCpts = [infer_expr(Env, C) || C <- Cpts], @@ -1582,3 +1585,61 @@ get_oracle_type({qid, _, ["Oracle", "check"]}, [OType| _], _ ) -> OTyp get_oracle_type({qid, _, ["Oracle", "check_query"]}, [OType| _], _ ) -> OType; get_oracle_type({qid, _, ["Oracle", "respond"]}, [OType| _], _ ) -> OType; get_oracle_type(_Fun, _Args, _Ret) -> false. + +lookup_name(Env, As, Name) -> + lookup_name(Env, As, Name, []). + +lookup_name(Env, As, Id, Options) -> + case aeso_tc_env:lookup_env(Env, term, As, qname(Id)) of + false -> + type_error({unbound_variable, Id}), + {Id, fresh_uvar(As)}; + {QId, {_, Ty}} -> + NS = aeso_tc_env:namespace(Env), + CurFn = aeso_tc_env:current_function(Env), + %% Variables and functions cannot be used when CurFn is `none`. + %% i.e. they cannot be used in toplevel constants + [ begin + when_warning( + warn_unused_variables, + fun() -> used_variable(NS, name(CurFn), QId) end), + when_warning( + warn_unused_functions, + fun() -> register_function_call(NS ++ qname(CurFn), QId) end) + end || CurFn =/= none ], + + when_warning(warn_unused_constants, fun() -> used_constant(NS, QId) end), + + Freshen = proplists:get_value(freshen, Options, false), + check_stateful(Env, Id, Ty), + Ty1 = case Ty of + {type_sig, _, _, _, _, _} -> aeso_tc_constraints:freshen_type_sig(As, Ty); + _ when Freshen -> aeso_tc_constraints:freshen_type(As, Ty); + _ -> Ty + end, + {set_qname(QId, Id), Ty1} + end. + +check_stateful(Env, Id, Type = {type_sig, _, _, _, _, _}) -> + IsStatefulType = aeso_syntax:get_ann(stateful, Type, false), + IsStatefulType andalso (check_stateful_not_in_guard(Env, Id) andalso check_stateful_in_stateful_fun(Env, Id)), + ok; + check_stateful(Env, _Id, _Type) -> + when_warning(warn_unused_stateful, fun() -> used_stateful(aeso_tc_env:current_function(Env)) end), + ok. + + check_stateful_not_in_guard(Env, Id) -> + case aeso_tc_env:in_guard(Env) of + false -> true; + true -> + type_error({stateful_not_allowed_in_guards, Id}), + false + end. + + check_stateful_in_stateful_fun(Env, Id) -> + case aeso_tc_env:stateful(Env) of + true -> true; + false -> + type_error({stateful_not_allowed, Id, aeso_tc_env:current_function(Env)}), + false + end. diff --git a/src/aeso_tc_constraints.erl b/src/aeso_tc_constraints.erl index fcf5ec4..b20a011 100644 --- a/src/aeso_tc_constraints.erl +++ b/src/aeso_tc_constraints.erl @@ -13,6 +13,8 @@ , add_field_constraint/5 , add_dependent_type_constraint/5 , add_record_create_constraint/3 + , freshen_type/2 + , freshen_type_sig/2 ]). %% -- Duplicated types ------------------------------------------------------- @@ -51,12 +53,6 @@ is_first_order(A) -> aeso_tc_type_utils:is_first_order(A). app_t(A, B, C) -> aeso_tc_type_utils:app_t(A, B, C). fresh_uvar(A) -> aeso_tc_type_utils:fresh_uvar(A). -%% ------- - -freshen(A) -> aeso_tc_env:freshen(A). -create_freshen_tvars() -> aeso_tc_env:create_freshen_tvars(). -destroy_freshen_tvars() -> aeso_tc_env:destroy_freshen_tvars(). - %% --------------------------------------------------------------------------- -type env() :: aeso_tc_env:env(). @@ -555,3 +551,51 @@ solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) -> {StillPossible, _} -> {ambiguous_record, Fields, StillPossible} end. + +create_freshen_tvars() -> + aeso_tc_ets_manager:ets_new(freshen_tvars, [set]). + +destroy_freshen_tvars() -> + aeso_tc_ets_manager:ets_delete(freshen_tvars). + +freshen(Type) -> + freshen(aeso_syntax:get_ann(Type), Type). + +freshen(Ann, {tvar, _, Name}) -> + NewT = case aeso_tc_ets_manager:ets_lookup(freshen_tvars, Name) of + [] -> fresh_uvar(Ann); + [{Name, T}] -> T + end, + aeso_tc_ets_manager:ets_insert(freshen_tvars, {Name, NewT}), + NewT; +freshen(Ann, {bytes_t, _, any}) -> + X = fresh_uvar(Ann), + aeso_tc_constraints:add_is_bytes_constraint(X), + X; +freshen(Ann, T) when is_tuple(T) -> + list_to_tuple(freshen(Ann, tuple_to_list(T))); +freshen(Ann, [A | B]) -> + [freshen(Ann, A) | freshen(Ann, B)]; +freshen(_, X) -> + X. + +freshen_type(Ann, Type) -> + create_freshen_tvars(), + Type1 = freshen(Ann, Type), + destroy_freshen_tvars(), + Type1. + +freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) -> + FunT = freshen_type(Ann, aeso_tc_type_utils:typesig_to_fun_t(TypeSig)), + apply_typesig_constraint(Ann, Constr, FunT), + FunT. + +apply_typesig_constraint(_Ann, none, _FunT) -> ok; +apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) -> + aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann}); +apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) -> + aeso_tc_constraints:add_add_bytes_constraint(Ann, concat, A, B, C); +apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) -> + aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C); +apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) -> + aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}). diff --git a/src/aeso_tc_env.erl b/src/aeso_tc_env.erl index 92dc276..c76ce9d 100644 --- a/src/aeso_tc_env.erl +++ b/src/aeso_tc_env.erl @@ -54,8 +54,6 @@ ]). -export([ lookup_env/4 - , lookup_name/3 - , lookup_name/4 , lookup_type/2 , lookup_record_field/2 , lookup_record_field/3 @@ -68,13 +66,6 @@ , empty_env/0 ]). -%% Freshening --export([ fresh_uvar/1 - , freshen/1 - , create_freshen_tvars/0 - , destroy_freshen_tvars/0 - ]). - -export([destroy_and_report_type_errors/1]). -export_type([env/0]). @@ -153,7 +144,6 @@ name(A) -> aeso_tc_name_manip:name(A). qname(A) -> aeso_tc_name_manip:qname(A). qid(A, B) -> aeso_tc_name_manip:qid(A, B). qcon(A, B) -> aeso_tc_name_manip:qcon(A, B). -set_qname(A, B) -> aeso_tc_name_manip:set_qname(A, B). %% ------- @@ -163,10 +153,6 @@ type_error(A) -> aeso_tc_errors:type_error(A). warn_potential_shadowing(A, B, C) -> aeso_tc_warnings:warn_potential_shadowing(A, B, C). used_include(A) -> aeso_tc_warnings:used_include(A). -used_variable(A, B, C) -> aeso_tc_warnings:used_variable(A, B, C). -used_stateful(A) -> aeso_tc_warnings:used_stateful(A). -register_function_call(A, B) -> aeso_tc_warnings:register_function_call(A, B). -used_constant(A, B) -> aeso_tc_warnings:used_constant(A, B). %% ------- @@ -581,54 +567,6 @@ lookup_env1(#env{ namespace = Current, used_namespaces = UsedNamespaces, scopes end end. -lookup_name(Env, As, Name) -> - lookup_name(Env, As, Name, []). - -lookup_name(Env = #env{ namespace = NS, current_function = CurFn }, As, Id, Options) -> - case lookup_env(Env, term, As, qname(Id)) of - false -> - type_error({unbound_variable, Id}), - {Id, fresh_uvar(As)}; - {QId, {_, Ty}} -> - %% Variables and functions cannot be used when CurFn is `none`. - %% i.e. they cannot be used in toplevel constants - [ begin - when_warning( - warn_unused_variables, - fun() -> used_variable(NS, name(CurFn), QId) end), - when_warning( - warn_unused_functions, - fun() -> register_function_call(NS ++ qname(CurFn), QId) end) - end || CurFn =/= none ], - - when_warning(warn_unused_constants, fun() -> used_constant(NS, QId) end), - - Freshen = proplists:get_value(freshen, Options, false), - check_stateful(Env, Id, Ty), - Ty1 = case Ty of - {type_sig, _, _, _, _, _} -> freshen_type_sig(As, Ty); - _ when Freshen -> freshen_type(As, Ty); - _ -> Ty - end, - {set_qname(QId, Id), Ty1} - end. - -check_stateful(#env{ in_guard = true }, Id, Type = {type_sig, _, _, _, _, _}) -> - case aeso_syntax:get_ann(stateful, Type, false) of - false -> ok; - true -> - type_error({stateful_not_allowed_in_guards, Id}) - end; -check_stateful(#env{ stateful = false, current_function = Fun }, Id, Type = {type_sig, _, _, _, _, _}) -> - case aeso_syntax:get_ann(stateful, Type, false) of - false -> ok; - true -> - type_error({stateful_not_allowed, Id, Fun}) - end; -check_stateful(#env{ current_function = Fun }, _Id, _Type) -> - when_warning(warn_unused_stateful, fun() -> used_stateful(Fun) end), - ok. - -spec lookup_record_field(env(), name()) -> [field_info()]. lookup_record_field(Env, FieldName) -> maps:get(FieldName, Env#env.fields, []). @@ -1001,51 +939,3 @@ unqualify1(NS, Xs) -> _ -> Xs catch _:_ -> Xs end. - -create_freshen_tvars() -> - aeso_tc_ets_manager:ets_new(freshen_tvars, [set]). - -destroy_freshen_tvars() -> - aeso_tc_ets_manager:ets_delete(freshen_tvars). - -freshen_type(Ann, Type) -> - create_freshen_tvars(), - Type1 = freshen(Ann, Type), - destroy_freshen_tvars(), - Type1. - -freshen(Type) -> - freshen(aeso_syntax:get_ann(Type), Type). - -freshen(Ann, {tvar, _, Name}) -> - NewT = case aeso_tc_ets_manager:ets_lookup(freshen_tvars, Name) of - [] -> fresh_uvar(Ann); - [{Name, T}] -> T - end, - aeso_tc_ets_manager:ets_insert(freshen_tvars, {Name, NewT}), - NewT; -freshen(Ann, {bytes_t, _, any}) -> - X = fresh_uvar(Ann), - aeso_tc_constraints:add_is_bytes_constraint(X), - X; -freshen(Ann, T) when is_tuple(T) -> - list_to_tuple(freshen(Ann, tuple_to_list(T))); -freshen(Ann, [A | B]) -> - [freshen(Ann, A) | freshen(Ann, B)]; -freshen(_, X) -> - X. - -freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) -> - FunT = freshen_type(Ann, aeso_tc_type_utils:typesig_to_fun_t(TypeSig)), - apply_typesig_constraint(Ann, Constr, FunT), - FunT. - -apply_typesig_constraint(_Ann, none, _FunT) -> ok; -apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) -> - aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann}); -apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) -> - aeso_tc_constraints:add_add_bytes_constraint(Ann, concat, A, B, C); -apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) -> - aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C); -apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) -> - aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}).