path: root/lib/dialyzer/test/opaque_SUITE_data/src/proper/proper_types.erl

%%% Copyright 2010-2013 Manolis Papadakis <manopapad@gmail.com>,
%%%                     Eirini Arvaniti <eirinibob@gmail.com>
%%%                 and Kostis Sagonas <kostis@cs.ntua.gr>
%%%
%%% 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-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @author Manolis Papadakis

%%% @doc Type manipulation functions and predefined types.
%%%
%%% == Basic types ==
%%% This module defines all the basic types of the PropEr type system as
%%% functions. See the <a href="#index">function index</a> for an overview.
%%%
%%% Types can be combined in tuples or lists to produce other types. Exact
%%% values (such as exact numbers, atoms, binaries and strings) can be combined
%%% with types inside such structures, like in this example of the type of a
%%% tagged tuple: ``{'result', integer()}''.
%%%
%%% When including the PropEr header file, all
%%% <a href="#index">API functions</a> of this module are automatically
%%% imported, unless `PROPER_NO_IMPORTS' is defined.
%%%
%%% == Customized types ==
%%% The following operators can be applied to basic types in order to produce
%%% new ones:
%%%
%%% <dl>
%%% <dt>`?LET(<Xs>, <Xs_type>, <In>)'</dt>
%%% <dd>To produce an instance of this type, all appearances of the variables
%%%   in `<Xs>' are replaced inside `<In>' by their corresponding values in a
%%%   randomly generated instance of `<Xs_type>'. It's OK for the `<In>' part to
%%%   evaluate to a type - in that case, an instance of the inner type is
%%%   generated recursively.</dd>
%%% <dt>`?SUCHTHAT(<X>, <Type>, <Condition>)'</dt>
%%% <dd>This produces a specialization of `<Type>', which only includes those
%%%   members of `<Type>' that satisfy the constraint `<Condition>' - that is,
%%%   those members for which the function `fun(<X>) -> <Condition> end' returns
%%%   `true'. If the constraint is very strict - that is, only a small
%%%   percentage of instances of `<Type>' pass the test - it will take a lot of
%%%   tries for the instance generation subsystem to randomly produce a valid
%%%   instance. This will result in slower testing, and testing may even be
%%%   stopped short, in case the `constraint_tries' limit is reached (see the
%%%   "Options" section in the documentation of the {@link proper} module). If
%%%   this is the case, it would be more appropriate to generate valid instances
%%%   of the specialized type using the `?LET' macro. Also make sure that even
%%%   small instances can satisfy the constraint, since PropEr will only try
%%%   small instances at the start of testing. If this is not possible, you can
%%%   instruct PropEr to start at a larger size, by supplying a suitable value
%%%   for the `start_size' option (see the "Options" section in the
%%%   documentation of the {@link proper} module).</dd>
%%% <dt>`?SUCHTHATMAYBE(<X>, <Type>, <Condition>)'</dt>
%%% <dd>Equivalent to the `?SUCHTHAT' macro, but the constraint `<Condition>'
%%%   is considered non-strict: if the `constraint_tries' limit is reached, the
%%%   generator will just return an instance of `<Type>' instead of failing,
%%%   even if that instance doesn't satisfy the constraint.</dd>
%%% <dt>`?SHRINK(<Generator>, <List_of_alt_gens>)'</dt>
%%% <dd>This creates a type whose instances are generated by evaluating the
%%%   statement block `<Generator>' (this may evaluate to a type, which will
%%%   then be generated recursively). If an instance of such a type is to be
%%%   shrunk, the generators in `<List_of_alt_gens>' are first run to produce
%%%   hopefully simpler instances of the type. Thus, the generators in the
%%%   second argument should be simpler than the default. The simplest ones
%%%   should be at the front of the list, since those are the generators
%%%   preferred by the shrinking subsystem. Like the main `<Generator>', the
%%%   alternatives may also evaluate to a type, which is generated recursively.
%%%   </dd>
%%% <dt>`?LETSHRINK(<List_of_variables>, <List_of_types>, <Generator>)'</dt>
%%% <dd>This is created by combining a `?LET' and a `?SHRINK' macro. Instances
%%%   are generated by applying a randomly generated list of values inside
%%%   `<Generator>' (just like a `?LET', with the added constraint that the
%%%   variables and types must be provided in a list - alternatively,
%%%   `<List_of_types>' may be a list or vector type). When shrinking instances
%%%   of such a type, the sub-instances that were combined to produce it are
%%%   first tried in place of the failing instance.</dd>
%%% <dt>`?LAZY(<Generator>)'</dt>
%%% <dd>This construct returns a type whose only purpose is to delay the
%%%   evaluation of `<Generator>' (`<Generator>' can return a type, which will
%%%   be generated recursively). Using this, you can simulate the lazy
%%%   generation of instances:
%%%   ``` stream() -> ?LAZY(frequency([ {1,[]}, {3,[0|stream()]} ])). '''
%%%   The above type produces lists of zeroes with an average length of 3. Note
%%%   that, had we not enclosed the generator with a `?LAZY' macro, the
%%%   evaluation would continue indefinitely, due to the eager evaluation of
%%%   the Erlang language.</dd>
%%% <dt>`non_empty(<List_or_binary_type>)'</dt>
%%% <dd>See the documentation for {@link non_empty/1}.</dd>
%%% <dt>`noshrink(<Type>)'</dt>
%%% <dd>See the documentation for {@link noshrink/1}.</dd>
%%% <dt>`default(<Default_value>, <Type>)'</dt>
%%% <dd>See the documentation for {@link default/2}.</dd>
%%% <dt>`with_parameter(<Parameter>, <Value>, <Type>)'</dt>
%%% <dd>See the documentation for {@link with_parameter/3}.</dd>
%%% <dt>`with_parameters(<Param_value_pairs>, <Type>)'</dt>
%%% <dd>See the documentation for {@link with_parameters/2}.</dd>
%%% </dl>
%%%
%%% == Size manipulation ==
%%% The following operators are related to the `size' parameter, which controls
%%% the maximum size of produced instances. The actual size of a produced
%%% instance is chosen randomly, but can never exceed the value of the `size'
%%% parameter at the moment of generation. A more accurate definition is the
%%% following: the maximum instance of `size S' can never be smaller than the
%%% maximum instance of `size S-1'. The actual size of an instance is measured
%%% differently for each type: the actual size of a list is its length, while
%%% the actual size of a tree may be the number of its internal nodes. Some
%%% types, e.g. unions, have no notion of size, thus their generation is not
%%% influenced by the value of `size'. The `size' parameter starts at 1 and
%%% grows automatically during testing.
%%%
%%% <dl>
%%% <dt>`?SIZED(<S>, <Generator>)'</dt>
%%% <dd>Creates a new type, whose instances are produced by replacing all
%%%   appearances of the `<S>' parameter inside the statement block
%%%   `<Generator>' with the value of the `size' parameter. It's OK for the
%%%   `<Generator>' to return a type - in that case, an instance of the inner
%%%   type is generated recursively.</dd>
%%% <dt>`resize(<New_size>, <Type>)'</dt>
%%% <dd>See the documentation for {@link resize/2}.</dd>
%%% </dl>

