Skip to content

Commit

Permalink
Introduce the ?TYPE macro
Browse files Browse the repository at this point in the history
It allows explicitly using PropEr's "native types" feature.

This is more powerful than the current automatic parse transform-based inference:
* it can be used outside of `?FORALL` to produce PropEr types & combine
  them with other PropEr or native types.
* it allows using the "native types" feature with the proper parse transform disabled
* it allows expressing more types directly, without creating additional type aliases,
  for example: `?TYPE(atom() | float())`.

The semantics are identical to automatic inference, if the expression was wrapped
in a simple `id` type (when the syntax allows expressing such a type). For example:

```erlang
-record(foo, {}).
-type id(X) :: X.

% semantically equivalent definitions:
?FORALL(X, id(#foo{}), Prop).
?FORALL(X, ?TYPE(#foo{}), Prop).
```
  • Loading branch information
michalmuskala committed Jun 28, 2022
1 parent cfc29e7 commit 50fb72d
Show file tree
Hide file tree
Showing 4 changed files with 75 additions and 10 deletions.
1 change: 1 addition & 0 deletions include/proper_common.hrl
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@
proper_types:add_constraint(RawType,fun(X) -> Condition end,true)).
-define(SUCHTHATMAYBE(X,RawType,Condition),
proper_types:add_constraint(RawType,fun(X) -> Condition end,false)).
-define(TYPE(X), proper_types:native_type(?MODULE, ??X)).

%%------------------------------------------------------------------------------
%% Targeted macros
Expand Down
38 changes: 29 additions & 9 deletions src/proper_typeserver.erl
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,23 @@
%%%
%%% PropEr can parse types expressed in Erlang's type language and convert them
%%% to its own type format. Such expressions can be used instead of regular type
%%% constructors in the second argument of `?FORALL's. No extra notation is
%%% required; PropEr will detect which calls correspond to native types by
%%% applying a parse transform during compilation. This parse transform is
%%% automatically applied to any module that includes the `proper.hrl' header
%%% file. You can disable this feature by compiling your modules with
%%% `-DPROPER_NO_TRANS'. Note that this will currently also disable the
%%% automatic exporting of properties.
%%% constructors in the second argument of `?FORALL's. Such types can be expressed
%%% in two ways:
%%% <ul>
%%% <li> directly, with no extra notation required; PropEr will detect which calls
%%% correspond to native types by applying a parse transform during compilation.
%%% This parse transform is automatically applied to any module that includes
%%% the `proper.hrl' header file.</li>
%%% <li> by leveraging the `?TYPE` macro; This allows urestricted use of Erlang's
%%% type language and does not require applying the parse transform.</li>
%%% </ul>
%%%
%%% You can disable the parse transform (and automatic detection of native types)
%%% by compiling your modules with `-DPROPER_NO_TRANS' flag. Note that this will
%%% currently also disable the automatic exporting of properties.
%%%
%%% The use of native types in properties is subject to the following usage
%%% rules:
%%% The use of automatically-detected native types in properties is subject
%%% to the following usage rules:
%%% <ul>
%%% <li>Native types cannot be used outside of `?FORALL's.</li>
%%% <li>Inside `?FORALL's, native types can be combined with other native
Expand Down Expand Up @@ -154,6 +161,19 @@
%%% </li>
%%% </ul>
%%%
%%% The `?TYPE` macro for explicitly taking advantage of PropEr's native type
%%% support is subject to the following usage rules:
%%% <ul>
%%% <li>It is allowed in any position to produce a PropEr type, including
%%% outside of `?FORALL`.</li>
%%% <li>The same restriction on allowed recursive native types as in `?FORALL` apply.</li>
%%% <li>There's no risk of confusion between expressions and native types,
%%% inside `?TYPE` everything is interpreted as a native type, and as such
%%% `?TYPE([integer()])` will produce an arbitrary integer list.</li>
%%% <li>It is not checked for correct syntax - using invalid syntax can produce
%%% errors when the property is evaluated, which are hard to understand.</li>
%%% </ul>
%%%
%%% You can use <a href="#index">these</a> functions to try out the type
%%% translation subsystem.
%%%
Expand Down
42 changes: 42 additions & 0 deletions test/no_transforms.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
%%% -*- coding: utf-8 -*-
%%% -*- erlang-indent-level: 2 -*-
%%% -------------------------------------------------------------------
%%% Copyright 2010-2011 Manolis Papadakis <[email protected]>,
%%% Eirini Arvaniti <[email protected]>
%%% and Kostis Sagonas <[email protected]>
%%%
%%% This file is part of PropEr.
%%%
%%% PropEr is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU General Public License as published by
%%% the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% PropEr is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%%% GNU General Public License for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>.

%%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @doc This module tests whether proper works with parse transforms disabled.

-module(no_transforms).
-export([prop_1/0, prop_2/0]).

-define(PROPER_NO_TRANS, true).

-include_lib("proper/include/proper.hrl").

-type local_integer() :: integer().
-type local_float() :: float().

prop_1() -> ?FORALL(X, ?TYPE(local_integer() | local_float()), is_number(X)).

prop_2() -> ?FORALL(X, native_type(), is_integer(X) orelse is_atom(X)).

native_type() ->
?TYPE(local_integer() | atom()).
4 changes: 3 additions & 1 deletion test/proper_tests.erl
Original file line number Diff line number Diff line change
Expand Up @@ -837,7 +837,9 @@ parse_transform_test_() ->
?_assertError(undef, auto_export_test2:prop_1()),
?_assertError(undef, no_native_parse_test:prop_1()),
?_passes(let_tests:prop_1()),
?_failsWith([3*42], let_tests:prop_2())].
?_failsWith([3*42], let_tests:prop_2()),
?_passes(no_transforms:prop_1()),
?_passes(no_transforms:prop_2())].

native_type_props_test_() ->
[?_passes(?FORALL({X,Y}, {my_native_type(),my_proper_type()},
Expand Down

0 comments on commit 50fb72d

Please sign in to comment.