Split unfolding from the type checker

src/aeso_ast_infer_types.erl

@@ -14,8 +14,6 @@
 
 -export([ infer/1
         , infer/2
-        , unfold_types_in_type/2
-        , unfold_types_in_type/3
         ]).
 
 %% Newly exported
@@ -24,7 +22,6 @@
         , freshen_type_sig/2
         , infer_const/2
         , app_t/3
-        , unify/4
         , create_freshen_tvars/0
         , destroy_freshen_tvars/0
         , freshen/1
@@ -100,7 +97,6 @@ used_stateful(A) -> aeso_tc_warnings:used_stateful(A).
 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).
-used_typedef(A, B) -> aeso_tc_warnings:used_typedef(A, B).
 
 %% -------
 
@@ -123,6 +119,11 @@ ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B).
 
 unify(A, B, C, D) -> aeso_tc_unify:unify(A, B, C, D).
 
+%% -------
+
+unfold_types_in_type(A, B) -> aeso_tc_type_unfolding:unfold_types_in_type(A, B).
+unfold_record_types(A, B) -> aeso_tc_type_unfolding:unfold_record_types(A, B).
+
 %% -- The rest ---------------------------------------------------------------
 
 map_t(As, K, V) -> {app_t, As, {id, As, "map"}, [K, V]}.
@@ -1585,113 +1586,6 @@ get_oracle_type({qid, _, ["Oracle", "check_query"]},  [OType| _], _    ) -> OTyp
 get_oracle_type({qid, _, ["Oracle", "respond"]},      [OType| _], _    ) -> OType;
 get_oracle_type(_Fun, _Args, _Ret) -> false.
 