-module(proper_types).
-export([is_inst/2, is_inst/3]).

-export([integer/2, float/2, atom/0, binary/0, binary/1, bitstring/0,
	 bitstring/1, list/1, vector/2, union/1, weighted_union/1, tuple/1,
	 loose_tuple/1, exactly/1, fixed_list/1, function/2, any/0,
	 shrink_list/1, safe_union/1, safe_weighted_union/1]).
-export([integer/0, non_neg_integer/0, pos_integer/0, neg_integer/0, range/2,
	 float/0, non_neg_float/0, number/0, boolean/0, byte/0, char/0,
	 list/0, tuple/0, string/0, wunion/1, term/0, timeout/0, arity/0]).
-export([int/0, nat/0, largeint/0, real/0, bool/0, choose/2, elements/1,
	 oneof/1, frequency/1, return/1, default/2, orderedlist/1, function0/1,
	 function1/1, function2/1, function3/1, function4/1,
	 weighted_default/2]).
-export([resize/2, non_empty/1, noshrink/1]).

-export([cook_outer/1, is_type/1, equal_types/2, is_raw_type/1, to_binary/1,
	 from_binary/1, get_prop/2, find_prop/2, safe_is_instance/2,
	 is_instance/2, unwrap/1, weakly/1, strongly/1, satisfies_all/2,
	 new_type/2, subtype/2]).
-export([lazy/1, sized/1, bind/3, shrinkwith/2, add_constraint/3,
	 native_type/2, distlist/3, with_parameter/3, with_parameters/2,
	 parameter/1, parameter/2]).
-export([le/2]).

-export_type([type/0, raw_type/0, extint/0, extnum/0]).

-include("proper_internal.hrl").


%%------------------------------------------------------------------------------
%% Comparison with erl_types
%%------------------------------------------------------------------------------

%% Missing types
%% -------------------
%% will do:
%%	records, maybe_improper_list(T,S), nonempty_improper_list(T,S)
%%	maybe_improper_list(), maybe_improper_list(T), iolist, iodata
%% don't need:
%%	nonempty_{list,string,maybe_improper_list}
%% won't do:
%%	pid, port, ref, identifier, none, no_return, module, mfa, node
%%	array, dict, digraph, set, gb_tree, gb_set, queue, tid

%% Missing type information
%% ------------------------
%% bin types:
%%	other unit sizes? what about size info?
%% functions:
%%	generally some fun, unspecified number of arguments but specified
%%	return type
%% any:
%%	doesn't cover functions and improper lists


%%------------------------------------------------------------------------------
%% Type declaration macros
%%------------------------------------------------------------------------------

-define(BASIC(PropList), new_type(PropList,basic)).
-define(WRAPPER(PropList), new_type(PropList,wrapper)).
-define(CONSTRUCTED(PropList), new_type(PropList,constructed)).
-define(CONTAINER(PropList), new_type(PropList,container)).
-define(SUBTYPE(Type,PropList), subtype(PropList,Type)).


%%------------------------------------------------------------------------------
%% Types
%%------------------------------------------------------------------------------

-type type_kind() :: 'basic' | 'wrapper' | 'constructed' | 'container' | atom().
-type instance_test() :: fun((proper_gen:imm_instance()) -> boolean())
                       | {'typed',
                          fun((proper_types:type(),
                               proper_gen:imm_instance()) -> boolean())}.
-type index() :: pos_integer().
%% @alias
-type value() :: term().
%% @private_type
%% @alias
-type extint()  :: integer() | 'inf'.
%% @private_type
%% @alias
-type extnum()  :: number()  | 'inf'.
-type constraint_fun() :: fun((proper_gen:instance()) -> boolean()).

-opaque type() :: {'$type', [type_prop()]}.
%% A type of the PropEr type system
%% @type raw_type(). You can consider this as an equivalent of {@type type()}.
-type raw_type() :: type() | [raw_type()] | loose_tuple(raw_type()) | term().
-type type_prop_name() :: 'kind' | 'generator' | 'reverse_gen' | 'parts_type'
			| 'combine' | 'alt_gens' | 'shrink_to_parts'
			| 'size_transform' | 'is_instance' | 'shrinkers'
			| 'noshrink' | 'internal_type' | 'internal_types'
			| 'get_length' | 'split' | 'join' | 'get_indices'
			| 'remove' | 'retrieve' | 'update' | 'constraints'
			| 'parameters' | 'env' | 'subenv'.

-type type_prop_value() :: term().
-type type_prop() ::
      {'kind', type_kind()}
    | {'generator', proper_gen:generator()}
    | {'reverse_gen', proper_gen:reverse_gen()}
    | {'parts_type', type()}
    | {'combine', proper_gen:combine_fun()}
    | {'alt_gens', proper_gen:alt_gens()}
    | {'shrink_to_parts', boolean()}
    | {'size_transform', fun((size()) -> size())}
    | {'is_instance', instance_test()}
    | {'shrinkers', [proper_shrink:shrinker()]}
    | {'noshrink', boolean()}
    | {'internal_type', raw_type()}
    | {'internal_types', tuple() | maybe_improper_list(type(),type() | [])}
      %% The items returned by 'remove' must be of this type.
    | {'get_length', fun((proper_gen:imm_instance()) -> length())}
      %% If this is a container type, this should return the number of elements
      %% it contains.
    | {'split', fun((proper_gen:imm_instance()) -> [proper_gen:imm_instance()])
	      | fun((length(),proper_gen:imm_instance()) ->
		    {proper_gen:imm_instance(),proper_gen:imm_instance()})}
      %% If present, the appropriate form depends on whether get_length is
      %% defined: if get_length is undefined, this must be in the one-argument
      %% form (e.g. a tree should be split into its subtrees), else it must be
      %% in the two-argument form (e.g. a list should be split in two at the
      %% index provided).
    | {'join', fun((proper_gen:imm_instance(),proper_gen:imm_instance()) ->
		   proper_gen:imm_instance())}
    | {'get_indices', fun((proper_types:type(),
                           proper_gen:imm_instance()) -> [index()])}
      %% If this is a container type, this should return a list of indices we
      %% can use to remove or insert elements from the given instance.
    | {'remove', fun((index(),proper_gen:imm_instance()) ->
		     proper_gen:imm_instance())}
    | {'retrieve', fun((index(), proper_gen:imm_instance() | tuple()
			       | maybe_improper_list(type(),type() | [])) ->
		       value() | type())}
    | {'update', fun((index(),value(),proper_gen:imm_instance()) ->
		     proper_gen:imm_instance())}
    | {'constraints', [{constraint_fun(), boolean()}]}
      %% A list of constraints on instances of this type: each constraint is a
      %% tuple of a fun that must return 'true' for each valid instance and a
      %% boolean field that specifies whether the condition is strict.
    | {'parameters', [{atom(),value()}]}
    | {'env', term()}
    | {'subenv', term()}.


