@@ -27,11 +27,8 @@ defmodule Module.Types.Descr do
2727 @ bit_top ( 1 <<< 7 ) - 1
2828 @ bit_number @ bit_integer ||| @ bit_float
2929
30- # Remark: those use AST for BDDs
31- defmacrop bdd_leaf ( arg1 , arg2 ) , do: { arg1 , arg2 }
32-
33- defmacrop domain_key ( key ) ,
34- do: { :domain_key , key }
30+ defmacro bdd_leaf ( arg1 , arg2 ) , do: { arg1 , arg2 }
31+ defmacro domain_key ( key ) , do: { :domain_key , key }
3532
3633 @ domain_key_types [
3734 { :domain_key , :binary } ,
@@ -454,11 +451,7 @@ defmodule Module.Types.Descr do
454451 defp intersection ( :map , v1 , v2 ) , do: map_intersection ( v1 , v2 )
455452 defp intersection ( :optional , 1 , 1 ) , do: 1
456453 defp intersection ( :tuple , v1 , v2 ) , do: tuple_intersection ( v1 , v2 )
457-
458- defp intersection ( :fun , v1 , v2 ) do
459- bdd = fun_intersection ( v1 , v2 )
460- if bdd == :bdd_bot , do: 0 , else: bdd
461- end
454+ defp intersection ( :fun , v1 , v2 ) , do: fun_intersection ( v1 , v2 )
462455
463456 defp intersection ( :dynamic , v1 , v2 ) do
464457 descr = dynamic_intersection ( v1 , v2 )
@@ -548,11 +541,7 @@ defmodule Module.Types.Descr do
548541 defp difference ( :map , v1 , v2 ) , do: map_difference ( v1 , v2 )
549542 defp difference ( :optional , 1 , 1 ) , do: 0
550543 defp difference ( :tuple , v1 , v2 ) , do: tuple_difference ( v1 , v2 )
551-
552- defp difference ( :fun , v1 , v2 ) do
553- bdd = fun_difference ( v1 , v2 )
554- if bdd == :bdd_bot , do: 0 , else: bdd
555- end
544+ defp difference ( :fun , v1 , v2 ) , do: fun_difference ( v1 , v2 )
556545
557546 @ doc """
558547 Compute the negation of a type.
@@ -4425,23 +4414,7 @@ defmodule Module.Types.Descr do
44254414
44264415 ## BDD helpers
44274416
4428- defp bdd_map ( bdd , fun ) do
4429- case bdd do
4430- :bdd_bot ->
4431- :bdd_bot
4432-
4433- :bdd_top ->
4434- :bdd_top
4435-
4436- { _ , _ } ->
4437- fun . ( bdd )
4438-
4439- { literal , left , union , right } ->
4440- { fun . ( literal ) , bdd_map ( left , fun ) , bdd_map ( union , fun ) , bdd_map ( right , fun ) }
4441- end
4442- end
4443-
4444- defp bdd_union ( bdd1 , bdd2 ) do
4417+ def bdd_union ( bdd1 , bdd2 ) do
44454418 case { bdd1 , bdd2 } do
44464419 { :bdd_top , _bdd } ->
44474420 :bdd_top
@@ -4478,7 +4451,7 @@ defmodule Module.Types.Descr do
44784451 end
44794452 end
44804453
4481- defp bdd_difference ( bdd1 , bdd2 ) do
4454+ def bdd_difference ( bdd1 , bdd2 ) do
44824455 case { bdd1 , bdd2 } do
44834456 { _bdd , :bdd_top } ->
44844457 :bdd_bot
@@ -4567,22 +4540,14 @@ defmodule Module.Types.Descr do
45674540 end
45684541 end
45694542
4570- defp bdd_compare ( bdd1 , bdd2 ) do
4571- case { bdd_head ( bdd1 ) , bdd_head ( bdd2 ) } do
4572- { lit1 , lit2 } when lit1 < lit2 -> { :lt , bdd_expand ( bdd1 ) , bdd2 }
4573- { lit1 , lit2 } when lit1 > lit2 -> { :gt , bdd1 , bdd_expand ( bdd2 ) }
4574- _ -> { :eq , bdd1 , bdd2 }
4575- end
4576- end
4577-
45784543 # Version of i \ (u1 v u2) that only computes the union if i is not bottom
45794544 defp bdd_difference_union ( :bdd_bot , _u1 , _u2 ) ,
45804545 do: :bdd_bot
45814546
45824547 defp bdd_difference_union ( i , u1 , u2 ) ,
45834548 do: bdd_difference ( i , bdd_union ( u1 , u2 ) )
45844549
4585- defp bdd_intersection ( bdd1 , bdd2 ) do
4550+ def bdd_intersection ( bdd1 , bdd2 ) do
45864551 case { bdd1 , bdd2 } do
45874552 { :bdd_top , bdd } ->
45884553 bdd
@@ -4647,15 +4612,15 @@ defmodule Module.Types.Descr do
46474612 do: bdd_intersection ( i , bdd_union ( u1 , u2 ) )
46484613
46494614 # Lazy negation: eliminate the union, then perform normal negation (switching leaves)
4650- defp bdd_negation ( :bdd_top ) , do: :bdd_bot
4651- defp bdd_negation ( :bdd_bot ) , do: :bdd_top
4652- defp bdd_negation ( { _ , _ } = pair ) , do: { pair , :bdd_bot , :bdd_bot , :bdd_top }
4615+ def bdd_negation ( :bdd_top ) , do: :bdd_bot
4616+ def bdd_negation ( :bdd_bot ) , do: :bdd_top
4617+ def bdd_negation ( { _ , _ } = pair ) , do: { pair , :bdd_bot , :bdd_bot , :bdd_top }
46534618
4654- defp bdd_negation ( { lit , c , u , d } ) do
4619+ def bdd_negation ( { lit , c , u , d } ) do
46554620 { lit , bdd_negation ( bdd_union ( c , u ) ) , :bdd_bot , bdd_negation ( bdd_union ( d , u ) ) }
46564621 end
46574622
4658- defp bdd_to_dnf ( bdd ) , do: bdd_to_dnf ( [ ] , [ ] , [ ] , bdd )
4623+ def bdd_to_dnf ( bdd ) , do: bdd_to_dnf ( [ ] , [ ] , [ ] , bdd )
46594624
46604625 defp bdd_to_dnf ( acc , _pos , _neg , :bdd_bot ) , do: acc
46614626 defp bdd_to_dnf ( acc , pos , neg , :bdd_top ) , do: [ { pos , neg } | acc ]
@@ -4674,6 +4639,30 @@ defmodule Module.Types.Descr do
46744639 |> bdd_to_dnf ( pos , [ lit | neg ] , d )
46754640 end
46764641
4642+ defp bdd_compare ( bdd1 , bdd2 ) do
4643+ case { bdd_head ( bdd1 ) , bdd_head ( bdd2 ) } do
4644+ { lit1 , lit2 } when lit1 < lit2 -> { :lt , bdd_expand ( bdd1 ) , bdd2 }
4645+ { lit1 , lit2 } when lit1 > lit2 -> { :gt , bdd1 , bdd_expand ( bdd2 ) }
4646+ _ -> { :eq , bdd1 , bdd2 }
4647+ end
4648+ end
4649+
4650+ defp bdd_map ( bdd , fun ) do
4651+ case bdd do
4652+ :bdd_bot ->
4653+ :bdd_bot
4654+
4655+ :bdd_top ->
4656+ :bdd_top
4657+
4658+ { _ , _ } ->
4659+ fun . ( bdd )
4660+
4661+ { literal , left , union , right } ->
4662+ { fun . ( literal ) , bdd_map ( left , fun ) , bdd_map ( union , fun ) , bdd_map ( right , fun ) }
4663+ end
4664+ end
4665+
46774666 @ compile { :inline , bdd_expand: 1 , bdd_head: 1 }
46784667 defp bdd_expand ( { _ , _ } = pair ) , do: { pair , :bdd_top , :bdd_bot , :bdd_bot }
46794668 defp bdd_expand ( bdd ) , do: bdd
0 commit comments