-%% During type inference, record types are represented by their
-%% names. But, before we pass the typed program to the code generator,
-%% we replace record types annotating expressions with their
-%% definition. This enables the code generator to see the fields.
-unfold_record_types(Env, T) ->
-    unfold_types(Env, T, [unfold_record_types]).
-
-unfold_types(Env, {typed, Attr, E, Type}, Options) ->
-    Options1 = [{ann, Attr} | lists:keydelete(ann, 1, Options)],
-    {typed, Attr, unfold_types(Env, E, Options), unfold_types_in_type(Env, Type, Options1)};
-unfold_types(Env, {arg, Attr, Id, Type}, Options) ->
-    {arg, Attr, Id, unfold_types_in_type(Env, Type, Options)};
-unfold_types(Env, {type_sig, Ann, Constr, NamedArgs, Args, Ret}, Options) ->
-    {type_sig, Ann, Constr,
-               unfold_types_in_type(Env, NamedArgs, Options),
-               unfold_types_in_type(Env, Args, Options),
-               unfold_types_in_type(Env, Ret, Options)};
-unfold_types(Env, {type_def, Ann, Name, Args, Def}, Options) ->
-    {type_def, Ann, Name, Args, unfold_types_in_type(Env, Def, Options)};
-unfold_types(Env, {fun_decl, Ann, Name, Type}, Options) ->
-    {fun_decl, Ann, Name, unfold_types(Env, Type, Options)};
-unfold_types(Env, {letfun, Ann, Name, Args, Type, [{guarded, AnnG, [], Body}]}, Options) ->
-    {letfun, Ann, Name, unfold_types(Env, Args, Options), unfold_types_in_type(Env, Type, Options), [{guarded, AnnG, [], unfold_types(Env, Body, Options)}]};
-unfold_types(Env, T, Options) when is_tuple(T) ->
-    list_to_tuple(unfold_types(Env, tuple_to_list(T), Options));
-unfold_types(Env, [H|T], Options) ->
-    [unfold_types(Env, H, Options)|unfold_types(Env, T, Options)];
-unfold_types(_Env, X, _Options) ->
-    X.
-
-unfold_types_in_type(Env, T) ->
-    unfold_types_in_type(Env, T, []).
-
-unfold_types_in_type(Env, {app_t, Ann, Id = {id, _, "map"}, Args = [KeyType0, _]}, Options) ->
-    Args1 = [KeyType, _] = unfold_types_in_type(Env, Args, Options),
-    Ann1 = proplists:get_value(ann, Options, aeso_syntax:get_ann(KeyType0)),
-    [ type_error({map_in_map_key, Ann1, KeyType0}) || has_maps(KeyType) ],
-    {app_t, Ann, Id, Args1};
-unfold_types_in_type(Env, {app_t, Ann, Id, Args}, Options) when ?is_type_id(Id) ->
-    when_warning(warn_unused_typedefs, fun() -> used_typedef(Id, length(Args)) end),
-    UnfoldRecords  = proplists:get_value(unfold_record_types, Options, false),
-    UnfoldVariants = proplists:get_value(unfold_variant_types, Options, false),
-    case aeso_tc_env:lookup_type(Env, Id) of
-        {_, {_, {Formals, {record_t, Fields}}}} when UnfoldRecords, length(Formals) == length(Args) ->
-            {record_t,
-             unfold_types_in_type(Env,
-               subst_tvars(lists:zip(Formals, Args), Fields), Options)};
-        {_, {_, {Formals, {alias_t, Type}}}} when length(Formals) == length(Args) ->
-            unfold_types_in_type(Env, subst_tvars(lists:zip(Formals, Args), Type), Options);
-        {_, {_, {Formals, {variant_t, Constrs}}}} when UnfoldVariants, length(Formals) == length(Args) ->
-            %% TODO: unfolding variant types will not work well if we add recursive types!
-            {variant_t,
-             unfold_types_in_type(Env,
-                subst_tvars(lists:zip(Formals, Args), Constrs), Options)};
-        _ ->
-            %% Not a record type, or ill-formed record type.
-            {app_t, Ann, Id, unfold_types_in_type(Env, Args, Options)}
-    end;
-unfold_types_in_type(Env, Id, Options) when ?is_type_id(Id) ->
-    %% Like the case above, but for types without parameters.
-    when_warning(warn_unused_typedefs, fun() -> used_typedef(Id, 0) end),
-    UnfoldRecords = proplists:get_value(unfold_record_types, Options, false),
-    UnfoldVariants = proplists:get_value(unfold_variant_types, Options, false),
-    case aeso_tc_env:lookup_type(Env, Id) of
-        {_, {_, {[], {record_t, Fields}}}} when UnfoldRecords ->
-            {record_t, unfold_types_in_type(Env, Fields, Options)};
-        {_, {_, {[], {variant_t, Constrs}}}} when UnfoldVariants ->
-            {variant_t, unfold_types_in_type(Env, Constrs, Options)};
-        {_, {_, {[], {alias_t, Type1}}}} ->
-            unfold_types_in_type(Env, Type1, Options);
-        _ ->
-            %% Not a record type, or ill-formed record type
-            Id
-    end;
-unfold_types_in_type(Env, {field_t, Attr, Name, Type}, Options) ->
-    {field_t, Attr, Name, unfold_types_in_type(Env, Type, Options)};
-unfold_types_in_type(Env, {constr_t, Ann, Con, Types}, Options) ->
-    {constr_t, Ann, Con, unfold_types_in_type(Env, Types, Options)};
-unfold_types_in_type(Env, {named_arg_t, Ann, Con, Types, Default}, Options) ->
-    {named_arg_t, Ann, Con, unfold_types_in_type(Env, Types, Options), Default};
-unfold_types_in_type(Env, T, Options) when is_tuple(T) ->
-    list_to_tuple(unfold_types_in_type(Env, tuple_to_list(T), Options));
-unfold_types_in_type(Env, [H|T], Options) ->
-    [unfold_types_in_type(Env, H, Options)|unfold_types_in_type(Env, T, Options)];
-unfold_types_in_type(_Env, X, _Options) ->
-    X.
-
-has_maps({app_t, _, {id, _, "map"}, _}) ->
-    true;
-has_maps(L) when is_list(L) ->
-    lists:any(fun has_maps/1, L);
-has_maps(T) when is_tuple(T) ->
-    has_maps(tuple_to_list(T));
-has_maps(_) -> false.
-
-subst_tvars(Env, Type) ->
-    subst_tvars1([{V, T} || {{tvar, _, V}, T} <- Env], Type).
-
-subst_tvars1(Env, T={tvar, _, Name}) ->
-    proplists:get_value(Name, Env, T);
-subst_tvars1(Env, [H|T]) ->
-    [subst_tvars1(Env, H)|subst_tvars1(Env, T)];
-subst_tvars1(Env, Type) when is_tuple(Type) ->
-    list_to_tuple(subst_tvars1(Env, tuple_to_list(Type)));
-subst_tvars1(_Env, X) ->
-    X.
-
 fresh_uvar(Attrs) ->
     {uvar, Attrs, make_ref()}.
 

src/aeso_compiler.erl

@@ -272,7 +272,7 @@ to_sophia_value(ContractString, FunName, ok, Data, Options0) ->
         Code = string_to_code(ContractString, Options),
         #{ unfolded_typed_ast := TypedAst, type_env  := TypeEnv} = Code,
         {ok, _, Type0} = get_decode_type(FunName, TypedAst),
-        Type   = aeso_ast_infer_types:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),
+        Type   = aeso_tc_type_unfolding:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),
 
         try
             {ok, aeso_vm_decode:from_fate(Type, aeb_fate_encoding:deserialize(Data))}
@@ -323,7 +323,7 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
         ArgTypes      = lists:map(GetType, Args),
         Type0         = {tuple_t, [], ArgTypes},
         %% user defined data types such as variants needed to match against