%%------------------------------------------------------------------------------
%% Type manipulation functions
%%------------------------------------------------------------------------------

%% TODO: We shouldn't need the fully qualified type name in the range of these
%%       functions.

%% @private
%% TODO: just cook/1 ?
-spec cook_outer(raw_type()) -> proper_types:type().
cook_outer(Type = {'$type',_Props}) ->
    Type;
cook_outer(RawType) ->
    if
	is_tuple(RawType) -> tuple(tuple_to_list(RawType));
	%% CAUTION: this must handle improper lists
	is_list(RawType)  -> fixed_list(RawType);
	%% default case (covers integers, floats, atoms, binaries, ...):
	true              -> exactly(RawType)
    end.

%% @private
-spec is_type(term()) -> boolean().
is_type({'$type',_Props}) ->
    true;
is_type(_) ->
    false.

%% @private
-spec equal_types(proper_types:type(), proper_types:type()) -> boolean().
equal_types(SameType, SameType) ->
    true;
equal_types(_, _) ->
    false.

%% @private
-spec is_raw_type(term()) -> boolean().
is_raw_type({'$type',_TypeProps}) ->
    true;
is_raw_type(X) ->
    if
	is_tuple(X) -> is_raw_type_list(tuple_to_list(X));
	is_list(X)  -> is_raw_type_list(X);
	true        -> false
    end.

-spec is_raw_type_list(maybe_improper_list()) -> boolean().
%% CAUTION: this must handle improper lists
is_raw_type_list(List) ->
    proper_arith:safe_any(fun is_raw_type/1, List).

%% @private
-spec to_binary(proper_types:type()) -> binary().
to_binary(Type) ->
    term_to_binary(Type).

%% @private
%% TODO: restore: -spec from_binary(binary()) -> proper_types:type().
from_binary(Binary) ->
    binary_to_term(Binary).

-spec type_from_list([type_prop()]) -> proper_types:type().
type_from_list(KeyValueList) ->
    {'$type',KeyValueList}.

-spec add_prop(type_prop_name(), type_prop_value(), proper_types:type()) ->
	  proper_types:type().
add_prop(PropName, Value, {'$type',Props}) ->
    {'$type',lists:keystore(PropName, 1, Props, {PropName, Value})}.

-spec add_props([type_prop()], proper_types:type()) -> proper_types:type().
add_props(PropList, {'$type',OldProps}) ->
    {'$type', lists:foldl(fun({N,_}=NV,Acc) ->
                    lists:keystore(N, 1, Acc, NV)
                end, OldProps, PropList)}.

-spec append_to_prop(type_prop_name(), type_prop_value(),
		     proper_types:type()) -> proper_types:type().
append_to_prop(PropName, Value, {'$type',Props}) ->
    Val = case lists:keyfind(PropName, 1, Props) of
        {PropName, V} ->
            V;
        _ ->
            []
    end,
    {'$type', lists:keystore(PropName, 1, Props,
                             {PropName, lists:reverse([Value|Val])})}.

-spec append_list_to_prop(type_prop_name(), [type_prop_value()],
			  proper_types:type()) -> proper_types:type().
append_list_to_prop(PropName, List, {'$type',Props}) ->
    {PropName, Val} = lists:keyfind(PropName, 1, Props),
    {'$type', lists:keystore(PropName, 1, Props, {PropName, Val++List})}.

%% @private
-spec get_prop(type_prop_name(), proper_types:type()) -> type_prop_value().
get_prop(PropName, {'$type',Props}) ->
    {_PropName, Val} = lists:keyfind(PropName, 1, Props),
    Val.

%% @private
-spec find_prop(type_prop_name(), proper_types:type()) ->
	  {'ok',type_prop_value()} | 'error'.
find_prop(PropName, {'$type',Props}) ->
    case lists:keyfind(PropName, 1, Props) of
        {PropName, Value} ->
            {ok, Value};
        _ ->
            error
    end.

%% @private
-spec new_type([type_prop()], type_kind()) -> proper_types:type().
new_type(PropList, Kind) ->
    Type = type_from_list(PropList),
    add_prop(kind, Kind, Type).

%% @private
-spec subtype([type_prop()], proper_types:type()) -> proper_types:type().
%% TODO: should the 'is_instance' function etc. be reset for subtypes?
subtype(PropList, Type) ->
    add_props(PropList, Type).

%% @private
-spec is_inst(proper_gen:instance(), raw_type()) ->
	  boolean() | {'error',{'typeserver',term()}}.
is_inst(Instance, RawType) ->
    is_inst(Instance, RawType, 10).

%% @private
-spec is_inst(proper_gen:instance(), raw_type(), size()) ->
	  boolean() | {'error',{'typeserver',term()}}.
is_inst(Instance, RawType, Size) ->
    proper:global_state_init_size(Size),
    Result = safe_is_instance(Instance, RawType),
    proper:global_state_erase(),
    Result.

%% @private
-spec safe_is_instance(proper_gen:imm_instance(), raw_type()) ->
	  boolean() | {'error',{'typeserver',term()}}.
safe_is_instance(ImmInstance, RawType) ->
    try is_instance(ImmInstance, RawType) catch
	throw:{'$typeserver',SubReason} -> {error, {typeserver,SubReason}}
    end.

%% @private
-spec is_instance(proper_gen:imm_instance(), raw_type()) -> boolean().
%% TODO: If the second argument is not a type, let it pass (don't even check for
%%	 term equality?) - if it's a raw type, don't cook it, instead recurse
%%	 into it.
is_instance(ImmInstance, RawType) ->
    CleanInstance = proper_gen:clean_instance(ImmInstance),
    Type = cook_outer(RawType),
    (case get_prop(kind, Type) of
	 wrapper     -> wrapper_test(ImmInstance, Type);
	 constructed -> constructed_test(ImmInstance, Type);
	 _           -> false
     end
     orelse
     case find_prop(is_instance, Type) of
	 {ok,{typed, IsInstance}} -> IsInstance(Type, ImmInstance);
	 {ok,IsInstance} -> IsInstance(ImmInstance);
	 error           -> false
     end)
    andalso weakly(satisfies_all(CleanInstance, Type)).

-spec wrapper_test(proper_gen:imm_instance(), proper_types:type()) -> boolean().
wrapper_test(ImmInstance, Type) ->
    %% TODO: check if it's actually a raw type that's returned?
    lists:any(fun(T) -> is_instance(ImmInstance, T) end, unwrap(Type)).

%% @private
%% TODO: restore:-spec unwrap(proper_types:type()) -> [proper_types:type(),...].
%% TODO: check if it's actually a raw type that's returned?
unwrap(Type) ->
    RawInnerTypes = proper_gen:alt_gens(Type) ++ [proper_gen:normal_gen(Type)],
    [cook_outer(T) || T <- RawInnerTypes].

