1 files changed, 140 insertions, 0 deletions
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
new file mode 100644
index 0000000000..9c103d3886
--- /dev/null
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -0,0 +1,140 @@
+%%
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2019. All Rights Reserved.
+%%
+%% Licensed under the Apache License, Version 2.0 (the "License");
+%% you may not use this file except in compliance with the License.
+%% You may obtain a copy of the License at
+%%
+%%     http://www.apache.org/licenses/LICENSE-2.0
+%%
+%% Unless required by applicable law or agreed to in writing, software
+%% distributed under the License is distributed on an "AS IS" BASIS,
+%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+%% See the License for the specific language governing permissions and
+%% limitations under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(beam_types_prop).
+
+-compile([export_all, nowarn_export_all]).
+
+%% This module has only supports proper, as we don't have an eqc license to
+%% test with.
+
+-proptest([proper]).
+
+-ifdef(PROPER).
+
+-include_lib("compiler/src/beam_types.hrl").
+
+-include_lib("proper/include/proper.hrl").
+-define(MOD_eqc,proper).
+
+consistency() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            consistency_check(TypeA, TypeB)).
+
+consistency_check(A, B) ->
+    consistency_check_1(A, B),
+    consistency_check_1(B, A),
+    true.
+
+consistency_check_1(A, B) ->
+    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = beam_types:join(A, beam_types:meet(A, B)),
+    ok.
+
+commutativity() ->
+    ?FORALL({TypeA, TypeB},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(), {TypeA, TypeB})),
+            commutativity_check(TypeA, TypeB)).
+
+commutativity_check(A, B) ->
+    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+    true = beam_types:join(A, B) =:= beam_types:join(B, A),
+    true.
+
+%%%
+%%% Generators
+%%%
+
+type() ->
+    type(0).
+
+type(Depth) ->
+    oneof(nested_types(Depth) ++
+              numerical_types() ++
+              list_types() ++
+              other_types()).
+
+other_types() ->
+    [any, gen_atom(), gen_binary(), none].
+
+list_types() ->
+    [cons, list, nil].
+
+numerical_types() ->
+    [gen_integer(), float, number].
+
+nested_types(Depth) when Depth >= 3 -> [];
+nested_types(Depth) -> [#t_map{}, gen_tuple(Depth + 1)].
+
+gen_atom() ->
+    ?LET(Size, range(0, ?ATOM_SET_SIZE),
+         case Size of
+             0 ->
+                 #t_atom{};
+             _ ->
+                 ?LET(Set, sized_list(Size, atom()),
+                      begin
+                          #t_atom{elements=ordsets:from_list(Set)}
+                      end)
+         end).
+
+gen_binary() ->
+    ?SHRINK(#t_bitstring{unit=range(1, 128)},
+            [#t_bitstring{unit=[1, 2, 3, 5, 7, 8, 16, 32, 64]}]).
+
+gen_integer() ->
+    oneof([gen_integer_bounded(), #t_integer{}]).
+
+gen_integer_bounded() ->
+    ?LET(A, integer(),
+         ?LET(B, integer(),
+              begin
+                  #t_integer{elements={min(A,B), max(A,B)}}
+              end)).
+
+gen_tuple(Depth) ->
+    ?SIZED(Size,
+           ?LET(Exact, oneof([true, false]),
+                ?LET(Elements, gen_tuple_elements(Size, Depth),
+                     begin
+                         #t_tuple{exact=Exact,
+                                  size=Size,
+                                  elements=Elements}
+                     end))).
+
+gen_tuple_elements(Size, Depth) ->
+    ?LET(Types, sized_list(rand:uniform(Size div 4 + 1), gen_element(Depth)),
+         maps:from_list([{rand:uniform(Size), T} || T <- Types])).
+
+gen_element(Depth) ->
+    ?LAZY(?SUCHTHAT(Type, type(Depth),
+                    case Type of
+                        any -> false;
+                        none -> false;
+                        _ -> true
+                    end)).
+
+sized_list(0, _Gen) -> [];
+sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)].
+
+-endif.