Types and specifications have been modified and added

1 files changed, 441 insertions, 104 deletions

diff --git a/lib/stdlib/src/sofs.erl b/lib/stdlib/src/sofs.erl
index a83f803330..d38b8ab37a 100644
--- a/lib/stdlib/src/sofs.erl
+++ b/lib/stdlib/src/sofs.erl
@@ -1,19 +1,19 @@
 %%
 %% %CopyrightBegin%
-%% 
-%% Copyright Ericsson AB 2001-2009. All Rights Reserved.
-%% 
+%%
+%% Copyright Ericsson AB 2001-2011. All Rights Reserved.
+%%
 %% The contents of this file are subject to the Erlang Public License,
 %% Version 1.1, (the "License"); you may not use this file except in
 %% compliance with the License. You should have received a copy of the
 %% Erlang Public License along with this software. If not, it can be
 %% retrieved online at http://www.erlang.org/.
-%% 
+%%
 %% Software distributed under the License is distributed on an "AS IS"
 %% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
 %% the License for the specific language governing rights and limitations
 %% under the License.
-%% 
+%%
 %% %CopyrightEnd%
 %%
 -module(sofs).
@@ -40,11 +40,11 @@
          substitution/2, projection/2, partition/1, partition/2,
          partition/3, multiple_relative_product/2, join/4]).
 