-spec constructed_test(proper_gen:imm_instance(), proper_types:type()) ->
	  boolean().
constructed_test({'$used',ImmParts,ImmInstance}, Type) ->
    PartsType = get_prop(parts_type, Type),
    Combine = get_prop(combine, Type),
    is_instance(ImmParts, PartsType) andalso
    begin
	%% TODO: check if it's actually a raw type that's returned?
	%% TODO: move construction code to proper_gen
	%% TODO: non-type => should we check for strict term equality?
	RawInnerType = Combine(proper_gen:clean_instance(ImmParts)),
	is_instance(ImmInstance, RawInnerType)
    end;
constructed_test({'$to_part',ImmInstance}, Type) ->
    PartsType = get_prop(parts_type, Type),
    get_prop(shrink_to_parts, Type) =:= true andalso
    %% TODO: we reject non-container types
    get_prop(kind, PartsType) =:= container andalso
    case {find_prop(internal_type,PartsType),
	  find_prop(internal_types,PartsType)} of
	{{ok,EachPartType},error} ->
	    %% The parts are in a list or a vector.
	    is_instance(ImmInstance, EachPartType);
	{error,{ok,PartTypesList}} ->
	    %% The parts are in a fixed list.
	    %% TODO: It should always be a proper list.
	    lists:any(fun(T) -> is_instance(ImmInstance,T) end, PartTypesList)
    end;
constructed_test(_CleanInstance, _Type) ->
    %% TODO: can we do anything better?
    false.

%% @private
-spec weakly({boolean(),boolean()}) -> boolean().
weakly({B1,_B2}) -> B1.

%% @private
-spec strongly({boolean(),boolean()}) -> boolean().
strongly({_B1,B2}) -> B2.

-spec satisfies(proper_gen:instance(), {constraint_fun(),boolean()})
	  -> {boolean(),boolean()}.
satisfies(Instance, {Test,false}) ->
    {true,Test(Instance)};
satisfies(Instance, {Test,true}) ->
    Result = Test(Instance),
    {Result,Result}.

%% @private
-spec satisfies_all(proper_gen:instance(), proper_types:type()) ->
	  {boolean(),boolean()}.
satisfies_all(Instance, Type) ->
    case find_prop(constraints, Type) of
	{ok, Constraints} ->
	    L = [satisfies(Instance, C) || C <- Constraints],
	    {L1,L2} = lists:unzip(L),
	    {lists:all(fun(B) -> B end, L1), lists:all(fun(B) -> B end, L2)};
	error ->
	    {true,true}
    end.


%%------------------------------------------------------------------------------
%% Type definition functions
%%------------------------------------------------------------------------------

%% @private
-spec lazy(proper_gen:nosize_generator()) -> proper_types:type().
lazy(Gen) ->
    ?WRAPPER([
	{generator, Gen}
    ]).

%% @private
-spec sized(proper_gen:sized_generator()) -> proper_types:type().
sized(Gen) ->
    ?WRAPPER([
        {generator, Gen}
    ]).

%% @private
-spec bind(raw_type(), proper_gen:combine_fun(), boolean()) ->
	  proper_types:type().
bind(RawPartsType, Combine, ShrinkToParts) ->
    PartsType = cook_outer(RawPartsType),
    ?CONSTRUCTED([
	{parts_type, PartsType},
	{combine, Combine},
	{shrink_to_parts, ShrinkToParts}
    ]).

%% @private
-spec shrinkwith(proper_gen:nosize_generator(), proper_gen:alt_gens()) ->
	  proper_types:type().
shrinkwith(Gen, DelaydAltGens) ->
    ?WRAPPER([
	{generator, Gen},
	{alt_gens, DelaydAltGens}
    ]).

%% @private
-spec add_constraint(raw_type(), constraint_fun(), boolean()) ->
	  proper_types:type().
add_constraint(RawType, Condition, IsStrict) ->
    Type = cook_outer(RawType),
    append_to_prop(constraints, {Condition,IsStrict}, Type).

%% @private
-spec native_type(mod_name(), string()) -> proper_types:type().
native_type(Mod, TypeStr) ->
    ?WRAPPER([
	{generator, fun() ->  proper_gen:native_type_gen(Mod,TypeStr) end}
    ]).


%%------------------------------------------------------------------------------
%% Basic types
%%------------------------------------------------------------------------------

%% @doc All integers between `Low' and `High', bounds included.
%% `Low' and `High' must be Erlang expressions that evaluate to integers, with
%% `Low =< High'. Additionally, `Low' and `High' may have the value `inf', in
%% which case they represent minus infinity and plus infinity respectively.
%% Instances shrink towards 0 if `Low =< 0 =< High', or towards the bound with
%% the smallest absolute value otherwise.
-spec integer(extint(), extint()) -> proper_types:type().
integer(Low, High) ->
    ?BASIC([
	{env, {Low, High}},
	{generator, {typed, fun integer_gen/2}},
	{is_instance, {typed, fun integer_is_instance/2}},
	{shrinkers, [fun number_shrinker/3]}
    ]).

integer_gen(Type, Size) ->
    {Low, High} = get_prop(env, Type),
    proper_gen:integer_gen(Size, Low, High).

integer_is_instance(Type, X) ->
    {Low, High} = get_prop(env, Type),
    is_integer(X) andalso le(Low, X) andalso le(X, High).

number_shrinker(X, Type, S) ->
    {Low, High} = get_prop(env, Type),
    proper_shrink:number_shrinker(X, Low, High, S).

%% @doc All floats between `Low' and `High', bounds included.
%% `Low' and `High' must be Erlang expressions that evaluate to floats, with
%% `Low =< High'. Additionally, `Low' and `High' may have the value `inf', in
%% which case they represent minus infinity and plus infinity respectively.
%% Instances shrink towards 0.0 if `Low =< 0.0 =< High', or towards the bound
%% with the smallest absolute value otherwise.
-spec float(extnum(), extnum()) -> proper_types:type().
float(Low, High) ->
    ?BASIC([
	{env, {Low, High}},
	{generator, {typed, fun float_gen/2}},
	{is_instance, {typed, fun float_is_instance/2}},
	{shrinkers, [fun number_shrinker/3]}
    ]).

float_gen(Type, Size) ->
    {Low, High} = get_prop(env, Type),
    proper_gen:float_gen(Size, Low, High).

float_is_instance(Type, X) ->
    {Low, High} = get_prop(env, Type),
    is_float(X) andalso le(Low, X) andalso le(X, High).

%% @private
-spec le(extnum(), extnum()) -> boolean().
le(inf, _B) -> true;
le(_A, inf) -> true;
le(A, B)    -> A =< B.

