Fill AACI and coerce type specs

Any error reasons or paths are just term() still, and ACI doesn't have a defined spec in the compiler, so whatever, but the AACI types, the erlang representation of terms, and the four different kinds of coerce function are all spec'd now.

Also some internal type substitution functions were given types, just in the hopes of catching some errors, but dyalizer doesn't seem to complain at all no matter how badly I break my code. Strange approach to making a type system, but oh well.
This commit is contained in:
Jarvis Carroll 2026-02-26 12:54:28 +00:00
parent bda4e89e58
commit 540b2c513b
2 changed files with 115 additions and 7 deletions

View File

@ -25,11 +25,43 @@
%%% Types
-export_type([aaci/0]).
-export_type([aaci/0, annotated_type/0, erlang_repr/0]).
-include_lib("eunit/include/eunit.hrl").
-type aaci() :: {aaci, term(), term(), term()}.
-type aaci() :: {aaci, string(), #{string() => function_spec()}, #{string() => typedef()}}.
-type function_spec() :: {[{string(), annotated_type()}], annotated_type()}.
-type typedef() :: {[string()], typedef_rhs()}.
-type annotated_type() :: {opaque_type(), already_normalized | opaque_type(), builtin_type(annotated_type())}.
-type builtin_type(T) :: {bytes, [integer() | any]}
| {record, [{string(), T}]}
| {variant, [{string(), [T]}]}
| {tuple, [T]}
| {list, [T]}
| {map, [T]}
| integer
| boolean
| bits
| char
| string
| address
| signature
| contract
| channel
| unknown_type.
-type opaque_type() :: string() | {string(), [opaque_type()]} | builtin_type(opaque_type()).
-type typedef_rhs() :: {var, string()} | string() | {string(), [opaque_type()]} | builtin_type(typedef_rhs()).
-type erlang_repr() :: integer()
| string()
| boolean()
| binary()
| tuple() % Tuples, variants, or raw addresses
| [erlang_repr()]
| #{erlang_repr() => erlang_repr()}.
%%% ACI/AACI
@ -47,6 +79,9 @@ prepare_from_file(Path) ->
Error -> Error
end.
-spec prepare(ACI) -> AACI
when ACI :: term(),
AACI :: aaci().
prepare(ACI) ->
% We want to take the types represented by the ACI, things like N1.T(N2.T),
@ -66,6 +101,12 @@ prepare(ACI) ->
{aaci, Name, Specs, TypeDefs}.
-spec convert_aci_types(ACI) -> {Name, OpaqueSpecs, TypeDefs}
when ACI :: term(),
Name :: string(),
OpaqueSpecs :: [{string(), [{string(), opaque_type()}], opaque_type()}],
TypeDefs :: #{string() => typedef()}.
convert_aci_types(ACI) ->
% Find the main contract, so we can get the specifications of its
% entrypoints.
@ -134,6 +175,12 @@ convert_typedefs_loop([Next | Rest], NamePrefix, Converted) ->
Def = opaque_type(Params, DefACI),
convert_typedefs_loop(Rest, NamePrefix, [Converted, {Name, Params, Def}]).
-spec collect_opaque_types(Tree, TypeDefs) -> TypeDefs
when Tree :: typedef_tree(),
TypeDefs :: #{string() => typedef()}.
-type typedef_tree() :: {string(), [string()], typedef_rhs()} | list(typedef_tree()).
collect_opaque_types([], Types) ->
Types;
collect_opaque_types([L | R], Types) ->
@ -144,6 +191,11 @@ collect_opaque_types({Name, Params, Def}, Types) ->
%%% ACI Type -> Opaque Type
-spec opaque_type(Params, ACIType) -> Opaque
when Params :: [string()],
ACIType :: binary() | map(),
Opaque :: typedef_rhs().
% Convert an ACI type defintion/spec into the 'opaque type' representation that
% our dereferencing algorithms can reason about.
opaque_type(Params, NameBin) when is_binary(NameBin) ->
@ -171,6 +223,8 @@ opaque_type(Params, Pair) when is_map(Pair) ->
[{Name, TypeArgs}] = maps:to_list(Pair),
{opaque_type_name(Name), [opaque_type(Params, Arg) || Arg <- TypeArgs]}.
-spec opaque_type_name(binary()) -> atom() | string().
% Atoms for any builtins that aren't qualified by a namespace in Sophia.
% Everything else stays as a string, user-defined or not.
opaque_type_name(<<"int">>) -> integer;
@ -280,6 +334,12 @@ annotate_function_specs([{Name, ArgsOpaque, ResultOpaque} | Rest], Types, Specs)
NewSpecs = maps:put(Name, {Args, Result}, Specs),
annotate_function_specs(Rest, Types, NewSpecs).
-spec annotate_type(Opaque, Types) -> {ok, Annotated} | {error, Reason}
when Opaque :: opaque_type(),
Types :: #{string() => typedef()},
Annotated :: annotated_type(),
Reason :: none().
annotate_type(T, Types) ->
case normalize_opaque_type(T, Types) of
{ok, AlreadyNormalized, NOpaque, NExpanded} ->
@ -445,6 +505,14 @@ substitute_opaque_types(Bindings, Types) ->
%%% Erlang to FATE
-spec erlang_args_to_fate(VarTypes, Terms) -> {ok, FATE} | {error, Errors}
when VarTypes :: [{string(), annotated_type()}],
Terms :: [erlang_repr()],
FATE :: gmb_fate_data:fate_type(),
Errors :: [{Reason, [PathStep]}],
Reason :: term(),
PathStep :: term().
erlang_args_to_fate(VarTypes, Terms) ->
DefLength = length(VarTypes),
ArgLength = length(Terms),
@ -454,6 +522,14 @@ erlang_args_to_fate(VarTypes, Terms) ->
DefLength < ArgLength -> {error, too_many_args}
end.
-spec erlang_to_fate(Type, Erlang) -> {ok, FATE} | {error, Errors}
when Type :: annotated_type(),
FATE :: gmb_fate_data:fate_type(),
Erlang :: erlang_repr(),
Errors :: [{Reason, [PathStep]}],
Reason :: term(),
PathStep :: term().
erlang_to_fate({_, _, integer}, S) when is_integer(S) ->
{ok, S};
erlang_to_fate({O, N, integer}, S) when is_list(S) ->
@ -794,6 +870,14 @@ coerce_direction(Type, Term, to_fate) ->
coerce_direction(Type, Term, from_fate) ->
fate_to_erlang(Type, Term).
-spec fate_to_erlang(Type, FATE) -> {ok, Erlang} | {error, Errors}
when Type :: annotated_type(),
FATE :: gmb_fate_data:fate_type(),
Erlang :: erlang_repr(),
Errors :: [{Reason, [PathStep]}],
Reason :: term(),
PathStep :: term().
fate_to_erlang({_, _, integer}, S) when is_integer(S) ->
{ok, S};
fate_to_erlang({_, _, address}, {address, Bin}) ->

View File

@ -10,14 +10,20 @@
-include_lib("eunit/include/eunit.hrl").
-spec parse_literal(String) -> Result
when String :: string(),
Result :: {ok, gmb_fate_data:fate_type()}
| {error, Reason :: term()}.
-spec parse_literal(Sophia) -> {ok, FATE} | {error, Reason}
when Sophia :: string(),
FATE :: gmb_fate_data:fate_type(),
Reason :: term().
parse_literal(String) ->
parse_literal(unknown_type(), String).
-spec parse_literal(Type, Sophia) -> {ok, FATE} | {error, Reason}
when Type :: hz_aaci:annotated_type(),
Sophia :: string(),
FATE :: gmb_fate_data:fate_type(),
Reason :: term().
parse_literal(Type, String) ->
case parse_expression(Type, {1, 1}, String) of
{ok, {Result, NewPos, NewString}} ->
@ -917,16 +923,34 @@ wrap_error(Reason, _) -> Reason.
%%% Pretty Printing
-spec fate_to_list(FATE) -> Sophia
when FATE :: gmb_fate_data:fate_type(),
Sophia :: string().
fate_to_list(Term) ->
fate_to_list(unknown_type(), Term).
-spec fate_to_list(Type, FATE) -> Sophia
when Type :: hz_aaci:annotated_type(),
FATE :: gmb_fate_data:fate_type(),
Sophia :: string().
fate_to_list(Type, Term) ->
IOList = fate_to_iolist(Type, Term),
unicode:characters_to_list(IOList).
-spec fate_to_iolist(FATE) -> Sophia
when FATE :: gmb_fate_data:fate_type(),
Sophia :: iolist().
fate_to_iolist(Term) ->
fate_to_iolist(unknown_type(), Term).
-spec fate_to_iolist(Type, FATE) -> Sophia
when Type :: hz_aaci:annotated_type(),
FATE :: gmb_fate_data:fate_type(),
Sophia :: iolist().
% Special case for singleton records, since they are erased during compilation.
fate_to_iolist({_, _, {record, [{FieldName, FieldType}]}}, Term) ->
singleton_record_to_iolist(FieldName, FieldType, Term);
@ -1430,6 +1454,6 @@ singleton_test() ->
% Also if we wanted an integer, the singleton is NOT dropped, so is also an
% error.
{error, {expected_close_paren, 1, 3}} = parse_literal({integer, alread_normalized, integer}, "(1,)"),
{error, {expected_close_paren, 1, 3}} = parse_literal({integer, already_normalized, integer}, "(1,)"),
ok.