--export([family_to_relation/1, family_specification/2, 
+-export([family_to_relation/1, family_specification/2,
          union_of_family/1, intersection_of_family/1,
          family_union/1, family_intersection/1,
          family_domain/1, family_range/1, family_field/1,
-         family_union/2, family_intersection/2, family_difference/2, 
+         family_union/2, family_intersection/2, family_difference/2,
          partition_family/2, family_projection/2]).
 
 -export([family_to_digraph/1, family_to_digraph/2,
@@ -64,9 +64,9 @@
 
 -compile({inline, [{external_fun,1},{element_type,1}]}).
 
--compile({inline, 
+-compile({inline,
           [{unify_types,2}, {match_types,2},
-           {test_rel,3}, {symdiff,3}, 
+           {test_rel,3}, {symdiff,3},
            {subst,3}]}).
 
 -compile({inline, [{fam_binop,3}]}).
@@ -80,13 +80,13 @@
 -define(TAG, 'Set').
 -define(ORDTAG, 'OrdSet').
 
--record(?TAG, {data = [], type = type}).
--record(?ORDTAG, {orddata = {}, ordtype = type}).
+-record(?TAG, {data = [] :: list(), type = type :: term()}).
+-record(?ORDTAG, {orddata = {} :: tuple(), ordtype = type :: term()}).
 
 -define(LIST(S), (S)#?TAG.data).
 -define(TYPE(S), (S)#?TAG.type).
-%%-define(SET(L, T), 
-%%       case is_type(T) of 
+%%-define(SET(L, T),
+%%       case is_type(T) of
 %%           true -> #?TAG{data = L, type = T};
 %%           false -> erlang:error(badtype, [T])
 %%       end
@@ -113,14 +113,40 @@
 -define(IS_SET_OF(X), is_list(X)).
 -define(FAMILY(X, Y), ?BINREL(X, ?SET_OF(Y))).
 
+-export_type([anyset/0, binary_relation/0, external_set/0, a_function/0,
+              family/0, relation/0, set_of_sets/0, set_fun/0, spec_fun/0,
+              type/0]).
+-export_type([ordset/0, a_set/0]).
+
+-type(anyset() :: ordset() | a_set()).
+-type(binary_relation() :: relation()).
+-type(external_set() :: term()).
+-type(a_function() :: relation()).
+-type(family() :: a_function()).
+-opaque(ordset() :: #?ORDTAG{}).
+-type(relation() :: a_set()).
+-opaque(a_set() :: #?TAG{}).
+-type(set_of_sets() :: a_set()).
+-type(set_fun() :: pos_integer()
+                 | {external, fun((external_set()) -> external_set())}
+                 | fun((anyset()) -> anyset())).
+-type(spec_fun() :: {external, fun((external_set()) -> boolean())}
+                  | fun((anyset()) -> boolean())).
+-type(type() :: term()).
+
+-type(tuple_of(_T) :: tuple()).
+
 %%
 %%  Exported functions
 %%
 
-%%% 
+%%%
 %%% Create sets
-%%% 
+%%%
 
+-spec(from_term(Term) -> AnySet when
+      AnySet :: anyset(),
+      Term :: term()).
 from_term(T) ->
     Type = case T of
                _ when is_list(T) -> [?ANYTYPE];
@@ -133,6 +159,10 @@ from_term(T) ->
             Set
     end.
 
+-spec(from_term(Term, Type) -> AnySet when
+      AnySet :: anyset(),
+      Term :: term(),
+      Type :: type()).
 from_term(L, T) ->
     case is_type(T) of
         true ->
@@ -146,14 +176,23 @@ from_term(L, T) ->
             erlang:error(badarg, [L, T])
     end.
 
+-spec(from_external(ExternalSet, Type) -> AnySet when
+      ExternalSet :: external_set(),
+      AnySet :: anyset(),
+      Type :: type()).
 from_external(L, ?SET_OF(Type)) ->
     ?SET(L, Type);
 from_external(T, Type) ->
     ?ORDSET(T, Type).
 
+-spec(empty_set() -> Set when
+      Set :: a_set()).
 empty_set() ->
     ?SET([], ?ANYTYPE).
 
+-spec(is_type(Term) -> Bool when
+      Bool :: boolean(),
+      Term :: term()).
 is_type(Atom) when ?IS_ATOM_TYPE(Atom), Atom =/= ?ANYTYPE ->
     true;
 is_type(?SET_OF(T)) ->
@@ -163,19 +202,26 @@ is_type(T) when tuple_size(T) > 0 ->
 is_type(_T) ->
     false.
 
+-spec(set(Terms) -> Set when
+      Set :: a_set(),
+      Terms :: [term()]).
 set(L) ->
     case catch usort(L) of
         {'EXIT', _} ->
             erlang:error(badarg, [L]);
-        SL -> 
+        SL ->
             ?SET(SL, ?ATOM_TYPE)
     end.
 
+-spec(set(Terms, Type) -> Set when
+      Set :: a_set(),
+      Terms :: [term()],
+      Type :: type()).
 set(L, ?SET_OF(Type) = T) when ?IS_ATOM_TYPE(Type), Type =/= ?ANYTYPE ->
     case catch usort(L) of
         {'EXIT', _} ->
             erlang:error(badarg, [L, T]);
-        SL -> 
+        SL ->
             ?SET(SL, Type)
     end;
 set(L, ?SET_OF(_) = T) ->
@@ -188,6 +234,12 @@ set(L, ?SET_OF(_) = T) ->
 set(L, T) ->
     erlang:error(badarg, [L, T]).
 
+-spec(from_sets(ListOfSets) -> Set when
+      Set :: a_set(),
+      ListOfSets :: [anyset()];
+               (TupleOfSets) -> Ordset when
+      Ordset :: ordset(),
+      TupleOfSets :: tuple_of(anyset())).
 from_sets(Ss) when is_list(Ss) ->
     case set_of_sets(Ss, [], ?ANYTYPE) of
         {error, Error} ->
@@ -205,6 +257,9 @@ from_sets(Tuple) when is_tuple(Tuple) ->
 from_sets(T) ->
     erlang:error(badarg, [T]).
 
+-spec(relation(Tuples) -> Relation when
+      Relation :: relation(),
+      Tuples :: [tuple()]).
 relation([]) ->
     ?SET([], ?BINREL(?ATOM_TYPE, ?ATOM_TYPE));
 relation(Ts = [T | _]) when is_tuple(T) ->
@@ -217,6 +272,11 @@ relation(Ts = [T | _]) when is_tuple(T) ->
 relation(E) ->
     erlang:error(badarg, [E]).
 
+-spec(relation(Tuples, Type) -> Relation when
+      N :: integer(),
+      Type :: N | type(),
+      Relation :: relation(),
+      Tuples :: [tuple()]).
 relation(Ts, TS) ->
     case catch rel(Ts, TS) of
         {'EXIT', _} ->
@@ -225,6 +285,9 @@ relation(Ts, TS) ->
 	    Set
     end.
 
+-spec(a_function(Tuples) -> Function when
+      Function :: a_function(),
+      Tuples :: [tuple()]).
 a_function(Ts) ->
     case catch func(Ts, ?BINREL(?ATOM_TYPE, ?ATOM_TYPE)) of
         {'EXIT', _} ->
@@ -235,6 +298,10 @@ a_function(Ts) ->
 	    Set
     end.
 
+-spec(a_function(Tuples, Type) -> Function when
+      Function :: a_function(),
+      Tuples :: [tuple()],
+      Type :: type()).
 a_function(Ts, T) ->
     case catch a_func(Ts, T) of
 	{'EXIT', _} ->
@@ -245,6 +312,9 @@ a_function(Ts, T) ->
 	    Set
     end.
 
+-spec(family(Tuples) -> Family when
+      Family :: family(),
+      Tuples :: [tuple()]).
 family(Ts) ->
     case catch fam2(Ts, ?FAMILY(?ATOM_TYPE, ?ATOM_TYPE)) of
         {'EXIT', _} ->
@@ -255,6 +325,10 @@ family(Ts) ->
 	    Set
     end.
 
+-spec(family(Tuples, Type) -> Family when
+      Family :: family(),
+      Tuples :: [tuple()],
+      Type :: type()).
 family(Ts, T) ->
     case catch fam(Ts, T) of
 	{'EXIT', _} ->
@@ -265,20 +339,30 @@ family(Ts, T) ->
 	    Set
     end.
 
-%%% 
+%%%
 %%% Functions on sets.
-%%% 
+%%%
 
+-spec(to_external(AnySet) -> ExternalSet when
+      ExternalSet :: external_set(),
+      AnySet :: anyset()).
 to_external(S) when ?IS_SET(S) ->
     ?LIST(S);
 to_external(S) when ?IS_ORDSET(S) ->
     ?ORDDATA(S).
 
+-spec(type(AnySet) -> Type when
+      AnySet :: anyset(),
+      Type :: type()).
 type(S) when ?IS_SET(S) ->
     ?SET_OF(?TYPE(S));
 type(S) when ?IS_ORDSET(S) ->
     ?ORDTYPE(S).
 
+-spec(to_sets(ASet) -> Sets when
+      ASet :: a_set() | ordset(),
+      Sets :: tuple_of(AnySet) | [AnySet],
+      AnySet :: anyset()).
 to_sets(S) when ?IS_SET(S) ->
     case ?TYPE(S) of
         ?SET_OF(Type) -> list_of_sets(?LIST(S), Type, []);
@@ -289,6 +373,9 @@ to_sets(S) when ?IS_ORDSET(S), is_tuple(?ORDTYPE(S)) ->
 to_sets(S) when ?IS_ORDSET(S) ->
     erlang:error(badarg, [S]).
 
+-spec(no_elements(ASet) -> NoElements when
+      ASet :: a_set() | ordset(),
+      NoElements :: pos_integer()).
 no_elements(S) when ?IS_SET(S) ->
     length(?LIST(S));
 no_elements(S) when ?IS_ORDSET(S), is_tuple(?ORDTYPE(S)) ->
@@ -296,6 +383,10 @@ no_elements(S) when ?IS_ORDSET(S), is_tuple(?ORDTYPE(S)) ->
 no_elements(S) when ?IS_ORDSET(S) ->
     erlang:error(badarg, [S]).
 
+-spec(specification(Fun, Set1) -> Set2 when
+      Fun :: spec_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 specification(Fun, S) when ?IS_SET(S) ->
     Type = ?TYPE(S),
     R = case external_fun(Fun) of
@@ -311,36 +402,62 @@ specification(Fun, S) when ?IS_SET(S) ->
 	    erlang:error(Bad, [Fun, S])
     end.
 
+-spec(union(Set1, Set2) -> Set3 when
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 union(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case unify_types(?TYPE(S1), ?TYPE(S2)) of
         [] -> erlang:error(type_mismatch, [S1, S2]);
         Type ->  ?SET(umerge(?LIST(S1), ?LIST(S2)), Type)
     end.
 
+-spec(intersection(Set1, Set2) -> Set3 when
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 intersection(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case unify_types(?TYPE(S1), ?TYPE(S2)) of
         [] -> erlang:error(type_mismatch, [S1, S2]);
         Type ->  ?SET(intersection(?LIST(S1), ?LIST(S2), []), Type)
     end.
 
+-spec(difference(Set1, Set2) -> Set3 when
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 difference(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case unify_types(?TYPE(S1), ?TYPE(S2)) of
         [] -> erlang:error(type_mismatch, [S1, S2]);
         Type ->  ?SET(difference(?LIST(S1), ?LIST(S2), []), Type)
     end.
 
+-spec(symdiff(Set1, Set2) -> Set3 when
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 symdiff(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case unify_types(?TYPE(S1), ?TYPE(S2)) of
         [] -> erlang:error(type_mismatch, [S1, S2]);
         Type ->  ?SET(symdiff(?LIST(S1), ?LIST(S2), []), Type)
     end.
 
+-spec(symmetric_partition(Set1, Set2) -> {Set3, Set4, Set5} when
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set(),
+      Set4 :: a_set(),
+      Set5 :: a_set()).
 symmetric_partition(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case unify_types(?TYPE(S1), ?TYPE(S2)) of
         [] -> erlang:error(type_mismatch, [S1, S2]);
         Type ->  sympart(?LIST(S1), ?LIST(S2), [], [], [], Type)
     end.
 
+-spec(product(Set1, Set2) -> BinRel when
+      BinRel :: binary_relation(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 product(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     if
         ?TYPE(S1) =:= ?ANYTYPE -> S1;
@@ -351,6 +468,9 @@ product(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
 	    ?SET(relprod(map(F, ?LIST(S1)), map(F, ?LIST(S2))), T)
     end.
 
+-spec(product(TupleOfSets) -> Relation when
+      Relation :: relation(),
+      TupleOfSets :: tuple_of(a_set())).
 product({S1, S2}) ->
     product(S1, S2);
 product(T) when is_tuple(T) ->
@@ -365,11 +485,15 @@ product(T) when is_tuple(T) ->
             case member([], L) of
                 true ->
 		    empty_set();
-                false -> 
+                false ->
                     ?SET(reverse(prod(L, [], [])), Type)
             end
     end.
 
+-spec(constant_function(Set, AnySet) -> Function when
+      AnySet :: anyset(),
+      Function :: a_function(),
+      Set :: a_set()).
 constant_function(S, E) when ?IS_SET(S) ->
     case {?TYPE(S), is_sofs_set(E)} of
 	{?ANYTYPE, true} -> S;
@@ -381,6 +505,10 @@ constant_function(S, E) when ?IS_SET(S) ->
 constant_function(S, E) when ?IS_ORDSET(S) ->
     erlang:error(badarg, [S, E]).
 
+-spec(is_equal(AnySet1, AnySet2) -> Bool when
+      AnySet1 :: anyset(),
+      AnySet2 :: anyset(),
+      Bool :: boolean()).
 is_equal(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case match_types(?TYPE(S1), ?TYPE(S2)) of
         true  -> ?LIST(S1) == ?LIST(S2);
@@ -396,12 +524,19 @@ is_equal(S1, S2) when ?IS_SET(S1), ?IS_ORDSET(S2) ->
 is_equal(S1, S2) when ?IS_ORDSET(S1), ?IS_SET(S2) ->
     erlang:error(type_mismatch, [S1, S2]).
 
+-spec(is_subset(Set1, Set2) -> Bool when
+      Bool :: boolean(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 is_subset(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case match_types(?TYPE(S1), ?TYPE(S2)) of
         true  -> subset(?LIST(S1), ?LIST(S2));
         false -> erlang:error(type_mismatch, [S1, S2])
     end.
 
+-spec(is_sofs_set(Term) -> Bool when
+      Bool :: boolean(),
+      Term :: term()).
 is_sofs_set(S) when ?IS_SET(S) ->
     true;
 is_sofs_set(S) when ?IS_ORDSET(S) ->
@@ -409,16 +544,26 @@ is_sofs_set(S) when ?IS_ORDSET(S) ->
 is_sofs_set(_S) ->
     false.
 
+-spec(is_set(AnySet) -> Bool when
+      AnySet :: anyset(),
+      Bool :: boolean()).
 is_set(S) when ?IS_SET(S) ->
     true;
 is_set(S) when ?IS_ORDSET(S) ->
     false.
 
-is_empty_set(S) when ?IS_SET(S) -> 
+-spec(is_empty_set(AnySet) -> Bool when
+      AnySet :: anyset(),
+      Bool :: boolean()).
+is_empty_set(S) when ?IS_SET(S) ->
     ?LIST(S) =:= [];
 is_empty_set(S) when ?IS_ORDSET(S) ->
     false.
 
+-spec(is_disjoint(Set1, Set2) -> Bool when
+      Bool :: boolean(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 is_disjoint(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
     case match_types(?TYPE(S1), ?TYPE(S2)) of
         true ->
@@ -433,6 +578,9 @@ is_disjoint(S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
 %%% Functions on set-of-sets.
 %%%
 
+-spec(union(SetOfSets) -> Set when
+      Set :: a_set(),
+      SetOfSets :: set_of_sets()).
 union(Sets) when ?IS_SET(Sets) ->
     case ?TYPE(Sets) of
         ?SET_OF(Type) -> ?SET(lunion(?LIST(Sets)), Type);
@@ -440,6 +588,9 @@ union(Sets) when ?IS_SET(Sets) ->
         _ -> erlang:error(badarg, [Sets])
     end.
 
+-spec(intersection(SetOfSets) -> Set when
+      Set :: a_set(),
+      SetOfSets :: set_of_sets()).
 intersection(Sets) when ?IS_SET(Sets) ->
     case ?LIST(Sets) of
         [] -> erlang:error(badarg, [Sets]);
@@ -451,32 +602,41 @@ intersection(Sets) when ?IS_SET(Sets) ->
             end
     end.
 
+-spec(canonical_relation(SetOfSets) -> BinRel when
+      BinRel :: binary_relation(),
+      SetOfSets :: set_of_sets()).
 canonical_relation(Sets) when ?IS_SET(Sets) ->
     ST = ?TYPE(Sets),
     case ST of
         ?SET_OF(?ANYTYPE) -> empty_set();
-        ?SET_OF(Type) -> 
+        ?SET_OF(Type) ->
             ?SET(can_rel(?LIST(Sets), []), ?BINREL(Type, ST));
         ?ANYTYPE -> Sets;
         _ -> erlang:error(badarg, [Sets])
     end.
 
-%%% 
+%%%
 %%% Functions on binary relations only.
-%%% 
+%%%
 
 rel2fam(R) ->
     relation_to_family(R).
 
+-spec(relation_to_family(BinRel) -> Family when
+      Family :: family(),
+      BinRel :: binary_relation()).
 %% Inlined.
 relation_to_family(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
-        ?BINREL(DT, RT) -> 
+        ?BINREL(DT, RT) ->
             ?SET(rel2family(?LIST(R)), ?FAMILY(DT, RT));
         ?ANYTYPE -> R;
         _Else    -> erlang:error(badarg, [R])
     end.
 
+-spec(domain(BinRel) -> Set when
+      BinRel :: binary_relation(),
+      Set :: a_set()).
 domain(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
         ?BINREL(DT, _)  -> ?SET(dom(?LIST(R)), DT);
@@ -484,6 +644,9 @@ domain(R) when ?IS_SET(R) ->
         _Else    -> erlang:error(badarg, [R])
     end.
 
+-spec(range(BinRel) -> Set when
+      BinRel :: binary_relation(),
+      Set :: a_set()).
 range(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
         ?BINREL(_, RT)  -> ?SET(ran(?LIST(R),  []), RT);
@@ -491,35 +654,63 @@ range(R) when ?IS_SET(R) ->
         _ -> erlang:error(badarg, [R])
     end.
 
+-spec(field(BinRel) -> Set when
+      BinRel :: binary_relation(),
+      Set :: a_set()).
 %% In "Introduction to LOGIC", Suppes defines the field of a binary
 %% relation to be the union of the domain and the range (or
 %% counterdomain).
 field(R) ->
     union(domain(R), range(R)).
 
+-spec(relative_product(ListOfBinRels) -> BinRel2 when
+      ListOfBinRels :: [BinRel, ...],
+      BinRel :: binary_relation(),
+      BinRel2 :: binary_relation()).
+%% The following clause is kept for backward compatibility.
+%% The list is due to Dialyzer's specs.
 relative_product(RT) when is_tuple(RT) ->
-    case relprod_n(RT, foo, false, false) of
-        {error, Reason} -> 
-            erlang:error(Reason, [RT]);
+    relative_product(tuple_to_list(RT));
+relative_product(RL) when is_list(RL) ->
+    case relprod_n(RL, foo, false, false) of
+        {error, Reason} ->
+            erlang:error(Reason, [RL]);
         Reply ->
             Reply
     end.
 
+-spec(relative_product(ListOfBinRels, BinRel1) -> BinRel2 when
+      ListOfBinRels :: [BinRel, ...],
+      BinRel :: binary_relation(),
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation();
+                      (BinRel1, BinRel2) -> BinRel3 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation(),
+      BinRel3 :: binary_relation()).
 relative_product(R1, R2) when ?IS_SET(R1), ?IS_SET(R2) ->
     relative_product1(converse(R1), R2);
+%% The following clause is kept for backward compatibility.
+%% The list is due to Dialyzer's specs.
 relative_product(RT, R) when is_tuple(RT), ?IS_SET(R) ->
+    relative_product(tuple_to_list(RT), R);
+relative_product(RL, R) when is_list(RL), ?IS_SET(R) ->
     EmptyR = case ?TYPE(R) of
                  ?BINREL(_, _) -> ?LIST(R) =:= [];
                  ?ANYTYPE -> true;
-                 _ -> erlang:error(badarg, [RT, R])
+                 _ -> erlang:error(badarg, [RL, R])
              end,
-    case relprod_n(RT, R, EmptyR, true) of
-        {error, Reason} -> 
-            erlang:error(Reason, [RT, R]);
+    case relprod_n(RL, R, EmptyR, true) of
+        {error, Reason} ->
+            erlang:error(Reason, [RL, R]);
         Reply ->
             Reply
     end.
 
+-spec(relative_product1(BinRel1, BinRel2) -> BinRel3 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation(),
+      BinRel3 :: binary_relation()).
 relative_product1(R1, R2) when ?IS_SET(R1), ?IS_SET(R2) ->
     {DTR1, RTR1} = case ?TYPE(R1) of
                      ?BINREL(_, _) = R1T -> R1T;
@@ -538,16 +729,23 @@ relative_product1(R1, R2) when ?IS_SET(R1), ?IS_SET(R2) ->
         false -> erlang:error(type_mismatch, [R1, R2])
     end.
 
+-spec(converse(BinRel1) -> BinRel2 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation()).
 converse(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
         ?BINREL(DT, RT) -> ?SET(converse(?LIST(R), []), ?BINREL(RT, DT));
         ?ANYTYPE -> R;
         _ -> erlang:error(badarg, [R])
     end.
-    
+
+-spec(image(BinRel, Set1) -> Set2 when
+      BinRel :: binary_relation(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 image(R, S) when ?IS_SET(R), ?IS_SET(S) ->
     case ?TYPE(R) of
-        ?BINREL(DT, RT) -> 
+        ?BINREL(DT, RT) ->
 	    case match_types(DT, ?TYPE(S)) of
 		true ->
 		    ?SET(usort(restrict(?LIST(S), ?LIST(R))), RT);
@@ -558,9 +756,13 @@ image(R, S) when ?IS_SET(R), ?IS_SET(S) ->
         _ -> erlang:error(badarg, [R, S])
     end.
 
+-spec(inverse_image(BinRel, Set1) -> Set2 when
+      BinRel :: binary_relation(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 inverse_image(R, S) when ?IS_SET(R), ?IS_SET(S) ->
     case ?TYPE(R) of
-        ?BINREL(DT, RT) -> 
+        ?BINREL(DT, RT) ->
 	    case match_types(RT, ?TYPE(S)) of
 		true ->
 		    NL = restrict(?LIST(S), converse(?LIST(R), [])),
@@ -572,17 +774,23 @@ inverse_image(R, S) when ?IS_SET(R), ?IS_SET(S) ->
         _ -> erlang:error(badarg, [R, S])
     end.
 
+-spec(strict_relation(BinRel1) -> BinRel2 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation()).
 strict_relation(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
-        Type = ?BINREL(_, _) -> 
+        Type = ?BINREL(_, _) ->
             ?SET(strict(?LIST(R), []), Type);
         ?ANYTYPE -> R;
         _ -> erlang:error(badarg, [R])
     end.
-    
+
+-spec(weak_relation(BinRel1) -> BinRel2 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation()).
 weak_relation(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
-        ?BINREL(DT, RT) -> 
+        ?BINREL(DT, RT) ->
             case unify_types(DT, RT) of
                 [] ->
                     erlang:error(badarg, [R]);
@@ -592,7 +800,12 @@ weak_relation(R) when ?IS_SET(R) ->
         ?ANYTYPE -> R;
         _ -> erlang:error(badarg, [R])
     end.
-    
+
+-spec(extension(BinRel1, Set, AnySet) -> BinRel2 when
+      AnySet :: anyset(),
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation(),
+      Set :: a_set()).
 extension(R, S, E) when ?IS_SET(R), ?IS_SET(S) ->
     case {?TYPE(R), ?TYPE(S), is_sofs_set(E)} of
 	{T=?BINREL(DT, RT), ST, true} ->
@@ -621,9 +834,12 @@ extension(R, S, E) when ?IS_SET(R), ?IS_SET(S) ->
 	    erlang:error(badarg, [R, S, E])
     end.
 
+-spec(is_a_function(BinRel) -> Bool when
+      Bool :: boolean(),
+      BinRel :: binary_relation()).
 is_a_function(R) when ?IS_SET(R) ->
     case ?TYPE(R) of
-        ?BINREL(_, _) -> 
+        ?BINREL(_, _) ->
             case ?LIST(R) of
                 [] -> true;
                 [{V,_} | Es] -> is_a_func(Es, V)
@@ -632,16 +848,28 @@ is_a_function(R) when ?IS_SET(R) ->
         _ -> erlang:error(badarg, [R])
     end.
 
+-spec(restriction(BinRel1, Set) -> BinRel2 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation(),
+      Set :: a_set()).
 restriction(Relation, Set) ->
     restriction(1, Relation, Set).
 
+-spec(drestriction(BinRel1, Set) -> BinRel2 when
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation(),
+      Set :: a_set()).
 drestriction(Relation, Set) ->
     drestriction(1, Relation, Set).
 
-%%% 
+%%%
 %%% Functions on functions only.
-%%% 
+%%%
 
+-spec(composite(Function1, Function2) -> Function3 when
+      Function1 :: a_function(),
+      Function2 :: a_function(),
+      Function3 :: a_function()).
 composite(Fn1, Fn2) when ?IS_SET(Fn1), ?IS_SET(Fn2) ->
     ?BINREL(DTF1, RTF1) = case ?TYPE(Fn1)of
 			      ?BINREL(_, _) = F1T -> F1T;
@@ -656,7 +884,7 @@ composite(Fn1, Fn2) when ?IS_SET(Fn1), ?IS_SET(Fn2) ->
     case match_types(RTF1, DTF2) of
         true when DTF1 =:= ?ANYTYPE -> Fn1;
         true when DTF2 =:= ?ANYTYPE -> Fn2;
-        true -> 
+        true ->
 	    case comp(?LIST(Fn1), ?LIST(Fn2)) of
 		SL when is_list(SL) ->
 		    ?SET(sort(SL), ?BINREL(DTF1, RTF2));
@@ -666,9 +894,12 @@ composite(Fn1, Fn2) when ?IS_SET(Fn1), ?IS_SET(Fn2) ->
         false -> erlang:error(type_mismatch, [Fn1, Fn2])
     end.
 
+-spec(inverse(Function1) -> Function2 when
+      Function1 :: a_function(),
+      Function2 :: a_function()).
 inverse(Fn) when ?IS_SET(Fn) ->
     case ?TYPE(Fn) of
-        ?BINREL(DT, RT) -> 
+        ?BINREL(DT, RT) ->
 	    case inverse1(?LIST(Fn)) of
 		SL when is_list(SL) ->
 		    ?SET(SL, ?BINREL(RT, DT));
@@ -678,11 +909,16 @@ inverse(Fn) when ?IS_SET(Fn) ->
         ?ANYTYPE -> Fn;
         _ -> erlang:error(badarg, [Fn])
     end.
-    
-%%% 
+
+%%%
 %%% Functions on relations (binary or other).
-%%% 
+%%%
 
+-spec(restriction(SetFun, Set1, Set2) -> Set3 when
+      SetFun :: set_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 %% Equivalent to range(restriction(inverse(substitution(Fun, S1)), S2)).
 restriction(I, R, S) when is_integer(I), ?IS_SET(R), ?IS_SET(S) ->
     RT = ?TYPE(R),
@@ -747,6 +983,11 @@ restriction(SetFun, S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
 	    end
     end.
 
+-spec(drestriction(SetFun, Set1, Set2) -> Set3 when
+      SetFun :: set_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set()).
 drestriction(I, R, S) when is_integer(I), ?IS_SET(R), ?IS_SET(S) ->
     RT = ?TYPE(R),
     ST = ?TYPE(S),
@@ -812,6 +1053,10 @@ drestriction(SetFun, S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
 	    end
     end.
 
+-spec(projection(SetFun, Set1) -> Set2 when
+      SetFun :: set_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 projection(I, Set) when is_integer(I), ?IS_SET(Set) ->
     Type = ?TYPE(Set),
     case check_for_sort(Type, I) of
@@ -827,6 +1072,10 @@ projection(I, Set) when is_integer(I), ?IS_SET(Set) ->
 projection(Fun, Set) ->
     range(substitution(Fun, Set)).
 
+-spec(substitution(SetFun, Set1) -> Set2 when
+      SetFun :: set_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set()).
 substitution(I, Set) when is_integer(I), ?IS_SET(Set) ->
     Type = ?TYPE(Set),
     case check_for_sort(Type, I) of
@@ -867,11 +1116,18 @@ substitution(SetFun, Set) when ?IS_SET(Set) ->
 	    end
     end.
 
+-spec(partition(SetOfSets) -> Partition when
+      SetOfSets :: set_of_sets(),
+      Partition :: a_set()).
 partition(Sets) ->
     F1 = relation_to_family(canonical_relation(Sets)),
     F2 = relation_to_family(converse(F1)),
     range(F2).
 
+-spec(partition(SetFun, Set) -> Partition when
+      SetFun :: set_fun(),
+      Partition :: a_set(),
+      Set :: a_set()).
 partition(I, Set) when is_integer(I), ?IS_SET(Set) ->
     Type = ?TYPE(Set),
     case check_for_sort(Type, I) of
@@ -887,6 +1143,12 @@ partition(I, Set) when is_integer(I), ?IS_SET(Set) ->
 partition(Fun, Set) ->
     range(partition_family(Fun, Set)).
 
+-spec(partition(SetFun, Set1, Set2) -> {Set3, Set4} when
+      SetFun :: set_fun(),
+      Set1 :: a_set(),
+      Set2 :: a_set(),
+      Set3 :: a_set(),
+      Set4 :: a_set()).
 partition(I, R, S) when is_integer(I), ?IS_SET(R), ?IS_SET(S) ->
     RT = ?TYPE(R),
     ST = ?TYPE(S),
@@ -954,21 +1216,32 @@ partition(SetFun, S1, S2) when ?IS_SET(S1), ?IS_SET(S2) ->
 	    end
     end.
 
+-spec(multiple_relative_product(TupleOfBinRels, BinRel1) -> BinRel2 when
+      TupleOfBinRels :: tuple_of(BinRel),
+      BinRel :: binary_relation(),
+      BinRel1 :: binary_relation(),
+      BinRel2 :: binary_relation()).
 multiple_relative_product(T, R) when is_tuple(T), ?IS_SET(R) ->
     case test_rel(R, tuple_size(T), eq) of
 	true when ?TYPE(R) =:= ?ANYTYPE ->
 	    empty_set();
-        true -> 
+        true ->
 	    MProd = mul_relprod(tuple_to_list(T), 1, R),
-	    relative_product(list_to_tuple(MProd));
-        false -> 
+	    relative_product(MProd);
+        false ->
 	    erlang:error(badarg, [T, R])
     end.
 
-join(R1, I1, R2, I2) 
+-spec(join(Relation1, I, Relation2, J) -> Relation3 when
+      Relation1 :: relation(),
+      Relation2 :: relation(),
+      Relation3 :: relation(),
+      I :: pos_integer(),
+      J :: pos_integer()).
+join(R1, I1, R2, I2)
   when ?IS_SET(R1), ?IS_SET(R2), is_integer(I1), is_integer(I2) ->
     case test_rel(R1, I1, lte) and test_rel(R2, I2, lte) of
-        false -> 
+        false ->
 	    erlang:error(badarg, [R1, I1, R2, I2]);
         true when ?TYPE(R1) =:= ?ANYTYPE -> R1;
         true when ?TYPE(R2) =:= ?ANYTYPE -> R2;
@@ -980,8 +1253,8 @@ join(R1, I1, R2, I2)
 		    true ->
 			fun({X,Y}) -> join_element(X, Y) end;
 		    false ->
-			fun({X,Y}) -> 
-				list_to_tuple(join_element(X, Y, I2)) 
+			fun({X,Y}) ->
+				list_to_tuple(join_element(X, Y, I2))
 			end
 		end,
 	    ?SET(replace(T, F, []), F({?TYPE(R1), ?TYPE(R2)}))
@@ -1001,9 +1274,15 @@ test_rel(R, I, C) ->
 %%% Family functions
 %%%
 
+-spec(fam2rel(Family) -> BinRel when
+      Family :: family(),
+      BinRel :: binary_relation()).
 fam2rel(F) ->
     family_to_relation(F).
 
+-spec(family_to_relation(Family) -> BinRel when
+      Family :: family(),
+      BinRel :: binary_relation()).
 %% Inlined.
 family_to_relation(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
@@ -1013,6 +1292,10 @@ family_to_relation(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_specification(Fun, Family1) -> Family2 when
+      Fun :: spec_fun(),
+      Family1 :: family(),
+      Family2 :: family()).
 family_specification(Fun, F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(_DT, Type) = FType ->
@@ -1032,6 +1315,9 @@ family_specification(Fun, F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [Fun, F])
     end.
 
+-spec(union_of_family(Family) -> Set when
+      Family :: family(),
+      Set :: a_set()).
 union_of_family(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(_DT, Type) ->
@@ -1040,6 +1326,9 @@ union_of_family(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(intersection_of_family(Family) -> Set when
+      Family :: family(),
+      Set :: a_set()).
 intersection_of_family(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(_DT, Type) ->
@@ -1052,6 +1341,9 @@ intersection_of_family(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_union(Family1) -> Family2 when
+      Family1 :: family(),
+      Family2 :: family()).
 family_union(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(DT, ?SET_OF(Type)) ->
@@ -1060,6 +1352,9 @@ family_union(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_intersection(Family1) -> Family2 when
+      Family1 :: family(),
+      Family2 :: family()).
 family_intersection(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(DT, ?SET_OF(Type)) ->
@@ -1073,6 +1368,9 @@ family_intersection(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_domain(Family1) -> Family2 when
+      Family1 :: family(),
+      Family2 :: family()).
 family_domain(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(FDT, ?BINREL(DT, _)) ->
@@ -1082,6 +1380,9 @@ family_domain(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_range(Family1) -> Family2 when
+      Family1 :: family(),
+      Family2 :: family()).
 family_range(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(DT, ?BINREL(_, RT)) ->
@@ -1091,15 +1392,30 @@ family_range(F) when ?IS_SET(F) ->
         _ -> erlang:error(badarg, [F])
     end.
 
+-spec(family_field(Family1) -> Family2 when
+      Family1 :: family(),
+      Family2 :: family()).
 family_field(F) ->
     family_union(family_domain(F), family_range(F)).
 
+-spec(family_union(Family1, Family2) -> Family3 when
+      Family1 :: family(),
+      Family2 :: family(),
+      Family3 :: family()).
 family_union(F1, F2) ->
     fam_binop(F1, F2, fun fam_union/3).
 
+-spec(family_intersection(Family1, Family2) -> Family3 when
+      Family1 :: family(),
+      Family2 :: family(),
+      Family3 :: family()).
 family_intersection(F1, F2) ->
     fam_binop(F1, F2, fun fam_intersect/3).
 
+-spec(family_difference(Family1, Family2) -> Family3 when
+      Family1 :: family(),
+      Family2 :: family(),
+      Family3 :: family()).
 family_difference(F1, F2) ->
     fam_binop(F1, F2, fun fam_difference/3).
 
@@ -1108,13 +1424,17 @@ fam_binop(F1, F2, FF) when ?IS_SET(F1), ?IS_SET(F2) ->
     case unify_types(?TYPE(F1), ?TYPE(F2)) of
         [] ->
             erlang:error(type_mismatch, [F1, F2]);
-        ?ANYTYPE -> 
+        ?ANYTYPE ->
             F1;
-        Type = ?FAMILY(_, _) -> 
+        Type = ?FAMILY(_, _) ->
 	    ?SET(FF(?LIST(F1), ?LIST(F2), []), Type);
         _ ->  erlang:error(badarg, [F1, F2])
     end.
 
+-spec(partition_family(SetFun, Set) -> Family when
+      Family :: family(),
+      SetFun :: set_fun(),
+      Set :: a_set()).
 partition_family(I, Set) when is_integer(I), ?IS_SET(Set) ->
     Type = ?TYPE(Set),
     case check_for_sort(Type, I) of
@@ -1159,8 +1479,12 @@ partition_family(SetFun, Set) when ?IS_SET(Set) ->
 	    end
     end.
 
+-spec(family_projection(SetFun, Family1) -> Family2 when
+      SetFun :: set_fun(),
+      Family1 :: family(),
+      Family2 :: family()).
 family_projection(SetFun, F) when ?IS_SET(F) ->
-    case ?TYPE(F) of 
+    case ?TYPE(F) of
         ?FAMILY(_, _) when [] =:= ?LIST(F) ->
 	    empty_set();
         ?FAMILY(DT, Type) ->
@@ -1172,7 +1496,7 @@ family_projection(SetFun, F) when ?IS_SET(F) ->
 			Bad ->
 			    erlang:error(Bad, [SetFun, F])
 		    end;
-		_ -> 
+		_ ->
 		    erlang:error(badarg, [SetFun, F])
 	    end;
 	?ANYTYPE -> F;
@@ -1183,6 +1507,9 @@ family_projection(SetFun, F) when ?IS_SET(F) ->
 %%% Digraph functions
 %%%
 
+-spec(family_to_digraph(Family) -> Graph when
+      Graph :: digraph(),
+      Family :: family()).
 family_to_digraph(F) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(_, _) -> fam2digraph(F, digraph:new());
@@ -1190,6 +1517,10 @@ family_to_digraph(F) when ?IS_SET(F) ->
         _Else -> erlang:error(badarg, [F])
     end.
 
+-spec(family_to_digraph(Family, GraphType) -> Graph when
+      Graph :: digraph(),
+      Family :: family(),
+      GraphType :: [digraph:d_type()]).
 family_to_digraph(F, Type) when ?IS_SET(F) ->
     case ?TYPE(F) of
         ?FAMILY(_, _) -> ok;
@@ -1208,12 +1539,19 @@ family_to_digraph(F, Type) when ?IS_SET(F) ->
         error:badarg -> erlang:error(badarg, [F, Type])
     end.
 
+-spec(digraph_to_family(Graph) -> Family when
+      Graph :: digraph(),
+      Family :: family()).
 digraph_to_family(G) ->
     case catch digraph_family(G) of
         {'EXIT', _} -> erlang:error(badarg, [G]);
         L -> ?SET(L, ?FAMILY(?ATOM_TYPE, ?ATOM_TYPE))
     end.
 
+-spec(digraph_to_family(Graph, Type) -> Family when
+      Graph :: digraph(),
+      Family :: family(),
+      Type :: type()).
 digraph_to_family(G, T) ->
     case {is_type(T), T} of
         {true, ?SET_OF(?FAMILY(_,_) = Type)} ->
@@ -1284,7 +1622,7 @@ rel(Ts, [Type]) ->
     end;
 rel(Ts, Sz) ->
     rel(Ts, Sz, erlang:make_tuple(Sz, ?ATOM_TYPE)).
-    
+
 atoms_only(Type, I) when ?IS_ATOM_TYPE(?REL_TYPE(I, Type)) ->
     atoms_only(Type, I+1);
 atoms_only(Type, I) when I > tuple_size(Type), ?IS_RELATION(Type) ->
@@ -1312,7 +1650,7 @@ rel_type([], SL, Type) when ?IS_RELATION(Type) ->
 %% Inlined.
 a_func(Ts, T) ->
     case {T, is_type(T)} of
-	{[?BINREL(DT, RT) = Type], true} when ?IS_ATOM_TYPE(DT), 
+	{[?BINREL(DT, RT) = Type], true} when ?IS_ATOM_TYPE(DT),
 					      ?IS_ATOM_TYPE(RT)  ->
 	    func(Ts, Type);
 	{[Type], true} ->
@@ -1333,16 +1671,16 @@ func([], _X0, L, Type) ->
 %% Inlined.
 fam(Ts, T) ->
     case {T, is_type(T)} of
-	{[?FAMILY(DT, RT) = Type], true} when ?IS_ATOM_TYPE(DT), 
+	{[?FAMILY(DT, RT) = Type], true} when ?IS_ATOM_TYPE(DT),
 					      ?IS_ATOM_TYPE(RT)  ->
 	    fam2(Ts, Type);
 	{[Type], true} ->
 	    func_type(Ts, [], Type, fun(?FAMILY(_,_)) -> true end)
     end.
 
-fam2([], Type) -> 
+fam2([], Type) ->
     ?SET([], Type);
-fam2(Ts, Type) -> 
+fam2(Ts, Type) ->
     fam2(sort(Ts), Ts, [], Type).
 
 fam2([{I,L} | T], I0, SL, Type) when I /= I0 ->
@@ -1383,7 +1721,7 @@ setify(E, Type0) ->
     {Type, OrdSet} = make_element(E, Type0, Type0),
     ?ORDSET(OrdSet, Type).
 
-is_no_lists(T) when is_tuple(T) -> 
+is_no_lists(T) when is_tuple(T) ->
    Sz = tuple_size(T),
    is_no_lists(T, Sz, Sz, []).
 
@@ -1404,7 +1742,7 @@ create([], T, _T0, L) ->
 
 make_element(C, ?ANYTYPE, _T0) ->
     make_element(C);
-make_element(C, Atom, ?ANYTYPE) when ?IS_ATOM_TYPE(Atom), 
+make_element(C, Atom, ?ANYTYPE) when ?IS_ATOM_TYPE(Atom),
                                      not is_list(C), not is_tuple(C) ->
     {Atom, C};
 make_element(C, Atom, Atom) when ?IS_ATOM_TYPE(Atom) ->
@@ -1585,12 +1923,12 @@ sympart([H1 | T1], [H2 | T2], L1, L12, L2, T) when H1 == H2 ->
 sympart([H1 | T1], [H2 | T2], L1, L12, L2, T) ->
     sympart2(T1, T2, L1, L12, [H2 | L2], T, H1);
 sympart(S1, [], L1, L12, L2, T) ->
-    {?SET(reverse(L1, S1), T), 
-     ?SET(reverse(L12), T), 
+    {?SET(reverse(L1, S1), T),
+     ?SET(reverse(L12), T),
      ?SET(reverse(L2), T)};
 sympart(_, S2, L1, L12, L2, T) ->
-    {?SET(reverse(L1), T), 
-     ?SET(reverse(L12), T), 
+    {?SET(reverse(L1), T),
+     ?SET(reverse(L12), T),
      ?SET(reverse(L2, S2), T)}.
 
 sympart1([H1 | T1], T2, L1, L12, L2, T, H2) when H1 < H2 ->
@@ -1600,8 +1938,8 @@ sympart1([H1 | T1], T2, L1, L12, L2, T, H2) when H1 == H2 ->
 sympart1([H1 | T1], T2, L1, L12, L2, T, H2) ->
     sympart2(T1, T2, L1, L12, [H2 | L2], T, H1);
 sympart1(_, T2, L1, L12, L2, T, H2) ->
-    {?SET(reverse(L1), T), 
-     ?SET(reverse(L12), T), 
+    {?SET(reverse(L1), T),
+     ?SET(reverse(L12), T),
      ?SET(reverse(L2, [H2 | T2]), T)}.
 
 sympart2(T1, [H2 | T2], L1, L12, L2, T, H1) when H1 > H2 ->
@@ -1611,8 +1949,8 @@ sympart2(T1, [H2 | T2], L1, L12, L2, T, H1) when H1 == H2 ->
 sympart2(T1, [H2 | T2], L1, L12, L2, T, H1) ->
     sympart1(T1, T2, [H1 | L1], L12, L2, T, H2);
 sympart2(T1, _, L1, L12, L2, T, H1) ->
-    {?SET(reverse(L1, [H1 | T1]), T), 
-     ?SET(reverse(L12), T), 
+    {?SET(reverse(L1, [H1 | T1]), T),
+     ?SET(reverse(L12), T),
      ?SET(reverse(L2), T)}.
 
 prod([[E | Es] | Xs], T, L) ->
@@ -1660,7 +1998,7 @@ lunion([[] | Ls]) ->
     lunion(Ls);
 lunion([S | Ss]) ->
     umerge(lunion(Ss, last(S), [S], []));
-lunion([]) -> 
+lunion([]) ->
     [].
 
 lunion([[E] = S | Ss], Last, SL, Ls) when E > Last -> % optimization
@@ -1669,7 +2007,7 @@ lunion([S | Ss], Last, SL, Ls) when hd(S) > Last ->
     lunion(Ss, last(S), [S | SL], Ls);
 lunion([S | Ss], _Last, SL, Ls) ->
     lunion(Ss, last(S), [S], [append(reverse(SL)) | Ls]);
-lunion([], _Last, SL, Ls) -> 
+lunion([], _Last, SL, Ls) ->
     [append(reverse(SL)) | Ls].
 
 %% The empty list is always the first list, if present.
@@ -1752,18 +2090,17 @@ relprod(B0, Bx0, By0, A0, L, Ax, [{Bx,By} | B], Ay) when Ay == Bx ->
 relprod(B0, Bx0, By0, A0, L, _Ax, _B, _Ay) ->
     relprod2(B0, Bx0, By0, A0, L).
 
-relprod_n({}, _R, _EmptyG, _IsR) ->
+relprod_n([], _R, _EmptyG, _IsR) ->
     {error, badarg};
-relprod_n(RT, R, EmptyR, IsR) ->
-    RL = tuple_to_list(RT),
+relprod_n(RL, R, EmptyR, IsR) ->
     case domain_type(RL, ?ANYTYPE) of
-        Error = {error, _Reason} -> 
+        Error = {error, _Reason} ->
             Error;
         DType ->
             Empty = any(fun is_empty_set/1, RL) or EmptyR,
             RType = range_type(RL, []),
             Type = ?BINREL(DType, RType),
-            Prod = 
+            Prod =
                 case Empty of
                     true when DType =:= ?ANYTYPE; RType =:= ?ANYTYPE ->
                         empty_set();
@@ -1771,7 +2108,7 @@ relprod_n(RT, R, EmptyR, IsR) ->
                         ?SET([], Type);
                     false ->
                         TL = ?LIST((relprod_n(RL))),
-                        Sz = tuple_size(RT),
+                        Sz = length(RL),
                         Fun = fun({X,A}) -> {X, flat(Sz, A, [])} end,
                         ?SET(map(Fun, TL), Type)
                 end,
@@ -1799,12 +2136,12 @@ flat(N, {T,A}, L) ->
 
 domain_type([T | Ts], T0) when ?IS_SET(T) ->
     case ?TYPE(T) of
-        ?BINREL(DT, _RT) -> 
+        ?BINREL(DT, _RT) ->
             case unify_types(DT, T0) of
                 [] -> {error, type_mismatch};
                 T1 -> domain_type(Ts, T1)
             end;
-        ?ANYTYPE -> 
+        ?ANYTYPE ->
             domain_type(Ts, T0);
         _ -> {error, badarg}
     end;
@@ -1813,12 +2150,12 @@ domain_type([], T0) ->
 
 range_type([T | Ts], L) ->
     case ?TYPE(T) of
-        ?BINREL(_DT, RT) -> 
+        ?BINREL(_DT, RT) ->
             range_type(Ts, [RT | L]);
-        ?ANYTYPE -> 
+        ?ANYTYPE ->
             ?ANYTYPE
     end;
-range_type([], L) -> 
+range_type([], L) ->
     list_to_tuple(reverse(L)).
 
 converse([{A,B} | X], L) ->
@@ -1861,7 +2198,7 @@ weak1([E={X,_Y} | Es], Ys, L, X0) when X == X0 -> % when X < Y
 weak1(Es, Ys, L, X) ->
     weak(Es, Ys, [{X,X} | L]).
 
-weak2([E={X,_Y} | Es], Ys, L, X0) when X == X0 -> % when X < _Y 
+weak2([E={X,_Y} | Es], Ys, L, X0) when X == X0 -> % when X < _Y
     weak2(Es, Ys, [E | L], X);
 weak2(Es, Ys, L, _X) ->
     weak(Es, Ys, L).
@@ -1910,7 +2247,7 @@ restrict_n(I, [T | Ts], Key, Keys, L) ->
     end;
 restrict_n(_I, _Ts, _Key, _Keys, L) ->
     L.
-    
+
 restrict_n(I, K, Ts, [Key | Keys], L, E) when K > Key ->
     restrict_n(I, K, Ts, Keys, L, E);
 restrict_n(I, K, Ts, [Key | Keys], L, E) when K == Key ->
@@ -1933,7 +2270,7 @@ restrict([{K,E} | Ts], _Key, Keys, L) ->
     restrict(Ts, K, Keys, L, E);
 restrict(_Ts, _Key, _Keys, L) ->
     L.
-    
+
 restrict(Ts, K, [Key | Keys], L, E) when K > Key ->
     restrict(Ts, K, Keys, L, E);
 restrict(Ts, K, [Key | Keys], L, E) when K == Key ->
@@ -1956,7 +2293,7 @@ diff_restrict_n(I, _Ts, _Key, _Keys, L) when I =:= 1 ->
     reverse(L);
 diff_restrict_n(_I, _Ts, _Key, _Keys, L) ->
     sort(L).
-    
+
 diff_restrict_n(I, K, Ts, [Key | Keys], L, T) when K > Key ->
     diff_restrict_n(I, K, Ts, Keys, L, T);
 diff_restrict_n(I, K, Ts, [Key | Keys], L, _T) when K == Key ->
@@ -1981,7 +2318,7 @@ diff_restrict([{K,E} | Ts], _Key, Keys, L) ->
     diff_restrict(Ts, K, Keys, L, E);
 diff_restrict(_Ts, _Key, _Keys, L) ->
     L.
-    
+
 diff_restrict(Ts, K, [Key | Keys], L, E) when K > Key ->
     diff_restrict(Ts, K, Keys, L, E);
 diff_restrict(Ts, K, [Key | Keys], L, _E) when K == Key ->
@@ -2041,7 +2378,7 @@ external_fun({external, Function}) when is_atom(Function) ->
     false;
 external_fun({external, Fun}) ->
     Fun;
-external_fun(_) -> 
+external_fun(_) ->
     false.
 
 %% Inlined.
@@ -2121,7 +2458,7 @@ partition3_n(I, _Ts, _Key, _Keys, L1, L2) when I =:= 1 ->
     [reverse(L1) | reverse(L2)];
 partition3_n(_I, _Ts, _Key, _Keys, L1, L2) ->
     [sort(L1) | sort(L2)].
-    
+
 partition3_n(I, K, Ts, [Key | Keys], L1, L2, T) when K > Key ->
     partition3_n(I, K, Ts, Keys, L1, L2, T);
 partition3_n(I, K, Ts, [Key | Keys], L1, L2, T) when K == Key ->
@@ -2146,7 +2483,7 @@ partition3([{K,E} | Ts], _Key, Keys, L1, L2) ->
     partition3(Ts, K, Keys, L1, L2, E);
 partition3(_Ts, _Key, _Keys, L1, L2) ->
     [L1 | L2].
-    
+
 partition3(Ts, K, [Key | Keys], L1, L2, E) when K > Key ->
     partition3(Ts, K, Keys, L1, L2, E);
 partition3(Ts, K, [Key | Keys], L1, L2, E) when K == Key ->
@@ -2192,7 +2529,7 @@ join_element(E1, E2, I2) ->
 
 join_element2([B | Bs], C, I2) when C =/= I2 ->
     [B | join_element2(Bs, C+1, I2)];
-join_element2([_ | Bs], _C, _I2) -> 
+join_element2([_ | Bs], _C, _I2) ->
     Bs.
 
 family2rel([{X,S} | F], L) ->
@@ -2297,7 +2634,7 @@ check_function([{X,_} | XL], R) ->
     check_function(X, XL, R);
 check_function([], R) ->
     R.
-    
+
 check_function(X0, [{X,_} | XL], R) when X0 /= X ->
     check_function(X, XL, R);
 check_function(X0, [{X,_} | _XL], _R) when X0 == X ->
@@ -2371,14 +2708,14 @@ term2set(T, Type) ->
     ?ORDSET(T, Type).
 
 fam2digraph(F, G) ->
-    Fun = fun({From, ToL}) -> 
+    Fun = fun({From, ToL}) ->
                   digraph:add_vertex(G, From),
                   Fun2 = fun(To) ->
                                  digraph:add_vertex(G, To),
                                  case digraph:add_edge(G, From, To) of
-                                     {error, {bad_edge, _}} -> 
+                                     {error, {bad_edge, _}} ->
                                          throw({error, cyclic});
-                                     _ -> 
+                                     _ ->
                                          true
                                  end
                          end,
@@ -2397,7 +2734,7 @@ digraph_fam([V | Vs], V0, G, L) when V /= V0 ->
 digraph_fam([], _V0, _G, L) ->
     reverse(L).
 
-%% -> bool()
+%% -> boolean()
 check_fun(T, F, FunT) ->
     true = is_type(FunT),
     {NT, _MaxI} = number_tuples(T, 1),
@@ -2424,7 +2761,7 @@ check_for_sort(T, _I) when T =:= ?ANYTYPE ->
 check_for_sort(T, I) when ?IS_RELATION(T), I =< ?REL_ARITY(T), I >= 1 ->
     I > 1;
 check_for_sort(_T, _I) ->
-    error. 
+    error.
 
 inverse_substitution(L, Fun, Sort) ->
     %% One easily sees that the inverse of the tuples created by
@@ -2477,11 +2814,11 @@ match_types(Type1, Type2) -> match_types1(Type1, Type2).
 
 match_types1(Atom, Atom) when ?IS_ATOM_TYPE(Atom) ->
     true;
-match_types1(?ANYTYPE, _) -> 
+match_types1(?ANYTYPE, _) ->
     true;
-match_types1(_, ?ANYTYPE) -> 
+match_types1(_, ?ANYTYPE) ->
     true;
-match_types1(?SET_OF(Type1), ?SET_OF(Type2)) -> 
+match_types1(?SET_OF(Type1), ?SET_OF(Type2)) ->
     match_types1(Type1, Type2);
 match_types1(T1, T2) when tuple_size(T1) =:= tuple_size(T2) ->
     match_typesl(tuple_size(T1), T1, T2);