%% @doc All atoms. All atoms used internally by PropEr start with a '`$'', so
%% such atoms will never be produced as instances of this type. You should also
%% refrain from using such atoms in your code, to avoid a potential clash.
%% Instances shrink towards the empty atom, ''.
-spec atom() -> proper_types:type().
atom() ->
    ?WRAPPER([
	{generator, fun proper_gen:atom_gen/1},
	{reverse_gen, fun proper_gen:atom_rev/1},
	{size_transform, fun(Size) -> erlang:min(Size,255) end},
	{is_instance, fun atom_is_instance/1}
    ]).

atom_is_instance(X) ->
    is_atom(X)
    %% We return false for atoms starting with '$', since these are
    %% atoms used internally and never produced by the atom generator.
    andalso (X =:= '' orelse hd(atom_to_list(X)) =/= $$).

%% @doc All binaries. Instances shrink towards the empty binary, `<<>>'.
-spec binary() -> proper_types:type().
binary() ->
    ?WRAPPER([
	{generator, fun proper_gen:binary_gen/1},
	{reverse_gen, fun proper_gen:binary_rev/1},
	{is_instance, fun erlang:is_binary/1}
    ]).

%% @doc All binaries with a byte size of `Len'.
%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
%% Instances shrink towards binaries of zeroes.
-spec binary(length()) -> proper_types:type().
binary(Len) ->
    ?WRAPPER([
	{env, Len},
	{generator, {typed, fun binary_len_gen/1}},
	{reverse_gen, fun proper_gen:binary_rev/1},
	{is_instance, {typed, fun binary_len_is_instance/2}}
    ]).

binary_len_gen(Type) ->
    Len = get_prop(env, Type),
    proper_gen:binary_len_gen(Len).

binary_len_is_instance(Type, X) ->
    Len = get_prop(env, Type),
    is_binary(X) andalso byte_size(X) =:= Len.

%% @doc All bitstrings. Instances shrink towards the empty bitstring, `<<>>'.
-spec bitstring() -> proper_types:type().
bitstring() ->
    ?WRAPPER([
	{generator, fun proper_gen:bitstring_gen/1},
	{reverse_gen, fun proper_gen:bitstring_rev/1},
	{is_instance, fun erlang:is_bitstring/1}
    ]).

%% @doc All bitstrings with a bit size of `Len'.
%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
%% Instances shrink towards bitstrings of zeroes
-spec bitstring(length()) -> proper_types:type().
bitstring(Len) ->
    ?WRAPPER([
	{env, Len},
	{generator, {typed, fun bitstring_len_gen/1}},
	{reverse_gen, fun proper_gen:bitstring_rev/1},
	{is_instance, {typed, fun bitstring_len_is_instance/2}}
    ]).

bitstring_len_gen(Type) ->
    Len = get_prop(env, Type),
    proper_gen:bitstring_len_gen(Len).

bitstring_len_is_instance(Type, X) ->
    Len = get_prop(env, Type),
    is_bitstring(X) andalso bit_size(X) =:= Len.

%% @doc All lists containing elements of type `ElemType'.
%% Instances shrink towards the empty list, `[]'.
-spec list(ElemType::raw_type()) -> proper_types:type().
% TODO: subtyping would be useful here (list, vector, fixed_list)
list(RawElemType) ->
    ElemType = cook_outer(RawElemType),
    ?CONTAINER([
	{generator, {typed, fun list_gen/2}},
	{is_instance, {typed, fun list_is_instance/2}},
	{internal_type, ElemType},
	{get_length, fun erlang:length/1},
	{split, fun lists:split/2},
	{join, fun lists:append/2},
	{get_indices, fun list_get_indices/2},
	{remove, fun proper_arith:list_remove/2},
	{retrieve, fun lists:nth/2},
	{update, fun proper_arith:list_update/3}
    ]).

list_gen(Type, Size) ->
    ElemType = get_prop(internal_type, Type),
    proper_gen:list_gen(Size, ElemType).

list_is_instance(Type, X) ->
    ElemType = get_prop(internal_type, Type),
    list_test(X, ElemType).

%% @doc A type that generates exactly the list `List'. Instances shrink towards
%% shorter sublists of the original list.
-spec shrink_list([term()]) -> proper_types:type().
shrink_list(List) ->
    ?CONTAINER([
	{env, List},
	{generator, {typed, fun shrink_list_gen/1}},
	{is_instance, {typed, fun shrink_list_is_instance/2}},
	{get_length, fun erlang:length/1},
	{split, fun lists:split/2},
	{join, fun lists:append/2},
	{get_indices, fun list_get_indices/2},
	{remove, fun proper_arith:list_remove/2}
    ]).

shrink_list_gen(Type) ->
    get_prop(env, Type).

shrink_list_is_instance(Type, X) ->
    List = get_prop(env, Type),
    is_sublist(X, List).

-spec is_sublist([term()], [term()]) -> boolean().
is_sublist([], _) -> true;
is_sublist(_, []) -> false;
is_sublist([H|T1], [H|T2]) -> is_sublist(T1, T2);
is_sublist(Slice, [_|T2]) -> is_sublist(Slice, T2).

-spec list_test(proper_gen:imm_instance(), proper_types:type()) -> boolean().
list_test(X, ElemType) ->
    is_list(X) andalso lists:all(fun(E) -> is_instance(E, ElemType) end, X).

%% @private
-spec list_get_indices(proper_gen:generator(), list()) -> [position()].
list_get_indices(_, List) ->
    lists:seq(1, length(List)).

%% @private
%% This assumes that:
%% - instances of size S are always valid instances of size >S
%% - any recursive calls inside Gen are lazy
-spec distlist(size(), proper_gen:sized_generator(), boolean()) ->
	  proper_types:type().
distlist(Size, Gen, NonEmpty) ->
    ParentType = case NonEmpty of
		     true  -> non_empty(list(Gen(Size)));
		     false -> list(Gen(Size))
		 end,
    ?SUBTYPE(ParentType, [
	{subenv, {Size, Gen, NonEmpty}},
	{generator, {typed, fun distlist_gen/1}}
    ]).

distlist_gen(Type) ->
    {Size, Gen, NonEmpty} = get_prop(subenv, Type),
    proper_gen:distlist_gen(Size, Gen, NonEmpty).

%% @doc All lists of length `Len' containing elements of type `ElemType'.
%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
-spec vector(length(), ElemType::raw_type()) -> proper_types:type().
vector(Len, RawElemType) ->
    ElemType = cook_outer(RawElemType),
    ?CONTAINER([
	{env, Len},
	{generator, {typed, fun vector_gen/1}},
	{is_instance, {typed, fun vector_is_instance/2}},
	{internal_type, ElemType},
	{get_indices, fun vector_get_indices/2},
	{retrieve, fun lists:nth/2},
	{update, fun proper_arith:list_update/3}
    ]).

vector_gen(Type) ->
    Len = get_prop(env, Type),
    ElemType = get_prop(internal_type, Type),
    proper_gen:vector_gen(Len, ElemType).

