<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Module proper_typeserver</title>
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="EDoc">
</head>
<body bgcolor="white">
<div class="navbar"><a name="#navbar_top"></a><table width="100%" border="0" cellspacing="0" cellpadding="2" summary="navigation bar"><tr><td><a href="overview-summary.html" target="overviewFrame">Overview</a></td><td><a href="http://www.erlang.org/"><img src="erlang.png" align="right" border="0" alt="erlang logo"></a></td></tr></table></div>
<hr>
<h1>Module proper_typeserver</h1>
<ul class="index"><li><a href="#description">Description</a></li><li><a href="#types">Data Types</a></li><li><a href="#index">Function Index</a></li><li><a href="#functions">Function Details</a></li></ul>Erlang type system - PropEr type system integration module.
<p>Copyright © 2010-2018 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas</p>
<p><b>Version:</b> Sep 22 2018 19:52:28</p>
<p><b>Behaviours:</b> <a href="gen_server.html"><tt>gen_server</tt></a>.</p>
<p><b>Authors:</b> Manolis Papadakis.</p>
<h2><a name="description">Description</a></h2><p>Erlang type system - PropEr type system integration module.</p>
<p>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 <code>?FORALL</code>s. 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 <code>proper.hrl</code> header
file. You can disable this feature by compiling your modules with
<code>-DPROPER_NO_TRANS</code>. Note that this will currently also disable the
automatic exporting of properties.</p>
The use of native types in properties is subject to the following usage
rules:
<ul>
<li>Native types cannot be used outside of <code>?FORALL</code>s.</li>
<li>Inside <code>?FORALL</code>s, native types can be combined with other native
types, and even with PropEr types, inside tuples and lists (the constructs
<code>[...]</code>, <code>{...}</code> and <code>++</code> are all allowed).</li>
<li>All other constructs of Erlang's built-in type system (e.g. <code>|</code> for
union, <code>_</code> as an alias of <code>any()</code>, <code><<_:_>></code> binary type syntax and
<code>fun((...) -> ...)</code> function type syntax) are not allowed in <code>?FORALL</code>s,
because they are rejected by the Erlang parser.</li>
<li>Anything other than a tuple constructor, list constructor, <code>++</code>
application, local or remote call will automatically be considered a
PropEr type constructor and not be processed further by the parse
transform.</li>
<li>Parametric native types are fully supported; of course, they can only
appear instantiated in a <code>?FORALL</code>. The arguments of parametric native
types are always interpreted as native types.</li>
<li>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:
<pre> my_proper_type() -> ?LET(...).
-type my_native_type() :: ... .</pre>
Then the following expressions are all legal:
<pre> vector(2, my_native_type())
function(0, my_native_type())
union([my_proper_type(), my_native_type()])</pre> </li>
<li>Some type constructors can take native types as arguments (but only
inside <code>?FORALL</code>s):
<ul>
<li><code>?SUCHTHAT</code>, <code>?SUCHTHATMAYBE</code>, <code>non_empty</code>, <code>noshrink</code>: these work
with native types too</li>
<li><code>?LAZY</code>, <code>?SHRINK</code>, <code>resize</code>, <code>?SIZED</code>: these don't work with native
types</li>
<li><code>?LET</code>, <code>?LETSHRINK</code>: only the top-level base type can be a native
type</li>
</ul></li>
<li>Native type declarations in the <code>?FORALL</code>s of a module can reference any
custom type declared in a <code>-type</code> or <code>-opaque</code> attribute of the same
module, as long as no module identifier is used.</li>
<li>Typed records cannot be referenced inside <code>?FORALL</code>s using the
<code>#rec_name{}</code> syntax. To use a typed record in a <code>?FORALL</code>, enclose the
record in a custom type like so:
<pre> -type rec_name() :: #rec_name{}.</pre>
and use the custom type instead.</li>
<li><code>?FORALL</code>s 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:
<pre> ?FORALL(..., a(), ...)</pre>
where:
<pre> -type a() :: {'a','none' | a()}.</pre>
are not accepted by PropEr. However, such types can be rewritten in a way
that allows PropEr to parse them:
<pre> ?FORALL(..., a(), ...)</pre>
where:
<pre> -type a() :: {'a','none'} | {'a',a()}.</pre>
This also means that recursive record declarations are not allowed:
<pre> ?FORALL(..., rec(), ...)</pre>
where:
<pre> -type rec() :: #rec{}.
-record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).</pre>
A little rewritting can usually remedy this problem as well:
<pre> ?FORALL(..., rec(), ...)</pre>
where:
<pre> -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
-record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).</pre>
</li>
<li>Remote types may be referenced in a <code>?FORALL</code>, 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
<code>debug_info</code> 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.</li>
<li>For native types to be translated correctly, both the module that
contains the <code>?FORALL</code> declaration as well as any module that contains
the declaration of a type referenced (directly or indirectly) from inside
a <code>?FORALL</code> must be present in the code path at runtime, either compiled
with <code>debug_info</code> enabled or in source form.</li>
<li>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
<code>no_auto_import</code> option.</li>
<li>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
<code>foo()</code> will shadow a type <code>foo()</code> if they are both present in the module.
The same rule applies to remote functions and types as well.</li>
<li>The above may cause some confusion when list syntax is used:
<ul>
<li>The expression <code>[integer()]</code> 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.</li>
<li>Assuming that a custom type foo/1 has been declared, the expression
<code>foo([integer()])</code> can only be interpreted as a native type declaration,
which means that the generic type of integer lists will be passed to
<code>foo/1</code>.</li>
</ul></li>
<li>Currently, PropEr does not detect the following mistakes:
<ul>
<li>inline record-field specializations that reference non-existent
fields</li>
<li>type parameters that are not present in the RHS of a <code>-type</code>
declaration</li>
<li>using <code>_</code> as a type variable in the LHS of a <code>-type</code> declaration</li>
<li>using the same variable in more than one position in the LHS of a
<code>-type</code> declaration</li>
</ul>
</li>
</ul>
<p>You can use <a href="#index">these</a> functions to try out the type
translation subsystem.</p>
CAUTION: These functions should never be used inside properties. They are
meant for demonstration purposes only.
<h2><a name="types">Data Types</a></h2>
<h3 class="typedecl"><a name="type-fin_type">fin_type()</a></h3>
<p><pre>fin_type() = <a href="proper_types.html#type-type">proper_types:type()</a></pre></p>
<h3 class="typedecl"><a name="type-mod_name">mod_name()</a></h3>
<p><pre>mod_name() = atom()</pre></p>
<h3 class="typedecl"><a name="type-rich_result">rich_result()</a></h3>
<p><pre>rich_result(T) = {ok, T} | {error, term()}</pre></p>
<h2><a name="index">Function Index</a></h2>
<table width="100%" border="1" cellspacing="0" cellpadding="2" summary="function index"><tr><td valign="top"><a href="#demo_is_instance-3">demo_is_instance/3</a></td><td>Checks if <code>Term</code> is a valid instance of native type <code>TypeExpr</code> (which
should be provided inside a string).</td></tr>
<tr><td valign="top"><a href="#demo_translate_type-2">demo_translate_type/2</a></td><td>Translates the native type expression <code>TypeExpr</code> (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 <a href="proper_gen.html"><code>proper_gen</code></a> module.</td></tr>
</table>
<h2><a name="functions">Function Details</a></h2>
<h3 class="function"><a name="demo_is_instance-3">demo_is_instance/3</a></h3>
<div class="spec">
<p><pre>demo_is_instance(Term :: term(),
Mod :: <a href="#type-mod_name">mod_name()</a>,
TypeExpr :: string()) ->
boolean() | {error, term()}</pre></p>
</div><p>Checks if <code>Term</code> is a valid instance of native type <code>TypeExpr</code> (which
should be provided inside a string). PropEr acts as if it found this type
expression inside the code of module <code>Mod</code>.</p>
<h3 class="function"><a name="demo_translate_type-2">demo_translate_type/2</a></h3>
<div class="spec">
<p><pre>demo_translate_type(Mod :: <a href="#type-mod_name">mod_name()</a>, TypeExpr :: string()) ->
<a href="#type-rich_result">rich_result</a>(<a href="#type-fin_type">fin_type()</a>)</pre></p>
</div><p>Translates the native type expression <code>TypeExpr</code> (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 <a href="proper_gen.html"><code>proper_gen</code></a> module. PropEr acts
as if it found this type expression inside the code of module <code>Mod</code>.</p>
<hr>
<div class="navbar"><a name="#navbar_bottom"></a><table width="100%" border="0" cellspacing="0" cellpadding="2" summary="navigation bar"><tr><td><a href="overview-summary.html" target="overviewFrame">Overview</a></td><td><a href="http://www.erlang.org/"><img src="erlang.png" align="right" border="0" alt="erlang logo"></a></td></tr></table></div>
<p><i>Generated by EDoc</i></p>
</body>
</html>
