@@ -7,7 +7,9 @@ defmodule Module.Types.Descr do
7
7
# types require specific data structures.
8
8
9
9
# Vocabulary:
10
- # DNF: disjunctive normal form
10
+ #
11
+ # * DNF - disjunctive normal form which is a pair of unions and negations.
12
+ # In the case of maps, we augment each pair with the open/closed tag.
11
13
12
14
# TODO: When we convert from AST to descr, we need to normalize
13
15
# the dynamic type.
@@ -25,8 +27,7 @@ defmodule Module.Types.Descr do
25
27
@ bit_tuple 1 <<< 8
26
28
@ bit_fun 1 <<< 9
27
29
@ bit_top ( 1 <<< 10 ) - 1
28
-
29
- @ bit_unset 1 <<< 10
30
+ @ bit_optional 1 <<< 10
30
31
31
32
@ atom_top { :negation , :sets . new ( version: 2 ) }
32
33
@ map_top [ { :open , % { } , [ ] } ]
@@ -37,11 +38,6 @@ defmodule Module.Types.Descr do
37
38
@ none % { }
38
39
@ dynamic % { dynamic: @ term }
39
40
40
- # Map helpers
41
-
42
- @ unset % { bitmap: @ bit_unset }
43
- @ term_or_unset % { bitmap: @ bit_top ||| @ bit_unset , atom: @ atom_top , map: @ map_top }
44
-
45
41
# Type definitions
46
42
47
43
def dynamic ( ) , do: @ dynamic
@@ -68,6 +64,15 @@ defmodule Module.Types.Descr do
68
64
@ boolset :sets . from_list ( [ true , false ] , version: 2 )
69
65
def boolean ( ) , do: % { atom: { :union , @ boolset } }
70
66
67
+ # Map helpers
68
+
69
+ @ not_set % { bitmap: @ bit_optional }
70
+ @ term_or_not_set % { bitmap: @ bit_top ||| @ bit_optional , atom: @ atom_top , map: @ map_top }
71
+
72
+ def not_set ( ) , do: @ not_set
73
+ def if_set ( type ) , do: Map . update ( type , :bitmap , @ bit_optional , & ( & 1 ||| @ bit_optional ) )
74
+ defp term_or_not_set ( ) , do: @ term_or_not_set
75
+
71
76
## Set operations
72
77
73
78
def term? ( descr ) , do: subtype_static ( @ term , Map . delete ( descr , :dynamic ) )
@@ -183,10 +188,12 @@ defmodule Module.Types.Descr do
183
188
def negation ( % { } = descr ) , do: difference ( term ( ) , descr )
184
189
185
190
@ doc """
186
- Check if a type is empty. For gradual types, check that the upper bound
187
- (the dynamic part) is empty. Stop as soon as one non-empty component is found.
188
- Simpler components (bitmap, atom) are checked first for speed since, if they are
189
- present, the type is non-empty as we normalize then during construction.
191
+ Check if a type is empty.
192
+
193
+ For gradual types, check that the upper bound (the dynamic part) is empty.
194
+ Stop as soon as one non-empty component is found. Simpler components
195
+ (bitmap, atom) are checked first for speed since, if they are present,
196
+ the type is non-empty as we normalize then during construction.
190
197
"""
191
198
def empty? ( % { } = descr ) do
192
199
descr = Map . get ( descr , :dynamic , descr )
@@ -196,8 +203,6 @@ defmodule Module.Types.Descr do
196
203
( not Map . has_key? ( descr , :map ) or map_empty? ( descr . map ) ) )
197
204
end
198
205
199
- def not_empty? ( descr ) , do: not empty? ( descr )
200
-
201
206
@ doc """
202
207
Converts a descr to its quoted representation.
203
208
"""
@@ -327,7 +332,7 @@ defmodule Module.Types.Descr do
327
332
@ doc """
328
333
Check if two types have a non-empty intersection.
329
334
"""
330
- def intersect? ( left , right ) , do: not_empty ?( intersection ( left , right ) )
335
+ def intersect? ( left , right ) , do: not empty ?( intersection ( left , right ) )
331
336
332
337
@ doc """
333
338
Checks if a type is a compatible subtype of another.
@@ -349,10 +354,10 @@ defmodule Module.Types.Descr do
349
354
{ input_dynamic , input_static } = Map . pop ( input_type , :dynamic , input_type )
350
355
expected_dynamic = Map . get ( expected_type , :dynamic , expected_type )
351
356
352
- if not empty? ( input_static ) do
353
- subtype_static ( input_static , expected_dynamic )
354
- else
357
+ if empty? ( input_static ) do
355
358
intersect? ( input_dynamic , expected_dynamic )
359
+ else
360
+ subtype_static ( input_static , expected_dynamic )
356
361
end
357
362
end
358
363
@@ -496,7 +501,7 @@ defmodule Module.Types.Descr do
496
501
# on top of the static type. Though, the latter may be used for printing purposes.
497
502
#
498
503
# There are two ways for a descr to represent a static type: either the
499
- # `:dynamic` field is unset , or it contains a type equal to the static component
504
+ # `:dynamic` field is not_set , or it contains a type equal to the static component
500
505
# (that is, there are no extra dynamic values).
501
506
502
507
defp dynamic_intersection ( left , right ) do
@@ -528,38 +533,12 @@ defmodule Module.Types.Descr do
528
533
end
529
534
end
530
535
531
- ## Not_set
532
-
533
- # `not_set()` is a special base type that represents an unset field in a map.
534
- # E.g., `%{a: integer(), b: not_set(), ...}` represents a map with an integer
535
- # field `a` and an unset field `b`, and possibly other fields.
536
-
537
- # The `if_set()` modifier is syntactic sugar for specifying the key as a union
538
- # of the key type and `not_set()`. For example, `%{:foo => if_set(integer())}`
539
- # is equivalent to `%{:foo => integer() or not_set()}`.
540
-
541
- # `not_set()` has no meaning outside of map types.
542
-
543
- def not_set ( ) , do: @ unset
544
- def if_set ( type ) , do: Map . update ( type , :bitmap , @ bit_unset , & ( & 1 ||| @ bit_unset ) )
545
-
546
- defp is_optional? ( type ) , do: ( Map . get ( type , :bitmap , 0 ) &&& @ bit_unset ) != 0
547
-
548
- defp remove_not_set ( type ) do
549
- case type do
550
- % { :bitmap => @ bit_unset } -> Map . delete ( type , :bitmap )
551
- % { :bitmap => bitmap } -> Map . put ( type , :bitmap , bitmap &&& ~~~ @ bit_unset )
552
- _ -> type
553
- end
554
- end
555
-
556
536
## Map
557
537
#
558
- # Map operations.
559
- #
560
538
# Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs
561
539
# `{map_literal, negated_literals}` where `map_literal` is a map type literal
562
540
# and `negated_literals` is a list of map type literals that are negated from it.
541
+ # Each pair is augmented with the :open or :closed tag.
563
542
#
564
543
# A map literal is a pair `{:open | :closed, %{keys => value_types}}`.
565
544
#
@@ -579,6 +558,29 @@ defmodule Module.Types.Descr do
579
558
# Set-theoretic operations take two DNFs (lists) and return a DNF (list).
580
559
# Simplifications can be done to prune the latter.
581
560
561
+ ## Not_set
562
+
563
+ # `not_set()` is a special base type that represents an not_set field in a map.
564
+ # E.g., `%{a: integer(), b: not_set(), ...}` represents a map with an integer
565
+ # field `a` and an not_set field `b`, and possibly other fields.
566
+
567
+ # The `if_set()` modifier is syntactic sugar for specifying the key as a union
568
+ # of the key type and `not_set()`. For example, `%{:foo => if_set(integer())}`
569
+ # is equivalent to `%{:foo => integer() or not_set()}`.
570
+
571
+ # `not_set()` has no meaning outside of map types.
572
+
573
+ defp optional? ( % { bitmap: bitmap } ) when ( bitmap &&& @ bit_optional ) != 0 , do: true
574
+ defp optional? ( _ ) , do: false
575
+
576
+ defp remove_not_set ( type ) do
577
+ case type do
578
+ % { bitmap: @ bit_optional } -> Map . delete ( type , :bitmap )
579
+ % { bitmap: bitmap } -> % { type | bitmap: bitmap &&& ~~~ @ bit_optional }
580
+ _ -> type
581
+ end
582
+ end
583
+
582
584
# Create a DNF from a specification of a map type.
583
585
defp map_new ( open_or_closed , pairs ) , do: [ { open_or_closed , Map . new ( pairs ) , [ ] } ]
584
586
@@ -634,36 +636,34 @@ defmodule Module.Types.Descr do
634
636
635
637
# Given two unions of maps, intersects each pair of maps.
636
638
defp map_intersection ( dnf1 , dnf2 ) do
637
- Enum . flat_map ( dnf1 , & map_intersection_aux ( & 1 , dnf2 ) )
638
- end
639
-
640
- # Intersects a map with a union of maps.
641
- defp map_intersection_aux ( { tag1 , pos1 , negs1 } , dnf2 ) do
642
- Enum . reduce ( dnf2 , [ ] , fn { tag2 , pos2 , negs2 } , acc ->
643
- try do
644
- { tag , fields } = map_literal_intersection ( tag1 , pos1 , tag2 , pos2 )
645
- [ { tag , fields , negs1 ++ negs2 } | acc ]
646
- catch
647
- :empty_intersection -> acc
648
- end
649
- end )
639
+ for { tag1 , pos1 , negs1 } <- dnf1 ,
640
+ { tag2 , pos2 , negs2 } <- dnf2 ,
641
+ reduce: [ ] do
642
+ acc ->
643
+ try do
644
+ { tag , fields } = map_literal_intersection ( tag1 , pos1 , tag2 , pos2 )
645
+ [ { tag , fields , negs1 ++ negs2 } | acc ]
646
+ catch
647
+ :empty -> acc
648
+ end
649
+ end
650
650
end
651
651
652
652
# Intersects two map literals; throws if their intersection is empty.
653
653
defp map_literal_intersection ( tag1 , map1 , tag2 , map2 ) do
654
- default1 = if tag1 == :open , do: @ term_or_unset , else: @ unset
655
- default2 = if tag2 == :open , do: @ term_or_unset , else: @ unset
654
+ default1 = if tag1 == :open , do: term_or_not_set ( ) , else: not_set ( )
655
+ default2 = if tag2 == :open , do: term_or_not_set ( ) , else: not_set ( )
656
656
657
657
# if any intersection of values is empty, the whole intersection is empty
658
658
new_fields =
659
659
( for { key , value_type } <- map1 do
660
660
value_type2 = Map . get ( map2 , key , default2 )
661
661
t = intersection ( value_type , value_type2 )
662
- if empty? ( t ) , do: throw ( :empty_intersection ) , else: { key , t }
662
+ if empty? ( t ) , do: throw ( :empty ) , else: { key , t }
663
663
end ++
664
664
for { key , value_type } <- map2 , not is_map_key ( map1 , key ) do
665
665
t = intersection ( default1 , value_type )
666
- if empty? ( t ) , do: throw ( :empty_intersection ) , else: { key , t }
666
+ if empty? ( t ) , do: throw ( :empty ) , else: { key , t }
667
667
end )
668
668
|> Map . new ( )
669
669
@@ -674,26 +674,19 @@ defmodule Module.Types.Descr do
674
674
end
675
675
676
676
defp map_difference ( dnf1 , dnf2 ) do
677
- case dnf2 do
678
- [ ] ->
679
- dnf1
680
-
681
- [ lit2 | dnf2 ] ->
682
- Enum . flat_map ( dnf1 , fn lit1 -> map_single_difference ( lit1 , lit2 ) end )
683
- |> map_difference ( dnf2 )
684
- end
685
- end
686
-
687
- # Computes the difference between two maps union.
688
- defp map_single_difference ( { tag1 , fields1 , negs1 } , { tag2 , fields2 , negs2 } ) do
689
- Enum . reduce ( negs2 , [ { tag1 , fields1 , [ { tag2 , fields2 } | negs1 ] } ] , fn
690
- { tag2 , fields2 } , acc ->
691
- try do
692
- { tag , fields } = map_literal_intersection ( tag1 , fields1 , tag2 , fields2 )
693
- [ { tag , fields , negs1 } | acc ]
694
- catch
695
- :empty_intersection -> acc
696
- end
677
+ Enum . reduce ( dnf2 , dnf1 , fn { tag2 , fields2 , negs2 } , dnf1 ->
678
+ Enum . reduce ( dnf1 , [ ] , fn { tag1 , fields1 , negs1 } , acc ->
679
+ acc = [ { tag1 , fields1 , [ { tag2 , fields2 } | negs1 ] } | acc ]
680
+
681
+ Enum . reduce ( negs2 , acc , fn { neg_tag2 , neg_fields2 } , acc ->
682
+ try do
683
+ { tag , fields } = map_literal_intersection ( tag1 , fields1 , neg_tag2 , neg_fields2 )
684
+ [ { tag , fields , negs1 } | acc ]
685
+ catch
686
+ :empty -> acc
687
+ end
688
+ end )
689
+ end )
697
690
end )
698
691
end
699
692
@@ -720,12 +713,12 @@ defmodule Module.Types.Descr do
720
713
for { neg_key , neg_type } <- neg_fields , not is_map_key ( fields , neg_key ) do
721
714
cond do
722
715
# key is required, and the positive map is closed: empty intersection
723
- tag == :closed and not is_optional ?( neg_type ) ->
716
+ tag == :closed and not optional ?( neg_type ) ->
724
717
throw ( :no_intersection )
725
718
726
719
# if the positive map is open
727
720
tag == :open ->
728
- diff = difference ( @ term_or_unset , neg_type )
721
+ diff = difference ( term_or_not_set ( ) , neg_type )
729
722
empty? ( diff ) or map_empty? ( tag , Map . put ( fields , neg_key , diff ) , negs )
730
723
end
731
724
end
@@ -737,11 +730,11 @@ defmodule Module.Types.Descr do
737
730
empty? ( diff ) or map_empty? ( tag , Map . put ( fields , key , diff ) , negs )
738
731
739
732
% { } ->
740
- if neg_tag == :closed and not is_optional ?( type ) do
733
+ if neg_tag == :closed and not optional ?( type ) do
741
734
throw ( :no_intersection )
742
735
else
743
736
# an absent key in a open negative map can be ignored
744
- default2 = if neg_tag == :open , do: @ term_or_unset , else: @ unset
737
+ default2 = if neg_tag == :open , do: @ term_or_not_set , else: @ not_set
745
738
diff = difference ( type , default2 )
746
739
empty? ( diff ) or map_empty? ( tag , Map . put ( fields , key , diff ) , negs )
747
740
end
@@ -760,7 +753,7 @@ defmodule Module.Types.Descr do
760
753
{ fst , snd } =
761
754
case single_split ( { tag , fields } , key ) do
762
755
# { .. } the open map in a positive intersection can be ignored
763
- :no_split -> { @ term_or_unset , @ term_or_unset }
756
+ :no_split -> { term_or_not_set ( ) , term_or_not_set ( ) }
764
757
# {typeof l, rest} is added to the positive accumulator
765
758
{ value_type , rest_of_map } -> { value_type , rest_of_map }
766
759
end
@@ -780,10 +773,10 @@ defmodule Module.Types.Descr do
780
773
781
774
cond do
782
775
value_type != nil -> { value_type , map_descr ( tag , rest_of_map ) }
783
- tag == :closed -> { @ unset , map_descr ( tag , rest_of_map ) }
776
+ tag == :closed -> { not_set ( ) , map_descr ( tag , rest_of_map ) }
784
777
# case where there is an open map with no keys { .. }
785
778
map_size ( fields ) == 0 -> :no_split
786
- true -> { @ term_or_unset , map_descr ( tag , rest_of_map ) }
779
+ true -> { term_or_not_set ( ) , map_descr ( tag , rest_of_map ) }
787
780
end
788
781
end
789
782
@@ -829,12 +822,12 @@ defmodule Module.Types.Descr do
829
822
try do
830
823
for { neg_key , neg_type } when not is_map_key ( fields , neg_key ) <- neg_fields do
831
824
# key is required, and the positive map is closed: empty intersection
832
- if tag == :closed and not is_optional ?( neg_type ) , do: throw ( :no_intersection )
825
+ if tag == :closed and not optional ?( neg_type ) , do: throw ( :no_intersection )
833
826
end
834
827
835
828
for { key , type } when not is_map_key ( neg_fields , key ) <- fields ,
836
829
# key is required, and the negative map is closed: empty intersection
837
- not is_optional ?( type ) and neg_tag == :closed do
830
+ not optional ?( type ) and neg_tag == :closed do
838
831
throw ( :no_intersection )
839
832
end
840
833
@@ -868,10 +861,10 @@ defmodule Module.Types.Descr do
868
861
869
862
defp fields_to_quoted ( tag , map ) do
870
863
for { key , type } <- map ,
871
- not ( tag == :open and is_optional ?( type ) and term? ( type ) ) do
864
+ not ( tag == :open and optional ?( type ) and term? ( type ) ) do
872
865
cond do
873
- is_optional ?( type ) and empty? ( type ) -> { literal ( key ) , { :not_set , [ ] , [ ] } }
874
- is_optional ?( type ) -> { literal ( key ) , { :if_set , [ ] , [ to_quoted ( type ) ] } }
866
+ optional ?( type ) and empty? ( type ) -> { literal ( key ) , { :not_set , [ ] , [ ] } }
867
+ optional ?( type ) -> { literal ( key ) , { :if_set , [ ] , [ to_quoted ( type ) ] } }
875
868
true -> { literal ( key ) , to_quoted ( type ) }
876
869
end
877
870
end
@@ -884,7 +877,7 @@ defmodule Module.Types.Descr do
884
877
# normalization algorithms on pairs.
885
878
886
879
# Takes a DNF of pairs and simplifies it into a equivalent single list (union)
887
- # of type pairs. The `term` argument should be either `@term_or_unset ` (for
880
+ # of type pairs. The `term` argument should be either `@term_or_not_set ` (for
888
881
# map value types) or `@term` in general.
889
882
# Remark: all lines of a pair dnf are naturally disjoint, because choosing a
890
883
# different edge means intersection with a literal or its negation.
@@ -909,15 +902,15 @@ defmodule Module.Types.Descr do
909
902
fn { t_i , s_i } , { accu , diff_of_t_i } ->
910
903
i = intersection ( t , t_i )
911
904
912
- if not_empty? ( i ) do
905
+ if empty? ( i ) do
906
+ { accu , diff_of_t_i }
907
+ else
913
908
diff_of_t_i = difference ( diff_of_t_i , t_i )
914
909
s_diff = difference ( s , s_i )
915
910
916
- if not_empty? ( s_diff ) ,
917
- do: { [ i | accu ] , diff_of_t_i } ,
918
- else: { accu , diff_of_t_i }
919
- else
920
- { accu , diff_of_t_i }
911
+ if empty? ( s_diff ) ,
912
+ do: { accu , diff_of_t_i } ,
913
+ else: { [ i | accu ] , diff_of_t_i }
921
914
end
922
915
end
923
916
)
0 commit comments