vector_is_instance(Type, X) ->
    Len = get_prop(env, Type),
    ElemType = get_prop(internal_type, Type),
    is_list(X)
    andalso length(X) =:= Len
    andalso lists:all(fun(E) -> is_instance(E, ElemType) end, X).

vector_get_indices(Type, _X) ->
    lists:seq(1, get_prop(env, Type)).

%% @doc The union of all types in `ListOfTypes'. `ListOfTypes' can't be empty.
%% The random instance generator is equally likely to choose any one of the
%% types in `ListOfTypes'. The shrinking subsystem will always try to shrink an
%% instance of a type union to an instance of the first type in `ListOfTypes',
%% thus you should write the simplest case first.
-spec union(ListOfTypes::[raw_type(),...]) -> proper_types:type().
union(RawChoices) ->
    Choices = [cook_outer(C) || C <- RawChoices],
    ?BASIC([
	{env, Choices},
	{generator, {typed, fun union_gen/1}},
	{is_instance, {typed, fun union_is_instance/2}},
	{shrinkers, [fun union_shrinker_1/3, fun union_shrinker_2/3]}
    ]).

union_gen(Type) ->
    Choices = get_prop(env,Type),
    proper_gen:union_gen(Choices).

union_is_instance(Type, X) ->
    Choices = get_prop(env, Type),
    lists:any(fun(C) -> is_instance(X, C) end, Choices).

union_shrinker_1(X, Type, S) ->
    Choices = get_prop(env, Type),
    proper_shrink:union_first_choice_shrinker(X, Choices, S).

union_shrinker_2(X, Type, S) ->
    Choices = get_prop(env, Type),
    proper_shrink:union_recursive_shrinker(X, Choices, S).

%% @doc A specialization of {@link union/1}, where each type in `ListOfTypes' is
%% assigned a frequency. Frequencies must be Erlang expressions that evaluate to
%% positive integers. Types with larger frequencies are more likely to be chosen
%% by the random instance generator. The shrinking subsystem will ignore the
%% frequencies and try to shrink towards the first type in the list.
-spec weighted_union(ListOfTypes::[{frequency(),raw_type()},...]) ->
          proper_types:type().
weighted_union(RawFreqChoices) ->
    CookFreqType = fun({Freq,RawType}) -> {Freq,cook_outer(RawType)} end,
    FreqChoices = lists:map(CookFreqType, RawFreqChoices),
    Choices = [T || {_F,T} <- FreqChoices],
    ?SUBTYPE(union(Choices), [
	{subenv, FreqChoices},
	{generator, {typed, fun weighted_union_gen/1}}
    ]).

weighted_union_gen(Gen) ->
    FreqChoices = get_prop(subenv, Gen),
    proper_gen:weighted_union_gen(FreqChoices).

%% @private
-spec safe_union([raw_type(),...]) -> proper_types:type().
safe_union(RawChoices) ->
    Choices = [cook_outer(C) || C <- RawChoices],
    subtype(
      [{subenv, Choices},
       {generator, {typed, fun safe_union_gen/1}}],
      union(Choices)).

safe_union_gen(Type) ->
    Choices = get_prop(subenv, Type),
    proper_gen:safe_union_gen(Choices).

%% @private
-spec safe_weighted_union([{frequency(),raw_type()},...]) ->
         proper_types:type().
safe_weighted_union(RawFreqChoices) ->
    CookFreqType = fun({Freq,RawType}) ->
			   {Freq,cook_outer(RawType)} end,
    FreqChoices = lists:map(CookFreqType, RawFreqChoices),
    Choices = [T || {_F,T} <- FreqChoices],
    subtype([{subenv, FreqChoices},
             {generator, {typed, fun safe_weighted_union_gen/1}}],
            union(Choices)).

safe_weighted_union_gen(Type) ->
    FreqChoices = get_prop(subenv, Type),
    proper_gen:safe_weighted_union_gen(FreqChoices).

%% @doc All tuples whose i-th element is an instance of the type at index i of
%% `ListOfTypes'. Also written simply as a tuple of types.
-spec tuple(ListOfTypes::[raw_type()]) -> proper_types:type().
tuple(RawFields) ->
    Fields = [cook_outer(F) || F <- RawFields],
    ?CONTAINER([
	{env, Fields},
	{generator, {typed, fun tuple_gen/1}},
	{is_instance, {typed, fun tuple_is_instance/2}},
	{internal_types, list_to_tuple(Fields)},
	{get_indices, fun tuple_get_indices/2},
	{retrieve, fun erlang:element/2},
	{update, fun tuple_update/3}
    ]).

tuple_gen(Type) ->
    Fields = get_prop(env, Type),
    proper_gen:tuple_gen(Fields).

tuple_is_instance(Type, X) ->
    Fields = get_prop(env, Type),
    is_tuple(X) andalso fixed_list_test(tuple_to_list(X), Fields).

tuple_get_indices(Type, _X) ->
    lists:seq(1, length(get_prop(env, Type))).

-spec tuple_update(index(), value(), tuple()) -> tuple().
tuple_update(Index, NewElem, Tuple) ->
    setelement(Index, Tuple, NewElem).

%% @doc Tuples whose elements are all of type `ElemType'.
%% Instances shrink towards the 0-size tuple, `{}'.
-spec loose_tuple(ElemType::raw_type()) -> proper_types:type().
loose_tuple(RawElemType) ->
    ElemType = cook_outer(RawElemType),
    ?WRAPPER([
	{env, ElemType},
	{generator, {typed, fun loose_tuple_gen/2}},
	{reverse_gen, {typed, fun loose_tuple_rev/2}},
	{is_instance, {typed, fun loose_tuple_is_instance/2}}
    ]).

loose_tuple_gen(Type, Size) ->
    ElemType = get_prop(env, Type),
    proper_gen:loose_tuple_gen(Size, ElemType).

loose_tuple_rev(Type, X) ->
    ElemType = get_prop(env, Type),
    proper_gen:loose_tuple_rev(X, ElemType).

loose_tuple_is_instance(Type, X) ->
    ElemType = get_prop(env, Type),
    is_tuple(X) andalso list_test(tuple_to_list(X), ElemType).

%% @doc Singleton type consisting only of `E'. `E' must be an evaluated term.
%% Also written simply as `E'.
-spec exactly(term()) -> proper_types:type().
exactly(E) ->
    ?BASIC([
	{env, E},
	{generator, {typed, fun exactly_gen/1}},
	{is_instance, {typed, fun exactly_is_instance/2}}
    ]).

exactly_gen(Type) ->
    E = get_prop(env, Type),
    proper_gen:exactly_gen(E).

exactly_is_instance(Type, X) ->
    E = get_prop(env, Type),
    X =:= E.

%% @doc All lists whose i-th element is an instance of the type at index i of
%% `ListOfTypes'. Also written simply as a list of types.
-spec fixed_list(ListOfTypes::maybe_improper_list(raw_type(),raw_type()|[])) ->
	  proper_types:type().
