diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b6cf3c..8e35c60 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] ### Added +- Added a check for number of type variables in a type signature; it is serialized using 8 bits, + so the upper limit is 256. ### Changed ### Removed diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 25abd28..dfbfe59 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -295,6 +295,11 @@ of `A`. - When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be a subtype of `t(B)`. +#### Type variable limitation + +Because of how FATE represents types as values there is a fixed upper limit (256) +of type variables that can be used in a single type signature. + ## Mutable state Sophia does not have arbitrary mutable state, but only a limited form of state diff --git a/docs/sophia_syntax.md b/docs/sophia_syntax.md index 5b975ab..6a9ae86 100644 --- a/docs/sophia_syntax.md +++ b/docs/sophia_syntax.md @@ -267,11 +267,11 @@ UnOp ::= '-' | '!' | 'bnot' | Operators | Type | --- | --- | `-` `+` `*` `/` `mod` `^` | arithmetic operators -| `!` `&&` `||` | logical operators +| `!` `&&` `\|\|` | logical operators | `band` `bor` `bxor` `bnot` `<<` `>>` | bitwise operators | `==` `!=` `<` `>` `=<` `>=` | comparison operators | `::` `++` | list operators -| `|>` | functional operators +| `\|>` | functional operators ## Operator precedence @@ -291,5 +291,5 @@ In order of highest to lowest precedence. | `bxor` | left | `bor` | left | `&&` | right -| `||` | right -| `|>` | left +| `\|\|` | right +| `\|>` | left diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index b78ea38..d6f8e5b 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1760,8 +1760,27 @@ desugar_clauses(Ann, Fun, {type_sig, _, _, _, ArgTypes, RetType}, Clauses) -> end. print_typesig({Name, TypeSig}) -> + assert_tvars(Name, TypeSig), ?PRINT_TYPES("Inferred ~s : ~s\n", [Name, pp(TypeSig)]). +assert_tvars(Name, TS) -> + TVars = assert_tvars_(TS, #{}), + case maps:size(TVars) > 256 of + true -> + type_error({too_many_tvars, Name, TS}); + false -> + ok + end. + +assert_tvars_({tvar, _, TV}, TVars) -> + TVars#{TV => ok}; +assert_tvars_(T, TVars) when is_tuple(T) -> + assert_tvars_(tuple_to_list(T), TVars); +assert_tvars_(Ts, TVars) when is_list(Ts) -> + lists:foldl(fun(T, TVars1) -> assert_tvars_(T, TVars1) end, TVars, Ts); +assert_tvars_(_, TVars) -> + TVars. + arg_type(ArgAnn, {id, Ann, "_"}) -> case aeso_syntax:get_ann(origin, Ann, user) of system -> fresh_uvar(ArgAnn); @@ -3389,7 +3408,7 @@ instantiate1(X) -> integer_to_tvar(X) when X < 26 -> [$a + X]; integer_to_tvar(X) -> - [integer_to_tvar(X div 26)] ++ [$a + (X rem 26)]. + integer_to_tvar(X div 26 - 1) ++ [$a + (X rem 26)]. %% Warnings @@ -3776,6 +3795,9 @@ mk_error({type_decl, _, {id, Pos, Name}, _}) -> Msg = io_lib:format("Empty type declarations are not supported. Type `~s` lacks a definition", [Name]), mk_t_err(pos(Pos), Msg); +mk_error({too_many_tvars, Name, {type_sig, Pos, _, _, _, _}}) -> + Msg = io_lib:format("Too many type variables (max 256) in definition of `~s`", [Name]), + mk_t_err(pos(Pos), Msg); mk_error({stateful_not_allowed, Id, Fun}) -> Msg = io_lib:format("Cannot reference stateful function `~s` in the definition of non-stateful function `~s`.", [pp(Id), pp(Fun)]), diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 3bd922d..c13b180 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -1302,6 +1302,10 @@ failing_contracts() -> <> ]) + , ?TYPE_ERROR(too_many_tvars, + [<> + ]) ]. validation_test_() -> diff --git a/test/contracts/too_many_tvars.aes b/test/contracts/too_many_tvars.aes new file mode 100644 index 0000000..4fa78ce --- /dev/null +++ b/test/contracts/too_many_tvars.aes @@ -0,0 +1,60 @@ +contract C = + entrypoint too_many( + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _)) = 0 + + entrypoint not_too_many( + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _, _, _, _, _), + (_, _, _, _, _, _)) = 0