-        Type          = aeso_ast_infer_types:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),
+        Type          = aeso_tc_type_unfolding:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),
         case aeb_fate_abi:decode_calldata(FunName, Calldata) of
             {ok, FateArgs} ->
                 try

src/aeso_tc_constraints.erl

@@ -34,12 +34,18 @@ 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().
-unify(A, B, C, D) -> aeso_ast_infer_types:unify(A, B, C, D).
-unfold_types_in_type(A, B) -> aeso_ast_infer_types:unfold_types_in_type(A, B).
 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).
+
+%% -------
+
+unfold_types_in_type(A, B) -> aeso_tc_type_unfolding:unfold_types_in_type(A, B).
+
+%% -------
+
 qname(A) -> aeso_tc_name_manip:qname(A).
 
 %% -------

src/aeso_tc_type_unfolding.erl

@@ -0,0 +1,134 @@
+-module(aeso_tc_type_unfolding).
+
+-export([ unfold_types_in_type/2
+        , unfold_types_in_type/3
+        , unfold_record_types/2
+        ]).
+
+%% -- Duplicated macros ------------------------------------------------------
+
+-define(is_type_id(T), element(1, T) =:= id orelse
+                       element(1, T) =:= qid orelse
+                       element(1, T) =:= con orelse
+                       element(1, T) =:= qcon).
+
+%% -- Moved functions --------------------------------------------------------
+
+type_error(A) -> aeso_tc_errors:type_error(A).
+
+%% -------
+
+used_typedef(A, B) -> aeso_tc_warnings:used_typedef(A, B).
+
+%% -------
+
+when_warning(A, B) -> aeso_tc_options:when_warning(A, B).
+
+%% ---------------------------------------------------------------------------
+
+%% During type inference, record types are represented by their
+%% names. But, before we pass the typed program to the code generator,
+%% we replace record types annotating expressions with their
+%% definition. This enables the code generator to see the fields.
+unfold_record_types(Env, T) ->
+    unfold_types(Env, T, [unfold_record_types]).
+
+unfold_types(Env, {typed, Attr, E, Type}, Options) ->
+    Options1 = [{ann, Attr} | lists:keydelete(ann, 1, Options)],
+    {typed, Attr, unfold_types(Env, E, Options), unfold_types_in_type(Env, Type, Options1)};
+unfold_types(Env, {arg, Attr, Id, Type}, Options) ->
+    {arg, Attr, Id, unfold_types_in_type(Env, Type, Options)};
+unfold_types(Env, {type_sig, Ann, Constr, NamedArgs, Args, Ret}, Options) ->
+    {type_sig, Ann, Constr,
+               unfold_types_in_type(Env, NamedArgs, Options),
+               unfold_types_in_type(Env, Args, Options),
+               unfold_types_in_type(Env, Ret, Options)};
+unfold_types(Env, {type_def, Ann, Name, Args, Def}, Options) ->
+    {type_def, Ann, Name, Args, unfold_types_in_type(Env, Def, Options)};
+unfold_types(Env, {fun_decl, Ann, Name, Type}, Options) ->
+    {fun_decl, Ann, Name, unfold_types(Env, Type, Options)};
+unfold_types(Env, {letfun, Ann, Name, Args, Type, [{guarded, AnnG, [], Body}]}, Options) ->
+    {letfun, Ann, Name, unfold_types(Env, Args, Options), unfold_types_in_type(Env, Type, Options), [{guarded, AnnG, [], unfold_types(Env, Body, Options)}]};
+unfold_types(Env, T, Options) when is_tuple(T) ->
+    list_to_tuple(unfold_types(Env, tuple_to_list(T), Options));
+unfold_types(Env, [H|T], Options) ->
+    [unfold_types(Env, H, Options)|unfold_types(Env, T, Options)];
+unfold_types(_Env, X, _Options) ->
+    X.
+
+unfold_types_in_type(Env, T) ->
+    unfold_types_in_type(Env, T, []).
+
+unfold_types_in_type(Env, {app_t, Ann, Id = {id, _, "map"}, Args = [KeyType0, _]}, Options) ->
+    Args1 = [KeyType, _] = unfold_types_in_type(Env, Args, Options),
+    Ann1 = proplists:get_value(ann, Options, aeso_syntax:get_ann(KeyType0)),
+    [ type_error({map_in_map_key, Ann1, KeyType0}) || has_maps(KeyType) ],
+    {app_t, Ann, Id, Args1};
+unfold_types_in_type(Env, {app_t, Ann, Id, Args}, Options) when ?is_type_id(Id) ->
+    when_warning(warn_unused_typedefs, fun() -> used_typedef(Id, length(Args)) end),
+    UnfoldRecords  = proplists:get_value(unfold_record_types, Options, false),
+    UnfoldVariants = proplists:get_value(unfold_variant_types, Options, false),
+    case aeso_tc_env:lookup_type(Env, Id) of
+        {_, {_, {Formals, {record_t, Fields}}}} when UnfoldRecords, length(Formals) == length(Args) ->
+            {record_t,
+             unfold_types_in_type(Env,
+               subst_tvars(lists:zip(Formals, Args), Fields), Options)};
+        {_, {_, {Formals, {alias_t, Type}}}} when length(Formals) == length(Args) ->
+            unfold_types_in_type(Env, subst_tvars(lists:zip(Formals, Args), Type), Options);
+        {_, {_, {Formals, {variant_t, Constrs}}}} when UnfoldVariants, length(Formals) == length(Args) ->
+            %% TODO: unfolding variant types will not work well if we add recursive types!
+            {variant_t,
+             unfold_types_in_type(Env,
+                subst_tvars(lists:zip(Formals, Args), Constrs), Options)};
+        _ ->
+            %% Not a record type, or ill-formed record type.
+            {app_t, Ann, Id, unfold_types_in_type(Env, Args, Options)}
+    end;
+unfold_types_in_type(Env, Id, Options) when ?is_type_id(Id) ->
+    %% Like the case above, but for types without parameters.
+    when_warning(warn_unused_typedefs, fun() -> used_typedef(Id, 0) end),
+    UnfoldRecords = proplists:get_value(unfold_record_types, Options, false),
+    UnfoldVariants = proplists:get_value(unfold_variant_types, Options, false),
+    case aeso_tc_env:lookup_type(Env, Id) of
+        {_, {_, {[], {record_t, Fields}}}} when UnfoldRecords ->
+            {record_t, unfold_types_in_type(Env, Fields, Options)};
+        {_, {_, {[], {variant_t, Constrs}}}} when UnfoldVariants ->
+            {variant_t, unfold_types_in_type(Env, Constrs, Options)};
+        {_, {_, {[], {alias_t, Type1}}}} ->
+            unfold_types_in_type(Env, Type1, Options);
+        _ ->
+            %% Not a record type, or ill-formed record type
+            Id
+    end;
+unfold_types_in_type(Env, {field_t, Attr, Name, Type}, Options) ->
+    {field_t, Attr, Name, unfold_types_in_type(Env, Type, Options)};
+unfold_types_in_type(Env, {constr_t, Ann, Con, Types}, Options) ->
+    {constr_t, Ann, Con, unfold_types_in_type(Env, Types, Options)};
+unfold_types_in_type(Env, {named_arg_t, Ann, Con, Types, Default}, Options) ->
+    {named_arg_t, Ann, Con, unfold_types_in_type(Env, Types, Options), Default};
+unfold_types_in_type(Env, T, Options) when is_tuple(T) ->
+    list_to_tuple(unfold_types_in_type(Env, tuple_to_list(T), Options));
+unfold_types_in_type(Env, [H|T], Options) ->
+    [unfold_types_in_type(Env, H, Options)|unfold_types_in_type(Env, T, Options)];
+unfold_types_in_type(_Env, X, _Options) ->
+    X.
+
+has_maps({app_t, _, {id, _, "map"}, _}) ->
+    true;
+has_maps(L) when is_list(L) ->
+    lists:any(fun has_maps/1, L);
+has_maps(T) when is_tuple(T) ->
+    has_maps(tuple_to_list(T));
+has_maps(_) -> false.
+
+subst_tvars(Env, Type) ->
+    subst_tvars1([{V, T} || {{tvar, _, V}, T} <- Env], Type).
+
+subst_tvars1(Env, T={tvar, _, Name}) ->
+    proplists:get_value(Name, Env, T);
+subst_tvars1(Env, [H|T]) ->
+    [subst_tvars1(Env, H)|subst_tvars1(Env, T)];
+subst_tvars1(Env, Type) when is_tuple(Type) ->
+    list_to_tuple(subst_tvars1(Env, tuple_to_list(Type)));
+subst_tvars1(_Env, X) ->
+    X.

src/aeso_tc_unify.erl

@@ -4,11 +4,14 @@
 
 %% -- Circular dependency ----------------------------------------------------
 
-unfold_types_in_type(A, B, C) -> aeso_ast_infer_types:unfold_types_in_type(A, B, C).
 opposite_variance(A) -> aeso_ast_infer_types:opposite_variance(A).
 
 %% -- Moved functions --------------------------------------------------------
 
+unfold_types_in_type(A, B, C) -> aeso_tc_type_unfolding:unfold_types_in_type(A, B, C).
+
+%% -------
+
 type_error(A) -> aeso_tc_errors:type_error(A).
 cannot_unify(A, B, C, D) -> aeso_tc_errors:cannot_unify(A, B, C, D).