%%
%% %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.