From fceb124f892490dd603a9dacac0cbefd0104ea6a Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 30 Apr 2023 11:01:51 +0300 Subject: [PATCH] Remove freshening from the type checker --- src/aeso_ast_infer_types.erl | 74 +++--------------------------------- src/aeso_tc_constraints.erl | 16 ++++---- src/aeso_tc_env.erl | 9 +++-- src/aeso_tc_fresh.erl | 60 +++++++++++++++++++++++++++++ src/aeso_tc_type_utils.erl | 4 ++ 5 files changed, 84 insertions(+), 79 deletions(-) create mode 100644 src/aeso_tc_fresh.erl diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 260f6a8..1db77eb 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -17,15 +17,7 @@ ]). %% Newly exported --export([ fresh_uvar/1 - , freshen_type/2 - , freshen_type_sig/2 - , infer_const/2 - , app_t/3 - , create_freshen_tvars/0 - , destroy_freshen_tvars/0 - , freshen/1 - , opposite_variance/1 +-export([ infer_const/2 ]). -export_type([ utype/0 , typesig/0 @@ -48,11 +40,6 @@ -type named_args_t() :: uvar() | [{named_arg_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), aeso_syntax:expr()}]. --define(is_type_id(T), element(1, T) =:= id orelse - element(1, T) =:= qid orelse - element(1, T) =:= con orelse - element(1, T) =:= qcon). - -type type() :: aeso_syntax:type(). -type name() :: string(). -type typesig() :: {type_sig, aeso_syntax:ann(), type_constraints(), [aeso_syntax:named_arg_t()], [type()], type()}. @@ -114,6 +101,7 @@ when_warning(A, B) -> aeso_tc_options:when_warning(A, B). %% ------- ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B). +app_t(A, B, C) -> aeso_tc_type_utils:app_t(A, B, C). %% ------- @@ -128,6 +116,10 @@ unfold_record_types(A, B) -> aeso_tc_type_unfolding:unfold_record_types(A, B). opposite_variance(A) -> aeso_tc_type_utils:opposite_variance(A). +%% ------- + +fresh_uvar(A) -> aeso_tc_fresh:fresh_uvar(A). + %% -- The rest --------------------------------------------------------------- map_t(As, K, V) -> {app_t, As, {id, As, "map"}, [K, V]}. @@ -943,9 +935,6 @@ arg_type(ArgAnn, {app_t, Attrs, Name, Args}) -> arg_type(_, T) -> T. -app_t(_Ann, Name, []) -> Name; -app_t(Ann, Name, Args) -> {app_t, Ann, Name, Args}. - %% Hack: don't allow passing the 'value' named arg if not stateful. This only %% works since the user can't create functions with named arguments. check_stateful_named_arg(Env, {id, _, "value"}, Default) -> @@ -1584,54 +1573,3 @@ 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. - -fresh_uvar(Attrs) -> - {uvar, Attrs, make_ref()}. - -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}). diff --git a/src/aeso_tc_constraints.erl b/src/aeso_tc_constraints.erl index fd6b53f..b1b0c62 100644 --- a/src/aeso_tc_constraints.erl +++ b/src/aeso_tc_constraints.erl @@ -28,14 +28,6 @@ element(1, T) =:= con orelse element(1, T) =:= qcon). -%% -- Circular dependency ---------------------------------------------------- - -fresh_uvar(A) -> aeso_ast_infer_types:fresh_uvar(A). -freshen(A) -> aeso_ast_infer_types:freshen(A). -create_freshen_tvars() -> aeso_ast_infer_types:create_freshen_tvars(). -destroy_freshen_tvars() -> aeso_ast_infer_types:destroy_freshen_tvars(). -app_t(A, B, C) -> aeso_ast_infer_types:app_t(A, B, C). - %% -- Moved functions -------------------------------------------------------- unify(A, B, C, D) -> aeso_tc_unify:unify(A, B, C, D). @@ -56,6 +48,14 @@ type_error(A) -> aeso_tc_errors:type_error(A). ensure_monomorphic(A, B) -> aeso_tc_type_utils:ensure_monomorphic(A, B). ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B). +app_t(A, B, C) -> aeso_tc_type_utils:app_t(A, B, C). + +%% ------- + +fresh_uvar(A) -> aeso_tc_fresh:fresh_uvar(A). +freshen(A) -> aeso_tc_fresh:freshen(A). +create_freshen_tvars() -> aeso_tc_fresh:create_freshen_tvars(). +destroy_freshen_tvars() -> aeso_tc_fresh:destroy_freshen_tvars(). %% --------------------------------------------------------------------------- diff --git a/src/aeso_tc_env.erl b/src/aeso_tc_env.erl index 4c2702f..d8b27b4 100644 --- a/src/aeso_tc_env.erl +++ b/src/aeso_tc_env.erl @@ -128,9 +128,6 @@ %% -- Circular dependency ---------------------------------------------------- -fresh_uvar(A) -> aeso_ast_infer_types:fresh_uvar(A). -freshen_type(A, B) -> aeso_ast_infer_types:freshen_type(A, B). -freshen_type_sig(A, B) -> aeso_ast_infer_types:freshen_type_sig(A, B). infer_const(A, B) -> aeso_ast_infer_types:infer_const(A, B). %% -- Duplicated types ------------------------------------------------------- @@ -170,6 +167,12 @@ used_constant(A, B) -> aeso_tc_warnings:used_constant(A, B). get_option(A, B) -> aeso_tc_options:get_option(A, B). when_warning(A, B) -> aeso_tc_options:when_warning(A, B). +%% ------- + +fresh_uvar(A) -> aeso_tc_fresh:fresh_uvar(A). +freshen_type(A, B) -> aeso_tc_fresh:freshen_type(A, B). +freshen_type_sig(A, B) -> aeso_tc_fresh:freshen_type_sig(A, B). + %% -- Getters ------------------------------------------------------------ contract_parents(#env{contract_parents = ContractParents}) -> diff --git a/src/aeso_tc_fresh.erl b/src/aeso_tc_fresh.erl new file mode 100644 index 0000000..882eed1 --- /dev/null +++ b/src/aeso_tc_fresh.erl @@ -0,0 +1,60 @@ +-module(aeso_tc_fresh). + +-export([ fresh_uvar/1 + , freshen/1 + , create_freshen_tvars/0 + , destroy_freshen_tvars/0 + , freshen_type/2 + , freshen_type_sig/2 + ]). + +fresh_uvar(Attrs) -> + {uvar, Attrs, make_ref()}. + +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}). diff --git a/src/aeso_tc_type_utils.erl b/src/aeso_tc_type_utils.erl index 9eebffb..5165376 100644 --- a/src/aeso_tc_type_utils.erl +++ b/src/aeso_tc_type_utils.erl @@ -8,6 +8,7 @@ , ensure_first_order/2 , ensure_monomorphic/2 , opposite_variance/1 + , app_t/3 ]). typesig_to_fun_t({type_sig, Ann, _Constr, Named, Args, Res}) -> @@ -86,3 +87,6 @@ opposite_variance(invariant) -> invariant; opposite_variance(covariant) -> contravariant; opposite_variance(contravariant) -> covariant; opposite_variance(bivariant) -> bivariant. + +app_t(_Ann, Name, []) -> Name; +app_t(Ann, Name, Args) -> {app_t, Ann, Name, Args}.