1%%
2%% %CopyrightBegin%
3%%
4%% Copyright Ericsson AB 2019. All Rights Reserved.
5%%
6%% Licensed under the Apache License, Version 2.0 (the "License");
7%% you may not use this file except in compliance with the License.
8%% You may obtain a copy of the License at
9%%
10%%     http://www.apache.org/licenses/LICENSE-2.0
11%%
12%% Unless required by applicable law or agreed to in writing, software
13%% distributed under the License is distributed on an "AS IS" BASIS,
14%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15%% See the License for the specific language governing permissions and
16%% limitations under the License.
17%%
18%% %CopyrightEnd%
19%%
20
21-module(beam_types).
22
23-define(BEAM_TYPES_INTERNAL, true).
24-include("beam_types.hrl").
25
26-import(lists, [foldl/3, reverse/1]).
27
28-export([meet/1, meet/2, join/1, join/2, subtract/2]).
29
30-export([is_boolean_type/1,
31         is_numerical_type/1,
32         get_bs_matchable_unit/1,
33         is_bs_matchable_type/1,
34         get_singleton_value/1,
35         is_singleton_type/1,
36         normalize/1]).
37
38-export([get_tuple_element/2, set_tuple_element/3]).
39
40-export([make_type_from_value/1]).
41
42-export([make_atom/1,
43         make_boolean/0,
44         make_cons/2,
45         make_float/1,
46         make_float/2,
47         make_integer/1,
48         make_integer/2]).
49
50-export([limit_depth/1]).
51
52%% This is exported to help catch errors in property test generators and is not
53%% meant to be used outside of test suites.
54-export([verified_type/1]).
55
56-define(IS_LIST_TYPE(N),
57        is_record(N, t_list) orelse
58        is_record(N, t_cons) orelse
59        N =:= nil).
60
61-define(IS_NUMBER_TYPE(N),
62        N =:= number orelse
63        is_record(N, t_float) orelse
64        is_record(N, t_integer)).
65
66%% Folds meet/2 over a list.
67
68-spec meet([type()]) -> type().
69
70meet([T1, T2 | Ts]) ->
71    meet([meet(T1, T2) | Ts]);
72meet([T]) -> T.
73
74%% Return the "meet" of Type1 and Type2, which is more specific than Type1 and
75%% Type2. This is identical to glb/2 but can operate on and produce unions.
76%%
77%%    A = #t_union{list=nil, number=[number], other=[#t_map{}]}
78%%    B = #t_union{number=[#t_integer{}], other=[#t_map{}]}
79%%
80%%    meet(A, B) ->
81%%         #t_union{number=[#t_integer{}], other=[#t_map{}]}
82%%
83%% The meet of two different types result in 'none', which is the bottom
84%% element for our type lattice:
85%%
86%%    meet(#t_integer{}, #t_map{}) -> none
87
88-spec meet(type(), type()) -> type().
89
90meet(T, T) ->
91    verified_type(T);
92meet(any, T) ->
93    verified_type(T);
94meet(T, any) ->
95    verified_type(T);
96meet(#t_union{}=A, B) ->
97    meet_unions(A, B);
98meet(A, #t_union{}=B) ->
99    meet_unions(B, A);
100meet(A, B) ->
101    glb(A, B).
102
103meet_unions(#t_union{atom=AtomA,list=ListA,number=NumberA,
104                     tuple_set=TSetA,other=OtherA},
105            #t_union{atom=AtomB,list=ListB,number=NumberB,
106                     tuple_set=TSetB,other=OtherB}) ->
107    Union = #t_union{atom=glb(AtomA, AtomB),
108                     list=glb(ListA, ListB),
109                     number=glb(NumberA, NumberB),
110                     tuple_set=meet_tuple_sets(TSetA, TSetB),
111                     other=glb(OtherA, OtherB)},
112    shrink_union(Union);
113meet_unions(#t_union{atom=AtomA}, #t_atom{}=B) ->
114    case glb(AtomA, B) of
115        none -> none;
116        Atom -> Atom
117    end;
118meet_unions(#t_union{number=NumberA}, B) when ?IS_NUMBER_TYPE(B) ->
119    case glb(NumberA, B) of
120        none -> none;
121        Number -> Number
122    end;
123meet_unions(#t_union{list=ListA}, B) when ?IS_LIST_TYPE(B) ->
124    case glb(ListA, B) of
125        none -> none;
126        List -> List
127    end;
128meet_unions(#t_union{tuple_set=Tuples}, #t_tuple{}=B) ->
129    Set = meet_tuple_sets(Tuples, new_tuple_set(B)),
130    shrink_union(#t_union{tuple_set=Set});
131meet_unions(#t_union{other=OtherA}, OtherB) ->
132    case glb(OtherA, OtherB) of
133        none -> none;
134        Other -> Other
135    end.
136
137meet_tuple_sets(none, _) ->
138    none;
139meet_tuple_sets(_, none) ->
140    none;
141meet_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) ->
142    new_tuple_set(glb(A, B));
143meet_tuple_sets(#t_tuple{}=Tuple, Records) ->
144    mts_tuple(Records, Tuple, []);
145meet_tuple_sets(Records, #t_tuple{}=Tuple) ->
146    meet_tuple_sets(Tuple, Records);
147meet_tuple_sets(RecordsA, RecordsB) ->
148    mts_records(RecordsA, RecordsB).
149
150mts_tuple([{Key, Type} | Records], Tuple, Acc) ->
151    case glb(Type, Tuple) of
152        none -> mts_tuple(Records, Tuple, Acc);
153        T -> mts_tuple(Records, Tuple, [{Key, T} | Acc])
154    end;
155mts_tuple([], _Tuple, [_|_]=Acc) ->
156    reverse(Acc);
157mts_tuple([], _Tuple, []) ->
158    none.
159
160mts_records(RecordsA, RecordsB) ->
161    mts_records(RecordsA, RecordsB, []).
162
163mts_records([{Key, A} | RsA], [{Key, B} | RsB], Acc) ->
164    case glb(A, B) of
165        none -> mts_records(RsA, RsB, Acc);
166        T -> mts_records(RsA, RsB, [{Key, T} | Acc])
167    end;
168mts_records([{KeyA, _} | _ ]=RsA, [{KeyB, _} | RsB], Acc) when KeyA > KeyB ->
169    mts_records(RsA, RsB, Acc);
170mts_records([{KeyA, _} | RsA], [{KeyB, _} | _] = RsB, Acc) when KeyA < KeyB ->
171    mts_records(RsA, RsB, Acc);
172mts_records(_RsA, [], [_|_]=Acc) ->
173    reverse(Acc);
174mts_records([], _RsB, [_|_]=Acc) ->
175    reverse(Acc);
176mts_records(_RsA, _RsB, []) ->
177    none.
178
179%% Folds join/2 over a list.
180
181-spec join([type()]) -> type().
182
183join([T | Ts]) ->
184    join_list(Ts, T).
185
186join_list([T | Ts], T) ->
187    join_list(Ts, T);
188join_list([T1 | Ts], T) ->
189    join_list(Ts, join(T1, T));
190join_list([], T) -> T.
191
192%% Return the "join" of Type1 and Type2, which is more general than Type1 and
193%% Type2. This is identical to lub/2 but can operate on and produce unions.
194%%
195%%    join(#t_integer{}, #t_map{}) -> #t_union{number=[#t_integer{}],
196%%                                             other=[#t_map{}]}
197
198-spec join(type(), type()) -> type().
199
200join(T, T) -> T;
201join(_T, any) -> any;
202join(any, _T) -> any;
203join(T, none) -> T;
204join(none, T) -> T;
205
206join(#t_union{}=A, B) ->
207    join_unions(A, B);
208join(A, #t_union{}=B) ->
209    join_unions(B, A);
210
211%% Union creation...
212join(#t_atom{}=A, #t_atom{}=B) ->
213    lub(A, B);
214join(#t_atom{}=A, B) when ?IS_LIST_TYPE(B) ->
215    #t_union{atom=A,list=B};
216join(#t_atom{}=A, B) when ?IS_NUMBER_TYPE(B) ->
217    #t_union{atom=A,number=B};
218join(#t_atom{}=A, #t_tuple{}=B) ->
219    #t_union{atom=A,tuple_set=new_tuple_set(B)};
220join(#t_atom{}=A, B) ->
221    #t_union{atom=A,other=B};
222join(A, #t_atom{}=B) ->
223    join(B, A);
224
225join(A, B) when ?IS_LIST_TYPE(A), ?IS_LIST_TYPE(B) ->
226    lub(A, B);
227join(A, B) when ?IS_LIST_TYPE(A), ?IS_NUMBER_TYPE(B) ->
228    #t_union{list=A,number=B};
229join(A, #t_tuple{}=B) when ?IS_LIST_TYPE(A) ->
230    #t_union{list=A,tuple_set=new_tuple_set(B)};
231join(A, B) when ?IS_LIST_TYPE(A) ->
232    #t_union{list=A,other=B};
233join(A, B) when ?IS_LIST_TYPE(B) ->
234    join(B, A);
235
236join(A, B) when ?IS_NUMBER_TYPE(A), ?IS_NUMBER_TYPE(B) ->
237    lub(A, B);
238join(A, #t_tuple{}=B) when ?IS_NUMBER_TYPE(A) ->
239    #t_union{number=A,tuple_set=new_tuple_set(B)};
240join(A, B) when ?IS_NUMBER_TYPE(A) ->
241    #t_union{number=A,other=B};
242join(A, B) when ?IS_NUMBER_TYPE(B) ->
243    join(B, A);
244
245join(#t_tuple{}=A, #t_tuple{}=B) ->
246    case {record_key(A), record_key(B)} of
247        {Same, Same} ->
248            lub(A, B);
249        {none, _Key} ->
250            lub(A, B);
251        {_Key, none} ->
252            lub(A, B);
253        {KeyA, KeyB} when KeyA < KeyB ->
254            #t_union{tuple_set=[{KeyA, A}, {KeyB, B}]};
255        {KeyA, KeyB} when KeyA > KeyB ->
256            #t_union{tuple_set=[{KeyB, B}, {KeyA, A}]}
257    end;
258join(#t_tuple{}=A, B) ->
259    %% All other combinations have been tried already, so B must be 'other'
260    #t_union{tuple_set=new_tuple_set(A),other=B};
261join(A, #t_tuple{}=B) ->
262    join(B, A);
263
264join(A, B) ->
265    lub(A, B).
266
267join_unions(#t_union{atom=AtomA,list=ListA,number=NumberA,
268                     tuple_set=TSetA,other=OtherA},
269            #t_union{atom=AtomB,list=ListB,number=NumberB,
270                     tuple_set=TSetB,other=OtherB}) ->
271    Union = #t_union{atom=lub(AtomA, AtomB),
272                     list=lub(ListA, ListB),
273                     number=lub(NumberA, NumberB),
274                     tuple_set=join_tuple_sets(TSetA, TSetB),
275                     other=lub(OtherA, OtherB)},
276    shrink_union(Union);
277join_unions(#t_union{atom=AtomA}=A, #t_atom{}=B) ->
278    A#t_union{atom=lub(AtomA, B)};
279join_unions(#t_union{list=ListA}=A, B) when ?IS_LIST_TYPE(B) ->
280    A#t_union{list=lub(ListA, B)};
281join_unions(#t_union{number=NumberA}=A, B) when ?IS_NUMBER_TYPE(B) ->
282    A#t_union{number=lub(NumberA, B)};
283join_unions(#t_union{tuple_set=TSetA}=A, #t_tuple{}=B) ->
284    Set = join_tuple_sets(TSetA, new_tuple_set(B)),
285    shrink_union(A#t_union{tuple_set=Set});
286join_unions(#t_union{other=OtherA}=A, B) ->
287    case lub(OtherA, B) of
288        any -> any;
289        T -> A#t_union{other=T}
290    end.
291
292join_tuple_sets(A, none) ->
293    A;
294join_tuple_sets(none, B) ->
295    B;
296join_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) ->
297    lub(A, B);
298join_tuple_sets(#t_tuple{}=Tuple, Records) ->
299    jts_tuple(Records, Tuple);
300join_tuple_sets(Records, #t_tuple{}=Tuple) ->
301    join_tuple_sets(Tuple, Records);
302join_tuple_sets(RecordsA, RecordsB) ->
303    jts_records(RecordsA, RecordsB).
304
305jts_tuple([{_Key, Tuple} | Records], Acc) ->
306    jts_tuple(Records, lub(Tuple, Acc));
307jts_tuple([], Acc) ->
308    Acc.
309
310jts_records(RsA, RsB) ->
311    jts_records(RsA, RsB, 0, []).
312
313jts_records([], [], _N, Acc) ->
314    reverse(Acc);
315jts_records(RsA, RsB, N, Acc) when N > ?TUPLE_SET_LIMIT ->
316    A = normalize_tuple_set(RsA, none),
317    B = normalize_tuple_set(RsB, A),
318    #t_tuple{} = normalize_tuple_set(Acc, B);
319jts_records([{Key, A} | RsA], [{Key, B} | RsB], N, Acc) ->
320    jts_records(RsA, RsB, N + 1, [{Key, lub(A, B)} | Acc]);
321jts_records([{KeyA, _} | _]=RsA, [{KeyB, B} | RsB], N, Acc) when KeyA > KeyB ->
322    jts_records(RsA, RsB, N + 1, [{KeyB, B} | Acc]);
323jts_records([{KeyA, A} | RsA], [{KeyB, _} | _] = RsB, N, Acc) when KeyA < KeyB ->
324    jts_records(RsA, RsB, N + 1, [{KeyA, A} | Acc]);
325jts_records([{KeyA, A} | RsA], [], N, Acc) ->
326    jts_records(RsA, [], N + 1, [{KeyA, A} | Acc]);
327jts_records([], [{KeyB, B} | RsB], N, Acc) ->
328    jts_records([], RsB, N + 1, [{KeyB, B} | Acc]).
329
330%% Subtract Type2 from Type1. Example:
331%%    subtract(list, cons) -> nil
332
333-spec subtract(type(), type()) -> type().
334
335subtract(#t_atom{elements=[_|_]=Set0}, #t_atom{elements=[_|_]=Set1}) ->
336    case ordsets:subtract(Set0, Set1) of
337        [] -> none;
338        [_|_]=Set -> #t_atom{elements=Set}
339    end;
340subtract(#t_bitstring{size_unit=UnitA}=T, #t_bs_matchable{tail_unit=UnitB}) ->
341    subtract_matchable(T, UnitA, UnitB);
342subtract(#t_bitstring{size_unit=UnitA}=T, #t_bitstring{size_unit=UnitB}) ->
343    subtract_matchable(T, UnitA, UnitB);
344subtract(#t_bs_context{tail_unit=UnitA}=T, #t_bs_matchable{tail_unit=UnitB}) ->
345    subtract_matchable(T, UnitA, UnitB);
346subtract(#t_bs_context{tail_unit=UnitA}=T, #t_bs_context{tail_unit=UnitB}) ->
347    subtract_matchable(T, UnitA, UnitB);
348subtract(#t_integer{elements={Min, Max}}, #t_integer{elements={N,N}}) ->
349    if
350        Min =:= N, Max =:= N ->
351            none;
352        Min =/= N, Max =/= N ->
353            #t_integer{elements={Min, Max}};
354        Min =:= N ->
355            #t_integer{elements={Min + 1, Max}};
356        Max =:= N ->
357            #t_integer{elements={Min, Max - 1}}
358    end;
359subtract(number, #t_float{elements=any}) -> #t_integer{};
360subtract(number, #t_integer{elements=any}) -> #t_float{};
361
362%% A list is essentially `#t_cons{} | nil`, so we're left with nil if we
363%% subtract a cons cell that is more general than the one in the list.
364subtract(#t_list{type=TypeA,terminator=TermA}=T,
365         #t_cons{type=TypeB,terminator=TermB}) ->
366    case {meet(TypeA, TypeB), meet(TermA, TermB)} of
367        {TypeA, TermA} -> nil;
368        _ -> T
369    end;
370subtract(#t_list{type=Type,terminator=Term}, nil) ->
371    #t_cons{type=Type,terminator=Term};
372
373subtract(#t_union{atom=Atom}=A, #t_atom{}=B)->
374    shrink_union(A#t_union{atom=subtract(Atom, B)});
375subtract(#t_union{number=Number}=A, B) when ?IS_NUMBER_TYPE(B) ->
376    shrink_union(A#t_union{number=subtract(Number, B)});
377subtract(#t_union{list=List}=A, B) when ?IS_LIST_TYPE(B) ->
378    shrink_union(A#t_union{list=subtract(List, B)});
379subtract(#t_union{tuple_set=[_|_]=Records0}=A, #t_tuple{}=B) ->
380    %% Filter out all records that are more specific than B.
381    NewSet = case [{Key, T} || {Key, T} <- Records0, meet(T, B) =/= T] of
382                 [_|_]=Records -> Records;
383                 [] -> none
384             end,
385    shrink_union(A#t_union{tuple_set=NewSet});
386subtract(#t_union{tuple_set=#t_tuple{}=Tuple}=A, #t_tuple{}=B) ->
387    %% Exclude Tuple if it's more specific than B.
388    case meet(Tuple, B) of
389        Tuple -> shrink_union(A#t_union{tuple_set=none});
390        _ -> A
391    end;
392subtract(#t_union{other=Other}=A, B) ->
393    shrink_union(A#t_union{other=subtract(Other, B)});
394
395subtract(A, B) ->
396    %% There's nothing left if A is more specific than B.
397    case meet(A, B) of
398        A -> none;
399        _Other -> A
400    end.
401
402subtract_matchable(T, UnitA, UnitB) ->
403    if
404        UnitA rem UnitB =:= 0 -> none;
405        UnitA rem UnitB =/= 0 -> T
406    end.
407
408%%%
409%%% Type operators
410%%%
411
412-spec get_bs_matchable_unit(type()) -> pos_integer() | error.
413get_bs_matchable_unit(#t_bitstring{size_unit=Unit}) ->
414    Unit;
415get_bs_matchable_unit(#t_bs_context{tail_unit=Unit}) ->
416    Unit;
417get_bs_matchable_unit(#t_bs_matchable{tail_unit=Unit}) ->
418    Unit;
419get_bs_matchable_unit(_) ->
420    error.
421
422-spec is_bs_matchable_type(type()) -> boolean().
423is_bs_matchable_type(Type) ->
424    get_bs_matchable_unit(Type) =/= error.
425
426-spec get_singleton_value(Type) -> Result when
427      Type :: type(),
428      Result :: {ok, term()} | error.
429get_singleton_value(#t_atom{elements=[Atom]}) ->
430    {ok, Atom};
431get_singleton_value(#t_float{elements={Float,Float}}) when Float =/= 0.0 ->
432    %% 0.0 is not actually a singleton as it has two encodings: 0.0 and -0.0
433    {ok, Float};
434get_singleton_value(#t_integer{elements={Int,Int}}) ->
435    {ok, Int};
436get_singleton_value(#t_map{super_key=none,super_value=none}) ->
437    {ok, #{}};
438get_singleton_value(#t_tuple{exact=true,size=Size,elements=Es}) ->
439    case gsv_elements(Size, Es, []) of
440        Values when is_list(Values) ->
441            {ok, list_to_tuple(Values)};
442        error ->
443            error
444    end;
445get_singleton_value(nil) ->
446    {ok, []};
447get_singleton_value(_) ->
448    error.
449
450gsv_elements(0, _Es, Acc) ->
451    %% The elements were added right-to-left, so it's already in order.
452    Acc;
453gsv_elements(N, Es, Acc) ->
454    ElementType = get_tuple_element(N, Es),
455    case get_singleton_value(ElementType) of
456        {ok, Value} -> gsv_elements(N - 1, Es, [Value | Acc]);
457        error -> error
458    end.
459
460-spec is_singleton_type(type()) -> boolean().
461is_singleton_type(Type) ->
462    get_singleton_value(Type) =/= error.
463
464-spec is_boolean_type(type()) -> boolean().
465is_boolean_type(#t_atom{elements=[F,T]}) ->
466    F =:= false andalso T =:= true;
467is_boolean_type(#t_atom{elements=[B]}) ->
468    is_boolean(B);
469is_boolean_type(#t_union{}=T) ->
470    is_boolean_type(normalize(T));
471is_boolean_type(_) ->
472    false.
473
474-spec is_numerical_type(type()) -> boolean().
475is_numerical_type(#t_integer{}) -> true;
476is_numerical_type(number) -> true;
477is_numerical_type(_) -> false.
478
479-spec set_tuple_element(Index, Type, Elements) -> Elements when
480      Index :: pos_integer(),
481      Type :: type(),
482      Elements :: tuple_elements().
483set_tuple_element(Index, _Type, Es) when Index > ?TUPLE_ELEMENT_LIMIT ->
484    Es;
485set_tuple_element(_Index, none, Es) ->
486    Es;
487set_tuple_element(Index, any, Es) ->
488    maps:remove(Index, Es);
489set_tuple_element(Index, Type, Es) ->
490    Es#{ Index => Type }.
491
492-spec get_tuple_element(Index, Elements) -> type() when
493      Index :: pos_integer(),
494      Elements :: tuple_elements().
495get_tuple_element(Index, Es) ->
496    case Es of
497        #{ Index := T } -> T;
498        #{} -> any
499    end.
500
501-spec normalize(type()) -> normal_type().
502normalize(#t_union{atom=Atom,list=List,number=Number,
503                   tuple_set=Tuples,other=Other}) ->
504    A = lub(Atom, List),
505    B = lub(A, Number),
506    C = lub(B, Other),
507    normalize_tuple_set(Tuples, C);
508normalize(T) ->
509    verified_normal_type(T).
510
511normalize_tuple_set([{_, A} | Records], B) ->
512    normalize_tuple_set(Records, lub(A, B));
513normalize_tuple_set([], B) ->
514    B;
515normalize_tuple_set(A, B) ->
516    lub(A, B).
517
518%%%
519%%% Type constructors
520%%%
521
522-spec make_type_from_value(term()) -> type().
523make_type_from_value(Value) ->
524    mtfv_1(Value).
525
526mtfv_1(A) when is_atom(A) ->
527    #t_atom{elements=[A]};
528mtfv_1(B) when is_bitstring(B) ->
529    case bit_size(B) of
530        0 ->
531            %% This is a bit of a hack, but saying that empty binaries have a
532            %% unit of 8 helps us get rid of is_binary/1 checks.
533            #t_bitstring{size_unit=8};
534        Size ->
535            #t_bitstring{size_unit=Size}
536    end;
537mtfv_1(F) when is_float(F) ->
538    make_float(F);
539mtfv_1(F) when is_function(F) ->
540    {arity, Arity} = erlang:fun_info(F, arity),
541    #t_fun{arity=Arity};
542mtfv_1(I) when is_integer(I) ->
543    make_integer(I);
544mtfv_1(L) when is_list(L) ->
545    case L of
546        [_|_] -> mtfv_cons(L, none);
547        [] -> nil
548    end;
549mtfv_1(M) when is_map(M) ->
550    {SKey, SValue} =
551        maps:fold(fun(Key, Value, {SKey0, SValue0}) ->
552                        SKey = join(mtfv_1(Key), SKey0),
553                        SValue = join(mtfv_1(Value), SValue0),
554                        {SKey, SValue}
555                  end, {none, none}, M),
556    #t_map{super_key=SKey,super_value=SValue};
557mtfv_1(T) when is_tuple(T) ->
558    {Es,_} = foldl(fun(Val, {Es0, Index}) ->
559                           Type = mtfv_1(Val),
560                           Es = set_tuple_element(Index, Type, Es0),
561                           {Es, Index + 1}
562                   end, {#{}, 1}, tuple_to_list(T)),
563    #t_tuple{exact=true,size=tuple_size(T),elements=Es};
564mtfv_1(_Term) ->
565    any.
566
567mtfv_cons([Head | Tail], Type) ->
568    mtfv_cons(Tail, join(mtfv_1(Head), Type));
569mtfv_cons(Terminator, Type) ->
570    #t_cons{type=Type,terminator=mtfv_1(Terminator)}.
571
572-spec make_atom(atom()) -> type().
573make_atom(Atom) when is_atom(Atom) ->
574    #t_atom{elements=[Atom]}.
575
576-spec make_boolean() -> type().
577make_boolean() ->
578    #t_atom{elements=[false,true]}.
579
580-spec make_cons(type(), type()) -> type().
581make_cons(Head0, Tail) ->
582    case meet(Tail, #t_cons{}) of
583        #t_cons{type=Type0,terminator=Term0} ->
584            %% Propagate element and terminator types. Note that if the tail is
585            %% the union of a list and something else, the new list could be
586            %% terminated by the other types in the union.
587            Type = join(Head0, Type0),
588            Term = join(subtract(Tail, #t_cons{}), Term0),
589            #t_cons{type=Type,terminator=Term};
590        _ ->
591            %% Tail can't be a cons cell, so we know it terminates the list.
592            #t_cons{type=Head0,terminator=Tail}
593    end.
594
595-spec make_float(float()) -> type().
596make_float(Float) when is_float(Float) ->
597    make_float(Float, Float).
598
599-spec make_float(float(), float()) -> type().
600make_float(Min, Max) when is_float(Min), is_float(Max), Min =< Max ->
601    #t_float{elements={Min, Max}}.
602
603-spec make_integer(integer()) -> type().
604make_integer(Int) when is_integer(Int) ->
605    make_integer(Int, Int).
606
607-spec make_integer(Min, Max) -> type() when
608      Min :: integer(),
609      Max :: integer().
610make_integer(Min, Max) when is_integer(Min), is_integer(Max), Min =< Max ->
611    #t_integer{elements={Min,Max}}.
612
613-spec limit_depth(type()) -> type().
614
615limit_depth(Type) ->
616    limit_depth(Type, ?MAX_TYPE_DEPTH).
617
618limit_depth(#t_cons{}=T, Depth) ->
619    limit_depth_list(T, Depth);
620limit_depth(#t_list{}=T, Depth) ->
621    limit_depth_list(T, Depth);
622limit_depth(#t_tuple{}=T, Depth) ->
623    limit_depth_tuple(T, Depth);
624limit_depth(#t_fun{}=T, Depth) ->
625    limit_depth_fun(T, Depth);
626limit_depth(#t_map{}=T, Depth) ->
627    limit_depth_map(T, Depth);
628limit_depth(#t_union{list=List0,tuple_set=TupleSet0,other=Other0}=U, Depth) ->
629    TupleSet = limit_depth_tuple(TupleSet0, Depth),
630    List = limit_depth_list(List0, Depth),
631    Other = limit_depth(Other0, Depth),
632    shrink_union(U#t_union{list=List,tuple_set=TupleSet,other=Other});
633limit_depth(Type, _Depth) ->
634    Type.
635
636limit_depth_fun(#t_fun{type=Type0}=T, Depth) ->
637    Type = if
638               Depth > 0 -> limit_depth(Type0, Depth - 1);
639               Depth =< 0 -> any
640           end,
641    T#t_fun{type=Type}.
642
643limit_depth_list(#t_cons{type=Type0,terminator=Term0}=T, Depth) ->
644    {Type, Term} = limit_depth_list_1(Type0, Term0, Depth),
645    T#t_cons{type=Type,terminator=Term};
646limit_depth_list(#t_list{type=Type0,terminator=Term0}=T, Depth) ->
647    {Type, Term} = limit_depth_list_1(Type0, Term0, Depth),
648    T#t_list{type=Type,terminator=Term};
649limit_depth_list(nil, _Depth) ->
650    nil;
651limit_depth_list(none, _Depth) ->
652    none.
653
654limit_depth_list_1(Type0, Terminator0, Depth) when Depth > 0 ->
655    Type = limit_depth(Type0, Depth - 1),
656    Terminator = limit_depth(Terminator0, Depth - 1),
657    {Type, Terminator};
658limit_depth_list_1(_Type, _Terminator, Depth) when Depth =< 0 ->
659    {any, any}.
660
661limit_depth_map(#t_map{ super_key=SKey0,
662                        super_value=SValue0 }, Depth) when Depth > 0 ->
663    SKey = limit_depth(SKey0, Depth - 1),
664    SValue = limit_depth(SValue0, Depth - 1),
665    #t_map{super_key=SKey,super_value=SValue};
666limit_depth_map(#t_map{}, Depth) when Depth =< 0 ->
667    #t_map{}.
668
669limit_depth_tuple(#t_tuple{elements=Es0}=T, Depth) ->
670    if
671        Depth > 0 ->
672            Es = maps:map(fun(_, E) -> limit_depth(E, Depth - 1) end, Es0),
673            T#t_tuple{elements=Es};
674        Depth =< 0 ->
675            #t_tuple{elements=#{}}
676    end;
677limit_depth_tuple([{{MinSize,_},_}|_], Depth) when Depth =< 0 ->
678    %% Preserve the minimum size of the tuple set.
679    #t_tuple{exact=false,size=MinSize};
680limit_depth_tuple([{SzTag,Tuple}|Ts], Depth) ->
681    [{SzTag, limit_depth_tuple(Tuple, Depth)} | limit_depth_tuple(Ts, Depth)];
682limit_depth_tuple([], _Depth) ->
683    [];
684limit_depth_tuple(none, _Depth) ->
685    none.
686
687%%%
688%%% Helpers
689%%%
690
691%% Return the greatest lower bound of the types Type1 and Type2. The GLB is a
692%% more specific type than Type1 and Type2, and is always a normal type.
693%%
694%%    glb(#t_integer{elements=any}, #t_integer{elements={0,3}}) ->
695%%         #t_integer{elements={0,3}}
696%%
697%% The GLB of two different types result in 'none', which is the bottom
698%% element for our type lattice:
699%%
700%%    glb(#t_integer{}, #t_map{}) -> none
701
702-spec glb(normal_type(), normal_type()) -> normal_type().
703
704glb(T, T) ->
705    verified_normal_type(T);
706glb(any, T) ->
707    verified_normal_type(T);
708glb(T, any) ->
709    verified_normal_type(T);
710glb(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
711    case ordsets:intersection(Set1, Set2) of
712        [] ->
713            none;
714        [_|_]=Set ->
715            #t_atom{elements=Set}
716    end;
717glb(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) ->
718    T;
719glb(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) ->
720    T;
721glb(#t_bitstring{size_unit=U1}, #t_bitstring{size_unit=U2}) ->
722    #t_bitstring{size_unit=U1 * U2 div gcd(U1, U2)};
723glb(#t_bitstring{size_unit=UnitA}=T, #t_bs_matchable{tail_unit=UnitB}) ->
724    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
725    T#t_bitstring{size_unit=Unit};
726glb(#t_bs_context{tail_unit=UnitA,slots=SlotCountA,valid=ValidSlotsA},
727    #t_bs_context{tail_unit=UnitB,slots=SlotCountB,valid=ValidSlotsB}) ->
728    CommonSlotMask = (1 bsl min(SlotCountA, SlotCountB)) - 1,
729    CommonSlotsA = ValidSlotsA band CommonSlotMask,
730    CommonSlotsB = ValidSlotsB band CommonSlotMask,
731    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
732    if
733        CommonSlotsA =:= CommonSlotsB ->
734            #t_bs_context{tail_unit=Unit,
735                          slots=max(SlotCountA, SlotCountB),
736                          valid=ValidSlotsA bor ValidSlotsB};
737        CommonSlotsA =/= CommonSlotsB ->
738            none
739    end;
740glb(#t_bs_context{tail_unit=UnitA}=T, #t_bs_matchable{tail_unit=UnitB}) ->
741    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
742    T#t_bs_context{tail_unit=Unit};
743glb(#t_bs_matchable{tail_unit=UnitA}, #t_bs_matchable{tail_unit=UnitB}) ->
744    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
745    #t_bs_matchable{tail_unit=Unit};
746glb(#t_bs_matchable{tail_unit=UnitA}, #t_bitstring{size_unit=UnitB}=T) ->
747    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
748    T#t_bitstring{size_unit=Unit};
749glb(#t_bs_matchable{tail_unit=UnitA}, #t_bs_context{tail_unit=UnitB}=T) ->
750    Unit = UnitA * UnitB div gcd(UnitA, UnitB),
751    T#t_bs_context{tail_unit=Unit};
752glb(#t_cons{type=TypeA,terminator=TermA},
753    #t_cons{type=TypeB,terminator=TermB}) ->
754    %% Note the use of meet/2; elements don't need to be normal types.
755    case {meet(TypeA, TypeB), meet(TermA, TermB)} of
756        {none, _} -> none;
757        {_, none} -> none;
758        {Type, Term} -> #t_cons{type=Type,terminator=Term}
759    end;
760glb(#t_cons{type=TypeA,terminator=TermA},
761    #t_list{type=TypeB,terminator=TermB}) ->
762    case {meet(TypeA, TypeB), meet(TermA, TermB)} of
763        {none, _} -> none;
764        {_, none} -> none;
765        {Type, Term} -> #t_cons{type=Type,terminator=Term}
766    end;
767glb(#t_float{}=T, #t_float{elements=any}) ->
768    T;
769glb(#t_float{elements=any}, #t_float{}=T) ->
770    T;
771glb(#t_float{elements={MinA,MaxA}}, #t_float{elements={MinB,MaxB}})
772  when MinA >= MinB, MinA =< MaxB;
773       MinB >= MinA, MinB =< MaxA ->
774    true = MinA =< MaxA andalso MinB =< MaxB,   %Assertion.
775    #t_float{elements={max(MinA, MinB),min(MaxA, MaxB)}};
776glb(#t_fun{arity=Same,type=TypeA}, #t_fun{arity=Same,type=TypeB}=T) ->
777    T#t_fun{type=meet(TypeA, TypeB)};
778glb(#t_fun{arity=any,type=TypeA}, #t_fun{type=TypeB}=T) ->
779    T#t_fun{type=meet(TypeA, TypeB)};
780glb(#t_fun{type=TypeA}=T, #t_fun{arity=any,type=TypeB}) ->
781    T#t_fun{type=meet(TypeA, TypeB)};
782glb(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) ->
783    T;
784glb(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) ->
785    T;
786glb(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}})
787  when MinA >= MinB, MinA =< MaxB;
788       MinB >= MinA, MinB =< MaxA ->
789    true = MinA =< MaxA andalso MinB =< MaxB,   %Assertion.
790    #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}};
791glb(#t_integer{}=T, number) ->
792    T;
793glb(#t_float{}=T, number) ->
794    T;
795glb(#t_list{type=TypeA,terminator=TermA},
796    #t_list{type=TypeB,terminator=TermB}) ->
797    %% A list is a union of `[type() | _]` and `[]`, so we're left with
798    %% nil when the element types are incompatible.
799    case {meet(TypeA, TypeB), meet(TermA, TermB)} of
800        {none, _} -> nil;
801        {_, none} -> nil;
802        {Type, Term} -> #t_list{type=Type,terminator=Term}
803    end;
804glb(#t_list{}=A, #t_cons{}=B) ->
805    glb(B, A);
806glb(#t_list{}, nil) ->
807    nil;
808glb(nil, #t_list{}) ->
809    nil;
810glb(number, #t_integer{}=T) ->
811    T;
812glb(number, #t_float{}=T) ->
813    T;
814glb(#t_map{super_key=SKeyA,super_value=SValueA},
815    #t_map{super_key=SKeyB,super_value=SValueB}) ->
816    %% Note the use of meet/2; elements don't need to be normal types.
817    SKey = meet(SKeyA, SKeyB),
818    SValue = meet(SValueA, SValueB),
819    #t_map{super_key=SKey,super_value=SValue};
820glb(#t_tuple{}=T1, #t_tuple{}=T2) ->
821    glb_tuples(T1, T2);
822glb(_, _) ->
823    %% Inconsistent types. There will be an exception at runtime.
824    none.
825
826glb_tuples(#t_tuple{size=Sz1,exact=Ex1}, #t_tuple{size=Sz2,exact=Ex2})
827  when Ex1, Sz1 < Sz2;
828       Ex2, Sz2 < Sz1 ->
829    none;
830glb_tuples(#t_tuple{size=Sz1,exact=Ex1,elements=Es1},
831           #t_tuple{size=Sz2,exact=Ex2,elements=Es2}) ->
832    Size = max(Sz1, Sz2),
833    Exact = Ex1 or Ex2,
834    case glb_elements(Es1, Es2) of
835        none ->
836            none;
837        Es ->
838            #t_tuple{size=Size,exact=Exact,elements=Es}
839    end.
840
841glb_elements(Es1, Es2) ->
842    Keys = maps:keys(Es1) ++ maps:keys(Es2),
843    glb_elements_1(Keys, Es1, Es2, #{}).
844
845glb_elements_1([Key | Keys], Es1, Es2, Acc) ->
846    case {Es1, Es2} of
847        {#{ Key := Type1 }, #{ Key := Type2 }} ->
848            %% Note the use of meet/2; elements don't need to be normal types.
849            case meet(Type1, Type2) of
850                none -> none;
851                Type -> glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
852            end;
853        {#{ Key := Type1 }, _} ->
854            glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
855        {_, #{ Key := Type2 }} ->
856            glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
857    end;
858glb_elements_1([], _Es1, _Es2, Acc) ->
859    Acc.
860
861%% Return the least upper bound of the types Type1 and Type2. The LUB is a more
862%% general type than Type1 and Type2, and is always a normal type.
863%%
864%% For example:
865%%
866%%    lub(#t_integer{elements=any}, #t_integer=elements={0,3}}) ->
867%%         #t_integer{}
868%%
869%% The LUB for two different types result in 'any' (not a union type!), which
870%% is the top element for our type lattice:
871%%
872%%    lub(#t_integer{}, #t_map{}) -> any
873
874-spec lub(normal_type(), normal_type()) -> normal_type().
875
876lub(T, T) ->
877    verified_normal_type(T);
878lub(none, T) ->
879    verified_normal_type(T);
880lub(T, none) ->
881    verified_normal_type(T);
882lub(any, _) ->
883    any;
884lub(_, any) ->
885    any;
886lub(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
887    Set = ordsets:union(Set1, Set2),
888    case ordsets:size(Set) of
889        Size when Size =< ?ATOM_SET_SIZE ->
890            #t_atom{elements=Set};
891        _Size ->
892            #t_atom{elements=any}
893    end;
894lub(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T;
895lub(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T;
896lub(#t_bitstring{size_unit=U1}, #t_bitstring{size_unit=U2}) ->
897    #t_bitstring{size_unit=gcd(U1, U2)};
898lub(#t_bitstring{size_unit=U1}, #t_bs_context{tail_unit=U2}) ->
899    #t_bs_matchable{tail_unit=gcd(U1, U2)};
900lub(#t_bitstring{size_unit=UnitA}, #t_bs_matchable{tail_unit=UnitB}) ->
901    lub_bs_matchable(UnitA, UnitB);
902lub(#t_bs_context{tail_unit=UnitA,slots=SlotsA,valid=ValidA},
903    #t_bs_context{tail_unit=UnitB,slots=SlotsB,valid=ValidB}) ->
904    #t_bs_context{tail_unit=gcd(UnitA, UnitB),
905                  slots=min(SlotsA, SlotsB),
906                  valid=ValidA band ValidB};
907lub(#t_bs_context{tail_unit=U1}, #t_bitstring{size_unit=U2}) ->
908    #t_bs_matchable{tail_unit=gcd(U1, U2)};
909lub(#t_bs_context{tail_unit=UnitA}, #t_bs_matchable{tail_unit=UnitB}) ->
910    lub_bs_matchable(UnitA, UnitB);
911lub(#t_bs_matchable{tail_unit=UnitA}, #t_bs_matchable{tail_unit=UnitB}) ->
912    lub_bs_matchable(UnitA, UnitB);
913lub(#t_bs_matchable{tail_unit=UnitA}, #t_bitstring{size_unit=UnitB}) ->
914    lub_bs_matchable(UnitA, UnitB);
915lub(#t_bs_matchable{tail_unit=UnitA}, #t_bs_context{tail_unit=UnitB}) ->
916    lub_bs_matchable(UnitA, UnitB);
917lub(#t_cons{type=TypeA,terminator=TermA},
918    #t_cons{type=TypeB,terminator=TermB}) ->
919    %% Note the use of join/2; elements don't need to be normal types.
920    #t_cons{type=join(TypeA,TypeB),terminator=join(TermA, TermB)};
921lub(#t_cons{type=TypeA,terminator=TermA},
922    #t_list{type=TypeB,terminator=TermB}) ->
923    #t_list{type=join(TypeA,TypeB),terminator=join(TermA, TermB)};
924lub(#t_cons{type=Type,terminator=Term}, nil) ->
925    #t_list{type=Type,terminator=Term};
926lub(#t_float{elements={MinA,MaxA}},
927    #t_float{elements={MinB,MaxB}}) ->
928    #t_float{elements={min(MinA,MinB),max(MaxA,MaxB)}};
929lub(#t_float{}, #t_float{}) ->
930    #t_float{};
931lub(#t_float{}, #t_integer{}) ->
932    number;
933lub(#t_float{}, number) ->
934    number;
935lub(#t_fun{arity=Same,type=TypeA}, #t_fun{arity=Same,type=TypeB}) ->
936    #t_fun{arity=Same,type=join(TypeA, TypeB)};
937lub(#t_fun{type=TypeA}, #t_fun{type=TypeB}) ->
938    #t_fun{type=join(TypeA, TypeB)};
939lub(#t_integer{elements={MinA,MaxA}},
940    #t_integer{elements={MinB,MaxB}}) ->
941    #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}};
942lub(#t_integer{}, #t_integer{}) ->
943    #t_integer{};
944lub(#t_integer{}, #t_float{}) ->
945    number;
946lub(#t_integer{}, number) ->
947    number;
948lub(#t_list{type=TypeA,terminator=TermA},
949    #t_list{type=TypeB,terminator=TermB}) ->
950    #t_list{type=join(TypeA, TypeB),terminator=join(TermA, TermB)};
951lub(#t_list{}=A, #t_cons{}=B) ->
952    lub(B, A);
953lub(nil=A, #t_cons{}=B) ->
954    lub(B, A);
955lub(nil, #t_list{}=T) ->
956    T;
957lub(#t_list{}=T, nil) ->
958    T;
959lub(number, #t_integer{}) ->
960    number;
961lub(number, #t_float{}) ->
962    number;
963lub(#t_map{super_key=SKeyA,super_value=SValueA},
964    #t_map{super_key=SKeyB,super_value=SValueB}) ->
965    %% Note the use of join/2; elements don't need to be normal types.
966    SKey = join(SKeyA, SKeyB),
967    SValue = join(SValueA, SValueB),
968    #t_map{super_key=SKey,super_value=SValue};
969lub(#t_tuple{size=Sz,exact=ExactA,elements=EsA},
970    #t_tuple{size=Sz,exact=ExactB,elements=EsB}) ->
971    Exact = ExactA and ExactB,
972    Es = lub_tuple_elements(Sz, EsA, EsB),
973    #t_tuple{size=Sz,exact=Exact,elements=Es};
974lub(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) ->
975    Sz = min(SzA, SzB),
976    Es = lub_tuple_elements(Sz, EsA, EsB),
977    #t_tuple{size=Sz,elements=Es};
978lub(_T1, _T2) ->
979    %%io:format("~p ~p\n", [_T1,_T2]),
980    any.
981
982lub_bs_matchable(UnitA, UnitB) ->
983    #t_bs_matchable{tail_unit=gcd(UnitA, UnitB)}.
984
985lub_tuple_elements(MinSize, EsA, EsB) ->
986    Es0 = lub_elements(EsA, EsB),
987    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
988
989lub_elements(Es1, Es2) ->
990    Keys = if
991               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
992               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
993           end,
994    lub_elements_1(Keys, Es1, Es2, #{}).
995
996lub_elements_1([Key | Keys], Es1, Es2, Acc0) ->
997    case {Es1, Es2} of
998        {#{ Key := Type1 }, #{ Key := Type2 }} ->
999            %% Note the use of join/2; elements don't need to be normal types.
1000            Acc = set_tuple_element(Key, join(Type1, Type2), Acc0),
1001            lub_elements_1(Keys, Es1, Es2, Acc);
1002        {#{}, #{}} ->
1003            lub_elements_1(Keys, Es1, Es2, Acc0)
1004    end;
1005lub_elements_1([], _Es1, _Es2, Acc) ->
1006    Acc.
1007
1008%%
1009
1010gcd(A, B) ->
1011    case A rem B of
1012        0 -> B;
1013        X -> gcd(B, X)
1014    end.
1015
1016%%
1017
1018record_key(#t_tuple{exact=true,size=Size,elements=#{ 1 := Tag }}) ->
1019    case is_singleton_type(Tag) of
1020        true -> {Size, Tag};
1021        false -> none
1022    end;
1023record_key(_) ->
1024    none.
1025
1026new_tuple_set(T) ->
1027    case record_key(T) of
1028        none -> T;
1029        Key -> [{Key, T}]
1030    end.
1031
1032%%
1033
1034shrink_union(#t_union{other=any}) ->
1035    any;
1036shrink_union(#t_union{atom=Atom,list=none,number=none,
1037                      tuple_set=none,other=none}) ->
1038    Atom;
1039shrink_union(#t_union{atom=none,list=List,number=none,
1040                      tuple_set=none,other=none}) ->
1041    List;
1042shrink_union(#t_union{atom=none,list=none,number=Number,
1043                      tuple_set=none,other=none}) ->
1044    Number;
1045shrink_union(#t_union{atom=none,list=none,number=none,
1046                      tuple_set=#t_tuple{}=Tuple,other=none}) ->
1047    Tuple;
1048shrink_union(#t_union{atom=none,list=none,number=none,
1049                      tuple_set=[{_Key, Record}],other=none}) ->
1050    #t_tuple{} = Record;                        %Assertion.
1051shrink_union(#t_union{atom=none,list=none,number=none,
1052                      tuple_set=none,other=Other}) ->
1053    Other;
1054shrink_union(#t_union{}=T) ->
1055    T.
1056
1057%% Verifies that the given type is well-formed.
1058
1059-spec verified_type(T) -> T when
1060      T :: type().
1061
1062verified_type(#t_union{atom=Atom,
1063                       list=List,
1064                       number=Number,
1065                       tuple_set=TSet,
1066                       other=Other}=T) ->
1067    _ = verified_normal_type(Atom),
1068    _ = verified_normal_type(List),
1069    _ = verified_normal_type(Number),
1070    _ = verify_tuple_set(TSet),
1071    _ = verified_normal_type(Other),
1072    T;
1073verified_type(T) ->
1074    verified_normal_type(T).
1075
1076verify_tuple_set([_|_]=T) ->
1077    _ = verify_tuple_set_1(T, 0),
1078    T;
1079verify_tuple_set(#t_tuple{}=T) ->
1080    none = record_key(T),                       %Assertion.
1081    T;
1082verify_tuple_set(none=T) ->
1083    T.
1084
1085verify_tuple_set_1([{_Tag, Record} | Records], Size) ->
1086    true = Size =< ?TUPLE_SET_LIMIT,            %Assertion.
1087    _ = verified_normal_type(Record),
1088    verify_tuple_set_1(Records, Size + 1);
1089verify_tuple_set_1([], _Size) ->
1090    ok.
1091
1092-spec verified_normal_type(T) -> T when
1093      T :: normal_type().
1094
1095verified_normal_type(any=T) -> T;
1096verified_normal_type(none=T) -> T;
1097verified_normal_type(#t_atom{elements=any}=T) -> T;
1098verified_normal_type(#t_atom{elements=[_|_]}=T) -> T;
1099verified_normal_type(#t_bitstring{size_unit=U}=T)
1100  when is_integer(U), U >= 1 ->
1101    T;
1102verified_normal_type(#t_bs_context{tail_unit=U}=T)
1103  when is_integer(U), U >= 1 ->
1104    T;
1105verified_normal_type(#t_bs_matchable{tail_unit=U}=T)
1106  when is_integer(U), U >= 1 ->
1107    T;
1108verified_normal_type(#t_cons{type=Type,terminator=Term}=T) ->
1109    _ = verified_type(Type),
1110    _ = verified_type(Term),
1111    T;
1112verified_normal_type(#t_fun{arity=Arity,type=ReturnType}=T)
1113  when Arity =:= any; is_integer(Arity) ->
1114    _ = verified_type(ReturnType),
1115    T;
1116verified_normal_type(#t_float{}=T) -> T;
1117verified_normal_type(#t_integer{elements=any}=T) -> T;
1118verified_normal_type(#t_integer{elements={Min,Max}}=T)
1119  when is_integer(Min), is_integer(Max), Min =< Max ->
1120    T;
1121verified_normal_type(#t_list{type=Type,terminator=Term}=T) ->
1122    _ = verified_type(Type),
1123    _ = verified_type(Term),
1124    T;
1125verified_normal_type(#t_map{}=T) -> T;
1126verified_normal_type(nil=T) -> T;
1127verified_normal_type(number=T) -> T;
1128verified_normal_type(#t_tuple{size=Size,elements=Es}=T) ->
1129    %% All known elements must have a valid index and type (which may be a
1130    %% union). 'any' is prohibited since it's implicit and should never be
1131    %% present in the map, and a 'none' element ought to have reduced the
1132    %% entire tuple to 'none'.
1133    maps:fold(fun(Index, Element, _) when is_integer(Index),
1134                                          1 =< Index, Index =< Size,
1135                                          Index =< ?TUPLE_ELEMENT_LIMIT,
1136                                          Element =/= any, Element =/= none ->
1137                      verified_type(Element)
1138              end, [], Es),
1139    T.
1140