fixed_list(MaybeImproperRawFields) ->
    %% CAUTION: must handle improper lists
    {Fields, Internal, Len, Retrieve, Update} =
	case proper_arith:cut_improper_tail(MaybeImproperRawFields) of
	    % TODO: have cut_improper_tail return the length and use it in test?
	    {ProperRawHead, ImproperRawTail} ->
		HeadLen = length(ProperRawHead),
		CookedHead = [cook_outer(F) || F <- ProperRawHead],
		CookedTail = cook_outer(ImproperRawTail),
		{{CookedHead,CookedTail},
		 CookedHead ++ CookedTail,
		 HeadLen + 1,
		 fun(I,L) -> improper_list_retrieve(I, L, HeadLen) end,
		 fun(I,V,L) -> improper_list_update(I, V, L, HeadLen) end};
	    ProperRawFields ->
		LocalFields = [cook_outer(F) || F <- ProperRawFields],
		{LocalFields,
		 LocalFields,
		 length(ProperRawFields),
		 fun lists:nth/2,
		 fun proper_arith:list_update/3}
	end,
    ?CONTAINER([
	{env, {Fields, Len}},
	{generator, {typed, fun fixed_list_gen/1}},
	{is_instance, {typed, fun fixed_list_is_instance/2}},
	{internal_types, Internal},
	{get_indices, fun fixed_list_get_indices/2},
	{retrieve, Retrieve},
	{update, Update}
    ]).

fixed_list_gen(Type) ->
    {Fields, _} = get_prop(env, Type),
    proper_gen:fixed_list_gen(Fields).

fixed_list_is_instance(Type, X) ->
    {Fields, _} = get_prop(env, Type),
    fixed_list_test(X, Fields).

fixed_list_get_indices(Type, _X) ->
    {_, Len} = get_prop(env, Type),
    lists:seq(1, Len).

-spec fixed_list_test(proper_gen:imm_instance(),
		      [proper_types:type()] | {[proper_types:type()],
					       proper_types:type()}) ->
	  boolean().
fixed_list_test(X, {ProperHead,ImproperTail}) ->
    is_list(X) andalso
    begin
	ProperHeadLen = length(ProperHead),
	proper_arith:head_length(X) >= ProperHeadLen andalso
	begin
	    {XHead,XTail} = lists:split(ProperHeadLen, X),
	    fixed_list_test(XHead, ProperHead)
	    andalso is_instance(XTail, ImproperTail)
	end
    end;
fixed_list_test(X, ProperFields) ->
    is_list(X)
    andalso length(X) =:= length(ProperFields)
    andalso lists:all(fun({E,T}) -> is_instance(E, T) end,
		      lists:zip(X, ProperFields)).

%% TODO: Move these 2 functions to proper_arith?
-spec improper_list_retrieve(index(), nonempty_improper_list(value(),value()),
			     pos_integer()) -> value().
improper_list_retrieve(Index, List, HeadLen) ->
    case Index =< HeadLen of
	true  -> lists:nth(Index, List);
	false -> lists:nthtail(HeadLen, List)
    end.

-spec improper_list_update(index(), value(),
			   nonempty_improper_list(value(),value()),
			   pos_integer()) ->
	  nonempty_improper_list(value(),value()).
improper_list_update(Index, Value, List, HeadLen) ->
    case Index =< HeadLen of
	%% TODO: This happens to work, but is not implied by list_update's spec.
	true  -> proper_arith:list_update(Index, Value, List);
	false -> lists:sublist(List, HeadLen) ++ Value
    end.

%% @doc All pure functions that map instances of `ArgTypes' to instances of
%% `RetType'. The syntax `function(Arity, RetType)' is also acceptable.
-spec function(ArgTypes::[raw_type()] | arity(), RetType::raw_type()) ->
          proper_types:type().
function(Arity, RawRetType) when is_integer(Arity), Arity >= 0, Arity =< 255 ->
    RetType = cook_outer(RawRetType),
    ?BASIC([
	{env, {Arity, RetType}},
	{generator, {typed, fun function_gen/1}},
	{is_instance, {typed, fun function_is_instance/2}}
    ]);
function(RawArgTypes, RawRetType) ->
    function(length(RawArgTypes), RawRetType).

function_gen(Type) ->
    {Arity, RetType} = get_prop(env, Type),
    proper_gen:function_gen(Arity, RetType).

function_is_instance(Type, X) ->
    {Arity, RetType} = get_prop(env, Type),
    is_function(X, Arity)
    %% TODO: what if it's not a function we produced?
    andalso equal_types(RetType, proper_gen:get_ret_type(X)).

%% @doc All Erlang terms (that PropEr can produce). For reasons of efficiency,
%% functions are never produced as instances of this type.<br />
%% CAUTION: Instances of this type are expensive to produce, shrink and instance-
%% check, both in terms of processing time and consumed memory. Only use this
%% type if you are certain that you need it.
-spec any() -> proper_types:type().
any() ->
    AllTypes = [integer(),float(),atom(),bitstring(),?LAZY(loose_tuple(any())),
		?LAZY(list(any()))],
    ?SUBTYPE(union(AllTypes), [
	{generator, fun proper_gen:any_gen/1}
    ]).


%%------------------------------------------------------------------------------
%% Type aliases
%%------------------------------------------------------------------------------

%% @equiv integer(inf, inf)
-spec integer() -> proper_types:type().
integer() -> integer(inf, inf).

%% @equiv integer(0, inf)
-spec non_neg_integer() -> proper_types:type().
non_neg_integer() -> integer(0, inf).

%% @equiv integer(1, inf)
-spec pos_integer() -> proper_types:type().
pos_integer() -> integer(1, inf).

%% @equiv integer(inf, -1)
-spec neg_integer() -> proper_types:type().
neg_integer() -> integer(inf, -1).

%% @equiv integer(Low, High)
-spec range(extint(), extint()) -> proper_types:type().
range(Low, High) -> integer(Low, High).

%% @equiv float(inf, inf)
-spec float() -> proper_types:type().
float() -> float(inf, inf).

%% @equiv float(0.0, inf)
-spec non_neg_float() -> proper_types:type().
non_neg_float() -> float(0.0, inf).

%% @equiv union([integer(), float()])
-spec number() -> proper_types:type().
number() -> union([integer(), float()]).

%% @doc The atoms `true' and `false'. Instances shrink towards `false'.
-spec boolean() -> proper_types:type().
boolean() -> union(['false', 'true']).

%% @equiv integer(0, 255)
-spec byte() -> proper_types:type().
byte() -> integer(0, 255).

