beam_types: Extend the type lattice tests

2 files changed, 126 insertions, 36 deletions

diff --git a/lib/compiler/test/beam_types_SUITE.erl b/lib/compiler/test/beam_types_SUITE.erl
index 297bd4026e..1b6397301b 100644
--- a/lib/compiler/test/beam_types_SUITE.erl
+++ b/lib/compiler/test/beam_types_SUITE.erl
@@ -25,18 +25,30 @@
 -export([all/0, suite/0, groups/0,
          init_per_suite/1, end_per_suite/1]).
 
--export([consistency/1, commutativity/1,
-         binary_consistency/1, integer_consistency/1]).
+-export([absorption/1,
+         associativity/1,
+         commutativity/1,
+         idempotence/1,
+         identity/1]).
+
+-export([binary_absorption/1,
+         integer_absorption/1]).
 
 suite() ->
     [{ct_hooks,[ts_install_cth]}].
 
 all() ->
-    [{group,property_tests}].
+    [{group,property_tests},
+     binary_absorption,
+     integer_absorption].
 
 groups() ->
-    [{property_tests,[], [consistency, commutativity,
-                          binary_consistency, integer_consistency]}].
+    [{property_tests,[parallel],
+      [absorption,
+       associativity,
+       commutativity,
+       idempotence,
+       identity]}].
 
 init_per_suite(Config) ->
     ct_property_test:init_per_suite(Config).
@@ -44,15 +56,27 @@ init_per_suite(Config) ->
 end_per_suite(Config) ->
     Config.
 
-consistency(Config) when is_list(Config) ->
-    %% manual test: proper:quickcheck(beam_types_prop:consistency()).
-    true = ct_property_test:quickcheck(beam_types_prop:consistency(), Config).
+absorption(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:absorption()).
+    true = ct_property_test:quickcheck(beam_types_prop:absorption(), Config).
+
+associativity(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:associativity()).
+    true = ct_property_test:quickcheck(beam_types_prop:associativity(), Config).
 
 commutativity(Config) when is_list(Config) ->
     %% manual test: proper:quickcheck(beam_types_prop:commutativity()).
     true = ct_property_test:quickcheck(beam_types_prop:commutativity(), Config).
 
-binary_consistency(Config) when is_list(Config) ->
+idempotence(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:idempotence()).
+    true = ct_property_test:quickcheck(beam_types_prop:idempotence(), Config).
+
+identity(Config) when is_list(Config) ->
+    %% manual test: proper:quickcheck(beam_types_prop:identity()).
+    true = ct_property_test:quickcheck(beam_types_prop:identity(), Config).
+
+binary_absorption(Config) when is_list(Config) ->
     %% These binaries should meet into {binary,12} as that's the best common
     %% unit for both types.
     A = #t_bitstring{unit=4},
@@ -66,7 +90,7 @@ binary_consistency(Config) when is_list(Config) ->
 
     ok.
 
-integer_consistency(Config) when is_list(Config) ->
+integer_absorption(Config) when is_list(Config) ->
     %% Integers that don't overlap fully should never meet.
     A = #t_integer{elements={3,5}},
     B = #t_integer{elements={4,6}},
@@ -78,3 +102,4 @@ integer_consistency(Config) when is_list(Config) ->
     A = beam_types:join(A, beam_types:meet(A, B)),
 
     ok.
+
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
index 9c103d3886..80966bbfc8 100644
--- a/lib/compiler/test/property_test/beam_types_prop.erl
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -22,8 +22,8 @@
 
 -compile([export_all, nowarn_export_all]).
 
-%% This module has only supports proper, as we don't have an eqc license to
-%% test with.
+%% This module only supports proper, as we don't have an eqc license to test
+%% with.
 
 -proptest([proper]).
 
@@ -34,31 +34,94 @@
 -include_lib("proper/include/proper.hrl").
 -define(MOD_eqc,proper).
 
