diff options
Diffstat (limited to 'lib/compiler/test/property_test/beam_types_prop.erl')
| -rw-r--r-- | lib/compiler/test/property_test/beam_types_prop.erl | 152 |
1 files changed, 120 insertions, 32 deletions
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl index 9c103d3886..8199d1bd5a 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,33 +34,99 @@ -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)). + +absorption_check(A, B) -> + %% a ∨ (a ∧ b) = a, + A = join(A, meet(A, B)), + + %% a ∧ (a ∨ b) = a. + A = meet(A, join(A, B)), -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. +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 = join(A, join(B, C)), + RHS_Join = join(join(A, B), C), + LHS_Join = RHS_Join, + + %% a ∧ (b ∧ c) = (a ∧ b) ∧ c. + LHS_Meet = meet(A, meet(B, C)), + RHS_Meet = meet(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), - true = beam_types:join(A, B) =:= beam_types:join(B, A), + %% a ∨ b = b ∨ a, + true = join(A, B) =:= join(B, A), + + %% a ∧ b = b ∧ a. + true = meet(A, B) =:= meet(B, A), + + true. + +idempotence() -> + numtests(?REPETITIONS, idempotence_1()). + +idempotence_1() -> + ?FORALL(Type, type(), idempotence_check(Type)). + +idempotence_check(Type) -> + %% a ∨ a = a, + Type = join(Type, Type), + + %% a ∧ a = a. + Type = meet(Type, Type), + + true. + +identity() -> + ?FORALL(Type, type(), identity_check(Type)). + +identity_check(Type) -> + %% a ∨ [bottom element] = a, + Type = join(Type, none), + + %% a ∧ [top element] = a. + Type = meet(Type, any), + true. +meet(A, B) -> beam_types:meet(A, B). +join(A, B) -> beam_types:join(A, B). + %%% %%% Generators %%% @@ -75,7 +141,10 @@ type(Depth) -> other_types()). other_types() -> - [any, gen_atom(), gen_binary(), none]. + [any, + gen_atom(), + gen_binary(), + none]. list_types() -> [cons, list, nil]. @@ -83,8 +152,8 @@ list_types() -> numerical_types() -> [gen_integer(), float, number]. -nested_types(Depth) when Depth >= 3 -> []; -nested_types(Depth) -> [#t_map{}, gen_tuple(Depth + 1)]. +nested_types(Depth) when Depth >= 3 -> [none]; +nested_types(Depth) -> [#t_map{}, gen_union(Depth + 1), gen_tuple(Depth + 1)]. gen_atom() -> ?LET(Size, range(0, ?ATOM_SET_SIZE), @@ -92,35 +161,54 @@ gen_atom() -> 0 -> #t_atom{}; _ -> - ?LET(Set, sized_list(Size, atom()), + ?LET(Set, sized_list(Size, gen_atom_val()), begin #t_atom{elements=ordsets:from_list(Set)} end) end). +gen_atom_val() -> + ?LET(N, range($0, $~), list_to_atom([N])). + gen_binary() -> - ?SHRINK(#t_bitstring{unit=range(1, 128)}, - [#t_bitstring{unit=[1, 2, 3, 5, 7, 8, 16, 32, 64]}]). + ?SHRINK(#t_bitstring{unit=range(1, 128)}, [#t_bitstring{unit=1}]). 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_union(Depth) -> + ?LAZY(oneof([gen_wide_union(Depth), gen_tuple_union(Depth)])). + +gen_wide_union(Depth) -> + ?LET({A, B, C, D}, {oneof(nested_types(Depth)), + oneof(numerical_types()), + oneof(list_types()), + oneof(other_types())}, + begin + T0 = join(A, B), + T1 = join(T0, C), + join(T1, D) + end). + +gen_tuple_union(Depth) -> + ?SIZED(Size, + ?LET(Tuples, sized_list(Size, gen_tuple(Depth)), + lists:foldl(fun join/2, none, Tuples))). gen_tuple_elements(Size, Depth) -> ?LET(Types, sized_list(rand:uniform(Size div 4 + 1), gen_element(Depth)), |