-module(simple1_api).
-export([t1/1, adt_t1/1, t2/1, adt_t2/1, tup/0, t3/0, t4/0, t5/0, t6/0, t7/0,
t8/0, adt_t3/0, adt_t4/0, adt_t7/0, adt_t8/0, adt_t5/0,
c1/2, c2/2, c2/0, c3/0, c4/0, tt1/0, tt2/0,
cmp1/0, cmp2/0, cmp3/0, cmp4/0,
ty_cmp1/0, ty_cmp2/0, ty_cmp3/0, ty_cmp4/0,
f1/0, f2/0, adt_f1/0, adt_f2/0, f3/0, f4/0, adt_f3/0, adt_f4/0,
adt_f4_a/0, adt_f4_b/0,
bool_t1/0, bool_t2/0, bool_t3/0, bool_t4/0, bool_t5/1, bool_t6/1,
bool_t7/0, bool_adt_t1/0, bool_adt_t2/0, bool_adt_t5/1,
bool_adt_t6/1, bool_t8/0, bool_adt_t8/2, bool_t9/0, bool_adt_t9/2,
bit_t1/0, bit_adt_t1/0, bit_t3/1, bit_adt_t2/0, bit_adt_t3/1,
bit_t5/1, bit_t4/1, bit_adt_t4/1, bit_t5/0, bit_adt_t5/0,
call_f/1, call_f_adt/1, call_m_adt/1, call_m/1, call_f_i/1,
call_m_i/1, call_m_adt_i/1, call_f_adt_i/1,
eq1/0, eq2/0, c5/0, c6/2, c7/2, c8/0]).
%%% Equal opaque types
-export_type([o1/0, o2/0]).
-export_type([d1/0, d2/0]).
-opaque o1() :: a | b | c.
-opaque o2() :: a | b | c.
-export_type([i1/0, i2/0, di1/0, di2/0]).
-export_type([b1/0, b2/0]).
-export_type([bit1/0]).
-export_type([a/0, i/0]).
%% The derived spec is
%% -spec t1('a' | 'b') -> simple1_api:o1('a') | simple1_api:o2('a').
%% but that is not tested...
t1(a) ->
o1();
t1(b) ->
o2().
-spec o1() -> o1().
o1() -> a.
-spec o2() -> o2().
o2() -> a.
%% The derived spec is
%% -spec adt_t1('a' | 'b') -> simple1_adt:o1('a') | simple1_adt:o2('a').
%% but that is not tested...
adt_t1(a) ->
simple1_adt:o1();
adt_t1(b) ->
simple1_adt:o2().
%%% Disjunct opaque types
-opaque d1() :: a | b | c.
-opaque d2() :: d | e | f.
%% -spec t2('a' | 'b') -> simple1_api:d1('a') | simple1_api:d2('d').
t2(a) ->
d1();
t2(b) ->
d2().
-spec d1() -> d1().
d1() -> a.
-spec d2() -> d2().
d2() -> d.
%% -spec adt_t2('a' | 'b') -> simple1_adt:d1('a') | simple1_adt:d2('d').
adt_t2(a) ->
simple1_adt:d1();
adt_t2(b) ->
simple1_adt:d2().
-spec tup() -> simple1_adt:tuple1(). % invalid type spec
tup() ->
{a, b}.
%%% Matching equal opaque types with different names
t3() ->
A = n1(),
B = n2(),
A = A, % OK, of course
A = B. % OK since o1() and o2() are local opaque types
t4() ->
A = n1(),
B = n2(),
true = A =:= A, % OK, of course
A =:= B. % OK since o1() and o2() are local opaque types
t5() ->
A = d1(),
B = d2(),
A =:= B. % can never evaluate to true
t6() ->
A = d1(),
B = d2(),
A = B. % can never succeed
t7() ->
A = d1(),
B = d2(),
A =/= B. % OK (always true?)
t8() ->
A = d1(),
B = d2(),
A /= B. % OK (always true?)
-spec n1() -> o1().
n1() -> a.
-spec n2() -> o2().
n2() -> a.
adt_t3() ->
A = simple1_adt:n1(),
B = simple1_adt:n2(),
true = A =:= A, % OK.
A =:= B. % opaque test, not OK
adt_t4() ->
A = simple1_adt:n1(),
B = simple1_adt:n2(),
A = A, % OK
A = B. % opaque terms
adt_t7() ->
A = simple1_adt:n1(),
B = simple1_adt:n2(),
false = A =/= A, % OK
A =/= B. % opaque test, not OK
adt_t8() ->
A = simple1_adt:n1(),
B = simple1_adt:n2(),
false = A /= A, % OK
A /= B. % opaque test, not OK
adt_t5() ->
A = simple1_adt:c1(),
B = simple1_adt:c2(),
A =:= B. % opaque test, not OK
%% Comparison in guard
-spec c1(simple1_adt:d1(), simple1_adt:d2()) -> boolean().
c1(A, B) when A =< B -> true. % succ type of A and B is any() (type spec is OK)
-spec c2(simple1_adt:d1(), simple1_adt:d2()) -> boolean().
c2(A, B) ->
if A =< B -> true end. % succ type of A and B is any() (type spec is OK)
c2() ->
A = simple1_adt:d1(),
B = simple1_adt:d2(),
if A =< B -> ok end. % opaque terms
c3() ->
B = simple1_adt:d2(),
if a =< B -> ok end. % opaque term
c4() ->
A = simple1_adt:d1(),
if A =< d -> ok end. % opaque term
tt1() ->
A = o1(),
is_integer(A). % OK
tt2() ->
A = simple1_adt:d1(),
is_integer(A). % breaks the opacity
%% Comparison with integers
-opaque i1() :: 1 | 2.
-opaque i2() :: 1 | 2.
-opaque di1() :: 1 | 2.
-opaque di2() :: 3 | 4.
-spec i1() -> i1().
i1() -> 1.
-type ty_i1() :: 1 | 2.
-spec ty_i1() -> ty_i1().
ty_i1() -> 1.
cmp1() ->
A = i1(),
if A > 3 -> ok end. % can never succeed
cmp2() ->
A = simple1_adt:i1(),
if A > 3 -> ok end. % opaque term
cmp3() ->
A = i1(),
if A < 3 -> ok end.
cmp4() ->
A = simple1_adt:i1(),
if A < 3 -> ok end. % opaque term
%% -type
ty_cmp1() ->
A = ty_i1(),
if A > 3 -> ok end. % can never succeed
ty_cmp2() ->
A = simple1_adt:ty_i1(),
if A > 3 -> ok end. % can never succeed
ty_cmp3() ->
A = ty_i1(),
if A < 3 -> ok end.
ty_cmp4() ->
A = simple1_adt:ty_i1(),
if A < 3 -> ok end.
%% is_function
f1() ->
T = n1(),
if is_function(T) -> ok end. % can never succeed
f2() ->
T = n1(),
is_function(T). % ok
adt_f1() ->
T = simple1_adt:n1(),
if is_function(T) -> ok end. % breaks the opacity
adt_f2() ->
T = simple1_adt:n1(),
is_function(T). % breaks the opacity
f3() ->
A = i1(),
T = n1(),
if is_function(T, A) -> ok end. % can never succeed
f4() ->
A = i1(),
T = n1(),
is_function(T, A). % ok
adt_f3() ->
A = simple1_adt:i1(),
T = simple1_adt:n1(),
if is_function(T, A) -> ok end. % breaks the opacity
adt_f4() ->
A = simple1_adt:i1(),
T = simple1_adt:n1(),
is_function(T, A). % breaks the opacity
adt_f4_a() ->
A = simple1_adt:i1(),
T = n1(),
is_function(T, A). % opaque term
adt_f4_b() ->
A = i1(),
T = simple1_adt:n1(),
is_function(T, A). % breaks the opacity
%% A few Boolean examples
bool_t1() ->
B = b2(),
if B -> ok end. % B =:= true can never succeed
bool_t2() ->
A = b1(),
B = b2(),
if A and not B -> ok end.
bool_t3() ->
A = b1(),
if not A -> ok end. % can never succeed
bool_t4() ->
A = n1(),
if not ((A >= 1) and not (A < 1)) -> ok end. % can never succeed
-spec bool_t5(i1()) -> integer().
bool_t5(A) ->
if [not (A > 1)] =:=
[false]-> 1 end.
-spec bool_t6(b1()) -> integer().
bool_t6(A) ->
if [not A] =:=
[false]-> 1 end.
-spec bool_t7() -> integer().
bool_t7() ->
A = i1(),
if [not A] =:= % cannot succeed
[false]-> 1 end.
bool_adt_t1() ->
B = simple1_adt:b2(),
if B -> ok end. % opaque term
bool_adt_t2() ->
A = simple1_adt:b1(),
B = simple1_adt:b2(),
if A and not B -> ok end. % opaque term
-spec bool_adt_t5(simple1_adt:i1()) -> integer().
bool_adt_t5(A) ->
if [not (A > 1)] =:= % succ type of A is any() (type spec is OK)
[false]-> 1 end.
-spec bool_adt_t6(simple1_adt:b1()) -> integer(). % invalid type spec
bool_adt_t6(A) ->
if [not A] =:= % succ type of A is 'true'
[false]-> 1 end.
-spec bool_t8() -> integer().
bool_t8() ->
A = i1(),
if [A and A] =:= % cannot succeed
[false]-> 1 end.
-spec bool_adt_t8(simple1_adt:b1(), simple1_adt:b2()) -> integer(). % invalid
bool_adt_t8(A, B) ->
if [A and B] =:=
[false]-> 1 end.
-spec bool_t9() -> integer().
bool_t9() ->
A = i1(),
if [A or A] =:= % cannot succeed
[false]-> 1 end.
-spec bool_adt_t9(simple1_adt:b1(), simple1_adt:b2()) -> integer(). % invalid
bool_adt_t9(A, B) ->
if [A or B] =:=
[false]-> 1 end.
-opaque b1() :: boolean().
-opaque b2() :: boolean().
-spec b1() -> b1().
b1() -> true.
-spec b2() -> b2().
b2() -> false.
%% Few (very few...) examples with bit syntax
bit_t1() ->
A = i1(),
<<100:(A)>>.
bit_adt_t1() ->
A = simple1_adt:i1(),
<<100:(A)>>. % breaks the opacity
bit_t3(A) ->
B = i1(),
case none:none() of
<<A:B>> -> 1
end.
bit_adt_t2() ->
A = simple1_adt:i1(),
case <<"hej">> of
<<_:A>> -> ok % breaks the opacity (but the message is strange)
end.
bit_adt_t3(A) ->
B = simple1_adt:i1(),
case none:none() of
<<A: % breaks the opacity (the message is less than perfect)
B>> -> 1
end.
bit_t5(A) ->
B = o1(),
case none:none() of % the type is any(); should fix that XXX
<<A:B>> -> 1 % can never match (local opaque type is OK)
end.
-spec bit_t4(<<_:1>>) -> integer().
bit_t4(A) ->
Sz = i1(),
case A of
<<_:Sz>> -> 1
end.
-spec bit_adt_t4(<<_:1>>) -> integer().
bit_adt_t4(A) ->
Sz = simple1_adt:i1(),
case A of
<<_:Sz>> -> 1 % breaks the opacity
end.
bit_t5() ->
A = bit1(),
case A of
<<_/binary>> -> 1
end.
bit_adt_t5() ->
A = simple1_adt:bit1(),
case A of
<<_/binary>> -> 1 % breaks the opacity
end.
-opaque bit1() :: binary().
-spec bit1() -> bit1().
bit1() ->
<<"hej">>.
%% Calls with variable module or function
call_f(A) ->
A = a(),
foo:A(A).
call_f_adt(A) ->
A = simple1_adt:a(),
foo:A(A). % breaks the opacity
call_m(A) ->
A = a(),
A:foo(A).
call_m_adt(A) ->
A = simple1_adt:a(),
A:foo(A). % breaks the opacity
-opaque a() :: atom().
-opaque i() :: integer().
-spec a() -> a().
a() ->
e.
call_f_i(A) ->
A = i(),
foo:A(A). % A is not atom() but i()
call_f_adt_i(A) ->
A = simple1_adt:i(),
foo:A(A). % A is not atom() but simple1_adt:i()
call_m_i(A) ->
A = i(),
A:foo(A). % A is not atom() but i()
call_m_adt_i(A) ->
A = simple1_adt:i(),
A:foo(A). % A is not atom() but simple1_adt:i()
-spec eq1() -> integer().
eq1() ->
A = simple1_adt:d2(),
B = simple1_adt:d1(),
if
A == B -> % opaque terms
0;
A == A ->
1;
A =:= A -> % compiler finds this one cannot match
2;
true -> % compiler finds this one cannot match
3
end.
eq2() ->
A = simple1_adt:d1(),
if
{A} >= {A} ->
1;
A >= 3 -> % opaque term
2;
A == 3 -> % opaque term
3;
A =:= 3 -> % opaque term
4;
A == A ->
5;
A =:= A -> % compiler finds this one cannot match
6
end.
c5() ->
A = simple1_adt:d1(),
A < 3. % opaque term
c6(A, B) ->
A = simple1_adt:d1(),
B = simple1_adt:d1(),
A =< B. % same type - no warning
c7(A, B) ->
A = simple1_adt:d1(),
B = simple1_adt:d2(),
A =< B. % opaque terms
c8() ->
D = digraph:new(),
E = ets:new(foo, []),
if {D, a} > {D, E} -> true; % OK
{1.0, 2} > {{D}, {E}} -> true; % OK
{D, 3} > {D, E} -> true % opaque term 2
end.
-spec i() -> i().
i() ->
1.