-consistency() ->
+%% The default repetitions of 100 is a bit too low to reliably cover all type
+%% combinations, so we crank it up a bit.
+-define(REPETITIONS, 1000).
+
+absorption() ->
+    numtests(?REPETITIONS, absorption_1()).
+
+absorption_1() ->
     ?FORALL({TypeA, TypeB},
             ?LET(TypeA, type(),
                  ?LET(TypeB, type(), {TypeA, TypeB})),
-            consistency_check(TypeA, TypeB)).
+            absorption_check(TypeA, TypeB)).
 
-consistency_check(A, B) ->
-    consistency_check_1(A, B),
-    consistency_check_1(B, A),
-    true.
+absorption_check(A, B) ->
+    %% a ∨ (a ∧ b) = a,
+    A = beam_types:join(A, beam_types:meet(A, B)),
 
-consistency_check_1(A, B) ->
+    %% a ∧ (a ∨ b) = a.
     A = beam_types:meet(A, beam_types:join(A, B)),
-    A = beam_types:join(A, beam_types:meet(A, B)),
-    ok.
+
+    true.
+
+associativity() ->
+    numtests(?REPETITIONS, associativity_1()).
+
+associativity_1() ->
+    ?FORALL({TypeA, TypeB, TypeC},
+            ?LET(TypeA, type(),
+                 ?LET(TypeB, type(),
+                      ?LET(TypeC, type(), {TypeA, TypeB, TypeC}))),
+            associativity_check(TypeA, TypeB, TypeC)).
+
+associativity_check(A, B, C) ->
+    %% a ∨ (b ∨ c) = (a ∨ b) ∨ c,
+    LHS_Join = beam_types:join(A, beam_types:join(B, C)),
+    RHS_Join = beam_types:join(beam_types:join(A, B), C),
+    LHS_Join = RHS_Join,
+
+    %% a ∧ (b ∧ c) = (a ∧ b) ∧ c.
+    LHS_Meet = beam_types:meet(A, beam_types:meet(B, C)),
+    RHS_Meet = beam_types:meet(beam_types:meet(A, B), C),
+    LHS_Meet = RHS_Meet,
+
+    true.
 
 commutativity() ->
+    numtests(?REPETITIONS, commutativity_1()).
+
+commutativity_1() ->
     ?FORALL({TypeA, TypeB},
             ?LET(TypeA, type(),
                  ?LET(TypeB, type(), {TypeA, TypeB})),
-            commutativity_check(TypeA, TypeB)).
+             commutativity_check(TypeA, TypeB)).
 
 commutativity_check(A, B) ->
-    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+    %% a ∨ b = b ∨ a,
     true = beam_types:join(A, B) =:= beam_types:join(B, A),
+
+    %% a ∧ b = b ∧ a.
+    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+
+    true.
+
+idempotence() ->
+    numtests(?REPETITIONS, idempotence_1()).
+
+idempotence_1() ->
+    ?FORALL(Type, type(), idempotence_check(Type)).
+
+idempotence_check(Type) ->
+    %% a ∨ a = a,
+    Type = beam_types:join(Type, Type),
+
+    %% a ∧ a = a.
+    Type = beam_types:meet(Type, Type),
+
+    true.
+
+identity() ->
+    ?FORALL(Type, type(), identity_check(Type)).
+
+identity_check(Type) ->
+    %% a ∨ [bottom element] = a,
+    Type = beam_types:join(Type, none),
+
+    %% a ∧ [top element] = a.
+    Type = beam_types:meet(Type, any),
+
     true.
 
 %%%
@@ -75,7 +138,10 @@ type(Depth) ->
               other_types()).
 
 other_types() ->
-    [any, gen_atom(), gen_binary(), none].
+    [any,
+     gen_atom(),
+     gen_binary(),
+     none].
 
 list_types() ->
     [cons, list, nil].
@@ -106,21 +172,19 @@ 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)).
+    ?LET({A, B}, {integer(), 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))).
+           ?LET({Exact, Elements}, {boolean(), 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)),
@@ -134,6 +198,7 @@ gen_element(Depth) ->
                         _ -> true
                     end)).
 
+
 sized_list(0, _Gen) -> [];
 sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)].