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