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