Module proper_typeserver

Erlang type system - PropEr type system integration module.

PropEr can parse types expressed in Erlang's type language and convert them to its own type format. Such expressions can be used instead of regular type constructors in the second argument of ?FORALLs. No extra notation is required; PropEr will detect which calls correspond to native types by applying a parse transform during compilation. This parse transform is automatically applied to any module that includes the proper.hrl header file. You can disable this feature by compiling your modules with -DPROPER_NO_TRANS. Note that this will currently also disable the automatic exporting of properties.

Native types cannot be used outside of ?FORALLs.

Inside ?FORALLs, native types can be combined with other native types, and even with PropEr types, inside tuples and lists (the constructs [...], {...} and ++ are all allowed).

All other constructs of Erlang's built-in type system (e.g. | for union, _ as an alias of any(), <<_:_>> binary type syntax and fun((...) -> ...) function type syntax) are not allowed in ?FORALLs, because they are rejected by the Erlang parser.

Anything other than a tuple constructor, list constructor, ++ application, local or remote call will automatically be considered a PropEr type constructor and not be processed further by the parse transform.

Parametric native types are fully supported; of course, they can only appear instantiated in a ?FORALL. The arguments of parametric native types are always interpreted as native types.

Parametric PropEr types, on the other hand, can take any kind of argument. You can even mix native and PropEr types in the arguments of a PropEr type. For example, assuming that the following declarations are present:

         my_proper_type() -> ?LET(...).
         -type my_native_type() :: ... .

Then the following expressions are all legal:

         vector(2, my_native_type())
         function(0, my_native_type())
         union([my_proper_type(), my_native_type()])

Some type constructors can take native types as arguments (but only inside ?FORALLs):

?SUCHTHAT, ?SUCHTHATMAYBE, non_empty, noshrink: these work with native types too
?LAZY, ?SHRINK, resize, ?SIZED: these don't work with native types
?LET, ?LETSHRINK: only the top-level base type can be a native type

Native type declarations in the ?FORALLs of a module can reference any custom type declared in a -type or -opaque attribute of the same module, as long as no module identifier is used.

Typed records cannot be referenced inside ?FORALLs using the #rec_name{} syntax. To use a typed record in a ?FORALL, enclose the record in a custom type like so:

         -type rec_name() :: #rec_name{}.

and use the custom type instead.

?FORALLs may contain references to self-recursive or mutually recursive native types, so long as each type in the hierarchy has a clear base case. Currently, PropEr requires that the toplevel of any recursive type declaration is either a (maybe empty) list or a union containing at least one choice that doesn't reference the type directly (it may, however, reference any of the types that are mutually recursive with it). This means, for example, that some valid recursive type declarations, such as this one:

         ?FORALL(..., a(), ...)

where:

         -type a() :: {'a','none' | a()}.

are not accepted by PropEr. However, such types can be rewritten in a way that allows PropEr to parse them:

         ?FORALL(..., a(), ...)

where:

         -type a() :: {'a','none'} | {'a',a()}.

This also means that recursive record declarations are not allowed:

         ?FORALL(..., rec(), ...)

where:

         -type rec() :: #rec{}.
         -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).

A little rewritting can usually remedy this problem as well:

         ?FORALL(..., rec(), ...)

where:

         -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
         -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).

Remote types may be referenced in a ?FORALL, so long as they are exported from the remote module. Currently, PropEr requires that any remote modules whose types are directly referenced from within properties are present in the code path at compile time, either compiled with debug_info enabled or in source form. If PropEr cannot find a remote module at all, finds only a compiled object file with no debug information or fails to compile the source file, all calls to that module will automatically be considered calls to PropEr type constructors.

For native types to be translated correctly, both the module that contains the ?FORALL declaration as well as any module that contains the declaration of a type referenced (directly or indirectly) from inside a ?FORALL must be present in the code path at runtime, either compiled with debug_info enabled or in source form.

Local types with the same name as an auto-imported BIF are not accepted by PropEr, unless the BIF in question has been declared in a no_auto_import option.

When an expression can be interpreted both as a PropEr type and as a native type, the former takes precedence. This means that a function foo() will shadow a type foo() if they are both present in the module. The same rule applies to remote functions and types as well.

The above may cause some confusion when list syntax is used:

The expression [integer()] can be interpreted both ways, so the PropEr way applies. Therefore, instances of this type will always be lists of length 1, not arbitrary integer lists, as would be expected when interpreting the expression as a native type.
Assuming that a custom type foo/1 has been declared, the expression foo([integer()]) can only be interpreted as a native type declaration, which means that the generic type of integer lists will be passed to foo/1.

Currently, PropEr does not detect the following mistakes:

inline record-field specializations that reference non-existent fields
type parameters that are not present in the RHS of a -type declaration
using _ as a type variable in the LHS of a -type declaration
using the same variable in more than one position in the LHS of a -type declaration

You can use these functions to try out the type translation subsystem.

demo_is_instance(Term :: term(),
                 Mod :: mod_name(),
                 TypeExpr :: string()) ->
                    boolean() | {error, term()}

Checks if Term is a valid instance of native type TypeExpr (which should be provided inside a string). PropEr acts as if it found this type expression inside the code of module Mod.

demo_translate_type/2

demo_translate_type(Mod :: mod_name(), TypeExpr :: string()) ->
                       rich_result(fin_type())

Translates the native type expression TypeExpr (which should be provided inside a string) into a PropEr type, which can then be passed to any of the demo functions defined in the proper_gen module. PropEr acts as if it found this type expression inside the code of module Mod.