1%% -*- erlang-indent-level: 2 -*-
2%%
3%% Licensed under the Apache License, Version 2.0 (the "License");
4%% you may not use this file except in compliance with the License.
5%% You may obtain a copy of the License at
6%%
7%%     http://www.apache.org/licenses/LICENSE-2.0
8%%
9%% Unless required by applicable law or agreed to in writing, software
10%% distributed under the License is distributed on an "AS IS" BASIS,
11%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12%% See the License for the specific language governing permissions and
13%% limitations under the License.
14%%
15%% @copyright 2000-2003 Richard Carlsson, 2006-2009 Tobias Lindahl
16%% @author Richard Carlsson <carlsson.richard@gmail.com>
17%% @author Tobias Lindahl <tobias.lindahl@gmail.com>
18%% @author Kostis Sagonas <kostis@cs.ntua.gr>
19%% @author Manouk Manoukian
20%% @doc Provides a representation of Erlang types.
21
22%% The initial author of this file is Richard Carlsson (2000-2004).
23%% In July 2006, the type representation was totally re-designed by
24%% Tobias Lindahl. This is the representation which is used currently.
25%% In late 2008, Manouk Manoukian and Kostis Sagonas added support for
26%% opaque types to the structure-based representation of types.
27%% During February and March 2009, Kostis Sagonas significantly
28%% cleaned up the type representation and added spec declarations.
29
30-module(erl_types).
31
32-export([any_none/1,
33	 any_none_or_unit/1,
34	 lookup_record/3,
35	 max/2,
36	 min/2,
37	 number_max/1, number_max/2,
38	 number_min/1, number_min/2,
39	 t_abstract_records/2,
40	 t_any/0,
41	 t_arity/0,
42	 t_atom/0,
43	 t_atom/1,
44	 t_atoms/1,
45	 t_atom_vals/1, t_atom_vals/2,
46	 t_binary/0,
47	 t_bitstr/0,
48	 t_bitstr/2,
49	 t_bitstr_base/1,
50	 t_bitstr_concat/1,
51	 t_bitstr_concat/2,
52	 t_bitstr_match/2,
53	 t_bitstr_unit/1,
54	 t_bitstrlist/0,
55	 t_boolean/0,
56	 t_byte/0,
57	 t_char/0,
58	 t_collect_vars/1,
59	 t_cons/0,
60	 t_cons/2,
61	 t_cons_hd/1, t_cons_hd/2,
62	 t_cons_tl/1, t_cons_tl/2,
63         t_contains_opaque/1, t_contains_opaque/2,
64         t_decorate_with_opaque/3,
65	 t_elements/1,
66	 t_find_opaque_mismatch/3,
67         t_find_unknown_opaque/3,
68	 t_fixnum/0,
69	 t_non_neg_fixnum/0,
70	 t_pos_fixnum/0,
71	 t_float/0,
72         t_var_names/1,
73	 t_form_to_string/1,
74         t_from_form/6,
75         t_from_form_without_remote/3,
76         t_from_form_check_remote/4,
77         t_check_record_fields/6,
78	 t_from_range/2,
79	 t_from_range_unsafe/2,
80	 t_from_term/1,
81	 t_fun/0,
82	 t_fun/1,
83	 t_fun/2,
84	 t_fun_args/1, t_fun_args/2,
85	 t_fun_arity/1, t_fun_arity/2,
86	 t_fun_range/1, t_fun_range/2,
87	 t_has_opaque_subtype/2,
88	 t_has_var/1,
89	 t_identifier/0,
90	 %% t_improper_list/2,
91         t_inf/1,
92         t_inf/2,
93         t_inf/3,
94         t_inf_lists/2,
95         t_inf_lists/3,
96	 t_integer/0,
97	 t_integer/1,
98	 t_non_neg_integer/0,
99	 t_pos_integer/0,
100	 t_integers/1,
101	 t_iodata/0,
102	 t_iolist/0,
103	 t_is_any/1,
104	 t_is_atom/1, t_is_atom/2,
105	 t_is_any_atom/2, t_is_any_atom/3,
106	 t_is_binary/1, t_is_binary/2,
107	 t_is_bitstr/1, t_is_bitstr/2,
108	 t_is_bitwidth/1,
109	 t_is_boolean/1, t_is_boolean/2,
110         t_is_byte/1,
111         t_is_char/1,
112	 t_is_cons/1, t_is_cons/2,
113	 t_is_equal/2,
114	 t_is_fixnum/1,
115	 t_is_float/1, t_is_float/2,
116	 t_is_fun/1, t_is_fun/2,
117         t_is_identifier/1,
118	 t_is_instance/2,
119	 t_is_integer/1, t_is_integer/2,
120	 t_is_list/1,
121	 t_is_map/1,
122	 t_is_map/2,
123	 t_is_matchstate/1,
124	 t_is_nil/1, t_is_nil/2,
125	 t_is_non_neg_integer/1,
126	 t_is_none/1,
127	 t_is_none_or_unit/1,
128	 t_is_number/1, t_is_number/2,
129	 t_is_opaque/1, t_is_opaque/2,
130	 t_is_pid/1, t_is_pid/2,
131	 t_is_port/1, t_is_port/2,
132	 t_is_maybe_improper_list/1, t_is_maybe_improper_list/2,
133	 t_is_reference/1, t_is_reference/2,
134	 t_is_singleton/1,
135	 t_is_singleton/2,
136	 t_is_string/1,
137	 t_is_subtype/2,
138	 t_is_tuple/1, t_is_tuple/2,
139	 t_is_unit/1,
140	 t_is_var/1,
141	 t_limit/2,
142	 t_list/0,
143	 t_list/1,
144	 t_list_elements/1, t_list_elements/2,
145	 t_list_termination/1, t_list_termination/2,
146	 t_map/0,
147	 t_map/1,
148	 t_map/3,
149	 t_map_entries/2, t_map_entries/1,
150	 t_map_def_key/2, t_map_def_key/1,
151	 t_map_def_val/2, t_map_def_val/1,
152	 t_map_get/2, t_map_get/3,
153	 t_map_is_key/2, t_map_is_key/3,
154	 t_map_update/2, t_map_update/3,
155	 t_map_pairwise_merge/4,
156	 t_map_put/2, t_map_put/3,
157         t_map_remove/3,
158	 t_matchstate/0,
159	 t_matchstate/2,
160	 t_matchstate_present/1,
161	 t_matchstate_slot/2,
162	 t_matchstate_slots/1,
163	 t_matchstate_update_present/2,
164	 t_matchstate_update_slot/3,
165	 t_mfa/0,
166	 t_module/0,
167	 t_nil/0,
168	 t_node/0,
169	 t_none/0,
170	 t_nonempty_list/0,
171	 t_nonempty_list/1,
172	 t_nonempty_string/0,
173	 t_number/0,
174	 t_number/1,
175	 t_number_vals/1, t_number_vals/2,
176	 t_opaque_from_records/1,
177	 t_opaque_structure/1,
178	 t_pid/0,
179	 t_port/0,
180	 t_maybe_improper_list/0,
181	 %% t_maybe_improper_list/2,
182	 t_product/1,
183	 t_reference/0,
184	 t_singleton_to_term/2,
185	 t_string/0,
186	 t_struct_from_opaque/2,
187	 t_subst/2,
188	 t_subtract/2,
189	 t_subtract_list/2,
190	 t_sup/1,
191	 t_sup/2,
192	 t_timeout/0,
193	 t_to_string/1,
194	 t_to_string/2,
195	 t_to_tlist/1,
196	 t_tuple/0,
197	 t_tuple/1,
198	 t_tuple_args/1, t_tuple_args/2,
199	 t_tuple_size/1, t_tuple_size/2,
200	 t_tuple_sizes/1,
201	 t_tuple_subtypes/1,
202         t_tuple_subtypes/2,
203	 t_unify/2,
204	 t_unit/0,
205	 t_unopaque/1, t_unopaque/2,
206	 t_var/1,
207	 t_var_name/1,
208         t_widen_to_number/1,
209	 %% t_assign_variables_to_subtype/2,
210	 type_is_defined/4,
211	 record_field_diffs_to_string/2,
212	 subst_all_vars_to_any/1,
213         lift_list_to_pos_empty/1, lift_list_to_pos_empty/2,
214         is_opaque_type/2,
215	 is_erl_type/1,
216	 atom_to_string/1,
217	 var_table__new/0,
218	 cache__new/0
219	]).
220
221-compile({no_auto_import,[min/2,max/2,map_get/2]}).
222
223-export_type([erl_type/0, opaques/0, type_table/0,
224              var_table/0, cache/0]).
225
226%%-define(DEBUG, true).
227
228-ifdef(DEBUG).
229-define(debug(__A), __A).
230-else.
231-define(debug(__A), ok).
232-endif.
233
234%%=============================================================================
235%%
236%% Definition of the type structure
237%%
238%%=============================================================================
239
240%%-----------------------------------------------------------------------------
241%% Limits
242%%
243
244-define(REC_TYPE_LIMIT, 2).
245-define(EXPAND_DEPTH, 16).
246-define(EXPAND_LIMIT, 10000).
247
248-define(TUPLE_TAG_LIMIT, 5).
249-define(TUPLE_ARITY_LIMIT, 8).
250-define(SET_LIMIT, 13).
251-define(MAX_BYTE, 255).
252-define(MAX_CHAR, 16#10ffff).
253
254-define(UNIT_MULTIPLIER, 8).
255
256-define(TAG_IMMED1_SIZE, 4).
257-define(BITS, (erlang:system_info(wordsize) * 8) - ?TAG_IMMED1_SIZE).
258
259-define(MAX_TUPLE_SIZE, (1 bsl 10)).
260
261%%-----------------------------------------------------------------------------
262%% Type tags and qualifiers
263%%
264
265-define(atom_tag,       atom).
266-define(binary_tag,     binary).
267-define(function_tag,   function).
268-define(identifier_tag, identifier).
269-define(list_tag,       list).
270-define(map_tag,        map).
271-define(matchstate_tag, matchstate).
272-define(nil_tag,        nil).
273-define(number_tag,     number).
274-define(opaque_tag,     opaque).
275-define(product_tag,    product).
276-define(tuple_set_tag,  tuple_set).
277-define(tuple_tag,      tuple).
278-define(union_tag,      union).
279-define(var_tag,        var).
280
281-type tag()  :: ?atom_tag | ?binary_tag | ?function_tag | ?identifier_tag
282              | ?list_tag | ?map_tag | ?matchstate_tag | ?nil_tag | ?number_tag
283              | ?opaque_tag | ?product_tag
284              | ?tuple_tag | ?tuple_set_tag | ?union_tag | ?var_tag.
285
286-define(float_qual,     float).
287-define(integer_qual,   integer).
288-define(nonempty_qual,  nonempty).
289-define(pid_qual,       pid).
290-define(port_qual,      port).
291-define(reference_qual, reference).
292-define(unknown_qual,   unknown).
293
294-type qual() :: ?float_qual | ?integer_qual | ?nonempty_qual | ?pid_qual
295              | ?port_qual | ?reference_qual | ?unknown_qual | {_, _}.
296
297%%-----------------------------------------------------------------------------
298%% The type representation
299%%
300
301-define(any,  any).
302-define(none, none).
303-define(unit, unit).
304%% Generic constructor - elements can be many things depending on the tag.
305-record(c, {tag			      :: tag(),
306	    elements  = []	      :: term(),
307	    qualifier = ?unknown_qual :: qual()}).
308
309-opaque erl_type() :: ?any | ?none | ?unit | #c{}.
310
311%%-----------------------------------------------------------------------------
312%% Auxiliary types and convenient macros
313%%
314
315-type parse_form() :: erl_parse:abstract_type().
316-type rng_elem()   :: 'pos_inf' | 'neg_inf' | integer().
317
318-record(int_set, {set :: [integer()]}).
319-record(int_rng, {from :: rng_elem(), to :: rng_elem()}).
320%% Note: the definition of #opaque{} was changed to 'mod' and 'name';
321%% it used to be an ordsets of {Mod, Name} pairs. The Dialyzer version
322%% was updated to 2.7 due to this change.
323-record(opaque,  {mod :: module(), name :: atom(),
324		  args = [] :: [erl_type()], struct :: erl_type()}).
325
326-define(atom(Set),                 #c{tag=?atom_tag, elements=Set}).
327-define(bitstr(Unit, Base),        #c{tag=?binary_tag, elements=[Unit,Base]}).
328-define(float,                     ?number(?any, ?float_qual)).
329-define(function(Domain, Range),   #c{tag=?function_tag,
330				      elements=[Domain, Range]}).
331-define(identifier(Types),         #c{tag=?identifier_tag, elements=Types}).
332-define(integer(Types),            ?number(Types, ?integer_qual)).
333-define(int_range(From, To),       ?integer(#int_rng{from=From, to=To})).
334-define(int_set(Set),              ?integer(#int_set{set=Set})).
335-define(list(Types, Term, Size),   #c{tag=?list_tag, elements=[Types,Term],
336				      qualifier=Size}).
337-define(nil,                       #c{tag=?nil_tag}).
338-define(nonempty_list(Types, Term),?list(Types, Term, ?nonempty_qual)).
339-define(number(Set, Qualifier),    #c{tag=?number_tag, elements=Set,
340				      qualifier=Qualifier}).
341-define(map(Pairs,DefKey,DefVal),
342	#c{tag=?map_tag, elements={Pairs,DefKey,DefVal}}).
343-define(opaque(Optypes),           #c{tag=?opaque_tag, elements=Optypes}).
344-define(product(Types),            #c{tag=?product_tag, elements=Types}).
345-define(tuple(Types, Arity, Qual), #c{tag=?tuple_tag, elements=Types,
346				      qualifier={Arity, Qual}}).
347-define(tuple_set(Tuples),         #c{tag=?tuple_set_tag, elements=Tuples}).
348-define(var(Id),                   #c{tag=?var_tag, elements=Id}).
349
350-define(matchstate(P, Slots),	   #c{tag=?matchstate_tag, elements=[P,Slots]}).
351-define(any_matchstate,            ?matchstate(t_bitstr(), ?any)).
352
353-define(byte,                      ?int_range(0, ?MAX_BYTE)).
354-define(char,                      ?int_range(0, ?MAX_CHAR)).
355-define(integer_pos,               ?int_range(1, pos_inf)).
356-define(integer_non_neg,           ?int_range(0, pos_inf)).
357-define(integer_neg,               ?int_range(neg_inf, -1)).
358
359-type opaques() :: [erl_type()] | 'universe'.
360
361-type file_line()    :: {file:name(), erl_anno:line()}.
362-type record_key()   :: {'record', atom()}.
363-type type_key()     :: {'type' | 'opaque', mfa()}.
364-type field()        :: {atom(), erl_parse:abstract_expr(), erl_type()}.
365-type record_value() :: {file_line(),
366                         [{RecordSize :: non_neg_integer(), [field()]}]}.
367-type type_value()   :: {{module(), file_line(),
368                          erl_parse:abstract_type(), ArgNames :: [atom()]},
369                         erl_type()}.
370-type type_table() :: #{record_key() | type_key() =>
371                        record_value() | type_value()}.
372
373-opaque var_table() :: #{atom() => erl_type()}.
374
375%%-----------------------------------------------------------------------------
376%% Unions
377%%
378
379-define(union(List), #c{tag=?union_tag, elements=[_,_,_,_,_,_,_,_,_,_]=List}).
380
381-define(atom_union(T),       ?union([T,?none,?none,?none,?none,?none,?none,?none,?none,?none])).
382-define(bitstr_union(T),     ?union([?none,T,?none,?none,?none,?none,?none,?none,?none,?none])).
383-define(function_union(T),   ?union([?none,?none,T,?none,?none,?none,?none,?none,?none,?none])).
384-define(identifier_union(T), ?union([?none,?none,?none,T,?none,?none,?none,?none,?none,?none])).
385-define(list_union(T),       ?union([?none,?none,?none,?none,T,?none,?none,?none,?none,?none])).
386-define(number_union(T),     ?union([?none,?none,?none,?none,?none,T,?none,?none,?none,?none])).
387-define(tuple_union(T),      ?union([?none,?none,?none,?none,?none,?none,T,?none,?none,?none])).
388-define(matchstate_union(T), ?union([?none,?none,?none,?none,?none,?none,?none,T,?none,?none])).
389-define(opaque_union(T),     ?union([?none,?none,?none,?none,?none,?none,?none,?none,T,?none])).
390-define(map_union(T),        ?union([?none,?none,?none,?none,?none,?none,?none,?none,?none,T])).
391-define(integer_union(T),    ?number_union(T)).
392-define(float_union(T),      ?number_union(T)).
393-define(nil_union(T),        ?list_union(T)).
394
395
396%%=============================================================================
397%%
398%% Primitive operations such as type construction and type tests
399%%
400%%=============================================================================
401
402%%-----------------------------------------------------------------------------
403%% Top and bottom
404%%
405
406-spec t_any() -> erl_type().
407
408t_any() ->
409  ?any.
410
411-spec t_is_any(erl_type()) -> boolean().
412
413t_is_any(Type) ->
414  do_opaque(Type, 'universe', fun is_any/1).
415
416is_any(?any) -> true;
417is_any(_) -> false.
418
419-spec t_none() -> erl_type().
420
421t_none() ->
422  ?none.
423
424-spec t_is_none(erl_type()) -> boolean().
425
426t_is_none(?none) -> true;
427t_is_none(_) -> false.
428
429%%-----------------------------------------------------------------------------
430%% Opaque types
431%%
432
433-spec t_opaque(module(), atom(), [_], erl_type()) -> erl_type().
434
435t_opaque(Mod, Name, Args, Struct) ->
436  O = #opaque{mod = Mod, name = Name, args = Args, struct = Struct},
437  ?opaque(set_singleton(O)).
438
439-spec t_is_opaque(erl_type(), [erl_type()]) -> boolean().
440
441t_is_opaque(?opaque(_) = Type, Opaques) ->
442  not is_opaque_type(Type, Opaques);
443t_is_opaque(_Type, _Opaques) -> false.
444
445-spec t_is_opaque(erl_type()) -> boolean().
446
447t_is_opaque(?opaque(_)) -> true;
448t_is_opaque(_) -> false.
449
450-spec t_has_opaque_subtype(erl_type(), opaques()) -> boolean().
451
452t_has_opaque_subtype(Type, Opaques) ->
453  do_opaque(Type, Opaques, fun has_opaque_subtype/1).
454
455has_opaque_subtype(?union(Ts)) ->
456  lists:any(fun t_is_opaque/1, Ts);
457has_opaque_subtype(T) ->
458  t_is_opaque(T).
459
460-spec t_opaque_structure(erl_type()) -> erl_type().
461
462t_opaque_structure(?opaque(Elements)) ->
463  t_sup([Struct || #opaque{struct = Struct} <- ordsets:to_list(Elements)]).
464
465-spec t_contains_opaque(erl_type()) -> boolean().
466
467t_contains_opaque(Type) ->
468  t_contains_opaque(Type, []).
469
470%% Returns 'true' iff there is an opaque type that is *not* one of
471%% the types of the second argument.
472
473-spec t_contains_opaque(erl_type(), [erl_type()]) -> boolean().
474
475t_contains_opaque(?any, _Opaques) -> false;
476t_contains_opaque(?none, _Opaques) -> false;
477t_contains_opaque(?unit, _Opaques) -> false;
478t_contains_opaque(?atom(_Set), _Opaques) -> false;
479t_contains_opaque(?bitstr(_Unit, _Base), _Opaques) -> false;
480t_contains_opaque(?float, _Opaques) -> false;
481t_contains_opaque(?function(Domain, Range), Opaques) ->
482  t_contains_opaque(Domain, Opaques)
483  orelse t_contains_opaque(Range, Opaques);
484t_contains_opaque(?identifier(_Types), _Opaques) -> false;
485t_contains_opaque(?int_range(_From, _To), _Opaques) -> false;
486t_contains_opaque(?int_set(_Set), _Opaques) -> false;
487t_contains_opaque(?integer(_Types), _Opaques) -> false;
488t_contains_opaque(?list(Type, Tail, _), Opaques) ->
489  t_contains_opaque(Type, Opaques) orelse t_contains_opaque(Tail, Opaques);
490t_contains_opaque(?map(_, _, _) = Map, Opaques) ->
491  list_contains_opaque(map_all_types(Map), Opaques);
492t_contains_opaque(?matchstate(_P, _Slots), _Opaques) -> false;
493t_contains_opaque(?nil, _Opaques) -> false;
494t_contains_opaque(?number(_Set, _Tag), _Opaques) -> false;
495t_contains_opaque(?opaque(_)=T, Opaques) ->
496  not is_opaque_type(T, Opaques)
497  orelse t_contains_opaque(t_opaque_structure(T));
498t_contains_opaque(?product(Types), Opaques) ->
499  list_contains_opaque(Types, Opaques);
500t_contains_opaque(?tuple(?any, _, _), _Opaques) -> false;
501t_contains_opaque(?tuple(Types, _, _), Opaques) ->
502  list_contains_opaque(Types, Opaques);
503t_contains_opaque(?tuple_set(_Set) = T, Opaques) ->
504  list_contains_opaque(t_tuple_subtypes(T), Opaques);
505t_contains_opaque(?union(List), Opaques) ->
506  list_contains_opaque(List, Opaques);
507t_contains_opaque(?var(_Id), _Opaques) -> false.
508
509-spec list_contains_opaque([erl_type()], [erl_type()]) -> boolean().
510
511list_contains_opaque(List, Opaques) ->
512  lists:any(fun(E) -> t_contains_opaque(E, Opaques) end, List).
513
514%% t_find_opaque_mismatch/2 of two types should only be used if their
515%% t_inf is t_none() due to some opaque type violation. However,
516%% 'error' is returned if a structure mismatch is found.
517%%
518%% The first argument of the function is the pattern and its second
519%% argument the type we are matching against the pattern.
520
521-spec t_find_opaque_mismatch(erl_type(), erl_type(), [erl_type()]) ->
522                                'error' | {'ok', erl_type(), erl_type()}.
523
524t_find_opaque_mismatch(T1, T2, Opaques) ->
525  try t_find_opaque_mismatch(T1, T2, T2, Opaques)
526  catch throw:error -> error
527  end.
528
529t_find_opaque_mismatch(?any, _Type, _TopType, _Opaques) -> error;
530t_find_opaque_mismatch(?none, _Type, _TopType, _Opaques) -> throw(error);
531t_find_opaque_mismatch(?list(T1, Tl1, _), ?list(T2, Tl2, _), TopType, Opaques) ->
532  t_find_opaque_mismatch_ordlists([T1, Tl1], [T2, Tl2], TopType, Opaques);
533t_find_opaque_mismatch(T1, ?opaque(_) = T2, TopType, Opaques) ->
534  case is_opaque_type(T2, Opaques) of
535    false ->
536      case t_is_opaque(T1) andalso compatible_opaque_types(T1, T2) =/= [] of
537        true  -> error;
538        false -> {ok, TopType, T2}
539      end;
540    true ->
541      t_find_opaque_mismatch(T1, t_opaque_structure(T2), TopType, Opaques)
542  end;
543t_find_opaque_mismatch(?opaque(_) = T1, T2, TopType, Opaques) ->
544  %% The generated message is somewhat misleading:
545  case is_opaque_type(T1, Opaques) of
546    false ->
547      case t_is_opaque(T2) andalso compatible_opaque_types(T1, T2) =/= [] of
548        true  -> error;
549        false -> {ok, TopType, T1}
550      end;
551    true ->
552      t_find_opaque_mismatch(t_opaque_structure(T1), T2, TopType, Opaques)
553  end;
554t_find_opaque_mismatch(?product(T1), ?product(T2), TopType, Opaques) ->
555  t_find_opaque_mismatch_ordlists(T1, T2, TopType, Opaques);
556t_find_opaque_mismatch(?tuple(T1, Arity, _), ?tuple(T2, Arity, _),
557                       TopType, Opaques) ->
558  t_find_opaque_mismatch_ordlists(T1, T2, TopType, Opaques);
559t_find_opaque_mismatch(?tuple(_, _, _) = T1, ?tuple_set(_) = T2,
560                       TopType, Opaques) ->
561  Tuples1 = t_tuple_subtypes(T1),
562  Tuples2 = t_tuple_subtypes(T2),
563  t_find_opaque_mismatch_lists(Tuples1, Tuples2, TopType, Opaques);
564t_find_opaque_mismatch(T1, ?union(U2), TopType, Opaques) ->
565  t_find_opaque_mismatch_lists([T1], U2, TopType, Opaques);
566t_find_opaque_mismatch(T1, T2, _TopType, Opaques) ->
567  case t_is_none(t_inf(T1, T2, Opaques)) of
568    false -> error;
569    true  -> throw(error)
570  end.
571
572t_find_opaque_mismatch_ordlists(L1, L2, TopType, Opaques) ->
573  List = lists:zipwith(fun(T1, T2) ->
574			   t_find_opaque_mismatch(T1, T2, TopType, Opaques)
575		       end, L1, L2),
576  t_find_opaque_mismatch_list(List).
577
578t_find_opaque_mismatch_lists(L1, L2, _TopType, Opaques) ->
579  List = [try t_find_opaque_mismatch(T1, T2, T2, Opaques)
580          catch throw:error -> error
581          end || T1 <- L1, T2 <- L2],
582  t_find_opaque_mismatch_list(List).
583
584t_find_opaque_mismatch_list([]) -> throw(error);
585t_find_opaque_mismatch_list([H|T]) ->
586  case H of
587    {ok, _T1, _T2} -> H;
588    error -> t_find_opaque_mismatch_list(T)
589  end.
590
591-spec t_find_unknown_opaque(erl_type(), erl_type(), opaques()) ->
592                               [pos_integer()].
593
594%% The nice thing about using two types and t_inf() as compared to
595%% calling t_contains_opaque/2 is that the traversal stops when
596%% there is a mismatch which means that unknown opaque types "below"
597%% the mismatch are not found.
598t_find_unknown_opaque(_T1, _T2, 'universe') -> [];
599t_find_unknown_opaque(T1, T2, Opaques) ->
600  try t_inf(T1, T2, {match, Opaques}) of
601    _ -> []
602  catch throw:{pos, Ns} -> Ns
603  end.
604
605-spec t_decorate_with_opaque(erl_type(), erl_type(), [erl_type()]) -> erl_type().
606
607%% The first argument can contain opaque types. The second argument
608%% is assumed to be taken from the contract.
609
610t_decorate_with_opaque(T1, T2, Opaques) ->
611  case
612    Opaques =:= [] orelse t_is_equal(T1, T2) orelse not t_contains_opaque(T2)
613  of
614    true -> T1;
615    false ->
616      T = t_inf(T1, T2),
617      case t_contains_opaque(T) of
618        false -> T1;
619        true ->
620          R = decorate(T1, T, Opaques),
621          ?debug(case catch
622                        not t_is_equal(t_unopaque(R), t_unopaque(T1))
623                        orelse
624                        t_is_equal(T1, T) andalso not t_is_equal(T1, R)
625                 of
626                   false -> ok;
627                   _ ->
628                     io:format("T1 = ~p,\n", [T1]),
629                     io:format("T2 = ~p,\n", [T2]),
630                     io:format("O = ~p,\n", [Opaques]),
631                     io:format("erl_types:t_decorate_with_opaque(T1,T2,O).\n"),
632                     throw({error, "Failed to handle opaque types"})
633                 end),
634          R
635      end
636  end.
637
638decorate(Type, ?none, _Opaques) -> Type;
639decorate(?function(Domain, Range), ?function(D, R), Opaques) ->
640  ?function(decorate(Domain, D, Opaques), decorate(Range, R, Opaques));
641decorate(?list(Types, Tail, Size), ?list(Ts, Tl, _Sz), Opaques) ->
642  ?list(decorate(Types, Ts, Opaques), decorate(Tail, Tl, Opaques), Size);
643decorate(?product(Types), ?product(Ts), Opaques) ->
644  ?product(list_decorate(Types, Ts, Opaques));
645decorate(?tuple(_, _, _)=T, ?tuple(?any, _, _), _Opaques) -> T;
646decorate(?tuple(?any, _, _)=T, ?tuple(_, _, _), _Opaques) -> T;
647decorate(?tuple(Types, Arity, Tag), ?tuple(Ts, Arity, _), Opaques) ->
648  ?tuple(list_decorate(Types, Ts, Opaques), Arity, Tag);
649decorate(?tuple_set(List), ?tuple(_, Arity, _) = T, Opaques) ->
650  decorate_tuple_sets(List, [{Arity, [T]}], Opaques);
651decorate(?tuple_set(List), ?tuple_set(L), Opaques) ->
652  decorate_tuple_sets(List, L, Opaques);
653decorate(?union(List), T, Opaques) when T =/= ?any ->
654  ?union(L) = force_union(T),
655  union_decorate(List, L, Opaques);
656decorate(T, ?union(L), Opaques) when T =/= ?any ->
657  ?union(List) = force_union(T),
658  union_decorate(List, L, Opaques);
659decorate(Type, ?opaque(_)=T, Opaques) ->
660  decorate_with_opaque(Type, T, Opaques);
661decorate(Type, _T, _Opaques) -> Type.
662
663%% Note: it is important that #opaque.struct is a subtype of the
664%% opaque type.
665decorate_with_opaque(Type, ?opaque(Set2), Opaques) ->
666  case decoration(set_to_list(Set2), Type, Opaques, [], false) of
667    {[], false} -> Type;
668    {List, All} when List =/= [] ->
669      NewType = sup_opaque(List),
670      case All of
671        true -> NewType;
672        false -> t_sup(NewType, Type)
673      end
674  end.
675
676decoration([#opaque{struct = S} = Opaque|OpaqueTypes], Type, Opaques,
677           NewOpaqueTypes0, All) ->
678  IsOpaque = is_opaque_type2(Opaque, Opaques),
679  I = t_inf(Type, S),
680  case not IsOpaque orelse t_is_none(I) of
681    true -> decoration(OpaqueTypes, Type, Opaques, NewOpaqueTypes0, All);
682    false ->
683      NewI = decorate(I, S, Opaques),
684      NewOpaque = combine(NewI, [Opaque]),
685      NewAll = All orelse t_is_equal(I, Type),
686      NewOpaqueTypes = NewOpaque ++ NewOpaqueTypes0,
687      decoration(OpaqueTypes, Type, Opaques, NewOpaqueTypes, NewAll)
688  end;
689decoration([], _Type, _Opaques, NewOpaqueTypes, All) ->
690  {NewOpaqueTypes, All}.
691
692-spec list_decorate([erl_type()], [erl_type()], opaques()) -> [erl_type()].
693
694list_decorate(List, L, Opaques) ->
695  [decorate(Elem, E, Opaques) || {Elem, E} <- lists:zip(List, L)].
696
697union_decorate(U1, U2, Opaques) ->
698  Union = union_decorate(U1, U2, Opaques, 0, []),
699  [A,B,F,I,L,N,T,M,_,Map] = U1,
700  [_,_,_,_,_,_,_,_,Opaque,_] = U2,
701  List = [A,B,F,I,L,N,T,M,Map],
702  DecList = [Dec ||
703              E <- List,
704              not t_is_none(E),
705              not t_is_none(Dec = decorate(E, Opaque, Opaques))],
706  t_sup([Union|DecList]).
707
708union_decorate([?none|Left1], [_|Left2], Opaques, N, Acc) ->
709  union_decorate(Left1, Left2, Opaques, N, [?none|Acc]);
710union_decorate([T1|Left1], [?none|Left2], Opaques, N, Acc) ->
711  union_decorate(Left1, Left2, Opaques, N+1, [T1|Acc]);
712union_decorate([T1|Left1], [T2|Left2], Opaques, N, Acc) ->
713  union_decorate(Left1, Left2, Opaques, N+1, [decorate(T1, T2, Opaques)|Acc]);
714union_decorate([], [], _Opaques, N, Acc) ->
715  if N =:= 0 -> ?none;
716     N =:= 1 ->
717      [Type] = [T || T <- Acc, T =/= ?none],
718      Type;
719     N >= 2  -> ?union(lists:reverse(Acc))
720  end.
721
722decorate_tuple_sets(List, L, Opaques) ->
723  decorate_tuple_sets(List, L, Opaques, []).
724
725decorate_tuple_sets([{Arity, Tuples}|List], [{Arity, Ts}|L], Opaques, Acc) ->
726  DecTs = decorate_tuples_in_sets(Tuples, Ts, Opaques),
727  decorate_tuple_sets(List, L, Opaques, [{Arity, DecTs}|Acc]);
728decorate_tuple_sets([ArTup|List], L, Opaques, Acc) ->
729  decorate_tuple_sets(List, L, Opaques, [ArTup|Acc]);
730decorate_tuple_sets([], _L, _Opaques, Acc) ->
731  ?tuple_set(lists:reverse(Acc)).
732
733decorate_tuples_in_sets([?tuple(Elements, _, ?any)], Ts, Opaques) ->
734  NewList = [list_decorate(Elements, Es, Opaques) || ?tuple(Es, _, _) <- Ts],
735  case t_sup([t_tuple(Es) || Es <- NewList]) of
736    ?tuple_set([{_Arity, Tuples}]) -> Tuples;
737    ?tuple(_, _, _)=Tuple -> [Tuple]
738  end;
739decorate_tuples_in_sets(Tuples, Ts, Opaques) ->
740  decorate_tuples_in_sets(Tuples, Ts, Opaques, []).
741
742decorate_tuples_in_sets([?tuple(Elements, Arity, Tag1) = T1|Tuples] = L1,
743                        [?tuple(Es, Arity, Tag2)|Ts] = L2, Opaques, Acc) ->
744  if
745    Tag1 < Tag2   -> decorate_tuples_in_sets(Tuples, L2, Opaques, [T1|Acc]);
746    Tag1 > Tag2   -> decorate_tuples_in_sets(L1, Ts, Opaques, Acc);
747    Tag1 =:= Tag2 ->
748      NewElements = list_decorate(Elements, Es, Opaques),
749      NewAcc = [?tuple(NewElements, Arity, Tag1)|Acc],
750      decorate_tuples_in_sets(Tuples, Ts, Opaques, NewAcc)
751  end;
752decorate_tuples_in_sets([T1|Tuples], L2, Opaques, Acc) ->
753  decorate_tuples_in_sets(Tuples, L2, Opaques, [T1|Acc]);
754decorate_tuples_in_sets([], _L, _Opaques, Acc) ->
755  lists:reverse(Acc).
756
757-spec t_opaque_from_records(type_table()) -> [erl_type()].
758
759t_opaque_from_records(RecMap) ->
760  OpaqueRecMap =
761    maps:filter(fun(Key, _Value) ->
762		    case Key of
763		      {opaque, _Name, _Arity} -> true;
764		      _  -> false
765		    end
766		end, RecMap),
767  OpaqueTypeMap =
768    maps:map(fun({opaque, Name, _Arity},
769                 {{Module, _FileLine, _Form, ArgNames}, _Type}) ->
770                 %% Args = args_to_types(ArgNames),
771                 %% List = lists:zip(ArgNames, Args),
772                 %% TmpVarTab = maps:to_list(List),
773                 %% Rep = t_from_form(Type, RecDict, TmpVarTab),
774                 Rep = t_any(), % not used for anything right now
775                 Args = [t_any() || _ <- ArgNames],
776                 t_opaque(Module, Name, Args, Rep)
777	     end, OpaqueRecMap),
778  [OpaqueType || {_Key, OpaqueType} <- maps:to_list(OpaqueTypeMap)].
779
780%% Decompose opaque instances of type arg2 to structured types, in arg1
781%% XXX: Same as t_unopaque
782-spec t_struct_from_opaque(erl_type(), [erl_type()]) -> erl_type().
783
784t_struct_from_opaque(?function(Domain, Range), Opaques) ->
785  ?function(t_struct_from_opaque(Domain, Opaques),
786	    t_struct_from_opaque(Range, Opaques));
787t_struct_from_opaque(?list(Types, Term, Size), Opaques) ->
788  ?list(t_struct_from_opaque(Types, Opaques),
789        t_struct_from_opaque(Term, Opaques), Size);
790t_struct_from_opaque(?opaque(_) = T, Opaques) ->
791  case is_opaque_type(T, Opaques) of
792    true  -> t_opaque_structure(T);
793    false -> T
794  end;
795t_struct_from_opaque(?product(Types), Opaques) ->
796  ?product(list_struct_from_opaque(Types, Opaques));
797t_struct_from_opaque(?tuple(?any, _, _) = T, _Opaques) -> T;
798t_struct_from_opaque(?tuple(Types, Arity, Tag), Opaques) ->
799  ?tuple(list_struct_from_opaque(Types, Opaques), Arity, Tag);
800t_struct_from_opaque(?tuple_set(Set), Opaques) ->
801  NewSet = [{Sz, [t_struct_from_opaque(T, Opaques) || T <- Tuples]}
802	    || {Sz, Tuples} <- Set],
803  ?tuple_set(NewSet);
804t_struct_from_opaque(?union(List), Opaques) ->
805  t_sup(list_struct_from_opaque(List, Opaques));
806t_struct_from_opaque(Type, _Opaques) -> Type.
807
808list_struct_from_opaque(Types, Opaques) ->
809  [t_struct_from_opaque(Type, Opaques) || Type <- Types].
810
811%%-----------------------------------------------------------------------------
812%% Unit type. Signals non termination.
813%%
814
815-spec t_unit() -> erl_type().
816
817t_unit() ->
818  ?unit.
819
820-spec t_is_unit(erl_type()) -> boolean().
821
822t_is_unit(?unit) -> true;
823t_is_unit(_) -> false.
824
825-spec t_is_none_or_unit(erl_type()) -> boolean().
826
827t_is_none_or_unit(?none) -> true;
828t_is_none_or_unit(?unit) -> true;
829t_is_none_or_unit(_) -> false.
830
831%%-----------------------------------------------------------------------------
832%% Atoms and the derived type boolean
833%%
834
835-spec t_atom() -> erl_type().
836
837t_atom() ->
838  ?atom(?any).
839
840-spec t_atom(atom()) -> erl_type().
841
842t_atom(A) when is_atom(A) ->
843  ?atom(set_singleton(A)).
844
845-spec t_atoms([atom()]) -> erl_type().
846
847t_atoms(List) when is_list(List) ->
848  t_sup([t_atom(A) || A <- List]).
849
850-spec t_atom_vals(erl_type()) -> 'unknown' | [atom(),...].
851
852t_atom_vals(Type) ->
853  t_atom_vals(Type, 'universe').
854
855-spec t_atom_vals(erl_type(), opaques()) -> 'unknown' | [atom(),...].
856
857t_atom_vals(Type, Opaques) ->
858  do_opaque(Type, Opaques, fun atom_vals/1).
859
860atom_vals(?atom(?any)) -> unknown;
861atom_vals(?atom(Set)) -> set_to_list(Set);
862atom_vals(?opaque(_)) -> unknown;
863atom_vals(Other) ->
864  ?atom(_) = Atm = t_inf(t_atom(), Other),
865  atom_vals(Atm).
866
867-spec t_is_atom(erl_type()) -> boolean().
868
869t_is_atom(Type) ->
870  t_is_atom(Type, 'universe').
871
872-spec t_is_atom(erl_type(), opaques()) -> boolean().
873
874t_is_atom(Type, Opaques) ->
875  do_opaque(Type, Opaques, fun is_atom1/1).
876
877is_atom1(?atom(_)) -> true;
878is_atom1(_) -> false.
879
880-spec t_is_any_atom(atom(), erl_type()) -> boolean().
881
882t_is_any_atom(Atom, SomeAtomsType) ->
883  t_is_any_atom(Atom, SomeAtomsType, 'universe').
884
885-spec t_is_any_atom(atom(), erl_type(), opaques()) -> boolean().
886
887t_is_any_atom(Atom, SomeAtomsType, Opaques) ->
888  do_opaque(SomeAtomsType, Opaques,
889            fun(AtomsType) -> is_any_atom(Atom, AtomsType) end).
890
891is_any_atom(Atom, ?atom(?any)) when is_atom(Atom) -> false;
892is_any_atom(Atom, ?atom(Set)) when is_atom(Atom) ->
893  set_is_singleton(Atom, Set);
894is_any_atom(Atom, _) when is_atom(Atom) -> false.
895
896%%------------------------------------
897
898-spec t_is_boolean(erl_type()) -> boolean().
899
900t_is_boolean(Type) ->
901  t_is_boolean(Type, 'universe').
902
903-spec t_is_boolean(erl_type(), opaques()) -> boolean().
904
905t_is_boolean(Type, Opaques) ->
906  do_opaque(Type, Opaques, fun is_boolean/1).
907
908-spec t_boolean() -> erl_type().
909
910t_boolean() ->
911  ?atom(set_from_list([false, true])).
912
913is_boolean(?atom(?any)) -> false;
914is_boolean(?atom(Set)) ->
915  case set_size(Set) of
916    1 -> set_is_element(true, Set) orelse set_is_element(false, Set);
917    2 -> set_is_element(true, Set) andalso set_is_element(false, Set);
918    N when is_integer(N), N > 2 -> false
919  end;
920is_boolean(_) -> false.
921
922%%-----------------------------------------------------------------------------
923%% Binaries
924%%
925
926-spec t_binary() -> erl_type().
927
928t_binary() ->
929  ?bitstr(8, 0).
930
931-spec t_is_binary(erl_type()) -> boolean().
932
933t_is_binary(Type) ->
934  t_is_binary(Type, 'universe').
935
936-spec t_is_binary(erl_type(), opaques()) -> boolean().
937
938t_is_binary(Type, Opaques) ->
939    do_opaque(Type, Opaques, fun is_binary/1).
940
941is_binary(?bitstr(U, B)) ->
942  ((U rem 8) =:= 0) andalso ((B rem 8) =:= 0);
943is_binary(_) -> false.
944
945%%-----------------------------------------------------------------------------
946%% Bitstrings
947%%
948
949-spec t_bitstr() -> erl_type().
950
951t_bitstr() ->
952  ?bitstr(1, 0).
953
954-spec t_bitstr(non_neg_integer(), non_neg_integer()) -> erl_type().
955
956t_bitstr(U, B) ->
957  NewB =
958    if
959      U =:= 0 -> B;
960      B >= (U * (?UNIT_MULTIPLIER + 1)) ->
961	(B rem U) + U * ?UNIT_MULTIPLIER;
962      true ->
963	B
964    end,
965  ?bitstr(U, NewB).
966
967-spec t_bitstr_unit(erl_type()) -> non_neg_integer().
968
969t_bitstr_unit(?bitstr(U, _)) -> U.
970
971-spec t_bitstr_base(erl_type()) -> non_neg_integer().
972
973t_bitstr_base(?bitstr(_, B)) -> B.
974
975-spec t_bitstr_concat([erl_type()]) -> erl_type().
976
977t_bitstr_concat(List) ->
978  t_bitstr_concat_1(List, t_bitstr(0, 0)).
979
980t_bitstr_concat_1([T|Left], Acc) ->
981  t_bitstr_concat_1(Left, t_bitstr_concat(Acc, T));
982t_bitstr_concat_1([], Acc) ->
983  Acc.
984
985-spec t_bitstr_concat(erl_type(), erl_type()) -> erl_type().
986
987t_bitstr_concat(T1, T2) ->
988  T1p = t_inf(t_bitstr(), T1),
989  T2p = t_inf(t_bitstr(), T2),
990  bitstr_concat(t_unopaque(T1p), t_unopaque(T2p)).
991
992-spec t_bitstr_match(erl_type(), erl_type()) -> erl_type().
993
994t_bitstr_match(T1, T2) ->
995  T1p = t_inf(t_bitstr(), T1),
996  T2p = t_inf(t_bitstr(), T2),
997  bitstr_match(t_unopaque(T1p), t_unopaque(T2p)).
998
999-spec t_is_bitstr(erl_type()) -> boolean().
1000
1001t_is_bitstr(Type) ->
1002  t_is_bitstr(Type, 'universe').
1003
1004-spec t_is_bitstr(erl_type(), opaques()) -> boolean().
1005
1006t_is_bitstr(Type, Opaques) ->
1007    do_opaque(Type, Opaques, fun is_bitstr/1).
1008
1009is_bitstr(?bitstr(_, _)) -> true;
1010is_bitstr(_) -> false.
1011
1012%%-----------------------------------------------------------------------------
1013%% Matchstates
1014%%
1015
1016-spec t_matchstate() -> erl_type().
1017
1018t_matchstate() ->
1019  ?any_matchstate.
1020
1021-spec t_matchstate(erl_type(), non_neg_integer()) -> erl_type().
1022
1023t_matchstate(Init, 0) ->
1024  ?matchstate(Init, Init);
1025t_matchstate(Init, Max) when is_integer(Max) ->
1026  Slots = [Init|[?none || _ <- lists:seq(1, Max)]],
1027  ?matchstate(Init, t_product(Slots)).
1028
1029-spec t_is_matchstate(erl_type()) -> boolean().
1030
1031t_is_matchstate(?matchstate(_, _)) -> true;
1032t_is_matchstate(_) -> false.
1033
1034-spec t_matchstate_present(erl_type()) -> erl_type().
1035
1036t_matchstate_present(Type) ->
1037  case t_inf(t_matchstate(), Type) of
1038    ?matchstate(P, _) -> P;
1039    _ -> ?none
1040  end.
1041
1042-spec t_matchstate_slot(erl_type(), non_neg_integer()) -> erl_type().
1043
1044t_matchstate_slot(Type, Slot) ->
1045  RealSlot = Slot + 1,
1046  case t_inf(t_matchstate(), Type) of
1047    ?matchstate(_, ?any) -> ?any;
1048    ?matchstate(_, ?product(Vals)) when length(Vals) >= RealSlot ->
1049      lists:nth(RealSlot, Vals);
1050    ?matchstate(_, ?product(_)) ->
1051      ?none;
1052    ?matchstate(_, SlotType) when RealSlot =:= 1 ->
1053      SlotType;
1054    _ ->
1055      ?none
1056  end.
1057
1058-spec t_matchstate_slots(erl_type()) -> erl_type().
1059
1060t_matchstate_slots(?matchstate(_, Slots)) ->
1061  Slots.
1062
1063-spec t_matchstate_update_present(erl_type(), erl_type()) -> erl_type().
1064
1065t_matchstate_update_present(New, Type) ->
1066  case t_inf(t_matchstate(), Type) of
1067    ?matchstate(_, Slots) ->
1068      ?matchstate(New, Slots);
1069    _ -> ?none
1070  end.
1071
1072-spec t_matchstate_update_slot(erl_type(), erl_type(), non_neg_integer()) -> erl_type().
1073
1074t_matchstate_update_slot(New, Type, Slot) ->
1075  RealSlot = Slot + 1,
1076  case t_inf(t_matchstate(), Type) of
1077    ?matchstate(Pres, Slots) ->
1078      NewSlots =
1079	case Slots of
1080	  ?any ->
1081	    ?any;
1082	  ?product(Vals) when length(Vals) >= RealSlot ->
1083	    NewTuple = setelement(RealSlot, list_to_tuple(Vals), New),
1084	    NewVals = tuple_to_list(NewTuple),
1085	    ?product(NewVals);
1086	  ?product(_) ->
1087	    ?none;
1088	  _ when RealSlot =:= 1 ->
1089	    New;
1090	  _ ->
1091	    ?none
1092	end,
1093      ?matchstate(Pres, NewSlots);
1094    _ ->
1095      ?none
1096  end.
1097
1098%%-----------------------------------------------------------------------------
1099%% Functions
1100%%
1101
1102-spec t_fun() -> erl_type().
1103
1104t_fun() ->
1105  ?function(?any, ?any).
1106
1107-spec t_fun(erl_type()) -> erl_type().
1108
1109t_fun(Range) ->
1110  ?function(?any, Range).
1111
1112-spec t_fun([erl_type()] | arity(), erl_type()) -> erl_type().
1113
1114t_fun(Domain, Range) when is_list(Domain) ->
1115  ?function(?product(Domain), Range);
1116t_fun(Arity, Range) when is_integer(Arity), 0 =< Arity, Arity =< 255 ->
1117  ?function(?product(lists:duplicate(Arity, ?any)), Range).
1118
1119-spec t_fun_args(erl_type()) -> 'unknown' | [erl_type()].
1120
1121t_fun_args(Type) ->
1122  t_fun_args(Type, 'universe').
1123
1124-spec t_fun_args(erl_type(), opaques()) -> 'unknown' | [erl_type()].
1125
1126t_fun_args(Type, Opaques) ->
1127  do_opaque(Type, Opaques, fun fun_args/1).
1128
1129fun_args(?function(?any, _)) ->
1130  unknown;
1131fun_args(?function(?product(Domain), _)) when is_list(Domain) ->
1132  Domain.
1133
1134-spec t_fun_arity(erl_type()) -> 'unknown' | non_neg_integer().
1135
1136t_fun_arity(Type) ->
1137  t_fun_arity(Type, 'universe').
1138
1139-spec t_fun_arity(erl_type(), opaques()) -> 'unknown' | non_neg_integer().
1140
1141t_fun_arity(Type, Opaques) ->
1142  do_opaque(Type, Opaques, fun fun_arity/1).
1143
1144fun_arity(?function(?any, _)) ->
1145  unknown;
1146fun_arity(?function(?product(Domain), _)) ->
1147  length(Domain).
1148
1149-spec t_fun_range(erl_type()) -> erl_type().
1150
1151t_fun_range(Type) ->
1152  t_fun_range(Type, 'universe').
1153
1154-spec t_fun_range(erl_type(), opaques()) -> erl_type().
1155
1156t_fun_range(Type, Opaques) ->
1157  do_opaque(Type, Opaques, fun fun_range/1).
1158
1159fun_range(?function(_, Range)) ->
1160  Range.
1161
1162-spec t_is_fun(erl_type()) -> boolean().
1163
1164t_is_fun(Type) ->
1165  t_is_fun(Type, 'universe').
1166
1167-spec t_is_fun(erl_type(), opaques()) -> boolean().
1168
1169t_is_fun(Type, Opaques) ->
1170  do_opaque(Type, Opaques, fun is_fun/1).
1171
1172is_fun(?function(_, _)) -> true;
1173is_fun(_) -> false.
1174
1175%%-----------------------------------------------------------------------------
1176%% Identifiers. Includes ports, pids and refs.
1177%%
1178
1179-spec t_identifier() -> erl_type().
1180
1181t_identifier() ->
1182  ?identifier(?any).
1183
1184-spec t_is_identifier(erl_type()) -> boolean().
1185
1186t_is_identifier(?identifier(_)) -> true;
1187t_is_identifier(_) -> false.
1188
1189%%------------------------------------
1190
1191-spec t_port() -> erl_type().
1192
1193t_port() ->
1194  ?identifier(set_singleton(?port_qual)).
1195
1196-spec t_is_port(erl_type()) -> boolean().
1197
1198t_is_port(Type) ->
1199  t_is_port(Type, 'universe').
1200
1201-spec t_is_port(erl_type(), opaques()) -> boolean().
1202
1203t_is_port(Type, Opaques) ->
1204  do_opaque(Type, Opaques, fun is_port1/1).
1205
1206is_port1(?identifier(?any)) -> false;
1207is_port1(?identifier(Set)) -> set_is_singleton(?port_qual, Set);
1208is_port1(_) -> false.
1209
1210%%------------------------------------
1211
1212-spec t_pid() -> erl_type().
1213
1214t_pid() ->
1215  ?identifier(set_singleton(?pid_qual)).
1216
1217-spec t_is_pid(erl_type()) -> boolean().
1218
1219t_is_pid(Type) ->
1220  t_is_pid(Type, 'universe').
1221
1222-spec t_is_pid(erl_type(), opaques()) -> boolean().
1223
1224t_is_pid(Type, Opaques) ->
1225  do_opaque(Type, Opaques, fun is_pid1/1).
1226
1227is_pid1(?identifier(?any)) -> false;
1228is_pid1(?identifier(Set)) -> set_is_singleton(?pid_qual, Set);
1229is_pid1(_) -> false.
1230
1231%%------------------------------------
1232
1233-spec t_reference() -> erl_type().
1234
1235t_reference() ->
1236  ?identifier(set_singleton(?reference_qual)).
1237
1238-spec t_is_reference(erl_type()) -> boolean().
1239
1240t_is_reference(Type) ->
1241  t_is_reference(Type, 'universe').
1242
1243-spec t_is_reference(erl_type(), opaques()) -> boolean().
1244
1245t_is_reference(Type, Opaques) ->
1246  do_opaque(Type, Opaques, fun is_reference1/1).
1247
1248is_reference1(?identifier(?any)) -> false;
1249is_reference1(?identifier(Set)) -> set_is_singleton(?reference_qual, Set);
1250is_reference1(_) -> false.
1251
1252%%-----------------------------------------------------------------------------
1253%% Numbers are divided into floats, integers, chars and bytes.
1254%%
1255
1256-spec t_number() -> erl_type().
1257
1258t_number() ->
1259  ?number(?any, ?unknown_qual).
1260
1261-spec t_number(integer()) -> erl_type().
1262
1263t_number(X) when is_integer(X) ->
1264  t_integer(X).
1265
1266-spec t_is_number(erl_type()) -> boolean().
1267
1268t_is_number(Type) ->
1269  t_is_number(Type, 'universe').
1270
1271-spec t_is_number(erl_type(), opaques()) -> boolean().
1272
1273t_is_number(Type, Opaques) ->
1274  do_opaque(Type, Opaques, fun is_number/1).
1275
1276is_number(?number(_, _)) -> true;
1277is_number(_) -> false.
1278
1279%% Currently, the type system collapses all floats to ?float and does
1280%% not keep any information about their values. As a result, the list
1281%% that this function returns contains only integers.
1282
1283-spec t_number_vals(erl_type()) -> 'unknown' | [integer(),...].
1284
1285t_number_vals(Type) ->
1286  t_number_vals(Type, 'universe').
1287
1288-spec t_number_vals(erl_type(), opaques()) -> 'unknown' | [integer(),...].
1289
1290t_number_vals(Type, Opaques) ->
1291  do_opaque(Type, Opaques, fun number_vals/1).
1292
1293number_vals(?int_set(Set)) -> set_to_list(Set);
1294number_vals(?number(_, _)) -> unknown;
1295number_vals(?opaque(_)) -> unknown;
1296number_vals(Other) ->
1297  Inf = t_inf(Other, t_number()),
1298  false = t_is_none(Inf), % sanity check
1299  number_vals(Inf).
1300
1301%%------------------------------------
1302
1303-spec t_float() -> erl_type().
1304
1305t_float() ->
1306  ?float.
1307
1308-spec t_is_float(erl_type()) -> boolean().
1309
1310t_is_float(Type) ->
1311  t_is_float(Type, 'universe').
1312
1313-spec t_is_float(erl_type(), opaques()) -> boolean().
1314
1315t_is_float(Type, Opaques) ->
1316  do_opaque(Type, Opaques, fun is_float1/1).
1317
1318is_float1(?float) -> true;
1319is_float1(_) -> false.
1320
1321%%------------------------------------
1322
1323-spec t_integer() -> erl_type().
1324
1325t_integer() ->
1326  ?integer(?any).
1327
1328-spec t_integer(integer()) -> erl_type().
1329
1330t_integer(I) when is_integer(I) ->
1331  ?int_set(set_singleton(I)).
1332
1333-spec t_integers([integer()]) -> erl_type().
1334
1335t_integers(List) when is_list(List) ->
1336  t_sup([t_integer(I) || I <- List]).
1337
1338-spec t_is_integer(erl_type()) -> boolean().
1339
1340t_is_integer(Type) ->
1341  t_is_integer(Type, 'universe').
1342
1343-spec t_is_integer(erl_type(), opaques()) -> boolean().
1344
1345t_is_integer(Type, Opaques) ->
1346  do_opaque(Type, Opaques, fun is_integer1/1).
1347
1348is_integer1(?integer(_)) -> true;
1349is_integer1(_) -> false.
1350
1351%%------------------------------------
1352
1353-spec t_byte() -> erl_type().
1354
1355t_byte() ->
1356  ?byte.
1357
1358-spec t_is_byte(erl_type()) -> boolean().
1359
1360t_is_byte(?int_range(neg_inf, _)) -> false;
1361t_is_byte(?int_range(_, pos_inf)) -> false;
1362t_is_byte(?int_range(From, To))
1363  when is_integer(From), From >= 0, is_integer(To), To =< ?MAX_BYTE -> true;
1364t_is_byte(?int_set(Set)) ->
1365  (set_min(Set) >= 0) andalso (set_max(Set) =< ?MAX_BYTE);
1366t_is_byte(_) -> false.
1367
1368%%------------------------------------
1369
1370-spec t_char() -> erl_type().
1371
1372t_char() ->
1373  ?char.
1374
1375-spec t_is_char(erl_type()) -> boolean().
1376
1377t_is_char(?int_range(neg_inf, _)) -> false;
1378t_is_char(?int_range(_, pos_inf)) -> false;
1379t_is_char(?int_range(From, To))
1380  when is_integer(From), From >= 0, is_integer(To), To =< ?MAX_CHAR -> true;
1381t_is_char(?int_set(Set)) ->
1382  (set_min(Set) >= 0) andalso (set_max(Set) =< ?MAX_CHAR);
1383t_is_char(_) -> false.
1384
1385%%-----------------------------------------------------------------------------
1386%% Lists
1387%%
1388
1389-spec t_cons() -> erl_type().
1390
1391t_cons() ->
1392  ?nonempty_list(?any, ?any).
1393
1394%% Note that if the tail argument can be a list, we must collapse the
1395%% content of the list to include both the content of the tail list
1396%% and the head of the cons. If for example the tail argument is any()
1397%% then there can be any list in the tail and the content of the
1398%% returned list must be any().
1399
1400-spec t_cons(erl_type(), erl_type()) -> erl_type().
1401
1402t_cons(?none,  _) -> ?none;
1403t_cons(_, ?none) -> ?none;
1404t_cons(?unit, _) -> ?none;
1405t_cons(_, ?unit) -> ?none;
1406t_cons(Hd, ?nil) ->
1407  ?nonempty_list(Hd, ?nil);
1408t_cons(Hd, ?list(Contents, Termination, _)) ->
1409  ?nonempty_list(t_sup(Contents, Hd), Termination);
1410t_cons(Hd, Tail) ->
1411  case cons_tail(t_inf(Tail, t_maybe_improper_list())) of
1412    ?list(Contents, Termination, _Size) ->
1413      %% Collapse the list part of the termination but keep the
1414      %% non-list part intact.
1415      NewTermination = t_sup(t_subtract(Tail, t_maybe_improper_list()),
1416			     Termination),
1417      ?nonempty_list(t_sup(Hd, Contents), NewTermination);
1418    ?nil -> ?nonempty_list(Hd, Tail);
1419    ?none -> ?nonempty_list(Hd, Tail);
1420    ?unit -> ?none
1421  end.
1422
1423cons_tail(Type) ->
1424  do_opaque(Type, 'universe', fun(T) -> T end).
1425
1426-spec t_is_cons(erl_type()) -> boolean().
1427
1428t_is_cons(Type) ->
1429  t_is_cons(Type, 'universe').
1430
1431-spec t_is_cons(erl_type(), opaques()) -> boolean().
1432
1433t_is_cons(Type, Opaques) ->
1434  do_opaque(Type, Opaques, fun is_cons/1).
1435
1436is_cons(?nonempty_list(_, _)) -> true;
1437is_cons(_) -> false.
1438
1439-spec t_cons_hd(erl_type()) -> erl_type().
1440
1441t_cons_hd(Type) ->
1442  t_cons_hd(Type, 'universe').
1443
1444-spec t_cons_hd(erl_type(), opaques()) -> erl_type().
1445
1446t_cons_hd(Type, Opaques) ->
1447  do_opaque(Type, Opaques, fun cons_hd/1).
1448
1449cons_hd(?nonempty_list(Contents, _Termination)) -> Contents.
1450
1451-spec t_cons_tl(erl_type()) -> erl_type().
1452
1453t_cons_tl(Type) ->
1454  t_cons_tl(Type, 'universe').
1455
1456-spec t_cons_tl(erl_type(), opaques()) -> erl_type().
1457
1458t_cons_tl(Type, Opaques) ->
1459  do_opaque(Type, Opaques, fun cons_tl/1).
1460
1461cons_tl(?nonempty_list(_Contents, Termination) = T) ->
1462  t_sup(Termination, T).
1463
1464-spec t_nil() -> erl_type().
1465
1466t_nil() ->
1467  ?nil.
1468
1469-spec t_is_nil(erl_type()) -> boolean().
1470
1471t_is_nil(Type) ->
1472  t_is_nil(Type, 'universe').
1473
1474-spec t_is_nil(erl_type(), opaques()) -> boolean().
1475
1476t_is_nil(Type, Opaques) ->
1477  do_opaque(Type, Opaques, fun is_nil/1).
1478
1479is_nil(?nil) -> true;
1480is_nil(_) -> false.
1481
1482-spec t_list() -> erl_type().
1483
1484t_list() ->
1485  ?list(?any, ?nil, ?unknown_qual).
1486
1487-spec t_list(erl_type()) -> erl_type().
1488
1489t_list(?none) -> ?none;
1490t_list(?unit) -> ?none;
1491t_list(Contents) ->
1492  ?list(Contents, ?nil, ?unknown_qual).
1493
1494-spec t_list_elements(erl_type()) -> erl_type().
1495
1496t_list_elements(Type) ->
1497  t_list_elements(Type, 'universe').
1498
1499-spec t_list_elements(erl_type(), opaques()) -> erl_type().
1500
1501t_list_elements(Type, Opaques) ->
1502  do_opaque(Type, Opaques, fun list_elements/1).
1503
1504list_elements(?list(Contents, _, _)) -> Contents;
1505list_elements(?nil) -> ?none.
1506
1507-spec t_list_termination(erl_type(), opaques()) -> erl_type().
1508
1509t_list_termination(Type, Opaques) ->
1510  do_opaque(Type, Opaques, fun t_list_termination/1).
1511
1512-spec t_list_termination(erl_type()) -> erl_type().
1513
1514t_list_termination(?nil) -> ?nil;
1515t_list_termination(?list(_, Term, _)) -> Term.
1516
1517-spec t_is_list(erl_type()) -> boolean().
1518
1519t_is_list(?list(_Contents, ?nil, _)) -> true;
1520t_is_list(?nil) -> true;
1521t_is_list(_) -> false.
1522
1523-spec t_nonempty_list() -> erl_type().
1524
1525t_nonempty_list() ->
1526  t_cons(?any, ?nil).
1527
1528-spec t_nonempty_list(erl_type()) -> erl_type().
1529
1530t_nonempty_list(Type) ->
1531  t_cons(Type, ?nil).
1532
1533-spec t_nonempty_string() -> erl_type().
1534
1535t_nonempty_string() ->
1536  t_nonempty_list(t_char()).
1537
1538-spec t_string() -> erl_type().
1539
1540t_string() ->
1541  t_list(t_char()).
1542
1543-spec t_is_string(erl_type()) -> boolean().
1544
1545t_is_string(X) ->
1546  t_is_list(X) andalso t_is_char(t_list_elements(X)).
1547
1548-spec t_maybe_improper_list() -> erl_type().
1549
1550t_maybe_improper_list() ->
1551  ?list(?any, ?any, ?unknown_qual).
1552
1553%% Should only be used if you know what you are doing. See t_cons/2
1554-spec t_maybe_improper_list(erl_type(), erl_type()) -> erl_type().
1555
1556t_maybe_improper_list(_Content, ?unit) -> ?none;
1557t_maybe_improper_list(?unit, _Termination) -> ?none;
1558t_maybe_improper_list(Content, Termination) ->
1559  %% Safety check: would be nice to have but does not work with remote types
1560  %% true = t_is_subtype(t_nil(), Termination),
1561  ?list(Content, Termination, ?unknown_qual).
1562
1563-spec t_is_maybe_improper_list(erl_type()) -> boolean().
1564
1565t_is_maybe_improper_list(Type) ->
1566  t_is_maybe_improper_list(Type, 'universe').
1567
1568-spec t_is_maybe_improper_list(erl_type(), opaques()) -> boolean().
1569
1570t_is_maybe_improper_list(Type, Opaques) ->
1571  do_opaque(Type, Opaques, fun is_maybe_improper_list/1).
1572
1573is_maybe_improper_list(?list(_, _, _)) -> true;
1574is_maybe_improper_list(?nil) -> true;
1575is_maybe_improper_list(_) -> false.
1576
1577%% %% Should only be used if you know what you are doing. See t_cons/2
1578%% -spec t_improper_list(erl_type(), erl_type()) -> erl_type().
1579%%
1580%% t_improper_list(?unit, _Termination) -> ?none;
1581%% t_improper_list(_Content, ?unit) -> ?none;
1582%% t_improper_list(Content, Termination) ->
1583%%   %% Safety check: would be nice to have but does not work with remote types
1584%%   %% false = t_is_subtype(t_nil(), Termination),
1585%%   ?list(Content, Termination, ?any).
1586
1587-spec lift_list_to_pos_empty(erl_type(), opaques()) -> erl_type().
1588
1589lift_list_to_pos_empty(Type, Opaques) ->
1590  do_opaque(Type, Opaques, fun lift_list_to_pos_empty/1).
1591
1592-spec lift_list_to_pos_empty(erl_type()) -> erl_type().
1593
1594lift_list_to_pos_empty(?nil) -> ?nil;
1595lift_list_to_pos_empty(?list(Content, Termination, _)) ->
1596  ?list(Content, Termination, ?unknown_qual).
1597
1598-spec t_widen_to_number(erl_type()) -> erl_type().
1599
1600%% Widens integers and floats to t_number().
1601%% Used by erl_bif_types:key_comparison_fail().
1602
1603t_widen_to_number(?any) -> ?any;
1604t_widen_to_number(?none) -> ?none;
1605t_widen_to_number(?unit) -> ?unit;
1606t_widen_to_number(?atom(_Set) = T) -> T;
1607t_widen_to_number(?bitstr(_Unit, _Base) = T) -> T;
1608t_widen_to_number(?float) -> t_number();
1609t_widen_to_number(?function(Domain, Range)) ->
1610  ?function(t_widen_to_number(Domain), t_widen_to_number(Range));
1611t_widen_to_number(?identifier(_Types) = T) -> T;
1612t_widen_to_number(?int_range(_From, _To)) -> t_number();
1613t_widen_to_number(?int_set(_Set)) -> t_number();
1614t_widen_to_number(?integer(_Types)) -> t_number();
1615t_widen_to_number(?list(Type, Tail, Size)) ->
1616  ?list(t_widen_to_number(Type), t_widen_to_number(Tail), Size);
1617t_widen_to_number(?map(Pairs, DefK, DefV)) ->
1618  L = [{t_widen_to_number(K), MNess, t_widen_to_number(V)} ||
1619        {K, MNess, V} <- Pairs],
1620  t_map(L, t_widen_to_number(DefK), t_widen_to_number(DefV));
1621t_widen_to_number(?matchstate(_P, _Slots) = T) -> T;
1622t_widen_to_number(?nil) -> ?nil;
1623t_widen_to_number(?number(_Set, _Tag)) -> t_number();
1624t_widen_to_number(?opaque(Set)) ->
1625  L = [Opaque#opaque{struct = t_widen_to_number(S)} ||
1626        #opaque{struct = S} = Opaque <- set_to_list(Set)],
1627  ?opaque(ordsets:from_list(L));
1628t_widen_to_number(?product(Types)) ->
1629  ?product(list_widen_to_number(Types));
1630t_widen_to_number(?tuple(?any, _, _) = T) -> T;
1631t_widen_to_number(?tuple(Types, Arity, Tag)) ->
1632  ?tuple(list_widen_to_number(Types), Arity, Tag);
1633t_widen_to_number(?tuple_set(_) = Tuples) ->
1634  t_sup([t_widen_to_number(T) || T <- t_tuple_subtypes(Tuples)]);
1635t_widen_to_number(?union(List)) ->
1636  ?union(list_widen_to_number(List));
1637t_widen_to_number(?var(_Id)= T) -> T.
1638
1639list_widen_to_number(List) ->
1640  [t_widen_to_number(E) || E <- List].
1641
1642%%-----------------------------------------------------------------------------
1643%% Maps
1644%%
1645%% Representation:
1646%%  ?map(Pairs, DefaultKey, DefaultValue)
1647%%
1648%% Pairs is a sorted dictionary of types with a mandatoriness tag on each pair
1649%% (t_map_dict()). DefaultKey and DefaultValue are plain types.
1650%%
1651%% A map M belongs to this type iff
1652%%   For each pair {KT, mandatory, VT} in Pairs, there exists a pair {K, V} in M
1653%%     such that K \in KT and V \in VT.
1654%%   For each pair {KT, optional, VT} in Pairs, either there exists no key K in
1655%%     M s.t. K in KT, or there exists a pair {K, V} in M such that K \in KT and
1656%%     V \in VT.
1657%%   For each remaining pair {K, V} in M (where remaining means that there is no
1658%%     key KT in Pairs s.t. K \in KT), K \in DefaultKey and V \in DefaultValue.
1659%%
1660%% Invariants:
1661%%  * The keys in Pairs are singleton types.
1662%%  * The values of Pairs must not be unit, and may only be none if the
1663%%      mandatoriness tag  is 'optional'.
1664%%  * There is no pair {K, 'optional', V} in Pairs s.t.
1665%%      K is a subtype of DefaultKey and V is equal to DefaultValue.
1666%%  * DefaultKey must be the empty type iff DefaultValue is the empty type.
1667%%  * DefaultKey must not be a singleton type.
1668%%  * For every key K in Pairs, DefaultKey - K must not be representable; i.e.
1669%%    t_subtract(DefaultKey, K) must return DefaultKey.
1670%%  * For every pair {K, 'optional', ?none} in Pairs, K must be a subtype of
1671%%    DefaultKey.
1672%%  * Pairs must be sorted and not contain any duplicate keys.
1673%%
1674%% These invariants ensure that equal map types are represented by equal terms.
1675
1676-define(mand, mandatory).
1677-define(opt, optional).
1678
1679-type t_map_mandatoriness() :: ?mand | ?opt.
1680-type t_map_pair() :: {erl_type(), t_map_mandatoriness(), erl_type()}.
1681-type t_map_dict() :: [t_map_pair()].
1682
1683-spec t_map() -> erl_type().
1684
1685t_map() ->
1686  t_map([], t_any(), t_any()).
1687
1688-spec t_map([{erl_type(), erl_type()}]) -> erl_type().
1689
1690t_map(L) ->
1691  lists:foldl(fun t_map_put/2, t_map(), L).
1692
1693-spec t_map(t_map_dict(), erl_type(), erl_type()) -> erl_type().
1694
1695t_map(Pairs0, DefK0, DefV0) ->
1696  DefK1 = lists:foldl(fun({K,_,_},Acc)->t_subtract(Acc,K)end, DefK0, Pairs0),
1697  {DefK2, DefV1} =
1698    case t_is_none_or_unit(DefK1) orelse t_is_none_or_unit(DefV0) of
1699      true  -> {?none, ?none};
1700      false -> {DefK1, DefV0}
1701    end,
1702  {Pairs1, DefK, DefV}
1703    = case is_singleton_type(DefK2) of
1704	true  -> {mapdict_insert({DefK2, ?opt, DefV1}, Pairs0), ?none, ?none};
1705	false -> {Pairs0,                                       DefK2, DefV1}
1706      end,
1707  Pairs = normalise_map_optionals(Pairs1, DefK, DefV),
1708  %% Validate invariants of the map representation.
1709  %% Since we needed to iterate over the arguments in order to normalise anyway,
1710  %% we might as well save us some future pain and do this even without
1711  %% define(DEBUG, true).
1712  try
1713    validate_map_elements(Pairs)
1714  catch error:badarg -> error(badarg, [Pairs0,DefK0,DefV0])
1715  end,
1716  case map_pairs_are_none(Pairs) of
1717    true -> ?none;
1718    false -> ?map(Pairs, DefK, DefV)
1719  end.
1720
1721normalise_map_optionals([], _, _) -> [];
1722normalise_map_optionals([E={K,?opt,?none}|T], DefK, DefV) ->
1723  Diff = t_subtract(DefK, K),
1724  case t_is_subtype(K, DefK) andalso DefK =:= Diff of
1725    true -> [E|normalise_map_optionals(T, DefK, DefV)];
1726    false -> normalise_map_optionals(T, Diff, DefV)
1727  end;
1728normalise_map_optionals([E={K,?opt,V}|T], DefK, DefV) ->
1729  case t_is_equal(V, DefV) andalso t_is_subtype(K, DefK) of
1730    true -> normalise_map_optionals(T, DefK, DefV);
1731    false -> [E|normalise_map_optionals(T, DefK, DefV)]
1732  end;
1733normalise_map_optionals([E|T], DefK, DefV) ->
1734  [E|normalise_map_optionals(T, DefK, DefV)].
1735
1736validate_map_elements([{K1,_,_}|Rest=[{K2,_,_}|_]]) ->
1737  case is_singleton_type(K1) andalso K1 < K2 of
1738    false -> error(badarg);
1739    true -> validate_map_elements(Rest)
1740  end;
1741validate_map_elements([{K,_,_}]) ->
1742  case is_singleton_type(K) of
1743    false -> error(badarg);
1744    true -> true
1745  end;
1746validate_map_elements([]) -> true.
1747
1748map_pairs_are_none([]) -> false;
1749map_pairs_are_none([{_,?mand,?none}|_]) -> true;
1750map_pairs_are_none([_|Ps]) -> map_pairs_are_none(Ps).
1751
1752-spec t_is_map(erl_type()) -> boolean().
1753
1754t_is_map(Type) ->
1755  t_is_map(Type, 'universe').
1756
1757-spec t_is_map(erl_type(), opaques()) -> boolean().
1758
1759t_is_map(Type, Opaques) ->
1760  do_opaque(Type, Opaques, fun is_map1/1).
1761
1762is_map1(?map(_, _, _)) -> true;
1763is_map1(_) -> false.
1764
1765-spec t_map_entries(erl_type()) -> t_map_dict().
1766
1767t_map_entries(M) ->
1768  t_map_entries(M, 'universe').
1769
1770-spec t_map_entries(erl_type(), opaques()) -> t_map_dict().
1771
1772t_map_entries(M, Opaques) ->
1773  do_opaque(M, Opaques, fun map_entries/1).
1774
1775map_entries(?map(Pairs,_,_)) ->
1776  Pairs.
1777
1778-spec t_map_def_key(erl_type()) -> erl_type().
1779
1780t_map_def_key(M) ->
1781  t_map_def_key(M, 'universe').
1782
1783-spec t_map_def_key(erl_type(), opaques()) -> erl_type().
1784
1785t_map_def_key(M, Opaques) ->
1786  do_opaque(M, Opaques, fun map_def_key/1).
1787
1788map_def_key(?map(_,DefK,_)) ->
1789  DefK.
1790
1791-spec t_map_def_val(erl_type()) -> erl_type().
1792
1793t_map_def_val(M) ->
1794  t_map_def_val(M, 'universe').
1795
1796-spec t_map_def_val(erl_type(), opaques()) -> erl_type().
1797
1798t_map_def_val(M, Opaques) ->
1799  do_opaque(M, Opaques, fun map_def_val/1).
1800
1801map_def_val(?map(_,_,DefV)) ->
1802  DefV.
1803
1804-spec mapdict_store(t_map_pair(), t_map_dict()) -> t_map_dict().
1805
1806mapdict_store(E={K,_,_}, [{K,_,_}|T]) -> [E|T];
1807mapdict_store(E1={K1,_,_}, [E2={K2,_,_}|T]) when K1 > K2 ->
1808  [E2|mapdict_store(E1, T)];
1809mapdict_store(E={_,_,_}, T) -> [E|T].
1810
1811-spec mapdict_insert(t_map_pair(), t_map_dict()) -> t_map_dict().
1812
1813mapdict_insert(E={K,_,_}, D=[{K,_,_}|_]) -> error(badarg, [E, D]);
1814mapdict_insert(E1={K1,_,_}, [E2={K2,_,_}|T]) when K1 > K2 ->
1815  [E2|mapdict_insert(E1, T)];
1816mapdict_insert(E={_,_,_}, T) -> [E|T].
1817
1818-type map_pairwise_merge_fun() :: fun((erl_type(),
1819				       t_map_mandatoriness(), erl_type(),
1820				       t_map_mandatoriness(), erl_type())
1821				      -> t_map_pair() | false).
1822
1823-spec t_map_pairwise_merge(map_pairwise_merge_fun(), erl_type(), erl_type(),
1824			   opaques()) -> t_map_dict().
1825t_map_pairwise_merge(F, MapA, MapB, Opaques) ->
1826  do_opaque(MapA, Opaques,
1827	    fun(UMapA) ->
1828		do_opaque(MapB, Opaques,
1829			  fun(UMapB) ->
1830			      map_pairwise_merge(F, UMapA, UMapB)
1831			  end)
1832	    end).
1833
1834%% Merges the pairs of two maps together. Missing pairs become (?opt, DefV) or
1835%% (?opt, ?none), depending on whether K \in DefK.
1836-spec map_pairwise_merge(map_pairwise_merge_fun(), erl_type(), erl_type())
1837			-> t_map_dict().
1838map_pairwise_merge(F, ?map(APairs, ADefK, ADefV),
1839		       ?map(BPairs, BDefK, BDefV)) ->
1840  map_pairwise_merge(F, APairs, ADefK, ADefV, BPairs, BDefK, BDefV).
1841
1842map_pairwise_merge(_, [], _, _, [], _, _) -> [];
1843map_pairwise_merge(F, As0, ADefK, ADefV, Bs0, BDefK, BDefV) ->
1844  {K1, AMNess1, AV1, As1, BMNess1, BV1, Bs1} =
1845    case {As0, Bs0} of
1846      {[{K,AMNess,AV}|As], [{K, BMNess,BV}|Bs]} ->
1847	{K, AMNess, AV, As, BMNess, BV, Bs};
1848      {[{K,AMNess,AV}|As], [{BK,_,     _ }|_]=Bs} when K < BK ->
1849        {K, AMNess, AV, As, ?opt, mapmerge_otherv(K, BDefK, BDefV), Bs};
1850      {As,                 [{K, BMNess,BV}|Bs]} ->
1851        {K, ?opt, mapmerge_otherv(K, ADefK, ADefV), As, BMNess, BV, Bs};
1852      {[{K,AMNess,AV}|As], []=Bs} ->
1853        {K, AMNess, AV, As, ?opt, mapmerge_otherv(K, BDefK, BDefV), Bs}
1854    end,
1855  MK = K1, %% Rename to make clear that we are matching below
1856  case F(K1, AMNess1, AV1, BMNess1, BV1) of
1857    false ->         map_pairwise_merge(F,As1,ADefK,ADefV,Bs1,BDefK,BDefV);
1858    {MK,_,_}=M -> [M|map_pairwise_merge(F,As1,ADefK,ADefV,Bs1,BDefK,BDefV)]
1859  end.
1860
1861%% Folds over the pairs in two maps simultaneously in reverse key order. Missing
1862%% pairs become (?opt, DefV) or (?opt, ?none), depending on whether K \in DefK.
1863-spec map_pairwise_merge_foldr(fun((erl_type(),
1864				    t_map_mandatoriness(), erl_type(),
1865				    t_map_mandatoriness(), erl_type(),
1866				    Acc) -> Acc),
1867			       Acc, erl_type(), erl_type()) -> Acc.
1868
1869map_pairwise_merge_foldr(F, AccIn, ?map(APairs, ADefK, ADefV),
1870			 ?map(BPairs, BDefK, BDefV)) ->
1871  map_pairwise_merge_foldr(F, AccIn, APairs, ADefK, ADefV, BPairs, BDefK, BDefV).
1872
1873map_pairwise_merge_foldr(_, Acc,   [],  _,     _,     [],  _,     _) -> Acc;
1874map_pairwise_merge_foldr(F, AccIn, As0, ADefK, ADefV, Bs0, BDefK, BDefV) ->
1875  {K1, AMNess1, AV1, As1, BMNess1, BV1, Bs1} =
1876    case {As0, Bs0} of
1877      {[{K,AMNess,AV}|As], [{K,BMNess,BV}|Bs]} ->
1878	{K, AMNess, AV, As, BMNess, BV, Bs};
1879      {[{K,AMNess,AV}|As], [{BK,_,     _ }|_]=Bs} when K < BK ->
1880	{K, AMNess, AV, As, ?opt, mapmerge_otherv(K, BDefK, BDefV), Bs};
1881      {As,                 [{K,BMNess,BV}|Bs]} ->
1882        {K, ?opt, mapmerge_otherv(K, ADefK, ADefV), As, BMNess, BV, Bs};
1883      {[{K,AMNess,AV}|As], []=Bs} ->
1884        {K, AMNess, AV, As, ?opt, mapmerge_otherv(K, BDefK, BDefV), Bs}
1885    end,
1886  F(K1, AMNess1, AV1, BMNess1, BV1,
1887    map_pairwise_merge_foldr(F,AccIn,As1,ADefK,ADefV,Bs1,BDefK,BDefV)).
1888
1889%% By observing that a missing pair in a map is equivalent to an optional pair,
1890%% with ?none or DefV value, depending on whether K \in DefK, we can simplify
1891%% merging by denormalising the map pairs temporarily, removing all 'false'
1892%% cases, at the cost of the creation of more tuples:
1893mapmerge_otherv(K, ODefK, ODefV) ->
1894  case t_inf(K, ODefK) of
1895    ?none      -> ?none;
1896    _KOrOpaque -> ODefV
1897  end.
1898
1899-spec t_map_put({erl_type(), erl_type()}, erl_type()) -> erl_type().
1900
1901t_map_put(KV, Map) ->
1902  t_map_put(KV, Map, 'universe').
1903
1904-spec t_map_put({erl_type(), erl_type()}, erl_type(), opaques()) -> erl_type().
1905
1906t_map_put(KV, Map, Opaques) ->
1907  do_opaque(Map, Opaques, fun(UM) -> map_put(KV, UM, Opaques) end).
1908
1909%% Key and Value are *not* unopaqued, but the map is
1910map_put(_, ?none, _) -> ?none;
1911map_put(_, ?unit, _) -> ?none;
1912map_put({Key, Value}, ?map(Pairs,DefK,DefV), Opaques) ->
1913  case t_is_none_or_unit(Key) orelse t_is_none_or_unit(Value) of
1914    true -> ?none;
1915    false ->
1916      case is_singleton_type(Key) of
1917	true ->
1918	  t_map(mapdict_store({Key, ?mand, Value}, Pairs), DefK, DefV);
1919	false ->
1920	  t_map([{K, MNess, case t_is_none(t_inf(K, Key, Opaques)) of
1921			      true -> V;
1922			      false -> t_sup(V, Value)
1923			    end} || {K, MNess, V} <- Pairs],
1924		t_sup(DefK, Key),
1925		t_sup(DefV, Value))
1926      end
1927  end.
1928
1929-spec t_map_remove(erl_type(), erl_type(), opaques()) -> erl_type().
1930
1931t_map_remove(Key, Map, Opaques) ->
1932  do_opaque(Map, Opaques, fun(UM) -> map_remove(Key, UM) end).
1933
1934map_remove(_, ?none) -> ?none;
1935map_remove(_, ?unit) -> ?none;
1936map_remove(Key, Map) ->
1937  %% ?map(lists:keydelete(Key, 1, Pairs), DefK, DefV).
1938  case is_singleton_type(Key) of
1939    false -> Map;
1940    true ->
1941      ?map(Pairs,DefK,DefV) = Map,
1942      case lists:keyfind(Key, 1, Pairs) of
1943        false -> Map;
1944        {Key, _, _} ->
1945          Pairs1 = lists:keydelete(Key, 1, Pairs),
1946          t_map(Pairs1, DefK, DefV)
1947      end
1948  end.
1949
1950-spec t_map_update({erl_type(), erl_type()}, erl_type()) -> erl_type().
1951
1952t_map_update(KV, Map) ->
1953  t_map_update(KV, Map, 'universe').
1954
1955-spec t_map_update({erl_type(), erl_type()}, erl_type(), opaques()) -> erl_type().
1956
1957t_map_update(_, ?none, _) -> ?none;
1958t_map_update(_, ?unit, _) -> ?none;
1959t_map_update(KV={Key, _}, M, Opaques) ->
1960  case t_is_subtype(t_atom('true'), t_map_is_key(Key, M, Opaques)) of
1961    false -> ?none;
1962    true -> t_map_put(KV, M, Opaques)
1963  end.
1964
1965-spec t_map_get(erl_type(), erl_type()) -> erl_type().
1966
1967t_map_get(Key, Map) ->
1968  t_map_get(Key, Map, 'universe').
1969
1970-spec t_map_get(erl_type(), erl_type(), opaques()) -> erl_type().
1971
1972t_map_get(Key, Map, Opaques) ->
1973  do_opaque(Map, Opaques,
1974	    fun(UM) ->
1975		do_opaque(Key, Opaques, fun(UK) -> map_get(UK, UM) end)
1976	    end).
1977
1978map_get(_, ?none) -> ?none;
1979map_get(_, ?unit) -> ?none;
1980map_get(Key, ?map(Pairs, DefK, DefV)) ->
1981  DefRes =
1982    case t_do_overlap(DefK, Key) of
1983      false -> t_none();
1984      true -> DefV
1985    end,
1986  case is_singleton_type(Key) of
1987    false ->
1988      lists:foldl(fun({K, _, V}, Res) ->
1989		      case t_do_overlap(K, Key) of
1990			false -> Res;
1991			true -> t_sup(Res, V)
1992		      end
1993		  end, DefRes, Pairs);
1994    true ->
1995      case lists:keyfind(Key, 1, Pairs) of
1996	false -> DefRes;
1997	{_, _, ValType} -> ValType
1998      end
1999  end.
2000
2001-spec t_map_is_key(erl_type(), erl_type()) -> erl_type().
2002
2003t_map_is_key(Key, Map) ->
2004  t_map_is_key(Key, Map, 'universe').
2005
2006-spec t_map_is_key(erl_type(), erl_type(), opaques()) -> erl_type().
2007
2008t_map_is_key(Key, Map, Opaques) ->
2009  do_opaque(Map, Opaques,
2010	    fun(UM) ->
2011		do_opaque(Key, Opaques, fun(UK) -> map_is_key(UK, UM) end)
2012	    end).
2013
2014map_is_key(_, ?none) -> ?none;
2015map_is_key(_, ?unit) -> ?none;
2016map_is_key(Key, ?map(Pairs, DefK, _DefV)) ->
2017  case is_singleton_type(Key) of
2018    true ->
2019      case lists:keyfind(Key, 1, Pairs) of
2020	{Key, ?mand, _}     -> t_atom(true);
2021	{Key, ?opt,  ?none} -> t_atom(false);
2022	{Key, ?opt,  _}     -> t_boolean();
2023	false ->
2024	  case t_do_overlap(DefK, Key) of
2025	    false -> t_atom(false);
2026	    true -> t_boolean()
2027	  end
2028      end;
2029    false ->
2030      case t_do_overlap(DefK, Key)
2031	orelse lists:any(fun({_,_,?none}) -> false;
2032			    ({K,_,_}) -> t_do_overlap(K, Key)
2033			 end, Pairs)
2034      of
2035	true -> t_boolean();
2036	false -> t_atom(false)
2037      end
2038  end.
2039
2040%%-----------------------------------------------------------------------------
2041%% Tuples
2042%%
2043
2044-spec t_tuple() -> erl_type().
2045
2046t_tuple() ->
2047  ?tuple(?any, ?any, ?any).
2048
2049-spec t_tuple(non_neg_integer() | [erl_type()]) -> erl_type().
2050
2051t_tuple(N) when is_integer(N), N > ?MAX_TUPLE_SIZE  ->
2052  t_tuple();
2053t_tuple(N) when is_integer(N) ->
2054  ?tuple(lists:duplicate(N, ?any), N, ?any);
2055t_tuple(List) ->
2056  case any_none_or_unit(List) of
2057    true -> t_none();
2058    false ->
2059      Arity = length(List),
2060      case get_tuple_tags(List) of
2061	[Tag] -> ?tuple(List, Arity, Tag);  %% Tag can also be ?any here
2062	TagList ->
2063	  SortedTagList = lists:sort(TagList),
2064	  Tuples = [?tuple([T|tl(List)], Arity, T) || T <- SortedTagList],
2065	  ?tuple_set([{Arity, Tuples}])
2066      end
2067  end.
2068
2069-spec get_tuple_tags([erl_type()]) -> [erl_type(),...].
2070
2071get_tuple_tags([Tag|_]) ->
2072  do_opaque(Tag, 'universe', fun tuple_tags/1);
2073get_tuple_tags(_) -> [?any].
2074
2075tuple_tags(?atom(?any)) -> [?any];
2076tuple_tags(?atom(Set)) ->
2077  case set_size(Set) > ?TUPLE_TAG_LIMIT of
2078    true -> [?any];
2079    false -> [t_atom(A) || A <- set_to_list(Set)]
2080  end;
2081tuple_tags(_) -> [?any].
2082
2083%% to be used for a tuple with known types for its arguments (not ?any)
2084-spec t_tuple_args(erl_type()) -> [erl_type()].
2085
2086t_tuple_args(Type) ->
2087  t_tuple_args(Type, 'universe').
2088
2089%% to be used for a tuple with known types for its arguments (not ?any)
2090-spec t_tuple_args(erl_type(), opaques()) -> [erl_type()].
2091
2092t_tuple_args(Type, Opaques) ->
2093  do_opaque(Type, Opaques, fun tuple_args/1).
2094
2095tuple_args(?tuple(Args, _, _)) when is_list(Args) -> Args.
2096
2097%% to be used for a tuple with a known size (not ?any)
2098-spec t_tuple_size(erl_type()) -> non_neg_integer().
2099
2100t_tuple_size(Type) ->
2101  t_tuple_size(Type, 'universe').
2102
2103%% to be used for a tuple with a known size (not ?any)
2104-spec t_tuple_size(erl_type(), opaques()) -> non_neg_integer().
2105
2106t_tuple_size(Type, Opaques) ->
2107  do_opaque(Type, Opaques, fun tuple_size1/1).
2108
2109tuple_size1(?tuple(_, Size, _)) when is_integer(Size) -> Size.
2110
2111-spec t_tuple_sizes(erl_type()) -> 'unknown' | [non_neg_integer(),...].
2112
2113t_tuple_sizes(Type) ->
2114  do_opaque(Type, 'universe', fun tuple_sizes/1).
2115
2116tuple_sizes(?tuple(?any, ?any, ?any)) -> unknown;
2117tuple_sizes(?tuple(_, Size, _)) when is_integer(Size) -> [Size];
2118tuple_sizes(?tuple_set(List)) -> [Size || {Size, _} <- List].
2119
2120-spec t_tuple_subtypes(erl_type(), opaques()) ->
2121         'unknown' | [erl_type(),...].
2122
2123t_tuple_subtypes(Type, Opaques) ->
2124  Fun = fun(?tuple_set(List)) ->
2125            t_tuple_subtypes_tuple_list(List, Opaques);
2126           (?opaque(_)) -> unknown;
2127           (T) -> t_tuple_subtypes(T)
2128        end,
2129  do_opaque(Type, Opaques, Fun).
2130
2131t_tuple_subtypes_tuple_list(List, Opaques) ->
2132  lists:append([t_tuple_subtypes_list(Tuples, Opaques) ||
2133                 {_Size, Tuples} <- List]).
2134
2135t_tuple_subtypes_list(List, Opaques) ->
2136  ListOfLists = [t_tuple_subtypes(E, Opaques) || E <- List, E =/= ?none],
2137  lists:append([L || L <- ListOfLists, L =/= 'unknown']).
2138
2139-spec t_tuple_subtypes(erl_type()) -> 'unknown' | [erl_type(),...].
2140
2141%% XXX. Not the same as t_tuple_subtypes(T, 'universe')...
2142t_tuple_subtypes(?tuple(?any, ?any, ?any)) -> unknown;
2143t_tuple_subtypes(?tuple(_, _, _) = T) -> [T];
2144t_tuple_subtypes(?tuple_set(List)) ->
2145  lists:append([Tuples || {_Size, Tuples} <- List]).
2146
2147-spec t_is_tuple(erl_type()) -> boolean().
2148
2149t_is_tuple(Type) ->
2150  t_is_tuple(Type, 'universe').
2151
2152-spec t_is_tuple(erl_type(), opaques()) -> boolean().
2153
2154t_is_tuple(Type, Opaques) ->
2155  do_opaque(Type, Opaques, fun is_tuple1/1).
2156
2157is_tuple1(?tuple(_, _, _)) -> true;
2158is_tuple1(?tuple_set(_)) -> true;
2159is_tuple1(_) -> false.
2160
2161%%-----------------------------------------------------------------------------
2162%% Non-primitive types, including some handy syntactic sugar types
2163%%
2164
2165-spec t_bitstrlist() -> erl_type().
2166
2167t_bitstrlist() ->
2168  t_iolist(1, t_bitstr()).
2169
2170-spec t_arity() -> erl_type().
2171
2172t_arity() ->
2173  t_from_range(0, 255).	% was t_byte().
2174
2175-spec t_pos_integer() -> erl_type().
2176
2177t_pos_integer() ->
2178  t_from_range(1, pos_inf).
2179
2180-spec t_non_neg_integer() -> erl_type().
2181
2182t_non_neg_integer() ->
2183  t_from_range(0, pos_inf).
2184
2185-spec t_is_non_neg_integer(erl_type()) -> boolean().
2186
2187t_is_non_neg_integer(?integer(_) = T) ->
2188  t_is_subtype(T, t_non_neg_integer());
2189t_is_non_neg_integer(_) -> false.
2190
2191-spec t_neg_integer() -> erl_type().
2192
2193t_neg_integer() ->
2194  t_from_range(neg_inf, -1).
2195
2196-spec t_fixnum() -> erl_type().
2197
2198t_fixnum() ->
2199  t_integer(). % Gross over-approximation
2200
2201-spec t_pos_fixnum() -> erl_type().
2202
2203t_pos_fixnum() ->
2204  t_pos_integer().  % Gross over-approximation
2205
2206-spec t_non_neg_fixnum() -> erl_type().
2207
2208t_non_neg_fixnum() ->
2209  t_non_neg_integer().  % Gross over-approximation
2210
2211-spec t_mfa() -> erl_type().
2212
2213t_mfa() ->
2214  t_tuple([t_atom(), t_atom(), t_arity()]).
2215
2216-spec t_module() -> erl_type().
2217
2218t_module() ->
2219  t_atom().
2220
2221-spec t_node() -> erl_type().
2222
2223t_node() ->
2224  t_atom().
2225
2226-spec t_iodata() -> erl_type().
2227
2228t_iodata() ->
2229  t_sup(t_iolist(), t_binary()).
2230
2231-spec t_iolist() -> erl_type().
2232
2233t_iolist() ->
2234  t_iolist(1, t_binary()).
2235
2236%% Added a second argument which currently is t_binary() | t_bitstr()
2237-spec t_iolist(non_neg_integer(), erl_type()) -> erl_type().
2238
2239t_iolist(N, T) when N > 0 ->
2240  t_maybe_improper_list(t_sup([t_iolist(N-1, T), T, t_byte()]),
2241		        t_sup(T, t_nil()));
2242t_iolist(0, T) ->
2243  t_maybe_improper_list(t_any(), t_sup(T, t_nil())).
2244
2245-spec t_timeout() -> erl_type().
2246
2247t_timeout() ->
2248  t_sup(t_non_neg_integer(), t_atom('infinity')).
2249
2250%%------------------------------------
2251
2252%% ?none is allowed in products. A product of size 1 is not a product.
2253
2254-spec t_product([erl_type()]) -> erl_type().
2255
2256t_product([T]) -> T;
2257t_product(Types) when is_list(Types) ->
2258  ?product(Types).
2259
2260%% This function is intended to be the inverse of the one above.
2261%% It should NOT be used with ?any, ?none or ?unit as input argument.
2262
2263-spec t_to_tlist(erl_type()) -> [erl_type()].
2264
2265t_to_tlist(?product(Types)) -> Types;
2266t_to_tlist(T) when T =/= ?any orelse T =/= ?none orelse T =/= ?unit -> [T].
2267
2268%%------------------------------------
2269
2270-spec t_var(atom() | integer()) -> erl_type().
2271
2272t_var(Atom) when is_atom(Atom) -> ?var(Atom);
2273t_var(Int) when is_integer(Int) -> ?var(Int).
2274
2275-spec t_is_var(erl_type()) -> boolean().
2276
2277t_is_var(?var(_)) -> true;
2278t_is_var(_) -> false.
2279
2280-spec t_var_name(erl_type()) -> atom() | integer().
2281
2282t_var_name(?var(Id)) -> Id.
2283
2284-spec t_has_var(erl_type()) -> boolean().
2285
2286t_has_var(?var(_)) -> true;
2287t_has_var(?function(Domain, Range)) ->
2288  t_has_var(Domain) orelse t_has_var(Range);
2289t_has_var(?list(Contents, Termination, _)) ->
2290  t_has_var(Contents) orelse t_has_var(Termination);
2291t_has_var(?product(Types)) -> t_has_var_list(Types);
2292t_has_var(?tuple(?any, ?any, ?any)) -> false;
2293t_has_var(?tuple(Elements, _, _)) ->
2294  t_has_var_list(Elements);
2295t_has_var(?tuple_set(_) = T) ->
2296  t_has_var_list(t_tuple_subtypes(T));
2297t_has_var(?map(_, DefK, _)= Map) ->
2298  t_has_var_list(map_all_values(Map)) orelse
2299    t_has_var(DefK);
2300t_has_var(?opaque(Set)) ->
2301  %% Assume variables in 'args' are also present i 'struct'
2302  t_has_var_list([O#opaque.struct || O <- set_to_list(Set)]);
2303t_has_var(?union(List)) ->
2304  t_has_var_list(List);
2305t_has_var(_) -> false.
2306
2307-spec t_has_var_list([erl_type()]) -> boolean().
2308
2309t_has_var_list([T|Ts]) ->
2310  t_has_var(T) orelse t_has_var_list(Ts);
2311t_has_var_list([]) -> false.
2312
2313-spec t_collect_vars(erl_type()) -> [erl_type()].
2314
2315t_collect_vars(T) ->
2316  Vs = t_collect_vars(T, maps:new()),
2317  [V || {V, _} <- maps:to_list(Vs)].
2318
2319-type ctab() :: #{erl_type() => 'any'}.
2320
2321-spec t_collect_vars(erl_type(), ctab()) -> ctab().
2322
2323t_collect_vars(?var(_) = Var, Acc) ->
2324  maps:put(Var, any, Acc);
2325t_collect_vars(?function(Domain, Range), Acc) ->
2326  Acc1 = t_collect_vars(Domain, Acc),
2327  t_collect_vars(Range, Acc1);
2328t_collect_vars(?list(Contents, Termination, _), Acc) ->
2329  Acc1 = t_collect_vars(Contents, Acc),
2330  t_collect_vars(Termination, Acc1);
2331t_collect_vars(?product(Types), Acc) ->
2332  t_collect_vars_list(Types, Acc);
2333t_collect_vars(?tuple(?any, ?any, ?any), Acc) ->
2334  Acc;
2335t_collect_vars(?tuple(Types, _, _), Acc) ->
2336  t_collect_vars_list(Types, Acc);
2337t_collect_vars(?tuple_set(_) = TS, Acc) ->
2338  t_collect_vars_list(t_tuple_subtypes(TS), Acc);
2339t_collect_vars(?map(_, DefK, _) = Map, Acc0) ->
2340  Acc = t_collect_vars_list(map_all_values(Map), Acc0),
2341  t_collect_vars(DefK, Acc);
2342t_collect_vars(?opaque(Set), Acc) ->
2343  %% Assume variables in 'args' are also present i 'struct'
2344  t_collect_vars_list([O#opaque.struct || O <- set_to_list(Set)], Acc);
2345t_collect_vars(?union(List), Acc) ->
2346  t_collect_vars_list(List, Acc);
2347t_collect_vars(_, Acc) ->
2348  Acc.
2349
2350t_collect_vars_list([T|Ts], Acc0) ->
2351  Acc = t_collect_vars(T, Acc0),
2352  t_collect_vars_list(Ts, Acc);
2353t_collect_vars_list([], Acc) -> Acc.
2354
2355%%=============================================================================
2356%%
2357%% Type construction from Erlang terms.
2358%%
2359%%=============================================================================
2360
2361%%-----------------------------------------------------------------------------
2362%% Make a type from a term. No type depth is enforced.
2363%%
2364
2365-spec t_from_term(term()) -> erl_type().
2366
2367t_from_term([H|T]) ->                  t_cons(t_from_term(H), t_from_term(T));
2368t_from_term([]) ->                     t_nil();
2369t_from_term(T) when is_atom(T) ->      t_atom(T);
2370t_from_term(T) when is_bitstring(T) -> t_bitstr(0, erlang:bit_size(T));
2371t_from_term(T) when is_float(T) ->     t_float();
2372t_from_term(T) when is_function(T) ->
2373  {arity, Arity} = erlang:fun_info(T, arity),
2374  t_fun(Arity, t_any());
2375t_from_term(T) when is_integer(T) ->   t_integer(T);
2376t_from_term(T) when is_map(T) ->
2377  Pairs = [{t_from_term(K), ?mand, t_from_term(V)}
2378	   || {K, V} <- maps:to_list(T)],
2379  {Stons, Rest} = lists:partition(fun({K,_,_}) -> is_singleton_type(K) end,
2380				  Pairs),
2381  {DefK, DefV}
2382    = lists:foldl(fun({K,_,V},{AK,AV}) -> {t_sup(K,AK), t_sup(V,AV)} end,
2383		  {t_none(), t_none()}, Rest),
2384  t_map(lists:keysort(1, Stons), DefK, DefV);
2385t_from_term(T) when is_pid(T) ->       t_pid();
2386t_from_term(T) when is_port(T) ->      t_port();
2387t_from_term(T) when is_reference(T) -> t_reference();
2388t_from_term(T) when is_tuple(T) ->
2389  t_tuple([t_from_term(E) || E <- tuple_to_list(T)]).
2390
2391%%-----------------------------------------------------------------------------
2392%% Integer types from a range.
2393%%-----------------------------------------------------------------------------
2394
2395%%-define(USE_UNSAFE_RANGES, true).
2396
2397-spec t_from_range(rng_elem(), rng_elem()) -> erl_type().
2398
2399-ifdef(USE_UNSAFE_RANGES).
2400
2401t_from_range(X, Y) ->
2402  t_from_range_unsafe(X, Y).
2403
2404-else.
2405
2406t_from_range(pos_inf, pos_inf) -> ?integer_pos;
2407t_from_range(neg_inf, neg_inf) -> ?integer_neg;
2408t_from_range(neg_inf, pos_inf) -> t_integer();
2409t_from_range(neg_inf, Y) when is_integer(Y), Y < 0  -> ?integer_neg;
2410t_from_range(neg_inf, Y) when is_integer(Y), Y >= 0 -> t_integer();
2411t_from_range(X, pos_inf) when is_integer(X), X >= 1 -> ?integer_pos;
2412t_from_range(X, pos_inf) when is_integer(X), X >= 0 -> ?integer_non_neg;
2413t_from_range(X, pos_inf) when is_integer(X), X < 0  -> t_integer();
2414t_from_range(X, Y) when is_integer(X), is_integer(Y), X > Y -> t_none();
2415t_from_range(X, Y) when is_integer(X), is_integer(Y) ->
2416  case ((Y - X) < ?SET_LIMIT) of
2417    true -> t_integers(lists:seq(X, Y));
2418    false ->
2419      case X >= 0 of
2420	false ->
2421	  if Y < 0 -> ?integer_neg;
2422	     true -> t_integer()
2423	  end;
2424	true ->
2425	  if Y =< ?MAX_BYTE, X >= 1 -> ?int_range(1, ?MAX_BYTE);
2426	     Y =< ?MAX_BYTE -> t_byte();
2427	     Y =< ?MAX_CHAR, X >= 1 -> ?int_range(1, ?MAX_CHAR);
2428	     Y =< ?MAX_CHAR -> t_char();
2429	     X >= 1         -> ?integer_pos;
2430	     X >= 0         -> ?integer_non_neg
2431	  end
2432      end
2433  end;
2434t_from_range(pos_inf, neg_inf) -> t_none().
2435
2436-endif.
2437
2438-spec t_from_range_unsafe(rng_elem(), rng_elem()) -> erl_type().
2439
2440t_from_range_unsafe(pos_inf, pos_inf) -> ?integer_pos;
2441t_from_range_unsafe(neg_inf, neg_inf) -> ?integer_neg;
2442t_from_range_unsafe(neg_inf, pos_inf) -> t_integer();
2443t_from_range_unsafe(neg_inf, Y) -> ?int_range(neg_inf, Y);
2444t_from_range_unsafe(X, pos_inf) -> ?int_range(X, pos_inf);
2445t_from_range_unsafe(X, Y) when is_integer(X), is_integer(Y), X =< Y ->
2446  if (Y - X) < ?SET_LIMIT -> t_integers(lists:seq(X, Y));
2447     true -> ?int_range(X, Y)
2448  end;
2449t_from_range_unsafe(X, Y) when is_integer(X), is_integer(Y) -> t_none();
2450t_from_range_unsafe(pos_inf, neg_inf) -> t_none().
2451
2452-spec t_is_fixnum(erl_type()) -> boolean().
2453
2454t_is_fixnum(?int_range(neg_inf, _)) -> false;
2455t_is_fixnum(?int_range(_, pos_inf)) -> false;
2456t_is_fixnum(?int_range(From, To)) ->
2457  is_fixnum(From) andalso is_fixnum(To);
2458t_is_fixnum(?int_set(Set)) ->
2459  is_fixnum(set_min(Set)) andalso is_fixnum(set_max(Set));
2460t_is_fixnum(_) -> false.
2461
2462-spec is_fixnum(integer()) -> boolean().
2463
2464is_fixnum(N) when is_integer(N) ->
2465  Bits = ?BITS,
2466  (N =< ((1 bsl (Bits - 1)) - 1)) andalso (N >= -(1 bsl (Bits - 1))).
2467
2468infinity_geq(pos_inf, _) -> true;
2469infinity_geq(_, pos_inf) -> false;
2470infinity_geq(_, neg_inf) -> true;
2471infinity_geq(neg_inf, _) -> false;
2472infinity_geq(A, B) -> A >= B.
2473
2474-spec t_is_bitwidth(erl_type()) -> boolean().
2475
2476t_is_bitwidth(?int_range(neg_inf, _)) -> false;
2477t_is_bitwidth(?int_range(_, pos_inf)) -> false;
2478t_is_bitwidth(?int_range(From, To)) ->
2479  infinity_geq(From, 0) andalso infinity_geq(?BITS, To);
2480t_is_bitwidth(?int_set(Set)) ->
2481  infinity_geq(set_min(Set), 0) andalso infinity_geq(?BITS, set_max(Set));
2482t_is_bitwidth(_) -> false.
2483
2484-spec number_min(erl_type()) -> rng_elem().
2485
2486number_min(Type) ->
2487  number_min(Type, 'universe').
2488
2489-spec number_min(erl_type(), opaques()) -> rng_elem().
2490
2491number_min(Type, Opaques) ->
2492  do_opaque(Type, Opaques, fun number_min2/1).
2493
2494number_min2(?int_range(From, _)) -> From;
2495number_min2(?int_set(Set)) -> set_min(Set);
2496number_min2(?number(?any, _Tag)) -> neg_inf.
2497
2498-spec number_max(erl_type()) -> rng_elem().
2499
2500number_max(Type) ->
2501  number_max(Type, 'universe').
2502
2503-spec number_max(erl_type(), opaques()) -> rng_elem().
2504
2505number_max(Type, Opaques) ->
2506  do_opaque(Type, Opaques, fun number_max2/1).
2507
2508number_max2(?int_range(_, To)) -> To;
2509number_max2(?int_set(Set)) -> set_max(Set);
2510number_max2(?number(?any, _Tag)) -> pos_inf.
2511
2512%% -spec int_range(rgn_elem(), rng_elem()) -> erl_type().
2513%%
2514%% int_range(neg_inf, pos_inf)         -> t_integer();
2515%% int_range(neg_inf, To)              -> ?int_range(neg_inf, To);
2516%% int_range(From, pos_inf)            -> ?int_range(From, pos_inf);
2517%% int_range(From, To) when From =< To -> t_from_range(From, To);
2518%% int_range(From, To) when To < From  -> ?none.
2519
2520in_range(_, ?int_range(neg_inf, pos_inf)) -> true;
2521in_range(X, ?int_range(From, pos_inf))    -> X >= From;
2522in_range(X, ?int_range(neg_inf, To))      -> X =< To;
2523in_range(X, ?int_range(From, To))         -> (X >= From) andalso (X =< To).
2524
2525-spec min(rng_elem(), rng_elem()) -> rng_elem().
2526
2527min(neg_inf, _) -> neg_inf;
2528min(_, neg_inf) -> neg_inf;
2529min(pos_inf, Y) -> Y;
2530min(X, pos_inf) -> X;
2531min(X, Y) when X =< Y -> X;
2532min(_, Y) -> Y.
2533
2534-spec max(rng_elem(), rng_elem()) -> rng_elem().
2535
2536max(neg_inf, Y) -> Y;
2537max(X, neg_inf) -> X;
2538max(pos_inf, _) -> pos_inf;
2539max(_, pos_inf) -> pos_inf;
2540max(X, Y) when X =< Y -> Y;
2541max(X, _) -> X.
2542
2543expand_range_from_set(Range = ?int_range(From, To), Set) ->
2544  Min = min(set_min(Set), From),
2545  Max = max(set_max(Set), To),
2546  if From =:= Min, To =:= Max -> Range;
2547     true -> t_from_range(Min, Max)
2548  end.
2549
2550%%=============================================================================
2551%%
2552%% Lattice operations
2553%%
2554%%=============================================================================
2555
2556%%-----------------------------------------------------------------------------
2557%% Supremum
2558%%
2559
2560-spec t_sup([erl_type()]) -> erl_type().
2561
2562t_sup([]) -> ?none;
2563t_sup(Ts) ->
2564  case lists:any(fun is_any/1, Ts) of
2565    true -> ?any;
2566    false ->
2567      t_sup1(Ts, [])
2568  end.
2569
2570t_sup1([H1, H2|T], L) ->
2571  t_sup1(T, [t_sup(H1, H2)|L]);
2572t_sup1([T], []) -> subst_all_vars_to_any(T);
2573t_sup1(Ts, L) ->
2574  t_sup1(Ts++L, []).
2575
2576-spec t_sup(erl_type(), erl_type()) -> erl_type().
2577
2578t_sup(?any, _) -> ?any;
2579t_sup(_, ?any) -> ?any;
2580t_sup(?none, T) -> T;
2581t_sup(T, ?none) -> T;
2582t_sup(?unit, T) -> T;
2583t_sup(T, ?unit) -> T;
2584t_sup(T, T) -> subst_all_vars_to_any(T);
2585t_sup(?var(_), _) -> ?any;
2586t_sup(_, ?var(_)) -> ?any;
2587t_sup(?atom(Set1), ?atom(Set2)) ->
2588  ?atom(set_union(Set1, Set2));
2589t_sup(?bitstr(U1, B1), ?bitstr(U2, B2)) ->
2590  t_bitstr(gcd(gcd(U1, U2), abs(B1-B2)), lists:min([B1, B2]));
2591t_sup(?function(Domain1, Range1), ?function(Domain2, Range2)) ->
2592  %% The domain is either a product or any.
2593  ?function(t_sup(Domain1, Domain2), t_sup(Range1, Range2));
2594t_sup(?identifier(Set1), ?identifier(Set2)) ->
2595  ?identifier(set_union(Set1, Set2));
2596t_sup(?opaque(Set1), ?opaque(Set2)) ->
2597  sup_opaque(set_to_list(ordsets:union(Set1, Set2)));
2598%%Disallow unions with opaque types
2599%%t_sup(T1=?opaque(_,_,_), T2) ->
2600%%  io:format("Debug: t_sup executed with args ~w and ~w~n",[T1, T2]), ?none;
2601%%t_sup(T1, T2=?opaque(_,_,_)) ->
2602%%  io:format("Debug: t_sup executed with args ~w and ~w~n",[T1, T2]), ?none;
2603t_sup(?matchstate(Pres1, Slots1), ?matchstate(Pres2, Slots2)) ->
2604  ?matchstate(t_sup(Pres1, Pres2), t_sup(Slots1, Slots2));
2605t_sup(?nil, ?nil) -> ?nil;
2606t_sup(?nil, ?list(Contents, Termination, _)) ->
2607  ?list(Contents, t_sup(?nil, Termination), ?unknown_qual);
2608t_sup(?list(Contents, Termination, _), ?nil) ->
2609  ?list(Contents, t_sup(?nil, Termination), ?unknown_qual);
2610t_sup(?list(Contents1, Termination1, Size1),
2611      ?list(Contents2, Termination2, Size2)) ->
2612  NewSize =
2613    case {Size1, Size2} of
2614      {?unknown_qual, ?unknown_qual} -> ?unknown_qual;
2615      {?unknown_qual, ?nonempty_qual} -> ?unknown_qual;
2616      {?nonempty_qual, ?unknown_qual} -> ?unknown_qual;
2617      {?nonempty_qual, ?nonempty_qual} -> ?nonempty_qual
2618    end,
2619  NewContents = t_sup(Contents1, Contents2),
2620  NewTermination = t_sup(Termination1, Termination2),
2621  TmpList = t_cons(NewContents, NewTermination),
2622  case NewSize of
2623    ?nonempty_qual -> TmpList;
2624    ?unknown_qual ->
2625      ?list(FinalContents, FinalTermination, _) = TmpList,
2626      ?list(FinalContents, FinalTermination, ?unknown_qual)
2627  end;
2628t_sup(?number(_, _), ?number(?any, ?unknown_qual) = T) -> T;
2629t_sup(?number(?any, ?unknown_qual) = T, ?number(_, _)) -> T;
2630t_sup(?float, ?float) -> ?float;
2631t_sup(?float, ?integer(_)) -> t_number();
2632t_sup(?integer(_), ?float) -> t_number();
2633t_sup(?integer(?any) = T, ?integer(_)) -> T;
2634t_sup(?integer(_), ?integer(?any) = T) -> T;
2635t_sup(?int_set(Set1), ?int_set(Set2)) ->
2636  case set_union(Set1, Set2) of
2637    ?any ->
2638      t_from_range(min(set_min(Set1), set_min(Set2)),
2639		   max(set_max(Set1), set_max(Set2)));
2640    Set -> ?int_set(Set)
2641  end;
2642t_sup(?int_range(From1, To1), ?int_range(From2, To2)) ->
2643  t_from_range(min(From1, From2), max(To1, To2));
2644t_sup(Range = ?int_range(_, _), ?int_set(Set)) ->
2645  expand_range_from_set(Range, Set);
2646t_sup(?int_set(Set), Range = ?int_range(_, _)) ->
2647  expand_range_from_set(Range, Set);
2648t_sup(?product(Types1), ?product(Types2)) ->
2649  L1 = length(Types1),
2650  L2 = length(Types2),
2651  if L1 =:= L2 -> ?product(t_sup_lists(Types1, Types2));
2652     true -> ?any
2653  end;
2654t_sup(?product(_), _) ->
2655  ?any;
2656t_sup(_, ?product(_)) ->
2657  ?any;
2658t_sup(?tuple(?any, ?any, ?any) = T, ?tuple(_, _, _)) -> T;
2659t_sup(?tuple(_, _, _), ?tuple(?any, ?any, ?any) = T) -> T;
2660t_sup(?tuple(?any, ?any, ?any) = T, ?tuple_set(_)) -> T;
2661t_sup(?tuple_set(_), ?tuple(?any, ?any, ?any) = T) -> T;
2662t_sup(?tuple(Elements1, Arity, Tag1) = T1,
2663      ?tuple(Elements2, Arity, Tag2) = T2) ->
2664  if Tag1 =:= Tag2 -> t_tuple(t_sup_lists(Elements1, Elements2));
2665     Tag1 =:= ?any -> t_tuple(t_sup_lists(Elements1, Elements2));
2666     Tag2 =:= ?any -> t_tuple(t_sup_lists(Elements1, Elements2));
2667     Tag1 < Tag2 -> ?tuple_set([{Arity, [T1, T2]}]);
2668     Tag1 > Tag2 -> ?tuple_set([{Arity, [T2, T1]}])
2669  end;
2670t_sup(?tuple(_, Arity1, _) = T1, ?tuple(_, Arity2, _) = T2) ->
2671  sup_tuple_sets([{Arity1, [T1]}], [{Arity2, [T2]}]);
2672t_sup(?tuple_set(List1), ?tuple_set(List2)) ->
2673  sup_tuple_sets(List1, List2);
2674t_sup(?tuple_set(List1), T2 = ?tuple(_, Arity, _)) ->
2675  sup_tuple_sets(List1, [{Arity, [T2]}]);
2676t_sup(?tuple(_, Arity, _) = T1, ?tuple_set(List2)) ->
2677  sup_tuple_sets([{Arity, [T1]}], List2);
2678t_sup(?map(_, ADefK, ADefV) = A, ?map(_, BDefK, BDefV) = B) ->
2679  Pairs =
2680    map_pairwise_merge(
2681      fun(K, MNess, V1, MNess, V2) -> {K, MNess, t_sup(V1, V2)};
2682	 (K, _,     V1, _,     V2) -> {K, ?opt,  t_sup(V1, V2)}
2683      end, A, B),
2684  t_map(Pairs, t_sup(ADefK, BDefK), t_sup(ADefV, BDefV));
2685t_sup(T1, T2) ->
2686  ?union(U1) = force_union(T1),
2687  ?union(U2) = force_union(T2),
2688  sup_union(U1, U2).
2689
2690sup_opaque([]) -> ?none;
2691sup_opaque(List) ->
2692  L = sup_opaq(List),
2693  ?opaque(ordsets:from_list(L)).
2694
2695sup_opaq(L0) ->
2696  L1 = [{{Mod,Name,Args}, T} ||
2697         #opaque{mod = Mod, name = Name, args = Args}=T <- L0],
2698  F = family(L1),
2699  [supl(Ts) || {_, Ts} <- F].
2700
2701supl([O]) -> O;
2702supl(Ts) -> supl(Ts, t_none()).
2703
2704supl([#opaque{struct = S}=O|L], S0) ->
2705  S1 = t_sup(S, S0),
2706  case L =:= [] of
2707    true -> O#opaque{struct = S1};
2708    false -> supl(L, S1)
2709  end.
2710
2711-spec t_sup_lists([erl_type()], [erl_type()]) -> [erl_type()].
2712
2713t_sup_lists([T1|Left1], [T2|Left2]) ->
2714  [t_sup(T1, T2)|t_sup_lists(Left1, Left2)];
2715t_sup_lists([], []) ->
2716  [].
2717
2718sup_tuple_sets(L1, L2) ->
2719  TotalArities = ordsets:union([Arity || {Arity, _} <- L1],
2720			       [Arity || {Arity, _} <- L2]),
2721  if length(TotalArities) > ?TUPLE_ARITY_LIMIT -> t_tuple();
2722     true ->
2723      case sup_tuple_sets(L1, L2, []) of
2724	[{_Arity, [OneTuple = ?tuple(_, _, _)]}] -> OneTuple;
2725	List -> ?tuple_set(List)
2726      end
2727  end.
2728
2729sup_tuple_sets([{Arity, Tuples1}|Left1], [{Arity, Tuples2}|Left2], Acc) ->
2730  NewAcc = [{Arity, sup_tuples_in_set(Tuples1, Tuples2)}|Acc],
2731  sup_tuple_sets(Left1, Left2, NewAcc);
2732sup_tuple_sets([{Arity1, _} = T1|Left1] = L1,
2733	       [{Arity2, _} = T2|Left2] = L2, Acc) ->
2734  if Arity1 < Arity2 -> sup_tuple_sets(Left1, L2, [T1|Acc]);
2735     Arity1 > Arity2 -> sup_tuple_sets(L1, Left2, [T2|Acc])
2736  end;
2737sup_tuple_sets([], L2, Acc) -> lists:reverse(Acc, L2);
2738sup_tuple_sets(L1, [], Acc) -> lists:reverse(Acc, L1).
2739
2740sup_tuples_in_set([?tuple(_, _, ?any) = T], L) ->
2741  [t_tuple(sup_tuple_elements([T|L]))];
2742sup_tuples_in_set(L, [?tuple(_, _, ?any) = T]) ->
2743  [t_tuple(sup_tuple_elements([T|L]))];
2744sup_tuples_in_set(L1, L2) ->
2745  FoldFun = fun(?tuple(_, _, Tag), AccTag) -> t_sup(Tag, AccTag) end,
2746  TotalTag0 = lists:foldl(FoldFun, ?none, L1),
2747  TotalTag  = lists:foldl(FoldFun, TotalTag0, L2),
2748  case TotalTag of
2749    ?atom(?any) ->
2750      %% We will reach the set limit. Widen now.
2751      [t_tuple(sup_tuple_elements(L1 ++ L2))];
2752    ?atom(Set) ->
2753      case set_size(Set) > ?TUPLE_TAG_LIMIT of
2754	true ->
2755	  %% We will reach the set limit. Widen now.
2756	  [t_tuple(sup_tuple_elements(L1 ++ L2))];
2757	false ->
2758	  %% We can go on and build the tuple set.
2759	  sup_tuples_in_set(L1, L2, [])
2760      end
2761  end.
2762
2763sup_tuple_elements([?tuple(Elements, _, _)|L]) ->
2764  lists:foldl(fun (?tuple(Es, _, _), Acc) -> t_sup_lists(Es, Acc) end,
2765	      Elements, L).
2766
2767sup_tuples_in_set([?tuple(Elements1, Arity, Tag1) = T1|Left1] = L1,
2768		  [?tuple(Elements2, Arity, Tag2) = T2|Left2] = L2, Acc) ->
2769  if
2770    Tag1 < Tag2   -> sup_tuples_in_set(Left1, L2, [T1|Acc]);
2771    Tag1 > Tag2   -> sup_tuples_in_set(L1, Left2, [T2|Acc]);
2772    Tag2 =:= Tag2 -> NewElements = t_sup_lists(Elements1, Elements2),
2773		     NewAcc = [?tuple(NewElements, Arity, Tag1)|Acc],
2774		     sup_tuples_in_set(Left1, Left2, NewAcc)
2775  end;
2776sup_tuples_in_set([], L2, Acc) -> lists:reverse(Acc, L2);
2777sup_tuples_in_set(L1, [], Acc) -> lists:reverse(Acc, L1).
2778
2779sup_union(U1, U2) ->
2780  sup_union(U1, U2, 0, []).
2781
2782sup_union([?none|Left1], [?none|Left2], N, Acc) ->
2783  sup_union(Left1, Left2, N, [?none|Acc]);
2784sup_union([T1|Left1], [T2|Left2], N, Acc) ->
2785  sup_union(Left1, Left2, N+1, [t_sup(T1, T2)|Acc]);
2786sup_union([], [], N, Acc) ->
2787  if N =:= 0 -> ?none;
2788     N =:= 1 ->
2789      [Type] = [T || T <- Acc, T =/= ?none],
2790      Type;
2791     N =:= length(Acc) -> ?any;
2792     true -> ?union(lists:reverse(Acc))
2793  end.
2794
2795force_union(T = ?atom(_)) ->          ?atom_union(T);
2796force_union(T = ?bitstr(_, _)) ->     ?bitstr_union(T);
2797force_union(T = ?function(_, _)) ->   ?function_union(T);
2798force_union(T = ?identifier(_)) ->    ?identifier_union(T);
2799force_union(T = ?list(_, _, _)) ->    ?list_union(T);
2800force_union(T = ?nil) ->              ?list_union(T);
2801force_union(T = ?number(_, _)) ->     ?number_union(T);
2802force_union(T = ?opaque(_)) ->        ?opaque_union(T);
2803force_union(T = ?map(_,_,_)) ->       ?map_union(T);
2804force_union(T = ?tuple(_, _, _)) ->   ?tuple_union(T);
2805force_union(T = ?tuple_set(_)) ->     ?tuple_union(T);
2806force_union(T = ?matchstate(_, _)) -> ?matchstate_union(T);
2807force_union(T = ?union(_)) ->         T.
2808
2809%%-----------------------------------------------------------------------------
2810%% An attempt to write the inverse operation of t_sup/1 -- XXX: INCOMPLETE !!
2811%%
2812
2813-spec t_elements(erl_type()) -> [erl_type()].
2814
2815t_elements(?none) -> [];
2816t_elements(?unit) -> [];
2817t_elements(?any = T) -> [T];
2818t_elements(?nil = T) -> [T];
2819t_elements(?atom(?any) = T) -> [T];
2820t_elements(?atom(Atoms)) ->
2821  [t_atom(A) || A <- Atoms];
2822t_elements(?bitstr(_, _) = T) -> [T];
2823t_elements(?function(_, _) = T) -> [T];
2824t_elements(?identifier(?any) = T) -> [T];
2825t_elements(?identifier(IDs)) ->
2826  [?identifier([T]) || T <- IDs];
2827t_elements(?list(_, _, _) = T) -> [T];
2828t_elements(?number(_, _) = T) ->
2829  case T of
2830    ?number(?any, ?unknown_qual) ->
2831      [?float, ?integer(?any)];
2832    ?float -> [T];
2833    ?integer(?any) -> [T];
2834    ?int_range(_, _) -> [T];
2835    ?int_set(Set) ->
2836      [t_integer(I) || I <- Set]
2837  end;
2838t_elements(?opaque(_) = T) ->
2839  do_elements(T);
2840t_elements(?map(_,_,_) = T) -> [T];
2841t_elements(?tuple(_, _, _) = T) -> [T];
2842t_elements(?tuple_set(_) = TS) ->
2843  case t_tuple_subtypes(TS) of
2844    unknown -> [];
2845    Elems -> Elems
2846  end;
2847t_elements(?union(_) = T) ->
2848  do_elements(T);
2849t_elements(?var(_)) -> [?any].  %% yes, vars exist -- what else to do here?
2850%% t_elements(T) ->
2851%%   io:format("T_ELEMENTS => ~p\n", [T]).
2852
2853do_elements(Type0) ->
2854  case do_opaque(Type0, 'universe', fun(T) -> T end) of
2855    ?union(List) -> lists:append([t_elements(T) || T <- List]);
2856    Type -> t_elements(Type)
2857  end.
2858
2859%%-----------------------------------------------------------------------------
2860%% Infimum
2861%%
2862
2863-spec t_inf([erl_type()]) -> erl_type().
2864
2865t_inf([H1, H2|T]) ->
2866  case t_inf(H1, H2) of
2867    ?none -> ?none;
2868    NewH -> t_inf([NewH|T])
2869  end;
2870t_inf([H]) -> H;
2871t_inf([]) -> ?none.
2872
2873-spec t_inf(erl_type(), erl_type()) -> erl_type().
2874
2875t_inf(T1, T2) ->
2876  t_inf(T1, T2, 'universe').
2877
2878%% 'match' should be used from t_find_unknown_opaque() only
2879-type t_inf_opaques() :: opaques() | {'match', [erl_type() | 'universe']}.
2880
2881-spec t_inf(erl_type(), erl_type(), t_inf_opaques()) -> erl_type().
2882
2883t_inf(?var(_), ?var(_), _Opaques) -> ?any;
2884t_inf(?var(_), T, _Opaques) -> subst_all_vars_to_any(T);
2885t_inf(T, ?var(_), _Opaques) -> subst_all_vars_to_any(T);
2886t_inf(?any, T, _Opaques) -> subst_all_vars_to_any(T);
2887t_inf(T, ?any, _Opaques) -> subst_all_vars_to_any(T);
2888t_inf(?none, _, _Opaques) -> ?none;
2889t_inf(_, ?none, _Opaques) -> ?none;
2890t_inf(?unit, _, _Opaques) -> ?unit;	% ?unit cases should appear below ?none
2891t_inf(_, ?unit, _Opaques) -> ?unit;
2892t_inf(T, T, _Opaques) -> subst_all_vars_to_any(T);
2893t_inf(?atom(Set1), ?atom(Set2), _) ->
2894  case set_intersection(Set1, Set2) of
2895    ?none ->  ?none;
2896    NewSet -> ?atom(NewSet)
2897  end;
2898t_inf(?bitstr(U1, B1), ?bitstr(0, B2), _Opaques) ->
2899  if B2 >= B1 andalso (B2-B1) rem U1 =:= 0 -> t_bitstr(0, B2);
2900     true -> ?none
2901  end;
2902t_inf(?bitstr(0, B1), ?bitstr(U2, B2), _Opaques) ->
2903  if B1 >= B2 andalso (B1-B2) rem U2 =:= 0 -> t_bitstr(0, B1);
2904     true -> ?none
2905  end;
2906t_inf(?bitstr(U1, B1), ?bitstr(U1, B1), _Opaques) ->
2907  t_bitstr(U1, B1);
2908t_inf(?bitstr(U1, B1), ?bitstr(U2, B2), _Opaques) when U2 > U1 ->
2909  inf_bitstr(U2, B2, U1, B1);
2910t_inf(?bitstr(U1, B1), ?bitstr(U2, B2), _Opaques) ->
2911  inf_bitstr(U1, B1, U2, B2);
2912t_inf(?function(Domain1, Range1), ?function(Domain2, Range2), Opaques) ->
2913  case t_inf(Domain1, Domain2, Opaques) of
2914    ?none -> ?none;
2915    Domain -> ?function(Domain, t_inf(Range1, Range2, Opaques))
2916  end;
2917t_inf(?identifier(Set1), ?identifier(Set2), _Opaques) ->
2918  case set_intersection(Set1, Set2) of
2919    ?none -> ?none;
2920    Set -> ?identifier(Set)
2921  end;
2922t_inf(?map(_, ADefK, ADefV) = A, ?map(_, BDefK, BDefV) = B, _Opaques) ->
2923  %% Because it simplifies the anonymous function, we allow Pairs to temporarily
2924  %% contain mandatory pairs with none values, since all such cases should
2925  %% result in a none result.
2926  Pairs =
2927    map_pairwise_merge(
2928      %% For optional keys in both maps, when the infinimum is none, we have
2929      %% essentially concluded that K must not be a key in the map.
2930      fun(K, ?opt, V1, ?opt, V2) -> {K, ?opt, t_inf(V1, V2)};
2931	 %% When a key is optional in one map, but mandatory in another, it
2932	 %% becomes mandatory in the infinumum
2933	 (K, _, V1, _, V2) -> {K, ?mand, t_inf(V1, V2)}
2934      end, A, B),
2935  t_map(Pairs, t_inf(ADefK, BDefK), t_inf(ADefV, BDefV));
2936t_inf(?matchstate(Pres1, Slots1), ?matchstate(Pres2, Slots2), _Opaques) ->
2937  ?matchstate(t_inf(Pres1, Pres2), t_inf(Slots1, Slots2));
2938t_inf(?nil, ?nil, _Opaques) -> ?nil;
2939t_inf(?nil, ?nonempty_list(_, _), _Opaques) ->
2940  ?none;
2941t_inf(?nonempty_list(_, _), ?nil, _Opaques) ->
2942  ?none;
2943t_inf(?nil, ?list(_Contents, Termination, _), Opaques) ->
2944  t_inf(?nil, t_unopaque(Termination), Opaques);
2945t_inf(?list(_Contents, Termination, _), ?nil, Opaques) ->
2946  t_inf(?nil, t_unopaque(Termination), Opaques);
2947t_inf(?list(Contents1, Termination1, Size1),
2948      ?list(Contents2, Termination2, Size2), Opaques) ->
2949  case t_inf(Termination1, Termination2, Opaques) of
2950    ?none -> ?none;
2951    Termination ->
2952      case t_inf(Contents1, Contents2, Opaques) of
2953	?none ->
2954	  %% If none of the lists are nonempty, then the infimum is nil.
2955	  case (Size1 =:= ?unknown_qual) andalso (Size2 =:= ?unknown_qual) of
2956	    true -> t_nil();
2957	    false -> ?none
2958	  end;
2959	Contents ->
2960	  Size =
2961	    case {Size1, Size2} of
2962	      {?unknown_qual, ?unknown_qual} -> ?unknown_qual;
2963	      {?unknown_qual, ?nonempty_qual} -> ?nonempty_qual;
2964	      {?nonempty_qual, ?unknown_qual} -> ?nonempty_qual;
2965	      {?nonempty_qual, ?nonempty_qual} -> ?nonempty_qual
2966	    end,
2967	  ?list(Contents, Termination, Size)
2968      end
2969  end;
2970t_inf(?number(_, _) = T1, ?number(_, _) = T2, _Opaques) ->
2971  case {T1, T2} of
2972    {T, T}                            -> T;
2973    {_, ?number(?any, ?unknown_qual)} -> T1;
2974    {?number(?any, ?unknown_qual), _} -> T2;
2975    {?float, ?integer(_)}             -> ?none;
2976    {?integer(_), ?float}             -> ?none;
2977    {?integer(?any), ?integer(_)}     -> T2;
2978    {?integer(_), ?integer(?any)}     -> T1;
2979    {?int_set(Set1), ?int_set(Set2)}  ->
2980      case set_intersection(Set1, Set2) of
2981	?none -> ?none;
2982	Set -> ?int_set(Set)
2983      end;
2984    {?int_range(From1, To1), ?int_range(From2, To2)} ->
2985      t_from_range(max(From1, From2), min(To1, To2));
2986    {Range = ?int_range(_, _), ?int_set(Set)} ->
2987      %% io:format("t_inf range, set args ~p ~p ~n", [T1, T2]),
2988      Ans2 =
2989	case set_filter(fun(X) -> in_range(X, Range) end, Set) of
2990	  ?none -> ?none;
2991	  NewSet -> ?int_set(NewSet)
2992	end,
2993      %% io:format("Ans2 ~p ~n", [Ans2]),
2994      Ans2;
2995    {?int_set(Set), ?int_range(_, _) = Range} ->
2996      case set_filter(fun(X) -> in_range(X, Range) end, Set) of
2997	?none -> ?none;
2998	NewSet -> ?int_set(NewSet)
2999      end
3000  end;
3001t_inf(?product(Types1), ?product(Types2), Opaques) ->
3002  L1 = length(Types1),
3003  L2 = length(Types2),
3004  if L1 =:= L2 -> ?product(t_inf_lists(Types1, Types2, Opaques));
3005     true -> ?none
3006  end;
3007t_inf(?product(_), _, _Opaques) ->
3008  ?none;
3009t_inf(_, ?product(_), _Opaques) ->
3010  ?none;
3011t_inf(?tuple(?any, ?any, ?any), ?tuple(_, _, _) = T, _Opaques) ->
3012  subst_all_vars_to_any(T);
3013t_inf(?tuple(_, _, _) = T, ?tuple(?any, ?any, ?any), _Opaques) ->
3014  subst_all_vars_to_any(T);
3015t_inf(?tuple(?any, ?any, ?any), ?tuple_set(_) = T, _Opaques) ->
3016  subst_all_vars_to_any(T);
3017t_inf(?tuple_set(_) = T, ?tuple(?any, ?any, ?any), _Opaques) ->
3018  subst_all_vars_to_any(T);
3019t_inf(?tuple(Elements1, Arity, _Tag1), ?tuple(Elements2, Arity, _Tag2), Opaques) ->
3020  case t_inf_lists_strict(Elements1, Elements2, Opaques) of
3021    bottom -> ?none;
3022    NewElements -> t_tuple(NewElements)
3023  end;
3024t_inf(?tuple_set(List1), ?tuple_set(List2), Opaques) ->
3025  inf_tuple_sets(List1, List2, Opaques);
3026t_inf(?tuple_set(List), ?tuple(_, Arity, _) = T, Opaques) ->
3027  inf_tuple_sets(List, [{Arity, [T]}], Opaques);
3028t_inf(?tuple(_, Arity, _) = T, ?tuple_set(List), Opaques) ->
3029  inf_tuple_sets(List, [{Arity, [T]}], Opaques);
3030%% be careful: here and in the next clause T can be ?opaque
3031t_inf(?union(U1), T, Opaques) ->
3032  ?union(U2) = force_union(T),
3033  inf_union(U1, U2, Opaques);
3034t_inf(T, ?union(U2), Opaques) ->
3035  ?union(U1) = force_union(T),
3036  inf_union(U1, U2, Opaques);
3037t_inf(?opaque(Set1), ?opaque(Set2), Opaques) ->
3038  inf_opaque(Set1, Set2, Opaques);
3039t_inf(?opaque(_) = T1, T2, Opaques) ->
3040  inf_opaque1(T2, T1, 1, Opaques);
3041t_inf(T1, ?opaque(_) = T2, Opaques) ->
3042  inf_opaque1(T1, T2, 2, Opaques);
3043%% and as a result, the cases for ?opaque should appear *after* ?union
3044t_inf(#c{}, #c{}, _) ->
3045  ?none.
3046
3047inf_opaque1(T1, ?opaque(Set2)=T2, Pos, Opaques) ->
3048  case Opaques =:= 'universe' orelse inf_is_opaque_type(T2, Pos, Opaques) of
3049    false -> ?none;
3050    true ->
3051      List2 = set_to_list(Set2),
3052      case inf_collect(T1, List2, Opaques, []) of
3053        [] -> ?none;
3054        OpL -> ?opaque(ordsets:from_list(OpL))
3055      end
3056  end.
3057
3058inf_is_opaque_type(T, Pos, {match, Opaques}) ->
3059  is_opaque_type(T, Opaques) orelse throw({pos, [Pos]});
3060inf_is_opaque_type(T, _Pos, Opaques) ->
3061  is_opaque_type(T, Opaques).
3062
3063inf_collect(T1, [T2|List2], Opaques, OpL) ->
3064  #opaque{struct = S2} = T2,
3065  case t_inf(T1, S2, Opaques) of
3066    ?none -> inf_collect(T1, List2, Opaques, OpL);
3067    Inf ->
3068      Op = T2#opaque{struct = Inf},
3069      inf_collect(T1, List2, Opaques, [Op|OpL])
3070  end;
3071inf_collect(_T1, [], _Opaques, OpL) ->
3072  OpL.
3073
3074combine(S, T1, T2) ->
3075  case is_compat_opaque_names(T1, T2) of
3076    true ->  combine(S, [T1]);
3077    false -> combine(S, [T1, T2])
3078  end.
3079
3080combine(?opaque(Set), Ts) ->
3081  [comb2(O, T) || O <- Set, T <- Ts];
3082combine(S, Ts) ->
3083  [T#opaque{struct = S} || T <- Ts].
3084
3085comb2(O, T) ->
3086  case is_compat_opaque_names(O, T) of
3087    true -> O;
3088    false -> T#opaque{struct = ?opaque(set_singleton(O))}
3089  end.
3090
3091%% Combining two lists this way can be very time consuming...
3092%% Note: two parameterized opaque types are not the same if their
3093%% actual parameters differ
3094inf_opaque(Set1, Set2, Opaques) ->
3095  List1 = inf_look_up(Set1, Opaques),
3096  List2 = inf_look_up(Set2, Opaques),
3097  List0 = [combine(Inf, T1, T2) ||
3098            {Is1, T1} <- List1,
3099            {Is2, T2} <- List2,
3100            not t_is_none(Inf = inf_opaque_types(Is1, T1, Is2, T2, Opaques))],
3101  List = lists:append(List0),
3102  sup_opaque(List).
3103
3104%% Optimization: do just one lookup.
3105inf_look_up(Set, Opaques) ->
3106  [{Opaques =:= 'universe' orelse inf_is_opaque_type2(T, Opaques), T} ||
3107    T <- set_to_list(Set)].
3108
3109inf_is_opaque_type2(T, {match, Opaques}) ->
3110  is_opaque_type2(T, Opaques);
3111inf_is_opaque_type2(T, Opaques) ->
3112  is_opaque_type2(T, Opaques).
3113
3114inf_opaque_types(IsOpaque1, T1, IsOpaque2, T2, Opaques) ->
3115  #opaque{struct = S1}=T1,
3116  #opaque{struct = S2}=T2,
3117  case
3118    Opaques =:= 'universe' orelse is_compat_opaque_names(T1, T2)
3119  of
3120    true -> t_inf(S1, S2, Opaques);
3121    false ->
3122      case {IsOpaque1, IsOpaque2} of
3123        {true, true}  -> t_inf(S1, S2, Opaques);
3124        {true, false} -> t_inf(S1, ?opaque(set_singleton(T2)), Opaques);
3125        {false, true} -> t_inf(?opaque(set_singleton(T1)), S2, Opaques);
3126        {false, false} when element(1, Opaques) =:= match ->
3127          throw({pos, [1, 2]});
3128        {false, false} -> t_none()
3129      end
3130  end.
3131
3132compatible_opaque_types(?opaque(Es1), ?opaque(Es2)) ->
3133  [{O1, O2} || O1 <- Es1, O2 <- Es2, is_compat_opaque_names(O1, O2)].
3134
3135is_compat_opaque_names(Opaque1, Opaque2) ->
3136  #opaque{mod = Mod1, name = Name1, args = Args1} = Opaque1,
3137  #opaque{mod = Mod2, name = Name2, args = Args2} = Opaque2,
3138  case {{Mod1, Name1, Args1}, {Mod2, Name2, Args2}} of
3139    {ModNameArgs, ModNameArgs} -> true;
3140    {{Mod, Name, Args1}, {Mod, Name, Args2}} ->
3141      is_compat_args(Args1, Args2);
3142    _ -> false
3143  end.
3144
3145is_compat_args([A1|Args1], [A2|Args2]) ->
3146  is_compat_arg(A1, A2) andalso is_compat_args(Args1, Args2);
3147is_compat_args([], []) -> true;
3148is_compat_args(_, _) -> false.
3149
3150-spec is_compat_arg(erl_type(), erl_type()) -> boolean().
3151
3152%% The intention is that 'true' is to be returned iff one of the
3153%% arguments is a specialization of the other argument in the sense
3154%% that every type is a specialization of any(). For example, {_,_} is
3155%% a specialization of any(), but not of tuple(). Does not handle
3156%% variables, but any() and unions (sort of). However, the
3157%% implementation is more relaxed as any() is compatible to anything.
3158
3159is_compat_arg(T, T) -> true;
3160is_compat_arg(_, ?any) -> true;
3161is_compat_arg(?any, _) -> true;
3162is_compat_arg(?function(Domain1, Range1), ?function(Domain2, Range2)) ->
3163  (is_compat_arg(Domain1, Domain2) andalso
3164   is_compat_arg(Range1, Range2));
3165is_compat_arg(?list(Contents1, Termination1, Size1),
3166              ?list(Contents2, Termination2, Size2)) ->
3167  (Size1 =:= Size2 andalso
3168   is_compat_arg(Contents1, Contents2) andalso
3169   is_compat_arg(Termination1, Termination2));
3170is_compat_arg(?product(Types1), ?product(Types2)) ->
3171  is_compat_list(Types1, Types2);
3172is_compat_arg(?map(Pairs1, DefK1, DefV1), ?map(Pairs2, DefK2, DefV2)) ->
3173  {Ks1, _, Vs1} = lists:unzip3(Pairs1),
3174  {Ks2, _, Vs2} = lists:unzip3(Pairs2),
3175  Key1 = t_sup([DefK1 | Ks1]),
3176  Key2 = t_sup([DefK2 | Ks2]),
3177  case is_compat_arg(Key1, Key2) of
3178    true ->
3179      Value1 = t_sup([DefV1 | Vs1]),
3180      Value2 = t_sup([DefV2 | Vs2]),
3181      is_compat_arg(Value1, Value2);
3182    false ->
3183      false
3184  end;
3185is_compat_arg(?tuple(?any, ?any, ?any), ?tuple(_, _, _)) -> false;
3186is_compat_arg(?tuple(_, _, _), ?tuple(?any, ?any, ?any)) -> false;
3187is_compat_arg(?tuple(Elements1, Arity, _),
3188              ?tuple(Elements2, Arity, _)) when Arity =/= ?any ->
3189  is_compat_list(Elements1, Elements2);
3190is_compat_arg(?tuple_set([{Arity, List}]),
3191              ?tuple(Elements2, Arity, _)) when Arity =/= ?any ->
3192  is_compat_list(sup_tuple_elements(List), Elements2);
3193is_compat_arg(?tuple(Elements1, Arity, _),
3194              ?tuple_set([{Arity, List}])) when Arity =/= ?any ->
3195  is_compat_list(Elements1, sup_tuple_elements(List));
3196is_compat_arg(?tuple_set(List1), ?tuple_set(List2)) ->
3197  try
3198    is_compat_list_list([sup_tuple_elements(T) || {_Arity, T} <- List1],
3199                        [sup_tuple_elements(T) || {_Arity, T} <- List2])
3200  catch _:_ -> false
3201  end;
3202is_compat_arg(?opaque(_) = T1, T2) ->
3203  is_compat_arg(t_opaque_structure(T1), T2);
3204is_compat_arg(T1, ?opaque(_) = T2) ->
3205  is_compat_arg(T1, t_opaque_structure(T2));
3206is_compat_arg(?union(List1)=T1, ?union(List2)=T2) ->
3207  case is_compat_union2(T1, T2) of
3208    {yes, Type1, Type2} -> is_compat_arg(Type1, Type2);
3209    no -> is_compat_list(List1, List2)
3210  end;
3211is_compat_arg(?union(List), T2) ->
3212  case unify_union(List) of
3213      {yes, Type} -> is_compat_arg(Type, T2);
3214      no -> false
3215  end;
3216is_compat_arg(T1, ?union(List)) ->
3217  case unify_union(List) of
3218      {yes, Type} -> is_compat_arg(T1, Type);
3219      no -> false
3220  end;
3221is_compat_arg(?var(_), _) -> exit(error);
3222is_compat_arg(_, ?var(_)) -> exit(error);
3223is_compat_arg(?none, _) -> false;
3224is_compat_arg(_, ?none) -> false;
3225is_compat_arg(?unit, _) -> false;
3226is_compat_arg(_, ?unit) -> false;
3227is_compat_arg(#c{}, #c{}) -> false.
3228
3229is_compat_list_list(LL1, LL2) ->
3230  length(LL1) =:= length(LL2) andalso is_compat_list_list1(LL1, LL2).
3231
3232is_compat_list_list1([], []) -> true;
3233is_compat_list_list1([L1|LL1], [L2|LL2]) ->
3234  is_compat_list(L1, L2) andalso is_compat_list_list1(LL1, LL2).
3235
3236is_compat_list(L1, L2) ->
3237  length(L1) =:= length(L2) andalso is_compat_list1(L1, L2).
3238
3239is_compat_list1([], []) -> true;
3240is_compat_list1([T1|L1], [T2|L2]) ->
3241  is_compat_arg(T1, T2) andalso is_compat_list1(L1, L2).
3242
3243is_compat_union2(?union(List1)=T1, ?union(List2)=T2) ->
3244  case {unify_union(List1), unify_union(List2)} of
3245    {{yes, Type1}, {yes, Type2}} -> {yes, Type1, Type2};
3246    {{yes, Type1}, no} -> {yes, Type1, T2};
3247    {no, {yes, Type2}} -> {yes, T1, Type2};
3248    {no, no} -> no
3249  end.
3250
3251-spec t_inf_lists([erl_type()], [erl_type()]) -> [erl_type()].
3252
3253t_inf_lists(L1, L2) ->
3254  t_inf_lists(L1, L2, 'universe').
3255
3256-spec t_inf_lists([erl_type()], [erl_type()], t_inf_opaques()) -> [erl_type()].
3257
3258t_inf_lists(L1, L2, Opaques) ->
3259  t_inf_lists(L1, L2, [], Opaques).
3260
3261-spec t_inf_lists([erl_type()], [erl_type()], [erl_type()], [erl_type()]) -> [erl_type()].
3262
3263t_inf_lists([T1|Left1], [T2|Left2], Acc, Opaques) ->
3264  t_inf_lists(Left1, Left2, [t_inf(T1, T2, Opaques)|Acc], Opaques);
3265t_inf_lists([], [], Acc, _Opaques) ->
3266  lists:reverse(Acc).
3267
3268%% Infimum of lists with strictness.
3269%% If any element is the ?none type, the value 'bottom' is returned.
3270
3271-spec t_inf_lists_strict([erl_type()], [erl_type()], [erl_type()]) -> 'bottom' | [erl_type()].
3272
3273t_inf_lists_strict(L1, L2, Opaques) ->
3274  t_inf_lists_strict(L1, L2, [], Opaques).
3275
3276-spec t_inf_lists_strict([erl_type()], [erl_type()], [erl_type()], [erl_type()]) -> 'bottom' | [erl_type()].
3277
3278t_inf_lists_strict([T1|Left1], [T2|Left2], Acc, Opaques) ->
3279  case t_inf(T1, T2, Opaques) of
3280    ?none -> bottom;
3281    T -> t_inf_lists_strict(Left1, Left2, [T|Acc], Opaques)
3282  end;
3283t_inf_lists_strict([], [], Acc, _Opaques) ->
3284  lists:reverse(Acc).
3285
3286inf_tuple_sets(L1, L2, Opaques) ->
3287  case inf_tuple_sets(L1, L2, [], Opaques) of
3288    [] -> ?none;
3289    [{_Arity, [?tuple(_, _, _) = OneTuple]}] -> OneTuple;
3290    List -> ?tuple_set(List)
3291  end.
3292
3293inf_tuple_sets([{Arity, Tuples1}|Ts1], [{Arity, Tuples2}|Ts2], Acc, Opaques) ->
3294  case inf_tuples_in_sets(Tuples1, Tuples2, Opaques) of
3295    [] -> inf_tuple_sets(Ts1, Ts2, Acc, Opaques);
3296    [?tuple_set([{Arity, NewTuples}])] ->
3297      inf_tuple_sets(Ts1, Ts2, [{Arity, NewTuples}|Acc], Opaques);
3298    NewTuples -> inf_tuple_sets(Ts1, Ts2, [{Arity, NewTuples}|Acc], Opaques)
3299  end;
3300inf_tuple_sets([{Arity1, _}|Ts1] = L1, [{Arity2, _}|Ts2] = L2, Acc, Opaques) ->
3301  if Arity1 < Arity2 -> inf_tuple_sets(Ts1, L2, Acc, Opaques);
3302     Arity1 > Arity2 -> inf_tuple_sets(L1, Ts2, Acc, Opaques)
3303  end;
3304inf_tuple_sets([], _, Acc, _Opaques) -> lists:reverse(Acc);
3305inf_tuple_sets(_, [], Acc, _Opaques) -> lists:reverse(Acc).
3306
3307inf_tuples_in_sets([?tuple(Elements1, _, ?any)], L2, Opaques) ->
3308  NewList = [t_inf_lists_strict(Elements1, Elements2, Opaques)
3309	     || ?tuple(Elements2, _, _) <- L2],
3310  [t_tuple(Es) || Es <- NewList, Es =/= bottom];
3311inf_tuples_in_sets(L1, [?tuple(Elements2, _, ?any)], Opaques) ->
3312  NewList = [t_inf_lists_strict(Elements1, Elements2, Opaques)
3313	     || ?tuple(Elements1, _, _) <- L1],
3314  [t_tuple(Es) || Es <- NewList, Es =/= bottom];
3315inf_tuples_in_sets(L1, L2, Opaques) ->
3316  inf_tuples_in_sets2(L1, L2, [], Opaques).
3317
3318inf_tuples_in_sets2([?tuple(Elements1, Arity, Tag)|Ts1],
3319                    [?tuple(Elements2, Arity, Tag)|Ts2], Acc, Opaques) ->
3320  case t_inf_lists_strict(Elements1, Elements2, Opaques) of
3321    bottom -> inf_tuples_in_sets2(Ts1, Ts2, Acc, Opaques);
3322    NewElements ->
3323      inf_tuples_in_sets2(Ts1, Ts2, [?tuple(NewElements, Arity, Tag)|Acc],
3324                          Opaques)
3325  end;
3326inf_tuples_in_sets2([?tuple(_, _, Tag1)|Ts1] = L1,
3327                    [?tuple(_, _, Tag2)|Ts2] = L2, Acc, Opaques) ->
3328  if Tag1 < Tag2 -> inf_tuples_in_sets2(Ts1, L2, Acc, Opaques);
3329     Tag1 > Tag2 -> inf_tuples_in_sets2(L1, Ts2, Acc, Opaques)
3330  end;
3331inf_tuples_in_sets2([], _, Acc, _Opaques) -> lists:reverse(Acc);
3332inf_tuples_in_sets2(_, [], Acc, _Opaques) -> lists:reverse(Acc).
3333
3334inf_union(U1, U2, Opaques) ->
3335  OpaqueFun =
3336    fun(Union1, Union2, InfFun) ->
3337	[_,_,_,_,_,_,_,_,Opaque,_] = Union1,
3338        [A,B,F,I,L,N,T,M,_,Map] = Union2,
3339        List = [A,B,F,I,L,N,T,M,Map],
3340        inf_union_collect(List, Opaque, InfFun, [], [])
3341    end,
3342  {O1, ThrowList1} =
3343    OpaqueFun(U1, U2, fun(E, Opaque) -> t_inf(Opaque, E, Opaques) end),
3344  {O2, ThrowList2}
3345    = OpaqueFun(U2, U1, fun(E, Opaque) -> t_inf(E, Opaque, Opaques) end),
3346  {Union, ThrowList3} = inf_union(U1, U2, 0, [], [], Opaques),
3347  ThrowList = lists:merge3(ThrowList1, ThrowList2, ThrowList3),
3348  case t_sup([O1, O2, Union]) of
3349    ?none when ThrowList =/= [] -> throw({pos, lists:usort(ThrowList)});
3350    Sup -> Sup
3351  end.
3352
3353inf_union_collect([], _Opaque, _InfFun, InfList, ThrowList) ->
3354  {t_sup(InfList), lists:usort(ThrowList)};
3355inf_union_collect([?none|L], Opaque, InfFun, InfList, ThrowList) ->
3356  inf_union_collect(L, Opaque, InfFun, [?none|InfList], ThrowList);
3357inf_union_collect([E|L], Opaque, InfFun, InfList, ThrowList) ->
3358  try InfFun(E, Opaque)of
3359    Inf ->
3360      inf_union_collect(L, Opaque, InfFun, [Inf|InfList], ThrowList)
3361  catch throw:{pos, Ns} ->
3362      inf_union_collect(L, Opaque, InfFun, InfList, Ns ++ ThrowList)
3363  end.
3364
3365inf_union([?none|Left1], [?none|Left2], N, Acc, ThrowList, Opaques) ->
3366  inf_union(Left1, Left2, N, [?none|Acc], ThrowList, Opaques);
3367inf_union([T1|Left1], [T2|Left2], N, Acc, ThrowList, Opaques) ->
3368  try t_inf(T1, T2, Opaques) of
3369    ?none -> inf_union(Left1, Left2, N, [?none|Acc], ThrowList, Opaques);
3370    T     -> inf_union(Left1, Left2, N+1, [T|Acc], ThrowList, Opaques)
3371  catch throw:{pos, Ns} ->
3372      inf_union(Left1, Left2, N, [?none|Acc], Ns ++ ThrowList, Opaques)
3373  end;
3374inf_union([], [], N, Acc, ThrowList, _Opaques) ->
3375  if N =:= 0 -> {?none, ThrowList};
3376     N =:= 1 ->
3377      [Type] = [T || T <- Acc, T =/= ?none],
3378      {Type, ThrowList};
3379     N >= 2  -> {?union(lists:reverse(Acc)), ThrowList}
3380  end.
3381
3382inf_bitstr(U1, B1, U2, B2) ->
3383  GCD = gcd(U1, U2),
3384  case (B2-B1) rem GCD of
3385    0 ->
3386      U = (U1*U2) div GCD,
3387      B = findfirst(0, 0, U1, B1, U2, B2),
3388      t_bitstr(U, B);
3389    _ ->
3390      ?none
3391  end.
3392
3393findfirst(N1, N2, U1, B1, U2, B2) ->
3394  Val1 = U1*N1+B1,
3395  Val2 = U2*N2+B2,
3396  if Val1 =:= Val2 ->
3397      Val1;
3398     Val1 > Val2 ->
3399      findfirst(N1, N2+1, U1, B1, U2, B2);
3400     Val1 < Val2 ->
3401      findfirst(N1+1, N2, U1, B1, U2, B2)
3402  end.
3403
3404%%-----------------------------------------------------------------------------
3405%% Substitution of variables
3406%%
3407
3408-type subst_table() :: #{any() => erl_type()}.
3409
3410-spec t_subst(erl_type(), subst_table()) -> erl_type().
3411
3412t_subst(T, Map) ->
3413  case t_has_var(T) of
3414    true -> t_subst_aux(T, Map);
3415    false -> T
3416  end.
3417
3418-spec subst_all_vars_to_any(erl_type()) -> erl_type().
3419
3420subst_all_vars_to_any(T) ->
3421  t_subst(T, #{}).
3422
3423t_subst_aux(?var(Id), Map) ->
3424  case maps:find(Id, Map) of
3425    error -> ?any;
3426    {ok, Type} -> Type
3427  end;
3428t_subst_aux(?list(Contents, Termination, Size), Map) ->
3429  case t_subst_aux(Contents, Map) of
3430    ?none -> ?none;
3431    NewContents ->
3432      %% Be careful here to make the termination collapse if necessary.
3433      case t_subst_aux(Termination, Map) of
3434	?nil -> ?list(NewContents, ?nil, Size);
3435	?any -> ?list(NewContents, ?any, Size);
3436	Other ->
3437	  ?list(NewContents2, NewTermination, _) = t_cons(NewContents, Other),
3438	  ?list(NewContents2, NewTermination, Size)
3439      end
3440  end;
3441t_subst_aux(?function(Domain, Range), Map) ->
3442  ?function(t_subst_aux(Domain, Map), t_subst_aux(Range, Map));
3443t_subst_aux(?product(Types), Map) ->
3444  ?product([t_subst_aux(T, Map) || T <- Types]);
3445t_subst_aux(?tuple(?any, ?any, ?any) = T, _Map) ->
3446  T;
3447t_subst_aux(?tuple(Elements, _Arity, _Tag), Map) ->
3448  t_tuple([t_subst_aux(E, Map) || E <- Elements]);
3449t_subst_aux(?tuple_set(_) = TS, Map) ->
3450  t_sup([t_subst_aux(T, Map) || T <- t_tuple_subtypes(TS)]);
3451t_subst_aux(?map(Pairs, DefK, DefV), Map) ->
3452  t_map([{K, MNess, t_subst_aux(V, Map)} || {K, MNess, V} <- Pairs],
3453	t_subst_aux(DefK, Map), t_subst_aux(DefV, Map));
3454t_subst_aux(?opaque(Es), Map) ->
3455  List = [Opaque#opaque{args = [t_subst_aux(Arg, Map) || Arg <- Args],
3456                        struct = t_subst_aux(S, Map)} ||
3457           Opaque = #opaque{args = Args, struct = S} <- set_to_list(Es)],
3458  ?opaque(ordsets:from_list(List));
3459t_subst_aux(?union(List), Map) ->
3460  ?union([t_subst_aux(E, Map) || E <- List]);
3461t_subst_aux(T, _Map) ->
3462  T.
3463
3464%%-----------------------------------------------------------------------------
3465%% Unification
3466%%
3467
3468-type t_unify_ret() :: {erl_type(), [{_, erl_type()}]}.
3469
3470-spec t_unify(erl_type(), erl_type()) -> t_unify_ret().
3471
3472t_unify(T1, T2) ->
3473  {T, VarMap} = t_unify(T1, T2, #{}),
3474  {t_subst(T, VarMap), lists:keysort(1, maps:to_list(VarMap))}.
3475
3476t_unify(?var(Id) = T, ?var(Id), VarMap) ->
3477  {T, VarMap};
3478t_unify(?var(Id1) = T, ?var(Id2), VarMap) ->
3479  case maps:find(Id1, VarMap) of
3480    error ->
3481      case maps:find(Id2, VarMap) of
3482	error -> {T, VarMap#{Id2 => T}};
3483	{ok, Type} -> t_unify(T, Type, VarMap)
3484      end;
3485    {ok, Type1} ->
3486      case maps:find(Id2, VarMap) of
3487	error -> {Type1, VarMap#{Id2 => T}};
3488	{ok, Type2} -> t_unify(Type1, Type2, VarMap)
3489      end
3490  end;
3491t_unify(?var(Id), Type, VarMap) ->
3492  case maps:find(Id, VarMap) of
3493    error -> {Type, VarMap#{Id => Type}};
3494    {ok, VarType} -> t_unify(VarType, Type, VarMap)
3495  end;
3496t_unify(Type, ?var(Id), VarMap) ->
3497  case maps:find(Id, VarMap) of
3498    error -> {Type, VarMap#{Id => Type}};
3499    {ok, VarType} -> t_unify(VarType, Type, VarMap)
3500  end;
3501t_unify(?function(Domain1, Range1), ?function(Domain2, Range2), VarMap) ->
3502  {Domain, VarMap1} = t_unify(Domain1, Domain2, VarMap),
3503  {Range, VarMap2} = t_unify(Range1, Range2, VarMap1),
3504  {?function(Domain, Range), VarMap2};
3505t_unify(?list(Contents1, Termination1, Size),
3506	?list(Contents2, Termination2, Size), VarMap) ->
3507  {Contents, VarMap1} = t_unify(Contents1, Contents2, VarMap),
3508  {Termination, VarMap2} = t_unify(Termination1, Termination2, VarMap1),
3509  {?list(Contents, Termination, Size), VarMap2};
3510t_unify(?product(Types1), ?product(Types2), VarMap) ->
3511  {Types, VarMap1} = unify_lists(Types1, Types2, VarMap),
3512  {?product(Types), VarMap1};
3513t_unify(?tuple(?any, ?any, ?any) = T, ?tuple(?any, ?any, ?any), VarMap) ->
3514  {T, VarMap};
3515t_unify(?tuple(Elements1, Arity, _),
3516	?tuple(Elements2, Arity, _), VarMap) when Arity =/= ?any ->
3517  {NewElements, VarMap1} = unify_lists(Elements1, Elements2, VarMap),
3518  {t_tuple(NewElements), VarMap1};
3519t_unify(?tuple_set([{Arity, _}]) = T1,
3520	?tuple(_, Arity, _) = T2, VarMap) when Arity =/= ?any ->
3521  unify_tuple_set_and_tuple1(T1, T2, VarMap);
3522t_unify(?tuple(_, Arity, _) = T1,
3523	?tuple_set([{Arity, _}]) = T2, VarMap) when Arity =/= ?any ->
3524  unify_tuple_set_and_tuple2(T1, T2, VarMap);
3525t_unify(?tuple_set(List1) = T1, ?tuple_set(List2) = T2, VarMap) ->
3526  try
3527    unify_lists(lists:append([T || {_Arity, T} <- List1]),
3528                lists:append([T || {_Arity, T} <- List2]), VarMap)
3529  of
3530    {Tuples, NewVarMap} -> {t_sup(Tuples), NewVarMap}
3531  catch _:_ -> throw({mismatch, T1, T2})
3532  end;
3533t_unify(?map(_, ADefK, ADefV) = A, ?map(_, BDefK, BDefV) = B, VarMap0) ->
3534  {DefK, VarMap1} = t_unify(ADefK, BDefK, VarMap0),
3535  {DefV, VarMap2} = t_unify(ADefV, BDefV, VarMap1),
3536  {Pairs, VarMap} =
3537    map_pairwise_merge_foldr(
3538      fun(K, MNess, V1, MNess, V2, {Pairs0, VarMap3}) ->
3539	  %% We know that the keys unify and do not contain variables, or they
3540	  %% would not be singletons
3541	  %% TODO: Should V=?none (known missing keys) be handled special?
3542	  {V, VarMap4} = t_unify(V1, V2, VarMap3),
3543	  {[{K,MNess,V}|Pairs0], VarMap4};
3544	 (K, _, V1, _, V2, {Pairs0, VarMap3}) ->
3545	  %% One mandatory and one optional; what should be done in this case?
3546	  {V, VarMap4} = t_unify(V1, V2, VarMap3),
3547	  {[{K,?mand,V}|Pairs0], VarMap4}
3548      end, {[], VarMap2}, A, B),
3549  {t_map(Pairs, DefK, DefV), VarMap};
3550t_unify(?opaque(_) = T1, ?opaque(_) = T2, VarMap) ->
3551  t_unify(t_opaque_structure(T1), t_opaque_structure(T2), VarMap);
3552t_unify(T1, ?opaque(_) = T2, VarMap) ->
3553  t_unify(T1, t_opaque_structure(T2), VarMap);
3554t_unify(?opaque(_) = T1, T2, VarMap) ->
3555  t_unify(t_opaque_structure(T1), T2, VarMap);
3556t_unify(T, T, VarMap) ->
3557  {T, VarMap};
3558t_unify(?union(_)=T1, ?union(_)=T2, VarMap) ->
3559  {Type1, Type2} = unify_union2(T1, T2),
3560  t_unify(Type1, Type2, VarMap);
3561t_unify(?union(_)=T1, T2, VarMap) ->
3562  t_unify(unify_union1(T1, T1, T2), T2, VarMap);
3563t_unify(T1, ?union(_)=T2, VarMap) ->
3564  t_unify(T1, unify_union1(T2, T1, T2), VarMap);
3565t_unify(T1, T2, _) ->
3566  throw({mismatch, T1, T2}).
3567
3568unify_union2(?union(List1)=T1, ?union(List2)=T2) ->
3569  case {unify_union(List1), unify_union(List2)} of
3570    {{yes, Type1}, {yes, Type2}} -> {Type1, Type2};
3571    {{yes, Type1}, no} -> {Type1, T2};
3572    {no, {yes, Type2}} -> {T1, Type2};
3573    {no, no} -> throw({mismatch, T1, T2})
3574  end.
3575
3576unify_union1(?union(List), T1, T2) ->
3577  case unify_union(List) of
3578    {yes, Type} -> Type;
3579    no -> throw({mismatch, T1, T2})
3580  end.
3581
3582unify_union(List) ->
3583  [A,B,F,I,L,N,T,M,O,Map] = List,
3584  if O =:= ?none -> no;
3585    true ->
3586      S = t_opaque_structure(O),
3587      {yes, t_sup([A,B,F,I,L,N,T,M,S,Map])}
3588  end.
3589
3590-spec is_opaque_type(erl_type(), [erl_type()]) -> boolean().
3591
3592%% An opaque type is a union of types. Returns true iff any of the type
3593%% names (Module and Name) of the first argument (the opaque type to
3594%% check) occurs in any of the opaque types of the second argument.
3595is_opaque_type(?opaque(Elements), Opaques) ->
3596  lists:any(fun(Opaque) -> is_opaque_type2(Opaque, Opaques) end, Elements).
3597
3598is_opaque_type2(#opaque{mod = Mod1, name = Name1, args = Args1}, Opaques) ->
3599  F1 = fun(?opaque(Es)) ->
3600           F2 = fun(#opaque{mod = Mod, name = Name, args = Args}) ->
3601                    is_type_name(Mod1, Name1, Args1, Mod, Name, Args)
3602                end,
3603           lists:any(F2, Es)
3604       end,
3605  lists:any(F1, Opaques).
3606
3607is_type_name(Mod, Name, Args1, Mod, Name, Args2) ->
3608  length(Args1) =:= length(Args2);
3609is_type_name(_Mod1, _Name1, _Args1, _Mod2, _Name2, _Args2) ->
3610  false.
3611
3612%% Two functions since t_unify is not symmetric.
3613unify_tuple_set_and_tuple1(?tuple_set([{Arity, List}]),
3614                           ?tuple(Elements2, Arity, _), VarMap) ->
3615  %% Can only work if the single tuple has variables at correct places.
3616  %% Collapse the tuple set.
3617  {NewElements, VarMap1} =
3618    unify_lists(sup_tuple_elements(List), Elements2, VarMap),
3619  {t_tuple(NewElements), VarMap1}.
3620
3621unify_tuple_set_and_tuple2(?tuple(Elements2, Arity, _),
3622                           ?tuple_set([{Arity, List}]), VarMap) ->
3623  %% Can only work if the single tuple has variables at correct places.
3624  %% Collapse the tuple set.
3625  {NewElements, VarMap1} =
3626    unify_lists(Elements2, sup_tuple_elements(List), VarMap),
3627  {t_tuple(NewElements), VarMap1}.
3628
3629unify_lists(L1, L2, VarMap) ->
3630  unify_lists(L1, L2, VarMap, []).
3631
3632unify_lists([T1|Left1], [T2|Left2], VarMap, Acc) ->
3633  {NewT, NewVarMap} = t_unify(T1, T2, VarMap),
3634  unify_lists(Left1, Left2, NewVarMap, [NewT|Acc]);
3635unify_lists([], [], VarMap, Acc) ->
3636  {lists:reverse(Acc), VarMap}.
3637
3638%%t_assign_variables_to_subtype(T1, T2) ->
3639%%  try
3640%%    Dict = assign_vars(T1, T2, dict:new()),
3641%%    {ok, dict:map(fun(_Param, List) -> t_sup(List) end, Dict)}
3642%%  catch
3643%%    throw:error -> error
3644%%  end.
3645
3646%%assign_vars(_, ?var(_), _Dict) ->
3647%%  erlang:error("Variable in right hand side of assignment");
3648%%assign_vars(?any, _, Dict) ->
3649%%  Dict;
3650%%assign_vars(?var(_) = Var, Type, Dict) ->
3651%%  store_var(Var, Type, Dict);
3652%%assign_vars(?function(Domain1, Range1), ?function(Domain2, Range2), Dict) ->
3653%%  DomainList =
3654%%    case Domain2 of
3655%%      ?any -> [];
3656%%      ?product(List) -> List
3657%%    end,
3658%%  case any_none([Range2|DomainList]) of
3659%%    true -> throw(error);
3660%%    false ->
3661%%      Dict1 = assign_vars(Domain1, Domain2, Dict),
3662%%      assign_vars(Range1, Range2, Dict1)
3663%%  end;
3664%%assign_vars(?list(_Contents, _Termination, ?any), ?nil, Dict) ->
3665%%  Dict;
3666%%assign_vars(?list(Contents1, Termination1, Size1),
3667%%	    ?list(Contents2, Termination2, Size2), Dict) ->
3668%%  Dict1 = assign_vars(Contents1, Contents2, Dict),
3669%%  Dict2 = assign_vars(Termination1, Termination2, Dict1),
3670%%  case {Size1, Size2} of
3671%%    {S, S} -> Dict2;
3672%%    {?any, ?nonempty_qual} -> Dict2;
3673%%    {_, _} -> throw(error)
3674%%  end;
3675%%assign_vars(?product(Types1), ?product(Types2), Dict) ->
3676%%  case length(Types1) =:= length(Types2) of
3677%%    true -> assign_vars_lists(Types1, Types2, Dict);
3678%%    false -> throw(error)
3679%%  end;
3680%%assign_vars(?tuple(?any, ?any, ?any), ?tuple(?any, ?any, ?any), Dict) ->
3681%%  Dict;
3682%%assign_vars(?tuple(?any, ?any, ?any), ?tuple(_, _, _), Dict) ->
3683%%  Dict;
3684%%assign_vars(?tuple(Elements1, Arity, _),
3685%%	    ?tuple(Elements2, Arity, _), Dict) when Arity =/= ?any ->
3686%%  assign_vars_lists(Elements1, Elements2, Dict);
3687%%assign_vars(?tuple_set(_) = T, ?tuple_set(List2), Dict) ->
3688%%  %% All Rhs tuples must already be subtypes of Lhs, so we can take
3689%%  %% each one separatly.
3690%%  assign_vars_lists([T || _ <- List2], List2, Dict);
3691%%assign_vars(?tuple(?any, ?any, ?any), ?tuple_set(_), Dict) ->
3692%%  Dict;
3693%%assign_vars(?tuple(_, Arity, _) = T1, ?tuple_set(List), Dict) ->
3694%%  case reduce_tuple_tags(List) of
3695%%    [Tuple = ?tuple(_, Arity, _)] -> assign_vars(T1, Tuple, Dict);
3696%%    _ -> throw(error)
3697%%  end;
3698%%assign_vars(?tuple_set(List), ?tuple(_, Arity, Tag) = T2, Dict) ->
3699%%  case [T || ?tuple(_, Arity1, Tag1) = T <- List,
3700%%	     Arity1 =:= Arity, Tag1 =:= Tag] of
3701%%    [] -> throw(error);
3702%%    [T1] -> assign_vars(T1, T2, Dict)
3703%%  end;
3704%%assign_vars(?union(U1), T2, Dict) ->
3705%%  ?union(U2) = force_union(T2),
3706%%  assign_vars_lists(U1, U2, Dict);
3707%%assign_vars(T, T, Dict) ->
3708%%  Dict;
3709%%assign_vars(T1, T2, Dict) ->
3710%%  case t_is_subtype(T2, T1) of
3711%%    false -> throw(error);
3712%%    true -> Dict
3713%%  end.
3714
3715%%assign_vars_lists([T1|Left1], [T2|Left2], Dict) ->
3716%%  assign_vars_lists(Left1, Left2, assign_vars(T1, T2, Dict));
3717%%assign_vars_lists([], [], Dict) ->
3718%%  Dict.
3719
3720%%store_var(?var(Id), Type, Dict) ->
3721%%  case dict:find(Id, Dict) of
3722%%    error -> dict:store(Id, [Type], Dict);
3723%%    {ok, _VarType0} -> dict:update(Id, fun(X) -> [Type|X] end, Dict)
3724%%  end.
3725
3726%%-----------------------------------------------------------------------------
3727%% Subtraction.
3728%%
3729%% Note that the subtraction is an approximation since we do not have
3730%% negative types. Also, tuples and products should be handled using
3731%% the cartesian product of the elements, but this is not feasible to
3732%% do.
3733%%
3734%% Example: {a|b,c|d}\{a,d} = {a,c}|{a,d}|{b,c}|{b,d} \ {a,d} =
3735%%                          = {a,c}|{b,c}|{b,d} = {a|b,c|d}
3736%%
3737%% Instead, we can subtract if all elements but one becomes none after
3738%% subtracting element-wise.
3739%%
3740%% Example: {a|b,c|d}\{a|b,d} = {a,c}|{a,d}|{b,c}|{b,d} \ {a,d}|{b,d} =
3741%%                            = {a,c}|{b,c} = {a|b,c}
3742
3743-spec t_subtract_list(erl_type(), [erl_type()]) -> erl_type().
3744
3745t_subtract_list(T1, [T2|Left]) ->
3746  t_subtract_list(t_subtract(T1, T2), Left);
3747t_subtract_list(T, []) ->
3748  T.
3749
3750-spec t_subtract(erl_type(), erl_type()) -> erl_type().
3751
3752t_subtract(_, ?any) -> ?none;
3753t_subtract(T, ?var(_)) -> T;
3754t_subtract(?any, _) -> ?any;
3755t_subtract(?var(_) = T, _) -> T;
3756t_subtract(T, ?unit) -> T;
3757t_subtract(?unit, _) -> ?unit;
3758t_subtract(?none, _) -> ?none;
3759t_subtract(T, ?none) -> T;
3760t_subtract(?atom(Set1), ?atom(Set2)) ->
3761  case set_subtract(Set1, Set2) of
3762    ?none -> ?none;
3763    Set -> ?atom(Set)
3764  end;
3765t_subtract(?bitstr(U1, B1), ?bitstr(U2, B2)) ->
3766  subtract_bin(t_bitstr(U1, B1), t_inf(t_bitstr(U1, B1), t_bitstr(U2, B2)));
3767t_subtract(?function(_, _) = T1, ?function(_, _) = T2) ->
3768  case t_is_subtype(T1, T2) of
3769    true -> ?none;
3770    false -> T1
3771  end;
3772t_subtract(?identifier(Set1), ?identifier(Set2)) ->
3773  case set_subtract(Set1, Set2) of
3774    ?none -> ?none;
3775    Set -> ?identifier(Set)
3776  end;
3777t_subtract(?opaque(_)=T1, ?opaque(_)=T2) ->
3778  opaque_subtract(T1, t_opaque_structure(T2));
3779t_subtract(?opaque(_)=T1, T2) ->
3780  opaque_subtract(T1, T2);
3781t_subtract(T1, ?opaque(_)=T2) ->
3782  t_subtract(T1, t_opaque_structure(T2));
3783t_subtract(?matchstate(Pres1, Slots1), ?matchstate(Pres2, _Slots2)) ->
3784  Pres = t_subtract(Pres1, Pres2),
3785  case t_is_none(Pres) of
3786    true -> ?none;
3787    false -> ?matchstate(Pres, Slots1)
3788  end;
3789t_subtract(?matchstate(Present, Slots), _) ->
3790  ?matchstate(Present, Slots);
3791t_subtract(?nil, ?nil) ->
3792  ?none;
3793t_subtract(?nil, ?nonempty_list(_, _)) ->
3794  ?nil;
3795t_subtract(?nil, ?list(_, _, _)) ->
3796  ?none;
3797t_subtract(?list(Contents, Termination, _Size) = T, ?nil) ->
3798  case Termination =:= ?nil of
3799    true -> ?nonempty_list(Contents, Termination);
3800    false -> T
3801  end;
3802t_subtract(?list(Contents1, Termination1, Size1) = T,
3803	   ?list(Contents2, Termination2, Size2)) ->
3804  case t_is_subtype(Contents1, Contents2) of
3805    true ->
3806      case t_is_subtype(Termination1, Termination2) of
3807	true ->
3808	  case {Size1, Size2} of
3809	    {?nonempty_qual, ?unknown_qual} -> ?none;
3810	    {?unknown_qual, ?nonempty_qual} -> ?nil;
3811	    {S, S} -> ?none
3812	  end;
3813	false ->
3814	  %% If the termination is not covered by the subtracted type
3815	  %% we cannot really say anything about the result.
3816	  T
3817      end;
3818    false ->
3819      %% All contents must be covered if there is going to be any
3820      %% change to the list.
3821      T
3822  end;
3823t_subtract(?float, ?float) -> ?none;
3824t_subtract(?number(_, _) = T1, ?float) -> t_inf(T1, t_integer());
3825t_subtract(?float, ?number(_Set, Tag)) ->
3826  case Tag of
3827    ?unknown_qual -> ?none;
3828    _ -> ?float
3829  end;
3830t_subtract(?number(_, _), ?number(?any, ?unknown_qual)) -> ?none;
3831t_subtract(?number(_, _) = T1, ?integer(?any)) -> t_inf(?float, T1);
3832t_subtract(?int_set(Set1), ?int_set(Set2)) ->
3833  case set_subtract(Set1, Set2) of
3834    ?none -> ?none;
3835    Set -> ?int_set(Set)
3836  end;
3837t_subtract(?int_range(From1, To1) = T1, ?int_range(_, _) = T2) ->
3838  case t_inf(T1, T2) of
3839    ?none -> T1;
3840    ?int_range(From1, To1) -> ?none;
3841    ?int_range(neg_inf, To) -> t_from_range(To + 1, To1);
3842    ?int_range(From, pos_inf) -> t_from_range(From1, From - 1);
3843    ?int_range(From, To) -> t_sup(t_from_range(From1, From - 1),
3844				  t_from_range(To + 1, To))
3845  end;
3846t_subtract(?int_range(From, To) = T1, ?int_set(Set)) ->
3847  NewFrom = case set_is_element(From, Set) of
3848	      true -> From + 1;
3849	      false -> From
3850	    end,
3851  NewTo = case set_is_element(To, Set) of
3852	    true -> To - 1;
3853	    false -> To
3854	  end,
3855  if (NewFrom =:= From) and (NewTo =:= To) -> T1;
3856     true -> t_from_range(NewFrom, NewTo)
3857  end;
3858t_subtract(?int_set(Set), ?int_range(From, To)) ->
3859  case set_filter(fun(X) -> not ((X =< From) orelse (X >= To)) end, Set) of
3860    ?none -> ?none;
3861    NewSet -> ?int_set(NewSet)
3862  end;
3863t_subtract(?integer(?any) = T1, ?integer(_)) -> T1;
3864t_subtract(?number(_, _) = T1, ?number(_, _)) -> T1;
3865t_subtract(?tuple(_, _, _), ?tuple(?any, ?any, ?any)) -> ?none;
3866t_subtract(?tuple_set(_), ?tuple(?any, ?any, ?any)) -> ?none;
3867t_subtract(?tuple(?any, ?any, ?any) = T1, ?tuple_set(_)) -> T1;
3868t_subtract(?tuple(Elements1, Arity1, _Tag1) = T1,
3869	   ?tuple(Elements2, Arity2, _Tag2)) ->
3870  if Arity1 =/= Arity2 -> T1;
3871     Arity1 =:= Arity2 ->
3872      NewElements = t_subtract_lists(Elements1, Elements2),
3873      case [E || E <- NewElements, E =/= ?none] of
3874	[] -> ?none;
3875	[_] -> t_tuple(replace_nontrivial_element(Elements1, NewElements));
3876	_ -> T1
3877      end
3878  end;
3879t_subtract(?tuple_set(List1) = T1, ?tuple(_, Arity, _) = T2) ->
3880  case orddict:find(Arity, List1) of
3881    error -> T1;
3882    {ok, List2} ->
3883      TuplesLeft0 = [Tuple || {_Arity, Tuple} <- orddict:erase(Arity, List1)],
3884      TuplesLeft1 = lists:append(TuplesLeft0),
3885      t_sup([t_subtract(L, T2) || L <- List2] ++ TuplesLeft1)
3886  end;
3887t_subtract(?tuple(_, Arity, _) = T1, ?tuple_set(List1)) ->
3888  case orddict:find(Arity, List1) of
3889    error -> T1;
3890    {ok, List2} -> t_inf([t_subtract(T1, L) || L <- List2])
3891  end;
3892t_subtract(?tuple_set(_) = T1, ?tuple_set(_) = T2) ->
3893  t_sup([t_subtract(T, T2) || T <- t_tuple_subtypes(T1)]);
3894t_subtract(?product(Elements1) = T1, ?product(Elements2)) ->
3895  Arity1 = length(Elements1),
3896  Arity2 = length(Elements2),
3897  if Arity1 =/= Arity2 -> T1;
3898     Arity1 =:= Arity2 ->
3899      NewElements = t_subtract_lists(Elements1, Elements2),
3900      case [E || E <- NewElements, E =/= ?none] of
3901	[] -> ?none;
3902	[_] -> t_product(replace_nontrivial_element(Elements1, NewElements));
3903	_ -> T1
3904      end
3905  end;
3906t_subtract(?map(APairs, ADefK, ADefV) = A, ?map(_, BDefK, BDefV) = B) ->
3907  case t_is_subtype(ADefK, BDefK) andalso t_is_subtype(ADefV, BDefV) of
3908    false -> A;
3909    true ->
3910      %% We fold over the maps to produce a list of constraints, where
3911      %% constraints are additional key-value pairs to put in Pairs. Only one
3912      %% constraint need to be applied to produce a type that excludes the
3913      %% right-hand-side type, so if more than one constraint is produced, we
3914      %% just return the left-hand-side argument.
3915      %%
3916      %% Each case of the fold may either conclude that
3917      %%  * The arguments constrain A at least as much as B, i.e. that A so far
3918      %%    is a subtype of B. In that case they return false
3919      %%  * That for the particular arguments, A being a subtype of B does not
3920      %%    hold, but the infinimum of A and B is nonempty, and by narrowing a
3921      %%    pair in A, we can create a type that excludes some elements in the
3922      %%    infinumum. In that case, they will return that pair.
3923      %%  * That for the particular arguments, A being a subtype of B does not
3924      %%    hold, and either the infinumum of A and B is empty, or it is not
3925      %%    possible with the current representation to create a type that
3926      %%    excludes elements from B without also excluding elements that are
3927      %%    only in A. In that case, it will return the pair from A unchanged.
3928      case
3929	map_pairwise_merge(
3930	  %% If V1 is a subtype of V2, the case that K does not exist in A
3931	  %% remain.
3932	  fun(K, ?opt, V1, ?mand, V2) -> {K, ?opt, t_subtract(V1, V2)};
3933	     (K, _,    V1, _,     V2) ->
3934	      %% If we subtract an optional key, that leaves a mandatory key
3935	      case t_subtract(V1, V2) of
3936		?none -> false;
3937		Partial -> {K, ?mand, Partial}
3938	      end
3939	  end, A, B)
3940      of
3941	  %% We produce a list of keys that are constrained. As only one of
3942	  %% these should apply at a time, we can't represent the difference if
3943	  %% more than one constraint is produced. If we applied all of them,
3944	  %% that would make an underapproximation, which we must not do.
3945	  [] -> ?none; %% A is a subtype of B
3946	  [E] -> t_map(mapdict_store(E, APairs), ADefK, ADefV);
3947	  _ -> A
3948      end
3949  end;
3950t_subtract(?product(P1), _) ->
3951  ?product(P1);
3952t_subtract(T, ?product(_)) ->
3953  T;
3954t_subtract(?union(U1), ?union(U2)) ->
3955  subtract_union(U1, U2);
3956t_subtract(T1, T2) ->
3957  ?union(U1) = force_union(T1),
3958  ?union(U2) = force_union(T2),
3959  subtract_union(U1, U2).
3960
3961-spec opaque_subtract(erl_type(), erl_type()) -> erl_type().
3962
3963opaque_subtract(?opaque(Set1), T2) ->
3964  List = [T1#opaque{struct = Sub} ||
3965           #opaque{struct = S1}=T1 <- set_to_list(Set1),
3966           not t_is_none(Sub = t_subtract(S1, T2))],
3967  case List of
3968    [] -> ?none;
3969    _ -> ?opaque(ordsets:from_list(List))
3970  end.
3971
3972-spec t_subtract_lists([erl_type()], [erl_type()]) -> [erl_type()].
3973
3974t_subtract_lists(L1, L2) ->
3975  t_subtract_lists(L1, L2, []).
3976
3977-spec t_subtract_lists([erl_type()], [erl_type()], [erl_type()]) -> [erl_type()].
3978
3979t_subtract_lists([T1|Left1], [T2|Left2], Acc) ->
3980  t_subtract_lists(Left1, Left2, [t_subtract(T1, T2)|Acc]);
3981t_subtract_lists([], [], Acc) ->
3982  lists:reverse(Acc).
3983
3984-spec subtract_union([erl_type(),...], [erl_type(),...]) -> erl_type().
3985
3986subtract_union(U1, U2) ->
3987  [A1,B1,F1,I1,L1,N1,T1,M1,O1,Map1] = U1,
3988  [A2,B2,F2,I2,L2,N2,T2,M2,O2,Map2] = U2,
3989  List1 = [A1,B1,F1,I1,L1,N1,T1,M1,?none,Map1],
3990  List2 = [A2,B2,F2,I2,L2,N2,T2,M2,?none,Map2],
3991  Sub1 = subtract_union(List1, List2, 0, []),
3992  O = if O1 =:= ?none -> O1;
3993         true -> t_subtract(O1, ?union(U2))
3994      end,
3995  Sub2 = if O2 =:= ?none -> Sub1;
3996            true -> t_subtract(Sub1, t_opaque_structure(O2))
3997         end,
3998  t_sup(O, Sub2).
3999
4000-spec subtract_union([erl_type()], [erl_type()], non_neg_integer(), [erl_type()]) -> erl_type().
4001
4002subtract_union([T1|Left1], [T2|Left2], N, Acc) ->
4003  case t_subtract(T1, T2) of
4004    ?none -> subtract_union(Left1, Left2, N, [?none|Acc]);
4005    T ->     subtract_union(Left1, Left2, N+1, [T|Acc])
4006  end;
4007subtract_union([], [], 0, _Acc) ->
4008  ?none;
4009subtract_union([], [], 1, Acc) ->
4010  [T] = [X || X <- Acc, X =/= ?none],
4011  T;
4012subtract_union([], [], N, Acc) when is_integer(N), N > 1 ->
4013  ?union(lists:reverse(Acc)).
4014
4015replace_nontrivial_element(El1, El2) ->
4016  replace_nontrivial_element(El1, El2, []).
4017
4018replace_nontrivial_element([T1|Left1], [?none|Left2], Acc) ->
4019  replace_nontrivial_element(Left1, Left2, [T1|Acc]);
4020replace_nontrivial_element([_|Left1], [T2|_], Acc) ->
4021  lists:reverse(Acc) ++ [T2|Left1].
4022
4023subtract_bin(?bitstr(U1, B1), ?bitstr(U1, B1)) ->
4024  ?none;
4025subtract_bin(?bitstr(U1, B1), ?none) ->
4026  t_bitstr(U1, B1);
4027subtract_bin(?bitstr(U1, B1), ?bitstr(0, B1)) ->
4028  t_bitstr(U1, B1+U1);
4029subtract_bin(?bitstr(U1, B1), ?bitstr(U1, B2)) ->
4030  if (B1+U1) =/= B2 -> t_bitstr(0, B1);
4031     true -> t_bitstr(U1, B1)
4032  end;
4033subtract_bin(?bitstr(U1, B1), ?bitstr(U2, B2)) ->
4034  if (2 * U1) =:= U2 ->
4035      if B1 =:= B2 ->
4036	  t_bitstr(U2, B1+U1);
4037	 (B1 + U1) =:= B2 ->
4038	  t_bitstr(U2, B1);
4039	 true ->
4040	  t_bitstr(U1, B1)
4041      end;
4042     true ->
4043      t_bitstr(U1, B1)
4044  end.
4045
4046%%-----------------------------------------------------------------------------
4047%% Relations
4048%%
4049
4050-spec t_is_equal(erl_type(), erl_type()) -> boolean().
4051
4052t_is_equal(T, T)  -> true;
4053t_is_equal(_, _) -> false.
4054
4055-spec t_is_subtype(erl_type(), erl_type()) -> boolean().
4056
4057t_is_subtype(T1, T2) ->
4058  Inf = t_inf(T1, T2),
4059  subtype_is_equal(T1, Inf).
4060
4061%% The subtype relation has to behave correctly irrespective of opaque
4062%% types.
4063subtype_is_equal(T, T)   -> true;
4064subtype_is_equal(T1, T2) ->
4065  t_is_equal(case t_contains_opaque(T1) of
4066               true  -> t_unopaque(T1);
4067               false -> T1
4068             end,
4069             case t_contains_opaque(T2) of
4070               true  -> t_unopaque(T2);
4071               false -> T2
4072             end).
4073
4074-spec t_is_instance(erl_type(), erl_type()) -> boolean().
4075
4076%% XXX. To be removed.
4077t_is_instance(ConcreteType, Type) ->
4078  t_is_subtype(ConcreteType, t_unopaque(Type)).
4079
4080-spec t_do_overlap(erl_type(), erl_type()) -> boolean().
4081
4082t_do_overlap(TypeA, TypeB) ->
4083  not (t_is_none_or_unit(t_inf(TypeA, TypeB))).
4084
4085-spec t_unopaque(erl_type()) -> erl_type().
4086
4087t_unopaque(T) ->
4088  t_unopaque(T, 'universe').
4089
4090-spec t_unopaque(erl_type(), opaques()) -> erl_type().
4091
4092t_unopaque(?opaque(_) = T, Opaques) ->
4093  case Opaques =:= 'universe' orelse is_opaque_type(T, Opaques) of
4094    true -> t_unopaque(t_opaque_structure(T), Opaques);
4095    false -> T
4096  end;
4097t_unopaque(?list(ElemT, Termination, Sz), Opaques) ->
4098  ?list(t_unopaque(ElemT, Opaques), t_unopaque(Termination, Opaques), Sz);
4099t_unopaque(?tuple(?any, _, _) = T, _) -> T;
4100t_unopaque(?tuple(ArgTs, Sz, Tag), Opaques) when is_list(ArgTs) ->
4101  NewArgTs = [t_unopaque(A, Opaques) || A <- ArgTs],
4102  ?tuple(NewArgTs, Sz, Tag);
4103t_unopaque(?tuple_set(Set), Opaques) ->
4104  NewSet = [{Sz, [t_unopaque(T, Opaques) || T <- Tuples]}
4105	    || {Sz, Tuples} <- Set],
4106  ?tuple_set(NewSet);
4107t_unopaque(?product(Types), Opaques) ->
4108  ?product([t_unopaque(T, Opaques) || T <- Types]);
4109t_unopaque(?function(Domain, Range), Opaques) ->
4110  ?function(t_unopaque(Domain, Opaques), t_unopaque(Range, Opaques));
4111t_unopaque(?union([A,B,F,I,L,N,T,M,O,Map]), Opaques) ->
4112  UL = t_unopaque(L, Opaques),
4113  UT = t_unopaque(T, Opaques),
4114  UF = t_unopaque(F, Opaques),
4115  UM = t_unopaque(M, Opaques),
4116  UMap = t_unopaque(Map, Opaques),
4117  {OF,UO} = case t_unopaque(O, Opaques) of
4118              ?opaque(_) = O1 -> {O1, []};
4119              Type -> {?none, [Type]}
4120            end,
4121  t_sup([?union([A,B,UF,I,UL,N,UT,UM,OF,UMap])|UO]);
4122t_unopaque(?map(Pairs,DefK,DefV), Opaques) ->
4123  t_map([{K, MNess, t_unopaque(V, Opaques)} || {K, MNess, V} <- Pairs],
4124	t_unopaque(DefK, Opaques),
4125	t_unopaque(DefV, Opaques));
4126t_unopaque(T, _) ->
4127  T.
4128
4129%%-----------------------------------------------------------------------------
4130%% K-depth abstraction.
4131%%
4132%% t_limit/2 is the exported function, which checks the type of the
4133%% second argument and calls the module local t_limit_k/2 function.
4134%%
4135
4136-spec t_limit(erl_type(), integer()) -> erl_type().
4137
4138t_limit(Term, K) when is_integer(K) ->
4139  t_limit_k(Term, K).
4140
4141t_limit_k(_, K) when K =< 0 -> ?any;
4142t_limit_k(?tuple(?any, ?any, ?any) = T, _K) -> T;
4143t_limit_k(?tuple(Elements, Arity, _), K) ->
4144  if K =:= 1 -> t_tuple(Arity);
4145     true -> t_tuple([t_limit_k(E, K-1) || E <- Elements])
4146  end;
4147t_limit_k(?tuple_set(_) = T, K) ->
4148  t_sup([t_limit_k(Tuple, K) || Tuple <- t_tuple_subtypes(T)]);
4149t_limit_k(?list(Elements, Termination, Size), K) ->
4150  NewTermination =
4151    if K =:= 1 ->
4152	%% We do not want to lose the termination information.
4153	t_limit_k(Termination, K);
4154       true -> t_limit_k(Termination, K - 1)
4155    end,
4156  NewElements = t_limit_k(Elements, K - 1),
4157  TmpList = t_cons(NewElements, NewTermination),
4158  case Size of
4159    ?nonempty_qual -> TmpList;
4160    ?unknown_qual ->
4161      ?list(NewElements1, NewTermination1, _) = TmpList,
4162      ?list(NewElements1, NewTermination1, ?unknown_qual)
4163  end;
4164t_limit_k(?function(Domain, Range), K) ->
4165  %% The domain is either a product or any() so we do not decrease the K.
4166  ?function(t_limit_k(Domain, K), t_limit_k(Range, K-1));
4167t_limit_k(?product(Elements), K) ->
4168  ?product([t_limit_k(X, K - 1) || X <- Elements]);
4169t_limit_k(?union(Elements), K) ->
4170  ?union([t_limit_k(X, K) || X <- Elements]);
4171t_limit_k(?opaque(Es), K) ->
4172  List = [begin
4173            NewS = t_limit_k(S, K),
4174            Opaque#opaque{struct = NewS}
4175          end || #opaque{struct = S} = Opaque <- set_to_list(Es)],
4176  ?opaque(ordsets:from_list(List));
4177t_limit_k(?map(Pairs0, DefK0, DefV0), K) ->
4178  Fun = fun({EK, MNess, EV}, {Exact, DefK1, DefV1}) ->
4179	    LV = t_limit_k(EV, K - 1),
4180	    case t_limit_k(EK, K - 1) of
4181	      EK -> {[{EK,MNess,LV}|Exact], DefK1, DefV1};
4182	      LK -> {Exact, t_sup(LK, DefK1), t_sup(LV, DefV1)}
4183	    end
4184	end,
4185  {Pairs, DefK2, DefV2} = lists:foldr(Fun, {[], DefK0, DefV0}, Pairs0),
4186  t_map(Pairs, t_limit_k(DefK2, K - 1), t_limit_k(DefV2, K - 1));
4187t_limit_k(T, _K) -> T.
4188
4189%%============================================================================
4190%%
4191%% Abstract records. Used for comparing contracts.
4192%%
4193%%============================================================================
4194
4195-spec t_abstract_records(erl_type(), type_table()) -> erl_type().
4196
4197t_abstract_records(?list(Contents, Termination, Size), RecDict) ->
4198  case t_abstract_records(Contents, RecDict) of
4199    ?none -> ?none;
4200    NewContents ->
4201      %% Be careful here to make the termination collapse if necessary.
4202      case t_abstract_records(Termination, RecDict) of
4203	?nil -> ?list(NewContents, ?nil, Size);
4204	?any -> ?list(NewContents, ?any, Size);
4205	Other ->
4206	  ?list(NewContents2, NewTermination, _) = t_cons(NewContents, Other),
4207	  ?list(NewContents2, NewTermination, Size)
4208      end
4209  end;
4210t_abstract_records(?function(Domain, Range), RecDict) ->
4211  ?function(t_abstract_records(Domain, RecDict),
4212	    t_abstract_records(Range, RecDict));
4213t_abstract_records(?product(Types), RecDict) ->
4214  ?product([t_abstract_records(T, RecDict) || T <- Types]);
4215t_abstract_records(?union(Types), RecDict) ->
4216  t_sup([t_abstract_records(T, RecDict) || T <- Types]);
4217t_abstract_records(?tuple(?any, ?any, ?any) = T, _RecDict) ->
4218  T;
4219t_abstract_records(?tuple(Elements, Arity, ?atom(_) = Tag), RecDict) ->
4220  [TagAtom] = atom_vals(Tag),
4221  case lookup_record(TagAtom, Arity - 1, RecDict) of
4222    error -> t_tuple([t_abstract_records(E, RecDict) || E <- Elements]);
4223    {ok, Fields} -> t_tuple([Tag|[T || {_Name, _Abstr, T} <- Fields]])
4224  end;
4225t_abstract_records(?tuple(Elements, _Arity, _Tag), RecDict) ->
4226  t_tuple([t_abstract_records(E, RecDict) || E <- Elements]);
4227t_abstract_records(?tuple_set(_) = Tuples, RecDict) ->
4228  t_sup([t_abstract_records(T, RecDict) || T <- t_tuple_subtypes(Tuples)]);
4229t_abstract_records(?opaque(_)=Type, RecDict) ->
4230  t_abstract_records(t_opaque_structure(Type), RecDict);
4231t_abstract_records(T, _RecDict) ->
4232  T.
4233
4234%%=============================================================================
4235%%
4236%% Prettyprinter
4237%%
4238%%=============================================================================
4239
4240-spec t_to_string(erl_type()) -> string().
4241
4242t_to_string(T) ->
4243  t_to_string(T, maps:new()).
4244
4245-spec t_to_string(erl_type(), type_table()) -> string().
4246
4247t_to_string(?any, _RecDict) ->
4248  "any()";
4249t_to_string(?none, _RecDict) ->
4250  "none()";
4251t_to_string(?unit, _RecDict) ->
4252  "no_return()";
4253t_to_string(?atom(?any), _RecDict) ->
4254  "atom()";
4255t_to_string(?atom(Set), _RecDict) ->
4256  case set_size(Set) of
4257    2 ->
4258      case set_is_element(true, Set) andalso set_is_element(false, Set) of
4259	true -> "boolean()";
4260	false -> set_to_string(Set)
4261      end;
4262    _ ->
4263      set_to_string(Set)
4264  end;
4265t_to_string(?bitstr(0, 0), _RecDict) ->
4266  "<<>>";
4267t_to_string(?bitstr(8, 0), _RecDict) ->
4268  "binary()";
4269t_to_string(?bitstr(1, 0), _RecDict) ->
4270  "bitstring()";
4271t_to_string(?bitstr(0, B), _RecDict) ->
4272  flat_format("<<_:~w>>", [B]);
4273t_to_string(?bitstr(U, 0), _RecDict) ->
4274  flat_format("<<_:_*~w>>", [U]);
4275t_to_string(?bitstr(U, B), _RecDict) ->
4276  flat_format("<<_:~w,_:_*~w>>", [B, U]);
4277t_to_string(?function(?any, ?any), _RecDict) ->
4278  "fun()";
4279t_to_string(?function(?any, Range), RecDict) ->
4280  "fun((...) -> " ++ t_to_string(Range, RecDict) ++ ")";
4281t_to_string(?function(?product(ArgList), Range), RecDict) ->
4282  "fun((" ++ comma_sequence(ArgList, RecDict) ++ ") -> "
4283    ++ t_to_string(Range, RecDict) ++ ")";
4284t_to_string(?identifier(Set), _RecDict) ->
4285  case Set of
4286    ?any -> "identifier()";
4287    _ ->
4288      flat_join([flat_format("~w()", [T]) || T <- set_to_list(Set)], " | ")
4289  end;
4290t_to_string(?opaque(Set), RecDict) ->
4291  flat_join([opaque_type(Mod, Name, Args, S, RecDict) ||
4292              #opaque{mod = Mod, name = Name, struct = S, args = Args}
4293                <- set_to_list(Set)],
4294            " | ");
4295t_to_string(?matchstate(Pres, Slots), RecDict) ->
4296  flat_format("ms(~ts,~ts)", [t_to_string(Pres, RecDict),
4297                              t_to_string(Slots,RecDict)]);
4298t_to_string(?nil, _RecDict) ->
4299  "[]";
4300t_to_string(?nonempty_list(Contents, Termination), RecDict) ->
4301  ContentString = t_to_string(Contents, RecDict),
4302  case Termination of
4303    ?nil ->
4304      case Contents of
4305	?char -> "nonempty_string()";
4306	_ -> "["++ContentString++",...]"
4307      end;
4308    ?any ->
4309      %% Just a safety check.
4310      case Contents =:= ?any of
4311	true -> ok;
4312	false ->
4313          %% XXX. See comment below.
4314          %% erlang:error({illegal_list, ?nonempty_list(Contents, Termination)})
4315          ok
4316      end,
4317      "nonempty_maybe_improper_list()";
4318    _ ->
4319      case t_is_subtype(t_nil(), Termination) of
4320	true ->
4321	  "nonempty_maybe_improper_list("++ContentString++","
4322	    ++t_to_string(Termination, RecDict)++")";
4323	false ->
4324	  "nonempty_improper_list("++ContentString++","
4325	    ++t_to_string(Termination, RecDict)++")"
4326      end
4327  end;
4328t_to_string(?list(Contents, Termination, ?unknown_qual), RecDict) ->
4329  ContentString = t_to_string(Contents, RecDict),
4330  case Termination of
4331    ?nil ->
4332      case Contents of
4333	?char -> "string()";
4334	_ -> "["++ContentString++"]"
4335      end;
4336    ?any ->
4337      %% Just a safety check.
4338      %% XXX. Types such as "maybe_improper_list(integer(), any())"
4339      %% are OK, but cannot be printed!?
4340      case Contents =:= ?any of
4341	true -> ok;
4342	false ->
4343          ok
4344          %% L = ?list(Contents, Termination, ?unknown_qual),
4345          %% erlang:error({illegal_list, L})
4346      end,
4347      "maybe_improper_list()";
4348    _ ->
4349      case t_is_subtype(t_nil(), Termination) of
4350	true ->
4351	  "maybe_improper_list("++ContentString++","
4352	    ++t_to_string(Termination, RecDict)++")";
4353	false ->
4354	  "improper_list("++ContentString++","
4355	    ++t_to_string(Termination, RecDict)++")"
4356      end
4357  end;
4358t_to_string(?int_set(Set), _RecDict) ->
4359  set_to_string(Set);
4360t_to_string(?byte, _RecDict) -> "byte()";
4361t_to_string(?char, _RecDict) -> "char()";
4362t_to_string(?integer_pos, _RecDict) -> "pos_integer()";
4363t_to_string(?integer_non_neg, _RecDict) -> "non_neg_integer()";
4364t_to_string(?integer_neg, _RecDict) -> "neg_integer()";
4365t_to_string(?int_range(From, To), _RecDict) ->
4366  flat_format("~w..~w", [From, To]);
4367t_to_string(?integer(?any), _RecDict) -> "integer()";
4368t_to_string(?float, _RecDict) -> "float()";
4369t_to_string(?number(?any, ?unknown_qual), _RecDict) -> "number()";
4370t_to_string(?product(List), RecDict) ->
4371  "<" ++ comma_sequence(List, RecDict) ++ ">";
4372t_to_string(?map([],?any,?any), _RecDict) -> "map()";
4373t_to_string(?map(Pairs0,DefK,DefV), RecDict) ->
4374  {Pairs, ExtraEl} =
4375    case {DefK, DefV} of
4376      {?none, ?none} -> {Pairs0, []};
4377      _ -> {Pairs0 ++ [{DefK,?opt,DefV}], []}
4378    end,
4379  Tos = fun(T) -> case T of
4380		    ?any -> "_";
4381		    _ -> t_to_string(T, RecDict)
4382		  end end,
4383  StrMand = [{Tos(K),Tos(V)}||{K,?mand,V}<-Pairs],
4384  StrOpt  = [{Tos(K),Tos(V)}||{K,?opt,V}<-Pairs],
4385  "#{" ++ flat_join([K ++ ":=" ++ V||{K,V}<-StrMand]
4386                    ++ [K ++ "=>" ++ V||{K,V}<-StrOpt]
4387                    ++ ExtraEl, ", ") ++ "}";
4388t_to_string(?tuple(?any, ?any, ?any), _RecDict) -> "tuple()";
4389t_to_string(?tuple(Elements, _Arity, ?any), RecDict) ->
4390  "{" ++ comma_sequence(Elements, RecDict) ++ "}";
4391t_to_string(?tuple(Elements, Arity, Tag), RecDict) ->
4392  [TagAtom] = atom_vals(Tag),
4393  case lookup_record(TagAtom, Arity-1, RecDict) of
4394    error -> "{" ++ comma_sequence(Elements, RecDict) ++ "}";
4395    {ok, FieldNames} ->
4396      record_to_string(TagAtom, Elements, FieldNames, RecDict)
4397  end;
4398t_to_string(?tuple_set(_) = T, RecDict) ->
4399  union_sequence(t_tuple_subtypes(T), RecDict);
4400t_to_string(?union(Types), RecDict) ->
4401  union_sequence([T || T <- Types, T =/= ?none], RecDict);
4402t_to_string(?var(Id), _RecDict) when is_atom(Id) ->
4403  flat_format("~s", [atom_to_list(Id)]);
4404t_to_string(?var(Id), _RecDict) when is_integer(Id) ->
4405  flat_format("var(~w)", [Id]).
4406
4407
4408record_to_string(Tag, [_|Fields], FieldNames, RecDict) ->
4409  FieldStrings = record_fields_to_string(Fields, FieldNames, RecDict, []),
4410  "#" ++ atom_to_string(Tag) ++ "{" ++ flat_join(FieldStrings, ",") ++ "}".
4411
4412record_fields_to_string([F|Fs], [{FName, _Abstr, DefType}|FDefs],
4413                        RecDict, Acc) ->
4414  NewAcc =
4415    case
4416      t_is_equal(F, t_any()) orelse
4417      (t_is_any_atom('undefined', F) andalso
4418       not t_is_none(t_inf(F, DefType)))
4419    of
4420      true -> Acc;
4421      false ->
4422	StrFV = atom_to_string(FName) ++ "::" ++ t_to_string(F, RecDict),
4423	[StrFV|Acc]
4424    end,
4425  record_fields_to_string(Fs, FDefs, RecDict, NewAcc);
4426record_fields_to_string([], [], _RecDict, Acc) ->
4427  lists:reverse(Acc).
4428
4429-spec record_field_diffs_to_string(erl_type(), type_table()) -> string().
4430
4431record_field_diffs_to_string(?tuple([_|Fs], Arity, Tag), RecDict) ->
4432  [TagAtom] = atom_vals(Tag),
4433  {ok, FieldNames} = lookup_record(TagAtom, Arity-1, RecDict),
4434  %% io:format("RecCElems = ~p\nRecTypes = ~p\n", [Fs, FieldNames]),
4435  FieldDiffs = field_diffs(Fs, FieldNames, RecDict, []),
4436  flat_join(FieldDiffs, " and ").
4437
4438field_diffs([F|Fs], [{FName, _Abstr, DefType}|FDefs], RecDict, Acc) ->
4439  %% Don't care about opacity for now.
4440  NewAcc =
4441    case not t_is_none(t_inf(F, DefType)) of
4442      true -> Acc;
4443      false ->
4444	Str = atom_to_string(FName) ++ "::" ++ t_to_string(DefType, RecDict),
4445	[Str|Acc]
4446    end,
4447  field_diffs(Fs, FDefs, RecDict, NewAcc);
4448field_diffs([], [], _, Acc) ->
4449  lists:reverse(Acc).
4450
4451comma_sequence(Types, RecDict) ->
4452  List = [case T =:= ?any of
4453	    true -> "_";
4454	    false -> t_to_string(T, RecDict)
4455	  end || T <- Types],
4456  flat_join(List, ",").
4457
4458union_sequence(Types, RecDict) ->
4459  List = [t_to_string(T, RecDict) || T <- Types],
4460  flat_join(List, " | ").
4461
4462-ifdef(DEBUG).
4463opaque_type(Mod, Name, _Args, S, RecDict) ->
4464  ArgsString = comma_sequence(_Args, RecDict),
4465  String = t_to_string(S, RecDict),
4466  opaque_name(Mod, Name, ArgsString) ++ "[" ++ String ++ "]".
4467-else.
4468opaque_type(Mod, Name, Args, _S, RecDict) ->
4469  ArgsString = comma_sequence(Args, RecDict),
4470  opaque_name(Mod, Name, ArgsString).
4471-endif.
4472
4473opaque_name(Mod, Name, Extra) ->
4474  S = mod_name(Mod, Name),
4475  flat_format("~ts(~ts)", [S, Extra]).
4476
4477mod_name(Mod, Name) ->
4478  flat_format("~w:~tw", [Mod, Name]).
4479
4480%%=============================================================================
4481%%
4482%% Build a type from parse forms.
4483%%
4484%%=============================================================================
4485
4486-type type_names() :: [type_key() | record_key()].
4487
4488-type mta()   :: {module(), atom(), arity()}.
4489-type mra()   :: {module(), atom(), arity()}.
4490-type site()  :: {'type', mta()} | {'spec', mfa()} | {'record', mra()}.
4491-type cache_key() :: {module(), atom(), expand_depth(),
4492                      [erl_type()], type_names()}.
4493-type mod_type_table() :: ets:tid().
4494-type mod_records() :: dict:dict(module(), type_table()).
4495-record(cache,
4496        {
4497          types = maps:new() :: #{cache_key() => {erl_type(), expand_limit()}},
4498          mod_recs = {mrecs, dict:new()} :: {'mrecs', mod_records()}
4499        }).
4500
4501-opaque cache() :: #cache{}.
4502
4503-spec t_from_form(parse_form(), sets:set(mfa()), site(), mod_type_table(),
4504                  var_table(), cache()) -> {erl_type(), cache()}.
4505
4506t_from_form(Form, ExpTypes, Site, RecDict, VarTab, Cache) ->
4507  t_from_form1(Form, ExpTypes, Site, RecDict, VarTab, Cache).
4508
4509%% Replace external types with with none().
4510-spec t_from_form_without_remote(parse_form(), site(), type_table()) ->
4511                                    erl_type().
4512
4513t_from_form_without_remote(Form, Site, TypeTable) ->
4514  Module = site_module(Site),
4515  ModRecs = dict:from_list([{Module, TypeTable}]),
4516  ExpTypes = replace_by_none,
4517  VarTab = var_table__new(),
4518  Cache0 = cache__new(),
4519  Cache = Cache0#cache{mod_recs = {mrecs, ModRecs}},
4520  {Type, _} = t_from_form1(Form, ExpTypes, Site, undefined, VarTab, Cache),
4521  Type.
4522
4523-type expand_limit() :: integer().
4524
4525-type expand_depth() :: integer().
4526
4527-record(from_form, {site   :: site() | {'check', mta()},
4528                    xtypes :: sets:set(mfa()) | 'replace_by_none',
4529                    mrecs  :: 'undefined' | mod_type_table(),
4530                    vtab   :: var_table(),
4531                    tnames :: type_names()}).
4532
4533-spec t_from_form_check_remote(parse_form(), sets:set(mfa()), mta(),
4534                               mod_type_table()) -> 'ok'.
4535t_from_form_check_remote(Form, ExpTypes, MTA, RecDict) ->
4536  State = #from_form{site   = {check, MTA},
4537                     xtypes = ExpTypes,
4538                     mrecs  = RecDict,
4539                     vtab   = var_table__new(),
4540                     tnames = []},
4541  D = (1 bsl 25), % unlimited
4542  L = (1 bsl 25),
4543  Cache0 = cache__new(),
4544  _ = t_from_form2(Form, State, D, L, Cache0),
4545  ok.
4546
4547%% REC_TYPE_LIMIT is used for limiting the depth of recursive types.
4548%% EXPAND_LIMIT is used for limiting the size of types by
4549%% limiting the number of elements of lists within one type form.
4550%% EXPAND_DEPTH is used in conjunction with EXPAND_LIMIT to make the
4551%% types balanced (unions will otherwise collapse to any()) by limiting
4552%% the depth the same way as t_limit/2 does.
4553
4554-spec t_from_form1(parse_form(), sets:set(mfa()) | 'replace_by_none',
4555                   site(), 'undefined' | mod_type_table(), var_table(),
4556                   cache()) -> {erl_type(), cache()}.
4557
4558t_from_form1(Form, ET, Site, MR, V, C) ->
4559  TypeNames = initial_typenames(Site),
4560  D = ?EXPAND_DEPTH,
4561  L = ?EXPAND_LIMIT,
4562  State = #from_form{site   = Site,
4563                     xtypes = ET,
4564                     mrecs  = MR,
4565                     vtab   = V,
4566                     tnames = TypeNames},
4567  t_from_form2(Form, State, D, L, C).
4568
4569t_from_form2(Form, State, D, L, C) ->
4570  {T0, L0, C0} = from_form(Form, State, D, L, C),
4571  if
4572    L0 =< 0 ->
4573      {T1, _, C1} = from_form(Form, State, 1, L, C0),
4574      from_form_loop(Form, State, 2, L, C1, T1);
4575    true ->
4576       {T0, C0}
4577  end.
4578
4579initial_typenames({type, _MTA}=Site) -> [Site];
4580initial_typenames({spec, _MFA}) -> [];
4581initial_typenames({record, _MRA}) -> [].
4582
4583from_form_loop(Form, State, D, Limit, C, T0) ->
4584  {T1, L1, C1} = from_form(Form, State, D, Limit, C),
4585  Delta = Limit - L1,
4586  if
4587    L1 =< 0 ->
4588      {T0, C1};
4589    Delta * 8 > Limit ->
4590      %% Save some time by assuming next depth will exceed the limit.
4591      {T1, C1};
4592    true ->
4593      D1 = D + 1,
4594      from_form_loop(Form, State, D1, Limit, C1, T1)
4595  end.
4596
4597-spec from_form(parse_form(),
4598                #from_form{},
4599                expand_depth(),
4600                expand_limit(),
4601                cache()) -> {erl_type(), expand_limit(), cache()}.
4602
4603%% If there is something wrong with parse_form()
4604%% throw({error, io_lib:chars()} is called;
4605%% for unknown remote types
4606%% self() ! {self(), ext_types, {RemMod, Name, ArgsLen}}
4607%% is called, unless 'replace_by_none' is given.
4608%%
4609%% It is assumed that site_module(S) can be found in MR.
4610
4611from_form(_, _S, D, L, C) when D =< 0 ; L =< 0 ->
4612  {t_any(), L, C};
4613from_form({var, _L, '_'}, _S, _D, L, C) ->
4614  {t_any(), L, C};
4615from_form({var, _L, Name}, S, _D, L, C) ->
4616  V = S#from_form.vtab,
4617  case maps:find(Name, V) of
4618    error -> {t_var(Name), L, C};
4619    {ok, Val} -> {Val, L, C}
4620  end;
4621from_form({ann_type, _L, [_Var, Type]}, S, D, L, C) ->
4622  from_form(Type, S, D, L, C);
4623from_form({paren_type, _L, [Type]}, S, D, L, C) ->
4624  from_form(Type, S, D, L, C);
4625from_form({remote_type, _L, [{atom, _, Module}, {atom, _, Type}, Args]},
4626	    S, D, L, C) ->
4627  remote_from_form(Module, Type, Args, S, D, L, C);
4628from_form({atom, _L, Atom}, _S, _D, L, C) ->
4629  {t_atom(Atom), L, C};
4630from_form({integer, _L, Int}, _S, _D, L, C) ->
4631  {t_integer(Int), L, C};
4632from_form({char, _L, Char}, _S, _D, L, C) ->
4633  {t_integer(Char), L, C};
4634from_form({op, _L, _Op, _Arg} = Op, _S, _D, L, C) ->
4635  case erl_eval:partial_eval(Op) of
4636    {integer, _, Val} ->
4637      {t_integer(Val), L, C};
4638    _ -> throw({error, io_lib:format("Unable to evaluate type ~w\n", [Op])})
4639  end;
4640from_form({op, _L, _Op, _Arg1, _Arg2} = Op, _S, _D, L, C) ->
4641  case erl_eval:partial_eval(Op) of
4642    {integer, _, Val} ->
4643      {t_integer(Val), L, C};
4644    _ -> throw({error, io_lib:format("Unable to evaluate type ~w\n", [Op])})
4645  end;
4646from_form({type, _L, any, []}, _S, _D, L, C) ->
4647  {t_any(), L, C};
4648from_form({type, _L, arity, []}, _S, _D, L, C) ->
4649  {t_arity(), L, C};
4650from_form({type, _L, atom, []}, _S, _D, L, C) ->
4651  {t_atom(), L, C};
4652from_form({type, _L, binary, []}, _S, _D, L, C) ->
4653  {t_binary(), L, C};
4654from_form({type, _L, binary, [Base, Unit]} = Type, _S, _D, L, C) ->
4655  case {erl_eval:partial_eval(Base), erl_eval:partial_eval(Unit)} of
4656    {{integer, _, B}, {integer, _, U}} when B >= 0, U >= 0 ->
4657      {t_bitstr(U, B), L, C};
4658    _ -> throw({error, io_lib:format("Unable to evaluate type ~w\n", [Type])})
4659  end;
4660from_form({type, _L, bitstring, []}, _S, _D, L, C) ->
4661  {t_bitstr(), L, C};
4662from_form({type, _L, bool, []}, _S, _D, L, C) ->
4663  {t_boolean(), L, C};	% XXX: Temporarily
4664from_form({type, _L, boolean, []}, _S, _D, L, C) ->
4665  {t_boolean(), L, C};
4666from_form({type, _L, byte, []}, _S, _D, L, C) ->
4667  {t_byte(), L, C};
4668from_form({type, _L, char, []}, _S, _D, L, C) ->
4669  {t_char(), L, C};
4670from_form({type, _L, float, []}, _S, _D, L, C) ->
4671  {t_float(), L, C};
4672from_form({type, _L, function, []}, _S, _D, L, C) ->
4673  {t_fun(), L, C};
4674from_form({type, _L, 'fun', []}, _S, _D, L, C) ->
4675  {t_fun(), L, C};
4676from_form({type, _L, 'fun', [{type, _, any}, Range]}, S, D, L, C) ->
4677  {T, L1, C1} = from_form(Range, S, D - 1, L - 1, C),
4678  {t_fun(T), L1, C1};
4679from_form({type, _L, 'fun', [{type, _, product, Domain}, Range]},
4680          S, D, L, C) ->
4681  {Dom1, L1, C1} = list_from_form(Domain, S, D, L, C),
4682  {Ran1, L2, C2} = from_form(Range, S, D, L1, C1),
4683  {t_fun(Dom1, Ran1), L2, C2};
4684from_form({type, _L, identifier, []}, _S, _D, L, C) ->
4685  {t_identifier(), L, C};
4686from_form({type, _L, integer, []}, _S, _D, L, C) ->
4687  {t_integer(), L, C};
4688from_form({type, _L, iodata, []}, _S, _D, L, C) ->
4689  {t_iodata(), L, C};
4690from_form({type, _L, iolist, []}, _S, _D, L, C) ->
4691  {t_iolist(), L, C};
4692from_form({type, _L, list, []}, _S, _D, L, C) ->
4693  {t_list(), L, C};
4694from_form({type, _L, list, [Type]}, S, D, L, C) ->
4695  {T, L1, C1} = from_form(Type, S, D - 1, L - 1, C),
4696  {t_list(T), L1, C1};
4697from_form({type, _L, map, any}, S, D, L, C) ->
4698  builtin_type(map, t_map(), S, D, L, C);
4699from_form({type, _L, map, List}, S, D0, L, C) ->
4700  {Pairs1, L5, C5} =
4701    fun PairsFromForm(_, L1, C1) when L1 =< 0 -> {[{?any,?opt,?any}], L1, C1};
4702	PairsFromForm([], L1, C1) -> {[], L1, C1};
4703	PairsFromForm([{type, _, Oper, [KF, VF]}|T], L1, C1) ->
4704        D = D0 - 1,
4705	{Key, L2, C2} = from_form(KF, S, D, L1, C1),
4706	{Val, L3, C3} = from_form(VF, S, D, L2, C2),
4707	{Pairs0, L4, C4} = PairsFromForm(T, L3 - 1, C3),
4708	case Oper of
4709	  map_field_assoc -> {[{Key,?opt, Val}|Pairs0], L4, C4};
4710	  map_field_exact -> {[{Key,?mand,Val}|Pairs0], L4, C4}
4711	end
4712    end(List, L, C),
4713  try
4714    Pairs2 = singleton_elements(Pairs1),
4715    {Pairs, DefK, DefV} = map_from_form(Pairs2, [], [], [], ?none, ?none),
4716    {t_map(Pairs, DefK, DefV), L5, C5}
4717  catch none -> {t_none(), L5, C5}
4718  end;
4719from_form({type, _L, mfa, []}, _S, _D, L, C) ->
4720  {t_mfa(), L, C};
4721from_form({type, _L, module, []}, _S, _D, L, C) ->
4722  {t_module(), L, C};
4723from_form({type, _L, nil, []}, _S, _D, L, C) ->
4724  {t_nil(), L, C};
4725from_form({type, _L, neg_integer, []}, _S, _D, L, C) ->
4726  {t_neg_integer(), L, C};
4727from_form({type, _L, non_neg_integer, []}, _S, _D, L, C) ->
4728  {t_non_neg_integer(), L, C};
4729from_form({type, _L, no_return, []}, _S, _D, L, C) ->
4730  {t_unit(), L, C};
4731from_form({type, _L, node, []}, _S, _D, L, C) ->
4732  {t_node(), L, C};
4733from_form({type, _L, none, []}, _S, _D, L, C) ->
4734  {t_none(), L, C};
4735from_form({type, _L, nonempty_list, []}, _S, _D, L, C) ->
4736  {t_nonempty_list(), L, C};
4737from_form({type, _L, nonempty_list, [Type]}, S, D, L, C) ->
4738  {T, L1, C1} = from_form(Type, S, D, L - 1, C),
4739  {t_nonempty_list(T), L1, C1};
4740from_form({type, _L, nonempty_improper_list, [Cont, Term]}, S, D, L, C) ->
4741  {T1, L1, C1} = from_form(Cont, S, D, L - 1, C),
4742  {T2, L2, C2} = from_form(Term, S, D, L1, C1),
4743  {t_cons(T1, T2), L2, C2};
4744from_form({type, _L, nonempty_maybe_improper_list, []}, _S, _D, L, C) ->
4745  {t_cons(?any, ?any), L, C};
4746from_form({type, _L, nonempty_maybe_improper_list, [Cont, Term]},
4747          S, D, L, C) ->
4748  {T1, L1, C1} = from_form(Cont, S, D, L - 1, C),
4749  {T2, L2, C2} = from_form(Term, S, D, L1, C1),
4750  {t_cons(T1, T2), L2, C2};
4751from_form({type, _L, nonempty_string, []}, _S, _D, L, C) ->
4752  {t_nonempty_string(), L, C};
4753from_form({type, _L, number, []}, _S, _D, L, C) ->
4754  {t_number(), L, C};
4755from_form({type, _L, pid, []}, _S, _D, L, C) ->
4756  {t_pid(), L, C};
4757from_form({type, _L, port, []}, _S, _D, L, C) ->
4758  {t_port(), L, C};
4759from_form({type, _L, pos_integer, []}, _S, _D, L, C) ->
4760  {t_pos_integer(), L, C};
4761from_form({type, _L, maybe_improper_list, []}, _S, _D, L, C) ->
4762  {t_maybe_improper_list(), L, C};
4763from_form({type, _L, maybe_improper_list, [Content, Termination]},
4764          S, D, L, C) ->
4765  {T1, L1, C1} = from_form(Content, S, D, L - 1, C),
4766  {T2, L2, C2} = from_form(Termination, S, D, L1, C1),
4767  {t_maybe_improper_list(T1, T2), L2, C2};
4768from_form({type, _L, product, Elements}, S, D, L, C) ->
4769  {Lst, L1, C1} = list_from_form(Elements, S, D - 1, L, C),
4770  {t_product(Lst), L1, C1};
4771from_form({type, _L, range, [From, To]} = Type, _S, _D, L, C) ->
4772  case {erl_eval:partial_eval(From), erl_eval:partial_eval(To)} of
4773    {{integer, _, FromVal}, {integer, _, ToVal}} ->
4774      {t_from_range(FromVal, ToVal), L, C};
4775    _ -> throw({error, io_lib:format("Unable to evaluate type ~w\n", [Type])})
4776  end;
4777from_form({type, _L, record, [Name|Fields]}, S, D, L, C) ->
4778  record_from_form(Name, Fields, S, D, L, C);
4779from_form({type, _L, reference, []}, _S, _D, L, C) ->
4780  {t_reference(), L, C};
4781from_form({type, _L, string, []}, _S, _D, L, C) ->
4782  {t_string(), L, C};
4783from_form({type, _L, term, []}, _S, _D, L, C) ->
4784  {t_any(), L, C};
4785from_form({type, _L, timeout, []}, _S, _D, L, C) ->
4786  {t_timeout(), L, C};
4787from_form({type, _L, tuple, any}, _S, _D, L, C) ->
4788  {t_tuple(), L, C};
4789from_form({type, _L, tuple, Args}, S, D, L, C) ->
4790  {Lst, L1, C1} = list_from_form(Args, S, D - 1, L, C),
4791  {t_tuple(Lst), L1, C1};
4792from_form({type, _L, union, Args}, S, D, L, C) ->
4793  {Lst, L1, C1} = list_from_form(Args, S, D, L, C),
4794  {t_sup(Lst), L1, C1};
4795from_form({user_type, _L, Name, Args}, S, D, L, C) ->
4796  type_from_form(Name, Args, S, D, L, C);
4797from_form({type, _L, Name, Args}, S, D, L, C) ->
4798  %% Compatibility: modules compiled before Erlang/OTP 18.0.
4799  type_from_form(Name, Args, S, D, L, C);
4800from_form({opaque, _L, Name, {Mod, Args, Rep}}, _S, _D, L, C) ->
4801  %% XXX. To be removed.
4802  {t_opaque(Mod, Name, Args, Rep), L, C}.
4803
4804builtin_type(Name, Type, S, D, L, C) ->
4805  #from_form{site = Site, mrecs = MR} = S,
4806  M = site_module(Site),
4807  case lookup_module_types(M, MR, C) of
4808    {R, C1} ->
4809      case lookup_type(Name, 0, R) of
4810        {_, {{_M, _FL, _F, _A}, _T}} ->
4811          type_from_form(Name, [], S, D, L, C1);
4812        error ->
4813          {Type, L, C1}
4814      end;
4815    error ->
4816      {Type, L, C}
4817  end.
4818
4819type_from_form(Name, Args, S, D, L, C) ->
4820  #from_form{site = Site, mrecs = MR, tnames = TypeNames} = S,
4821  ArgsLen = length(Args),
4822  Module = site_module(Site),
4823  TypeName = {type, {Module, Name, ArgsLen}},
4824  case can_unfold_more(TypeName, TypeNames) of
4825    true ->
4826      {R, C1} = lookup_module_types(Module, MR, C),
4827      type_from_form1(Name, Args, ArgsLen, R, TypeName, TypeNames, Site,
4828                      S, D, L, C1);
4829    false ->
4830      {t_any(), L, C}
4831  end.
4832
4833type_from_form1(Name, Args, ArgsLen, R, TypeName, TypeNames, Site,
4834                S, D, L, C) ->
4835  case lookup_type(Name, ArgsLen, R) of
4836    {_, {_, _}} when element(1, Site) =:= check ->
4837      {_ArgTypes, L1, C1} = list_from_form(Args, S, D, L, C),
4838      {t_any(), L1, C1};
4839    {Tag, {{Module, _FileName, Form, ArgNames}, Type}} ->
4840      NewTypeNames = [TypeName|TypeNames],
4841      S1 = S#from_form{tnames = NewTypeNames},
4842      {ArgTypes, L1, C1} = list_from_form(Args, S1, D, L, C),
4843      CKey = cache_key(Module, Name, ArgTypes, TypeNames, D),
4844      case cache_find(CKey, C) of
4845        {CachedType, DeltaL} ->
4846          {CachedType, L1 - DeltaL, C};
4847        error ->
4848          List = lists:zip(ArgNames, ArgTypes),
4849          TmpV = maps:from_list(List),
4850          S2 = S1#from_form{site = TypeName, vtab = TmpV},
4851          Fun = fun(DD, LL) -> from_form(Form, S2, DD, LL, C1) end,
4852          {NewType, L3, C3} =
4853            case Tag of
4854              type ->
4855                recur_limit(Fun, D, L1, TypeName, TypeNames);
4856              opaque ->
4857                {Rep, L2, C2} = recur_limit(Fun, D, L1, TypeName, TypeNames),
4858                Rep1 = choose_opaque_type(Rep, Type),
4859                Rep2 = case cannot_have_opaque(Rep1, TypeName, TypeNames) of
4860                         true -> Rep;
4861                         false ->
4862                           ArgTypes2 = subst_all_vars_to_any_list(ArgTypes),
4863                           t_opaque(Module, Name, ArgTypes2, Rep1)
4864                       end,
4865                {Rep2, L2, C2}
4866            end,
4867          C4 = cache_put(CKey, NewType, L1 - L3, C3),
4868          {NewType, L3, C4}
4869      end;
4870    error ->
4871      Msg = io_lib:format("Unable to find type ~tw/~w\n",
4872                          [Name, ArgsLen]),
4873      throw({error, Msg})
4874  end.
4875
4876remote_from_form(RemMod, Name, Args, S, D, L, C) ->
4877  #from_form{site = Site, xtypes = ET, mrecs = MR, tnames = TypeNames} = S,
4878  if
4879    ET =:= replace_by_none ->
4880      {t_none(), L, C};
4881    true ->
4882      ArgsLen = length(Args),
4883      MFA = {RemMod, Name, ArgsLen},
4884      case lookup_module_types(RemMod, MR, C) of
4885        error ->
4886          self() ! {self(), ext_types, MFA},
4887          {t_any(), L, C};
4888        {RemDict, C1} ->
4889          case sets:is_element(MFA, ET) of
4890            true ->
4891              RemType = {type, MFA},
4892              case can_unfold_more(RemType, TypeNames) of
4893                true ->
4894                  remote_from_form1(RemMod, Name, Args, ArgsLen, RemDict,
4895                                    RemType, TypeNames, Site, S, D, L, C1);
4896                false ->
4897                  {t_any(), L, C1}
4898              end;
4899            false ->
4900              self() ! {self(), ext_types, {RemMod, Name, ArgsLen}},
4901              {t_any(), L, C1}
4902          end
4903      end
4904  end.
4905
4906remote_from_form1(RemMod, Name, Args, ArgsLen, RemDict, RemType, TypeNames,
4907                  Site, S, D, L, C) ->
4908  case lookup_type(Name, ArgsLen, RemDict) of
4909    {_, {_, _}} when element(1, Site) =:= check ->
4910      {_ArgTypes, L1, C1} = list_from_form(Args, S, D, L, C),
4911      {t_any(), L1, C1};
4912    {Tag, {{Mod, _FileLine, Form, ArgNames}, Type}} ->
4913      NewTypeNames = [RemType|TypeNames],
4914      S1 = S#from_form{tnames = NewTypeNames},
4915      {ArgTypes, L1, C1} = list_from_form(Args, S1, D, L, C),
4916      CKey = cache_key(RemMod, Name, ArgTypes, TypeNames, D),
4917      case cache_find(CKey, C) of
4918        {CachedType, DeltaL} ->
4919          {CachedType, L - DeltaL, C};
4920        error ->
4921          List = lists:zip(ArgNames, ArgTypes),
4922          TmpVarTab = maps:from_list(List),
4923          S2 = S1#from_form{site = RemType, vtab = TmpVarTab},
4924          Fun = fun(DD, LL) -> from_form(Form, S2, DD, LL, C1) end,
4925          {NewType, L3, C3} =
4926            case Tag of
4927              type ->
4928                recur_limit(Fun, D, L1, RemType, TypeNames);
4929              opaque ->
4930                {NewRep, L2, C2} = recur_limit(Fun, D, L1, RemType, TypeNames),
4931                NewRep1 = choose_opaque_type(NewRep, Type),
4932                NewRep2 =
4933                  case cannot_have_opaque(NewRep1, RemType, TypeNames) of
4934                    true -> NewRep;
4935                    false ->
4936                      ArgTypes2 = subst_all_vars_to_any_list(ArgTypes),
4937                      t_opaque(Mod, Name, ArgTypes2, NewRep1)
4938                  end,
4939                {NewRep2, L2, C2}
4940            end,
4941          C4 = cache_put(CKey, NewType, L1 - L3, C3),
4942          {NewType, L3, C4}
4943      end;
4944    error ->
4945      Msg = io_lib:format("Unable to find remote type ~w:~tw()\n",
4946                          [RemMod, Name]),
4947      throw({error, Msg})
4948  end.
4949
4950subst_all_vars_to_any_list(Types) ->
4951  [subst_all_vars_to_any(Type) || Type <- Types].
4952
4953%% Opaque types (both local and remote) are problematic when it comes
4954%% to the limits (TypeNames, D, and L). The reason is that if any() is
4955%% substituted for a more specialized subtype of an opaque type, the
4956%% property stated along with decorate_with_opaque() (the type has to
4957%% be a subtype of the declared type) no longer holds.
4958%%
4959%% The less than perfect remedy: if the opaque type created from a
4960%% form is not a subset of the declared type, the declared type is
4961%% used instead, effectively bypassing the limits, and potentially
4962%% resulting in huge types.
4963choose_opaque_type(Type, DeclType) ->
4964  case
4965    t_is_subtype(subst_all_vars_to_any(Type),
4966                 subst_all_vars_to_any(DeclType))
4967  of
4968    true -> Type;
4969    false -> DeclType
4970  end.
4971
4972record_from_form({atom, _, Name}, ModFields, S, D0, L0, C) ->
4973  #from_form{site = Site, mrecs = MR, tnames = TypeNames} = S,
4974  RecordType = {record, Name},
4975  case can_unfold_more(RecordType, TypeNames) of
4976    true ->
4977      M = site_module(Site),
4978      {R, C1} = lookup_module_types(M, MR, C),
4979      case lookup_record(Name, R) of
4980        {ok, _} when element(1, Site) =:= check ->
4981          {t_any(), L0, C1};
4982        {ok, DeclFields} ->
4983          NewTypeNames = [RecordType|TypeNames],
4984          Site1 = {record, {M, Name, length(DeclFields)}},
4985          S1 = S#from_form{site = Site1, tnames = NewTypeNames},
4986          Fun = fun(D, L) ->
4987                    {GetModRec, L1, C2} =
4988                      get_mod_record(ModFields, DeclFields, S1, D, L, C1),
4989                    case GetModRec of
4990                      {error, FieldName} ->
4991                        throw({error,
4992                               io_lib:format("Illegal declaration of #~tw{~tw}\n",
4993                                             [Name, FieldName])});
4994                      {ok, NewFields} ->
4995                        S2 = S1#from_form{vtab = var_table__new()},
4996                        {NewFields1, L2, C3} =
4997                          fields_from_form(NewFields, S2, D, L1, C2),
4998                        Rec = t_tuple(
4999                                [t_atom(Name)|[Type
5000                                               || {_FieldName, Type} <- NewFields1]]),
5001                        {Rec, L2, C3}
5002                    end
5003                end,
5004          recur_limit(Fun, D0, L0, RecordType, TypeNames);
5005        error ->
5006          throw({error, io_lib:format("Unknown record #~tw{}\n", [Name])})
5007      end;
5008    false ->
5009       {t_any(), L0, C}
5010  end.
5011
5012get_mod_record([], DeclFields, _S, _D, L, C) ->
5013  {{ok, DeclFields}, L, C};
5014get_mod_record(ModFields, DeclFields, S, D, L, C) ->
5015  DeclFieldsDict = lists:keysort(1, DeclFields),
5016  {ModFieldsDict, L1, C1} = build_field_dict(ModFields, S, D, L, C),
5017  case get_mod_record_types(DeclFieldsDict, ModFieldsDict, []) of
5018    {error, _FieldName} = Error -> {Error, L1, C1};
5019    {ok, FinalKeyDict} ->
5020      Fields = [lists:keyfind(FieldName, 1, FinalKeyDict)
5021             || {FieldName, _, _} <- DeclFields],
5022      {{ok, Fields}, L1, C1}
5023  end.
5024
5025build_field_dict(FieldTypes, S, D, L, C) ->
5026  build_field_dict(FieldTypes, S, D, L, C, []).
5027
5028build_field_dict([{type, _, field_type, [{atom, _, Name}, Type]}|Left],
5029		 S, D, L, C, Acc) ->
5030  {T, L1, C1} = from_form(Type, S, D, L - 1, C),
5031  NewAcc = [{Name, Type, T}|Acc],
5032  build_field_dict(Left, S, D, L1, C1, NewAcc);
5033build_field_dict([], _S, _D, L, C, Acc) ->
5034  {lists:keysort(1, Acc), L, C}.
5035
5036get_mod_record_types([{FieldName, _Abstr, _DeclType}|Left1],
5037                     [{FieldName, TypeForm, ModType}|Left2],
5038                     Acc) ->
5039  get_mod_record_types(Left1, Left2, [{FieldName, TypeForm, ModType}|Acc]);
5040get_mod_record_types([{FieldName1, _Abstr, _DeclType} = DT|Left1],
5041                     [{FieldName2, _FormType, _ModType}|_] = List2,
5042                     Acc) when FieldName1 < FieldName2 ->
5043  get_mod_record_types(Left1, List2, [DT|Acc]);
5044get_mod_record_types(Left1, [], Acc) ->
5045  {ok, lists:keysort(1, Left1++Acc)};
5046get_mod_record_types(_, [{FieldName2, _FormType, _ModType}|_], _Acc) ->
5047  {error, FieldName2}.
5048
5049%% It is important to create a limited version of the record type
5050%% since nested record types can otherwise easily result in huge
5051%% terms.
5052fields_from_form([], _S, _D, L, C) ->
5053  {[], L, C};
5054fields_from_form([{Name, Abstr, _Type}|Tail], S, D, L, C) ->
5055  {T, L1, C1} = from_form(Abstr, S, D, L, C),
5056  {F, L2, C2} = fields_from_form(Tail, S, D, L1, C1),
5057  {[{Name, T}|F], L2, C2}.
5058
5059list_from_form([], _S, _D, L, C) ->
5060  {[], L, C};
5061list_from_form([H|Tail], S, D, L, C) ->
5062  {H1, L1, C1} = from_form(H, S, D, L - 1, C),
5063  {T1, L2, C2} = list_from_form(Tail, S, D, L1, C1),
5064  {[H1|T1], L2, C2}.
5065
5066%% Separates singleton types in keys (see is_singleton_type/1).
5067singleton_elements([]) ->
5068  [];
5069singleton_elements([{K,?mand,V}=Pair|Pairs]) ->
5070  case is_singleton_type(K) of
5071    true ->
5072      [Pair|singleton_elements(Pairs)];
5073    false ->
5074      singleton_elements([{K,?opt,V}|Pairs])
5075  end;
5076singleton_elements([{Key0,MNess,Val}|Pairs]) ->
5077  [{Key,MNess,Val} || Key <- separate_key(Key0)] ++ singleton_elements(Pairs).
5078
5079%% To be in sync with is_singleton_type/1.
5080%% Does not separate tuples and maps as doing that has potential
5081%% to be very expensive.
5082separate_key(?atom(Atoms)) when Atoms =/= ?any ->
5083  [t_atom(A) || A <- Atoms];
5084separate_key(?number(_, _) = T) ->
5085  t_elements(T);
5086separate_key(?union(List)) ->
5087  lists:append([separate_key(K) || K <- List, not t_is_none(K)]);
5088separate_key(Key) -> [Key].
5089
5090%% Sorts, combines non-singleton pairs, and applies precendence and
5091%% mandatoriness rules.
5092map_from_form([], ShdwPs, MKs, Pairs, DefK, DefV) ->
5093  verify_possible(MKs, ShdwPs),
5094  {promote_to_mand(MKs, Pairs), DefK, DefV};
5095map_from_form([{SKey,MNess,Val}|SPairs], ShdwPs0, MKs0, Pairs0, DefK0, DefV0) ->
5096  Key = lists:foldl(fun({K,_},S)->t_subtract(S,K)end, SKey, ShdwPs0),
5097  ShdwPs = case Key of ?none -> ShdwPs0; _ -> [{Key,Val}|ShdwPs0] end,
5098  MKs = case MNess of ?mand -> [SKey|MKs0]; ?opt -> MKs0 end,
5099  if MNess =:= ?mand, SKey =:= ?none -> throw(none);
5100     true -> ok
5101  end,
5102  {Pairs, DefK, DefV} =
5103    case is_singleton_type(Key) of
5104      true ->
5105	MNess1 = case Val =:= ?none of true -> ?opt; false -> MNess end,
5106	{mapdict_insert({Key,MNess1,Val}, Pairs0), DefK0, DefV0};
5107      false ->
5108	case Key =:= ?none orelse Val =:= ?none of
5109	  true  -> {Pairs0, DefK0,             DefV0};
5110	  false -> {Pairs0, t_sup(DefK0, Key), t_sup(DefV0, Val)}
5111	end
5112    end,
5113  map_from_form(SPairs, ShdwPs, MKs, Pairs, DefK, DefV).
5114
5115%% Verifies that all mandatory keys are possible, throws 'none' otherwise
5116verify_possible(MKs, ShdwPs) ->
5117  lists:foreach(fun(M) -> verify_possible_1(M, ShdwPs) end, MKs).
5118
5119verify_possible_1(M, ShdwPs) ->
5120  case lists:any(fun({K,_}) -> t_inf(M, K) =/= ?none end, ShdwPs) of
5121    true -> ok;
5122    false -> throw(none)
5123  end.
5124
5125-spec promote_to_mand([erl_type()], t_map_dict()) -> t_map_dict().
5126
5127promote_to_mand(_, []) -> [];
5128promote_to_mand(MKs, [E={K,_,V}|T]) ->
5129  [case lists:any(fun(M) -> t_is_equal(K,M) end, MKs) of
5130     true -> {K, ?mand, V};
5131     false -> E
5132   end|promote_to_mand(MKs, T)].
5133
5134-define(RECUR_EXPAND_LIMIT, 10).
5135-define(RECUR_EXPAND_DEPTH, 2).
5136
5137%% If more of the limited resources is spent on the non-recursive
5138%% forms, more warnings are found. And the analysis is also a bit
5139%% faster.
5140%%
5141%% Setting REC_TYPE_LIMIT to 1 would work also work well.
5142
5143recur_limit(Fun, D, L, _, _) when L =< ?RECUR_EXPAND_DEPTH,
5144                                  D =< ?RECUR_EXPAND_LIMIT ->
5145  Fun(D, L);
5146recur_limit(Fun, D, L, TypeName, TypeNames) ->
5147  case is_recursive(TypeName, TypeNames) of
5148    true ->
5149      {T, L1, C1} = Fun(?RECUR_EXPAND_DEPTH, ?RECUR_EXPAND_LIMIT),
5150      {T, L - L1, C1};
5151    false ->
5152      Fun(D, L)
5153  end.
5154
5155-spec t_check_record_fields(parse_form(), sets:set(mfa()), site(),
5156                            mod_type_table(), var_table(), cache()) -> cache().
5157
5158t_check_record_fields(Form, ExpTypes, Site, RecDict, VarTable, Cache) ->
5159  State = #from_form{site   = Site,
5160                     xtypes = ExpTypes,
5161                     mrecs  = RecDict,
5162                     vtab   = VarTable,
5163                     tnames = []},
5164  check_record_fields(Form, State, Cache).
5165
5166-spec check_record_fields(parse_form(), #from_form{}, cache()) -> cache().
5167
5168%% If there is something wrong with parse_form()
5169%% throw({error, io_lib:chars()} is called.
5170
5171check_record_fields({var, _L, _}, _S, C) -> C;
5172check_record_fields({ann_type, _L, [_Var, Type]}, S, C) ->
5173  check_record_fields(Type, S, C);
5174check_record_fields({paren_type, _L, [Type]}, S, C) ->
5175  check_record_fields(Type, S, C);
5176check_record_fields({remote_type, _L, [{atom, _, _}, {atom, _, _}, Args]},
5177                    S, C) ->
5178  list_check_record_fields(Args, S, C);
5179check_record_fields({atom, _L, _}, _S, C) -> C;
5180check_record_fields({integer, _L, _}, _S, C) -> C;
5181check_record_fields({char, _L, _}, _S, C) -> C;
5182check_record_fields({op, _L, _Op, _Arg}, _S, C) -> C;
5183check_record_fields({op, _L, _Op, _Arg1, _Arg2}, _S, C) -> C;
5184check_record_fields({type, _L, tuple, any}, _S, C) -> C;
5185check_record_fields({type, _L, map, any}, _S, C) -> C;
5186check_record_fields({type, _L, binary, [_Base, _Unit]}, _S, C) -> C;
5187check_record_fields({type, _L, 'fun', [{type, _, any}, Range]}, S, C) ->
5188  check_record_fields(Range, S, C);
5189check_record_fields({type, _L, range, [_From, _To]}, _S, C) -> C;
5190check_record_fields({type, _L, record, [Name|Fields]}, S, C) ->
5191  check_record(Name, Fields, S, C);
5192check_record_fields({type, _L, _, Args}, S, C) ->
5193  list_check_record_fields(Args, S, C);
5194check_record_fields({user_type, _L, _Name, Args}, S, C) ->
5195  list_check_record_fields(Args, S, C).
5196
5197check_record({atom, _, Name}, ModFields, S, C) ->
5198  #from_form{site = Site, mrecs = MR} = S,
5199  M = site_module(Site),
5200  {R, C1} = lookup_module_types(M, MR, C),
5201  {ok, DeclFields} = lookup_record(Name, R),
5202  case check_fields(Name, ModFields, DeclFields, S, C1) of
5203    {error, FieldName} ->
5204      throw({error, io_lib:format("Illegal declaration of #~tw{~tw}\n",
5205                                  [Name, FieldName])});
5206    C2 -> C2
5207  end.
5208
5209check_fields(RecName, [{type, _, field_type, [{atom, _, Name}, Abstr]}|Left],
5210             DeclFields, S, C) ->
5211  #from_form{site = Site0, xtypes = ET, mrecs = MR, vtab = V} = S,
5212  M = site_module(Site0),
5213  Site = {record, {M, RecName, length(DeclFields)}},
5214  {Type, C1} = t_from_form(Abstr, ET, Site, MR, V, C),
5215  {Name, _, DeclType} = lists:keyfind(Name, 1, DeclFields),
5216  TypeNoVars = subst_all_vars_to_any(Type),
5217  case t_is_subtype(TypeNoVars, DeclType) of
5218    false -> {error, Name};
5219    true -> check_fields(RecName, Left, DeclFields, S, C1)
5220  end;
5221check_fields(_RecName, [], _Decl, _S, C) ->
5222  C.
5223
5224list_check_record_fields([], _S, C) ->
5225  C;
5226list_check_record_fields([H|Tail], S, C) ->
5227  C1 = check_record_fields(H, S, C),
5228  list_check_record_fields(Tail, S, C1).
5229
5230site_module({_, {Module, _, _}}) ->
5231  Module.
5232
5233-spec cache__new() -> cache().
5234
5235cache__new() ->
5236  #cache{}.
5237
5238-spec cache_key(module(), atom(), [erl_type()],
5239                type_names(), expand_depth()) -> cache_key().
5240
5241%% If TypeNames is left out from the key, the cache is smaller, and
5242%% the form-to-type translation is faster. But it would be a shame if,
5243%% for example, any() is used, where a more complex type should be
5244%% used. There is also a slight risk of creating unnecessarily big
5245%% types.
5246
5247cache_key(Module, Name, ArgTypes, TypeNames, D) ->
5248  {Module, Name, D, ArgTypes, TypeNames}.
5249
5250-spec cache_find(cache_key(), cache()) ->
5251                    {erl_type(), expand_limit()} | 'error'.
5252
5253cache_find(Key, #cache{types = Types}) ->
5254  case maps:find(Key, Types) of
5255    {ok, Value} ->
5256      Value;
5257    error ->
5258      error
5259  end.
5260
5261-spec cache_put(cache_key(), erl_type(), expand_limit(), cache()) -> cache().
5262
5263cache_put(_Key, _Type, DeltaL, Cache) when DeltaL < 0 ->
5264  %% The type is truncated; do not reuse it.
5265  Cache;
5266cache_put(Key, Type, DeltaL, #cache{types = Types} = Cache) ->
5267  NewTypes = maps:put(Key, {Type, DeltaL}, Types),
5268  Cache#cache{types = NewTypes}.
5269
5270-spec t_var_names([parse_form()]) -> [atom()].
5271
5272t_var_names([{var, _, Name}|L]) when Name =/= '_' ->
5273  [Name|t_var_names(L)];
5274t_var_names([]) ->
5275  [].
5276
5277-spec t_form_to_string(parse_form()) -> string().
5278
5279t_form_to_string({var, _L, '_'}) -> "_";
5280t_form_to_string({var, _L, Name}) -> atom_to_list(Name);
5281t_form_to_string({atom, _L, Atom}) ->
5282  io_lib:write_string(atom_to_list(Atom), $'); % To quote or not to quote... '
5283t_form_to_string({integer, _L, Int}) -> integer_to_list(Int);
5284t_form_to_string({char, _L, Char}) -> integer_to_list(Char);
5285t_form_to_string({op, _L, _Op, _Arg} = Op) ->
5286  case erl_eval:partial_eval(Op) of
5287    {integer, _, _} = Int -> t_form_to_string(Int);
5288    _ -> io_lib:format("Badly formed type ~w", [Op])
5289  end;
5290t_form_to_string({op, _L, _Op, _Arg1, _Arg2} = Op) ->
5291  case erl_eval:partial_eval(Op) of
5292    {integer, _, _} = Int -> t_form_to_string(Int);
5293    _ -> io_lib:format("Badly formed type ~w", [Op])
5294  end;
5295t_form_to_string({ann_type, _L, [Var, Type]}) ->
5296  t_form_to_string(Var) ++ "::" ++ t_form_to_string(Type);
5297t_form_to_string({paren_type, _L, [Type]}) ->
5298  flat_format("(~ts)", [t_form_to_string(Type)]);
5299t_form_to_string({remote_type, _L, [{atom, _, Mod}, {atom, _, Name}, Args]}) ->
5300  ArgString = "(" ++ flat_join(t_form_to_string_list(Args), ",") ++ ")",
5301  flat_format("~w:~tw", [Mod, Name]) ++ ArgString;
5302t_form_to_string({type, _L, arity, []}) -> "arity()";
5303t_form_to_string({type, _L, binary, []}) -> "binary()";
5304t_form_to_string({type, _L, binary, [Base, Unit]} = Type) ->
5305  case {erl_eval:partial_eval(Base), erl_eval:partial_eval(Unit)} of
5306    {{integer, _, B}, {integer, _, U}} ->
5307      %% the following mirrors the clauses of t_to_string/2
5308      case {U, B} of
5309	{0, 0} -> "<<>>";
5310	{8, 0} -> "binary()";
5311	{1, 0} -> "bitstring()";
5312	{0, B} -> flat_format("<<_:~w>>", [B]);
5313	{U, 0} -> flat_format("<<_:_*~w>>", [U]);
5314	{U, B} -> flat_format("<<_:~w,_:_*~w>>", [B, U])
5315      end;
5316    _ -> io_lib:format("Badly formed bitstr type ~w", [Type])
5317  end;
5318t_form_to_string({type, _L, bitstring, []}) -> "bitstring()";
5319t_form_to_string({type, _L, 'fun', []}) -> "fun()";
5320t_form_to_string({type, _L, 'fun', [{type, _, any}, Range]}) ->
5321  "fun(...) -> " ++ t_form_to_string(Range);
5322t_form_to_string({type, _L, 'fun', [{type, _, product, Domain}, Range]}) ->
5323  "fun((" ++ flat_join(t_form_to_string_list(Domain), ",") ++ ") -> "
5324    ++ t_form_to_string(Range) ++ ")";
5325t_form_to_string({type, _L, iodata, []}) -> "iodata()";
5326t_form_to_string({type, _L, iolist, []}) -> "iolist()";
5327t_form_to_string({type, _L, list, [Type]}) ->
5328  "[" ++ t_form_to_string(Type) ++ "]";
5329t_form_to_string({type, _L, map, any}) -> "map()";
5330t_form_to_string({type, _L, map, Args}) ->
5331  "#{" ++ flat_join(t_form_to_string_list(Args), ",") ++ "}";
5332t_form_to_string({type, _L, map_field_assoc, [Key, Val]}) ->
5333  t_form_to_string(Key) ++ "=>" ++ t_form_to_string(Val);
5334t_form_to_string({type, _L, map_field_exact, [Key, Val]}) ->
5335  t_form_to_string(Key) ++ ":=" ++ t_form_to_string(Val);
5336t_form_to_string({type, _L, mfa, []}) -> "mfa()";
5337t_form_to_string({type, _L, module, []}) -> "module()";
5338t_form_to_string({type, _L, node, []}) -> "node()";
5339t_form_to_string({type, _L, nonempty_list, [Type]}) ->
5340  "[" ++ t_form_to_string(Type) ++ ",...]";
5341t_form_to_string({type, _L, nonempty_string, []}) -> "nonempty_string()";
5342t_form_to_string({type, _L, product, Elements}) ->
5343  "<" ++ flat_join(t_form_to_string_list(Elements), ",") ++ ">";
5344t_form_to_string({type, _L, range, [From, To]} = Type) ->
5345  case {erl_eval:partial_eval(From), erl_eval:partial_eval(To)} of
5346    {{integer, _, FromVal}, {integer, _, ToVal}} ->
5347      flat_format("~w..~w", [FromVal, ToVal]);
5348    _ -> flat_format("Badly formed type ~w",[Type])
5349  end;
5350t_form_to_string({type, _L, record, [{atom, _, Name}]}) ->
5351  flat_format("#~tw{}", [Name]);
5352t_form_to_string({type, _L, record, [{atom, _, Name}|Fields]}) ->
5353  FieldString = flat_join(t_form_to_string_list(Fields), ","),
5354  flat_format("#~tw{~ts}", [Name, FieldString]);
5355t_form_to_string({type, _L, field_type, [{atom, _, Name}, Type]}) ->
5356  flat_format("~tw::~ts", [Name, t_form_to_string(Type)]);
5357t_form_to_string({type, _L, term, []}) -> "term()";
5358t_form_to_string({type, _L, timeout, []}) -> "timeout()";
5359t_form_to_string({type, _L, tuple, any}) -> "tuple()";
5360t_form_to_string({type, _L, tuple, Args}) ->
5361  "{" ++ flat_join(t_form_to_string_list(Args), ",") ++ "}";
5362t_form_to_string({type, _L, union, Args}) ->
5363  flat_join(lists:map(fun(Arg) ->
5364                          case Arg of
5365                            {ann_type, _AL, _} ->
5366                              "(" ++ t_form_to_string(Arg) ++ ")";
5367                            _ ->
5368                              t_form_to_string(Arg)
5369                          end
5370                      end, Args),
5371            " | ");
5372t_form_to_string({type, _L, Name, []} = T) ->
5373   try
5374     M = mod,
5375     Site = {type, {M,Name,0}},
5376     V = var_table__new(),
5377     C = cache__new(),
5378     State = #from_form{site   = Site,
5379                        xtypes = sets:new(),
5380                        mrecs  = 'undefined',
5381                        vtab   = V,
5382                        tnames = []},
5383     {T1, _, _} = from_form(T, State, _Deep=1000, _ALot=1000000, C),
5384     t_to_string(T1)
5385  catch throw:{error, _} -> atom_to_string(Name) ++ "()"
5386  end;
5387t_form_to_string({user_type, _L, Name, List}) ->
5388  flat_format("~tw(~ts)",
5389              [Name, flat_join(t_form_to_string_list(List), ",")]);
5390t_form_to_string({type, L, Name, List}) ->
5391  %% Compatibility: modules compiled before Erlang/OTP 18.0.
5392  t_form_to_string({user_type, L, Name, List}).
5393
5394t_form_to_string_list(List) ->
5395  t_form_to_string_list(List, []).
5396
5397t_form_to_string_list([H|T], Acc) ->
5398  t_form_to_string_list(T, [t_form_to_string(H)|Acc]);
5399t_form_to_string_list([], Acc) ->
5400  lists:reverse(Acc).
5401
5402-spec atom_to_string(atom()) -> string().
5403
5404atom_to_string(Atom) ->
5405  flat_format("~tw", [Atom]).
5406
5407%%=============================================================================
5408%%
5409%% Utilities
5410%%
5411%%=============================================================================
5412
5413-spec any_none([erl_type()]) -> boolean().
5414
5415any_none([?none|_Left]) -> true;
5416any_none([_|Left]) -> any_none(Left);
5417any_none([]) -> false.
5418
5419-spec any_none_or_unit([erl_type()]) -> boolean().
5420
5421any_none_or_unit([?none|_]) -> true;
5422any_none_or_unit([?unit|_]) -> true;
5423any_none_or_unit([_|Left]) -> any_none_or_unit(Left);
5424any_none_or_unit([]) -> false.
5425
5426-spec is_erl_type(any()) -> boolean().
5427
5428is_erl_type(?any) -> true;
5429is_erl_type(?none) -> true;
5430is_erl_type(?unit) -> true;
5431is_erl_type(#c{}) -> true;
5432is_erl_type(_) -> false.
5433
5434-spec lookup_module_types(module(), mod_type_table(), cache()) ->
5435                             'error' | {type_table(), cache()}.
5436
5437lookup_module_types(Module, CodeTable, Cache) ->
5438  #cache{mod_recs = {mrecs, MRecs}} = Cache,
5439  case dict:find(Module, MRecs) of
5440    {ok, R} ->
5441      {R, Cache};
5442    error ->
5443      try ets:lookup_element(CodeTable, Module, 2) of
5444        R ->
5445          NewMRecs = dict:store(Module, R, MRecs),
5446          {R, Cache#cache{mod_recs = {mrecs, NewMRecs}}}
5447      catch
5448        _:_ -> error
5449      end
5450  end.
5451
5452-spec lookup_record(atom(), type_table()) ->
5453        'error' | {'ok', [{atom(), parse_form(), erl_type()}]}.
5454
5455lookup_record(Tag, Table) when is_atom(Tag) ->
5456  case maps:find({record, Tag}, Table) of
5457    {ok, {_FileLine, [{_Arity, Fields}]}} ->
5458      {ok, Fields};
5459    {ok, {_FileLine, List}} when is_list(List) ->
5460      %% This will have to do, since we do not know which record we
5461      %% are looking for.
5462      error;
5463    error ->
5464      error
5465  end.
5466
5467-spec lookup_record(atom(), arity(), type_table()) ->
5468        'error' | {'ok', [{atom(), parse_form(), erl_type()}]}.
5469
5470lookup_record(Tag, Arity, Table) when is_atom(Tag) ->
5471  case maps:find({record, Tag}, Table) of
5472    {ok, {_FileLine, [{Arity, Fields}]}} -> {ok, Fields};
5473    {ok, {_FileLine, OrdDict}} -> orddict:find(Arity, OrdDict);
5474    error -> error
5475  end.
5476
5477-spec lookup_type(_, _, _) -> {'type' | 'opaque', type_value()} | 'error'.
5478lookup_type(Name, Arity, Table) ->
5479  case maps:find({type, Name, Arity}, Table) of
5480    error ->
5481      case maps:find({opaque, Name, Arity}, Table) of
5482	error -> error;
5483	{ok, Found} -> {opaque, Found}
5484      end;
5485    {ok, Found} -> {type, Found}
5486  end.
5487
5488-spec type_is_defined('type' | 'opaque', atom(), arity(), type_table()) ->
5489        boolean().
5490
5491type_is_defined(TypeOrOpaque, Name, Arity, Table) ->
5492  maps:is_key({TypeOrOpaque, Name, Arity}, Table).
5493
5494cannot_have_opaque(Type, TypeName, TypeNames) ->
5495  t_is_none(Type) orelse is_recursive(TypeName, TypeNames).
5496
5497is_recursive(TypeName, TypeNames) ->
5498  lists:member(TypeName, TypeNames).
5499
5500can_unfold_more(TypeName, TypeNames) ->
5501  Fun = fun(E, Acc) -> case E of TypeName -> Acc + 1; _ -> Acc end end,
5502  lists:foldl(Fun, 0, TypeNames) < ?REC_TYPE_LIMIT.
5503
5504-spec do_opaque(erl_type(), opaques(), fun((_) -> T)) -> T.
5505
5506%% Probably a little faster than calling t_unopaque/2.
5507%% Unions that are due to opaque types are unopaqued.
5508do_opaque(?opaque(_) = Type, Opaques, Pred) ->
5509  case Opaques =:= 'universe' orelse is_opaque_type(Type, Opaques) of
5510    true -> do_opaque(t_opaque_structure(Type), Opaques, Pred);
5511    false -> Pred(Type)
5512  end;
5513do_opaque(?union(List) = Type, Opaques, Pred) ->
5514  [A,B,F,I,L,N,T,M,O,Map] = List,
5515  if O =:= ?none -> Pred(Type);
5516    true ->
5517      case Opaques =:= 'universe' orelse is_opaque_type(O, Opaques) of
5518        true ->
5519          S = t_opaque_structure(O),
5520          do_opaque(t_sup([A,B,F,I,L,N,T,M,S,Map]), Opaques, Pred);
5521        false -> Pred(Type)
5522      end
5523  end;
5524do_opaque(Type, _Opaques, Pred) ->
5525  Pred(Type).
5526
5527map_all_values(?map(Pairs,_,DefV)) ->
5528  [DefV|[V || {V, _, _} <- Pairs]].
5529
5530map_all_keys(?map(Pairs,DefK,_)) ->
5531  [DefK|[K || {_, _, K} <- Pairs]].
5532
5533map_all_types(M) ->
5534  map_all_keys(M) ++ map_all_values(M).
5535
5536%% Tests if a type has exactly one possible value.
5537-spec t_is_singleton(erl_type()) -> boolean().
5538
5539t_is_singleton(Type) ->
5540  t_is_singleton(Type, 'universe').
5541
5542-spec t_is_singleton(erl_type(), opaques()) -> boolean().
5543
5544t_is_singleton(Type, Opaques) ->
5545  do_opaque(Type, Opaques, fun is_singleton_type/1).
5546
5547%% To be in sync with separate_key/1.
5548%% Used to also recognize maps and tuples.
5549is_singleton_type(?nil) -> true;
5550is_singleton_type(?atom(?any)) -> false;
5551is_singleton_type(?atom(Set)) ->
5552  ordsets:size(Set) =:= 1;
5553is_singleton_type(?int_range(V, V)) -> true;
5554is_singleton_type(?int_set(Set)) ->
5555  ordsets:size(Set) =:= 1;
5556is_singleton_type(_) ->
5557  false.
5558
5559%% Returns the only possible value of a singleton type.
5560-spec t_singleton_to_term(erl_type(), opaques()) -> term().
5561
5562t_singleton_to_term(Type, Opaques) ->
5563  do_opaque(Type, Opaques, fun singleton_type_to_term/1).
5564
5565singleton_type_to_term(?nil) -> [];
5566singleton_type_to_term(?atom(Set)) when Set =/= ?any ->
5567  case ordsets:size(Set) of
5568    1 -> hd(ordsets:to_list(Set));
5569    _ -> error(badarg)
5570  end;
5571singleton_type_to_term(?int_range(V, V)) -> V;
5572singleton_type_to_term(?int_set(Set)) ->
5573  case ordsets:size(Set) of
5574    1 -> hd(ordsets:to_list(Set));
5575    _ -> error(badarg)
5576  end;
5577singleton_type_to_term(?tuple(Types, Arity, _)) when is_integer(Arity) ->
5578  lists:map(fun singleton_type_to_term/1, Types);
5579singleton_type_to_term(?tuple_set([{Arity, [OnlyTuple]}]))
5580  when is_integer(Arity) ->
5581  singleton_type_to_term(OnlyTuple);
5582singleton_type_to_term(?map(Pairs, ?none, ?none)) ->
5583  maps:from_list([{singleton_type_to_term(K), singleton_type_to_term(V)}
5584		  || {K,?mand,V} <- Pairs]).
5585
5586%% -----------------------------------
5587%% Set
5588%%
5589
5590set_singleton(Element) ->
5591  ordsets:from_list([Element]).
5592
5593set_is_singleton(Element, Set) ->
5594  set_singleton(Element) =:= Set.
5595
5596set_is_element(Element, Set) ->
5597  ordsets:is_element(Element, Set).
5598
5599set_union(?any, _) -> ?any;
5600set_union(_, ?any) -> ?any;
5601set_union(S1, S2)  ->
5602  case ordsets:union(S1, S2) of
5603    S when length(S) =< ?SET_LIMIT -> S;
5604    _ -> ?any
5605  end.
5606
5607%% The intersection and subtraction can return ?none.
5608%% This should always be handled right away since ?none is not a valid set.
5609%% However, ?any is considered a valid set.
5610
5611set_intersection(?any, S) -> S;
5612set_intersection(S, ?any) -> S;
5613set_intersection(S1, S2)  ->
5614  case ordsets:intersection(S1, S2) of
5615    [] -> ?none;
5616    S -> S
5617  end.
5618
5619set_subtract(_, ?any) -> ?none;
5620set_subtract(?any, _) -> ?any;
5621set_subtract(S1, S2) ->
5622  case ordsets:subtract(S1, S2) of
5623    [] -> ?none;
5624    S -> S
5625  end.
5626
5627set_from_list(List) ->
5628  case length(List) of
5629    L when L =< ?SET_LIMIT -> ordsets:from_list(List);
5630    L when L > ?SET_LIMIT -> ?any
5631  end.
5632
5633set_to_list(Set) ->
5634  ordsets:to_list(Set).
5635
5636set_filter(Fun, Set) ->
5637  case ordsets:filter(Fun, Set) of
5638    [] -> ?none;
5639    NewSet -> NewSet
5640  end.
5641
5642set_size(Set) ->
5643  ordsets:size(Set).
5644
5645set_to_string(Set) ->
5646  L = [case is_atom(X) of
5647	 true -> io_lib:write_string(atom_to_list(X), $'); % stupid emacs '
5648	 false -> flat_format("~tw", [X])
5649       end || X <- set_to_list(Set)],
5650  flat_join(L, " | ").
5651
5652set_min([H|_]) -> H.
5653
5654set_max(Set) ->
5655  hd(lists:reverse(Set)).
5656
5657flat_format(F, S) ->
5658  lists:flatten(io_lib:format(F, S)).
5659
5660flat_join(List, Sep) ->
5661  lists:flatten(lists:join(Sep, List)).
5662
5663%%=============================================================================
5664%%
5665%% Utilities for the binary type
5666%%
5667%%=============================================================================
5668
5669-spec gcd(integer(), integer()) -> integer().
5670
5671gcd(A, B) when B > A ->
5672  gcd1(B, A);
5673gcd(A, B) ->
5674  gcd1(A, B).
5675
5676-spec gcd1(integer(), integer()) -> integer().
5677
5678gcd1(A, 0) -> A;
5679gcd1(A, B) ->
5680  case A rem B of
5681    0 -> B;
5682    X -> gcd1(B, X)
5683  end.
5684
5685-spec bitstr_concat(erl_type(), erl_type()) -> erl_type().
5686
5687bitstr_concat(?none, _) -> ?none;
5688bitstr_concat(_, ?none) -> ?none;
5689bitstr_concat(?bitstr(U1, B1), ?bitstr(U2, B2)) ->
5690  t_bitstr(gcd(U1, U2), B1+B2).
5691
5692-spec bitstr_match(erl_type(), erl_type()) -> erl_type().
5693
5694bitstr_match(?none, _) -> ?none;
5695bitstr_match(_, ?none) -> ?none;
5696bitstr_match(?bitstr(0, B1), ?bitstr(0, B2)) when B1 =< B2 ->
5697  t_bitstr(0, B2-B1);
5698bitstr_match(?bitstr(0, _B1), ?bitstr(0, _B2)) ->
5699  ?none;
5700bitstr_match(?bitstr(0, B1), ?bitstr(U2, B2)) when B1 =< B2 ->
5701  t_bitstr(U2, B2-B1);
5702bitstr_match(?bitstr(0, B1), ?bitstr(U2, B2))  ->
5703  t_bitstr(U2, handle_base(U2, B2-B1));
5704bitstr_match(?bitstr(_, B1), ?bitstr(0, B2)) when B1 > B2 ->
5705  ?none;
5706bitstr_match(?bitstr(U1, B1), ?bitstr(U2, B2)) ->
5707  GCD = gcd(U1, U2),
5708  t_bitstr(GCD, handle_base(GCD, B2-B1)).
5709
5710-spec handle_base(integer(), integer()) -> integer().
5711
5712handle_base(Unit, Pos) when Pos >= 0 ->
5713  Pos rem Unit;
5714handle_base(Unit, Neg) ->
5715  (Unit+(Neg rem Unit)) rem Unit.
5716
5717family(L) ->
5718  R = sofs:relation(L),
5719  F = sofs:relation_to_family(R),
5720  sofs:to_external(F).
5721
5722%%=============================================================================
5723%%
5724%% Interface functions for abstract data types defined in this module
5725%%
5726%%=============================================================================
5727
5728-spec var_table__new() -> var_table().
5729
5730var_table__new() ->
5731  maps:new().
5732