%% @equiv integer(0, 16#10ffff)
-spec char() -> proper_types:type().
char() -> integer(0, 16#10ffff).

%% @equiv list(any())
-spec list() -> proper_types:type().
list() -> list(any()).

%% @equiv loose_tuple(any())
-spec tuple() -> proper_types:type().
tuple() -> loose_tuple(any()).

%% @equiv list(char())
-spec string() -> proper_types:type().
string() -> list(char()).

%% @equiv weighted_union(FreqChoices)
-spec wunion([{frequency(),raw_type()},...]) -> proper_types:type().
wunion(FreqChoices) -> weighted_union(FreqChoices).

%% @equiv any()
-spec term() -> proper_types:type().
term() -> any().

%% @equiv union([non_neg_integer() | infinity])
-spec timeout() -> proper_types:type().
timeout() -> union([non_neg_integer(), 'infinity']).

%% @equiv integer(0, 255)
-spec arity() -> proper_types:type().
arity() -> integer(0, 255).


%%------------------------------------------------------------------------------
%% QuickCheck compatibility types
%%------------------------------------------------------------------------------

%% @doc Small integers (bound by the current value of the `size' parameter).
%% Instances shrink towards `0'.
-spec int() -> proper_types:type().
int() -> ?SIZED(Size, integer(-Size,Size)).

%% @doc Small non-negative integers (bound by the current value of the `size'
%% parameter). Instances shrink towards `0'.
-spec nat() -> proper_types:type().
nat() -> ?SIZED(Size, integer(0,Size)).

%% @equiv integer()
-spec largeint() -> proper_types:type().
largeint() -> integer().

%% @equiv float()
-spec real() -> proper_types:type().
real() -> float().

%% @equiv boolean()
-spec bool() -> proper_types:type().
bool() -> boolean().

%% @equiv integer(Low, High)
-spec choose(extint(), extint()) -> proper_types:type().
choose(Low, High) -> integer(Low, High).

%% @equiv union(Choices)
-spec elements([raw_type(),...]) -> proper_types:type().
elements(Choices) -> union(Choices).

%% @equiv union(Choices)
-spec oneof([raw_type(),...]) -> proper_types:type().
oneof(Choices) -> union(Choices).

%% @equiv weighted_union(Choices)
-spec frequency([{frequency(),raw_type()},...]) -> proper_types:type().
frequency(FreqChoices) -> weighted_union(FreqChoices).

%% @equiv exactly(E)
-spec return(term()) -> proper_types:type().
return(E) -> exactly(E).

%% @doc Adds a default value, `Default', to `Type'.
%% The default serves as a primary shrinking target for instances, while it
%% is also chosen by the random instance generation subsystem half the time.
-spec default(raw_type(), raw_type()) -> proper_types:type().
default(Default, Type) ->
    union([Default, Type]).

%% @doc All sorted lists containing elements of type `ElemType'.
%% Instances shrink towards the empty list, `[]'.
-spec orderedlist(ElemType::raw_type()) -> proper_types:type().
orderedlist(RawElemType) ->
    ?LET(L, list(RawElemType), lists:sort(L)).

%% @equiv function(0, RetType)
-spec function0(raw_type()) -> proper_types:type().
function0(RetType) ->
    function(0, RetType).

%% @equiv function(1, RetType)
-spec function1(raw_type()) -> proper_types:type().
function1(RetType) ->
    function(1, RetType).

%% @equiv function(2, RetType)
-spec function2(raw_type()) -> proper_types:type().
function2(RetType) ->
    function(2, RetType).

%% @equiv function(3, RetType)
-spec function3(raw_type()) -> proper_types:type().
function3(RetType) ->
    function(3, RetType).

%% @equiv function(4, RetType)
-spec function4(raw_type()) -> proper_types:type().
function4(RetType) ->
    function(4, RetType).

%% @doc A specialization of {@link default/2}, where `Default' and `Type' are
%% assigned weights to be considered by the random instance generator. The
%% shrinking subsystem will ignore the weights and try to shrink using the
%% default value.
-spec weighted_default({frequency(),raw_type()}, {frequency(),raw_type()}) ->
	  proper_types:type().
weighted_default(Default, Type) ->
    weighted_union([Default, Type]).


%%------------------------------------------------------------------------------
%% Additional type specification functions
%%------------------------------------------------------------------------------

%% @doc Overrides the `size' parameter used when generating instances of
%% `Type' with `NewSize'. Has no effect on size-less types, such as unions.
%% Also, this will not affect the generation of any internal types contained in
%% `Type', such as the elements of a list - those will still be generated
%% using the test-wide value of `size'. One use of this function is to modify
%% types to produce instances that grow faster or slower, like so:
%% ```?SIZED(Size, resize(Size * 2, list(integer()))'''
%% The above specifies a list type that grows twice as fast as normal lists.
-spec resize(size(), Type::raw_type()) -> proper_types:type().
resize(NewSize, RawType) ->
    Type = cook_outer(RawType),
    case find_prop(size_transform, Type) of
	{ok,Transform} ->
	    add_prop(size_transform, fun(_S) -> Transform(NewSize) end, Type);
	error ->
	    add_prop(size_transform, fun(_S) -> NewSize end, Type)
    end.

%% @doc This is a predefined constraint that can be applied to random-length
%% list and binary types to ensure that the produced values are never empty.
%%
%% e.g. {@link list/0}, {@link string/0}, {@link binary/0})
-spec non_empty(ListType::raw_type()) -> proper_types:type().
non_empty(RawListType) ->
    ?SUCHTHAT(L, RawListType, L =/= [] andalso L =/= <<>>).

%% @doc Creates a new type which is equivalent to `Type', but whose instances
%% are never shrunk by the shrinking subsystem.
-spec noshrink(Type::raw_type()) -> proper_types:type().
noshrink(RawType) ->
    add_prop(noshrink, true, cook_outer(RawType)).

%% @doc Associates the atom key `Parameter' with the value `Value' while
%% generating instances of `Type'.
-spec with_parameter(atom(), value(), Type::raw_type()) -> proper_types:type().
with_parameter(Parameter, Value, RawType) ->
    with_parameters([{Parameter,Value}], RawType).

%% @doc Similar to {@link with_parameter/3}, but accepts a list of
%% `{Parameter, Value}' pairs.
-spec with_parameters([{atom(),value()}], Type::raw_type()) ->
          proper_types:type().
with_parameters(PVlist, RawType) ->
    Type = cook_outer(RawType),
    case find_prop(parameters, Type) of
	{ok,Params} when is_list(Params) ->
	    append_list_to_prop(parameters, PVlist, Type);
	error ->
	    add_prop(parameters, PVlist, Type)
    end.

%% @doc Returns the value associated with `Parameter', or `Default' in case
%% `Parameter' is not associated with any value.
-spec parameter(atom(), value()) -> value().
parameter(Parameter, Default) ->
    Parameters =
	case erlang:get('$parameters') of
	    undefined -> [];
	    List -> List
	end,
    proplists:get_value(Parameter, Parameters, Default).

%% @equiv parameter(Parameter, undefined)
-spec parameter(atom()) -> value().
parameter(Parameter) ->
    parameter(Parameter, undefined).