@@ -138,22 +138,18 @@ defmodule Module.Types.Descr do
138138 Creates a function from overlapping function clauses.
139139 """
140140 def fun_from_inferred_clauses ( args_clauses ) do
141- if true do
142- domain_clauses =
143- Enum . reduce ( args_clauses , [ ] , fn { args , return } , acc ->
144- domain = args |> Enum . map ( & upper_bound / 1 ) |> args_to_domain ( )
145- pivot_overlapping_clause ( domain , upper_bound ( return ) , acc )
146- end )
141+ domain_clauses =
142+ Enum . reduce ( args_clauses , [ ] , fn { args , return } , acc ->
143+ domain = args |> Enum . map ( & upper_bound / 1 ) |> args_to_domain ( )
144+ pivot_overlapping_clause ( domain , upper_bound ( return ) , acc )
145+ end )
147146
148- funs =
149- for { domain , return } <- domain_clauses ,
150- args <- domain_to_args ( domain ) ,
151- do: fun ( args , dynamic ( return ) )
147+ funs =
148+ for { domain , return } <- domain_clauses ,
149+ args <- domain_to_args ( domain ) ,
150+ do: fun ( args , dynamic ( return ) )
152151
153- Enum . reduce ( funs , & intersection / 2 )
154- else
155- dynamic ( fun ( ) )
156- end
152+ Enum . reduce ( funs , & intersection / 2 )
157153 end
158154
159155 defp pivot_overlapping_clause ( domain , return , [ { acc_domain , acc_return } | acc ] ) do
@@ -515,9 +511,6 @@ defmodule Module.Types.Descr do
515511 def empty? ( :term ) , do: false
516512
517513 def empty? ( % { } = descr ) do
518- # IO.puts("empty?")
519-
520- # IO.puts("checking if the type is empty")
521514 case :maps . get ( :dynamic , descr , descr ) do
522515 :term ->
523516 false
@@ -526,13 +519,6 @@ defmodule Module.Types.Descr do
526519 true
527520
528521 descr ->
529- # cond do
530- # not (Map.has_key?(descr, :tuple) or Map.has_key?(descr, :list) or Map.has_key?(descr, :fun)) ->
531- # IO.puts("descr: #{inspect(descr)}")
532- # true ->
533- # :ok
534- # end
535-
536522 not Map . has_key? ( descr , :atom ) and
537523 not Map . has_key? ( descr , :bitmap ) and
538524 not Map . has_key? ( descr , :optional ) and
@@ -543,8 +529,6 @@ defmodule Module.Types.Descr do
543529 end
544530 end
545531
546- # defp ahah(), do: IO.puts("empty?")
547-
548532 # For atom, bitmap, tuple, and optional, if the key is present,
549533 # then they are not empty,
550534 defp empty_key? ( :fun , value ) , do: fun_empty? ( value )
@@ -1341,34 +1325,13 @@ defmodule Module.Types.Descr do
13411325 # - arrow_intersections: The list of function arrows to process
13421326
13431327 # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
1344- defp aux_apply ( result , _input , rets_reached , arrow_intersections , depth \\ 0 )
1345-
1346- defp aux_apply ( result , _input , rets_reached , [ ] , depth ) do
1328+ defp aux_apply ( result , _input , rets_reached , [ ] ) do
13471329 if subtype? ( rets_reached , result ) , do: result , else: union ( result , rets_reached )
13481330 end
13491331
1350- defp aux_apply ( result , input , returns_reached , [ { dom , ret } | arrow_intersections ] , depth ) do
1351- # Performance warning thresholds
1352- if Map . has_key? ( input , :dynamic ) do
1353- IO . puts ( "aux_apply called with dynamic input" )
1354- raise "aux_apply called with dynamic input"
1355- end
1356-
1357- max_depth = 15
1358-
1359- if depth > max_depth do
1360- IO . puts ( "PERFORMANCE WARNING: aux_apply depth #{ depth } (threshold: #{ max_depth } )" )
1361- IO . puts ( "aux_apply [depth:#{ depth } ]" )
1362- IO . puts ( "input: #{ inspect ( input ) } " )
1363- IO . puts ( "returns_reached: #{ inspect ( returns_reached ) } " )
1364- IO . puts ( "dom: #{ inspect ( dom ) } " )
1365- IO . puts ( "ret: #{ inspect ( ret ) } " )
1366- IO . puts ( "arrow_intersections: #{ inspect ( arrow_intersections ) } " )
1367- IO . puts ( "--------------------------------" )
1368- end
1369-
1332+ defp aux_apply ( result , input , returns_reached , [ { args , ret } | arrow_intersections ] ) do
13701333 # Calculate the part of the input not covered by this arrow's domain
1371- dom_subtract = difference ( input , args_to_domain ( dom ) )
1334+ dom_subtract = difference ( input , args_to_domain ( args ) )
13721335
13731336 # Refine the return type by intersecting with this arrow's return type
13741337 ret_refine = intersection ( returns_reached , ret )
@@ -1384,7 +1347,7 @@ defmodule Module.Types.Descr do
13841347 if empty? ( dom_subtract ) do
13851348 result
13861349 else
1387- aux_apply ( result , dom_subtract , returns_reached , arrow_intersections , depth + 1 )
1350+ aux_apply ( result , dom_subtract , returns_reached , arrow_intersections )
13881351 end
13891352
13901353 # 2. Return type refinement
@@ -1394,7 +1357,7 @@ defmodule Module.Types.Descr do
13941357
13951358 # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
13961359 # should result in (atom() ∩ pid()), which is none().
1397- aux_apply ( result , input , ret_refine , arrow_intersections , depth + 1 )
1360+ aux_apply ( result , input , ret_refine , arrow_intersections )
13981361 end
13991362
14001363 # Takes all the paths from the root to the leaves finishing with a 1,
@@ -1423,8 +1386,6 @@ defmodule Module.Types.Descr do
14231386 # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty
14241387 # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty
14251388 defp fun_empty? ( bdd ) do
1426- # IO.puts("fun_empty?")
1427- # IO.puts("on bdd: #{inspect(bdd)}")
14281389 case bdd do
14291390 :fun_bottom -> true
14301391 :fun_top -> false
@@ -1467,7 +1428,7 @@ defmodule Module.Types.Descr do
14671428 # determines emptiness.
14681429 length ( neg_arguments ) == positive_arity and
14691430 subtype? ( args_to_domain ( neg_arguments ) , positive_domain ) and
1470- phi_starter ( neg_arguments , negation ( neg_return ) , positives )
1431+ phi_starter ( neg_arguments , neg_return , positives )
14711432 end )
14721433 end
14731434 end
@@ -1504,181 +1465,68 @@ defmodule Module.Types.Descr do
15041465 # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
15051466 #
15061467 # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
1507- # def descr_size(:term), do: 1
1508-
1509- # def descr_size(%{} = descr) do
1510- # Enum.reduce(descr, 0, fn {key, value}, acc ->
1511- # acc + descr_size(key, value)
1512- # end)
1513- # end
1514-
1515- # def descr_size(:tuple, dnf) do
1516- # Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
1517- # end
1518-
1519- # def descr_size(:fun, bdd), do: bdd_size(bdd)
1520-
1521- # def descr_size(:map, dnf) do
1522- # Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
1523- # acc + 1 + length(negs)
1524- # end)
1525- # end
1526-
1527- # def descr_size(:list, dnf) do
1528- # Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
1529- # acc + 1 + length(negs)
1530- # end)
1531- # end
1532-
1533- # def descr_size(_, _), do: 1
1534-
1535- # defp bdd_size({fun, l, r}) do
1536- # bdd_size(l) + bdd_size(r) + 1
1537- # end
1538-
1539- # defp bdd_size(:fun_top), do: 1
1540- # defp bdd_size(:fun_bottom), do: 0
1541-
1542- # defp list_dnf_size(dnf) do
1543- # Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
1544- # 1 + length(negs)
1545- # end)
1546- # end
1547-
1548- # defp all_distinct_non_empty_domains?([{args, _ret}]) do
1549- # not empty?(args_to_domain(args))
1550- # end
1551-
1552- # defp all_distinct_non_empty_domains?(positives) do
1553- # # For each two elements of positives, their domains are distinct
1554- # for {args1, _ret1} <- positives,
1555- # {args2, _ret2} <- positives,
1556- # args1 != args2,
1557- # reduce: true do
1558- # acc ->
1559- # # 1. check there are no empty args
1560- # dom1 = args_to_domain(args1)
1561- # dom2 = args_to_domain(args2)
1562- # if empty?(dom1) or empty?(dom2) do
1563- # false
1564- # else
1565- # d = disjoint?(dom1, dom2)
1566- # if not d do
1567- # end
1568- # acc and d
1569- # end
1570- # end
1571- # end
1572-
15731468 defp all_non_empty_domains? ( positives ) do
15741469 Enum . all? ( positives , fn { args , _ret } -> not empty? ( args_to_domain ( args ) ) end )
15751470 end
15761471
15771472 defp phi_starter ( arguments , return , positives ) do
1578- ### SPECIAL CASE: all the positives (intersection) functions have distinct domains
1579- # In that case, checking subtyping of it with a single arrow is simply:
1580- # checking that the union of the domains of the positives is a supertype of the domain of the arrow
1581- # and that applying the input type of the arrow to the intersection gives sth that is a subtype of the return type of the arrow
1473+ ### SPECIAL CASE: all the positives (intersection) functions have non-empty arguments
1474+ # In that case, checking subtyping of it with a single arrow is simply checking that the union
1475+ # of the domains of the positives is a supertype of the domain of the arrow
1476+ # and that applying the input type of the arrow to the intersection gives sth that
1477+ # is a subtype of the return type of the arrow
15821478 if all_non_empty_domains? ( positives ) and all_non_empty_domains? ( [ { arguments , return } ] ) do
1583- return = negation ( return )
1584-
1585- type_positives =
1586- Enum . map ( positives , fn { args , ret } -> fun ( args , ret ) end ) |> Enum . reduce ( & intersection / 2 )
1587-
1588- { :ok , _dom , static_arrows } = fun_normalize ( type_positives , length ( arguments ) , :static )
1589- result = fun_apply_static ( arguments , static_arrows , false )
1590-
1591- r = subtype? ( result , return )
1592-
1593- if r do
1594- r
1595- else
1596- false
1597- end
1479+ fun_apply_static ( arguments , [ positives ] , false )
1480+ |> subtype? ( return )
15981481 else
1599- # Show the caller of this function
1600- # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
1601- # IO.puts("Starting phi starter with return: #{inspect(return)}")
1602- # IO.puts("Starting phi starter with positives: #{inspect(positives)}")
1603- # Total size of the descrs in arguments, return, and positives
1604- # total_size =
1605- # arguments
1606- # |> Enum.map(&descr_size/1)
1607- # |> Enum.sum()
1608- # |> Kernel.+(descr_size(return))
1609- # |> Kernel.+(
1610- # Enum.reduce(positives, 0, fn {args, ret}, acc ->
1611- # acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
1612- # end)
1613- # )
1614-
1615- # start_time = DateTime.utc_now()
1616-
16171482 n = length ( arguments )
16181483 # Arity mismatch: if there is one positive function with a different arity,
16191484 # then it cannot be a subtype of the (arguments->type) functions.
16201485 if Enum . any? ( positives , fn { args , _ret } -> length ( args ) != n end ) do
16211486 false
16221487 else
16231488 # Initialize memoization cache
1624- # 1. check that the domain is a subtype of the union of all
1625- # the domains of the positives
1626- # domain = args_to_domain(arguments)
1627- # positives_domain = Enum.reduce(positives, none(), fn {args, _ret}, acc -> union(acc, args_to_domain(args)) end)
1628- # if not subtype?(domain, positives_domain) do
1629- # false
1630- # else
1631- # 2. check that the return type is a subtype of the union of all
1632- # the return types of the positives
1633-
16341489 Process . put ( :phi_cache , % { } )
16351490 arguments = Enum . map ( arguments , & { false , & 1 } )
1636- { result , call_count } = phi ( arguments , { false , return } , positives , 0 )
1637- cache_size = map_size ( Process . get ( :phi_cache , % { } ) )
1638- # Recursive calls
1639-
1640- result
1491+ phi ( arguments , { false , negation ( return ) } , positives )
16411492 end
1642-
1643- # end
16441493 end
16451494 end
16461495
1647- defp phi ( args , { b , t } , [ ] , call_count ) do
1648- { Enum . any? ( args , fn { bool , typ } -> bool and empty? ( typ ) end ) or ( b and empty? ( t ) ) , call_count }
1496+ defp phi ( args , { b , t } , [ ] ) do
1497+ Enum . any? ( args , fn { bool , typ } -> bool and empty? ( typ ) end ) or ( b and empty? ( t ) )
16491498 end
16501499
1651- defp phi ( args , { b , ret } , [ { arguments , return } | rest_positive ] , call_count ) do
1500+ defp phi ( args , { b , ret } , [ { arguments , return } | rest_positive ] ) do
16521501 # Create cache key from function arguments
16531502 cache_key = { args , { b , ret } , [ { arguments , return } | rest_positive ] }
16541503 cache = Process . get ( :phi_cache , % { } )
16551504
16561505 case Map . get ( cache , cache_key ) do
16571506 nil ->
16581507 # Compute result and cache it
1659- { result1 , call_count1 } =
1660- phi ( args , { true , intersection ( ret , return ) } , rest_positive , call_count + 1 )
1508+ result1 = phi ( args , { true , intersection ( ret , return ) } , rest_positive )
16611509
16621510 if not result1 do
16631511 Process . put ( :phi_cache , Map . put ( cache , cache_key , false ) )
1664- { false , call_count }
1512+ false
16651513 else
16661514 # This doesn't stop if one intermediate result is false?
1667- { result2 , call_count2 } =
1515+ result2 =
16681516 Enum . with_index ( arguments )
1669- |> Enum . reduce_while ( { true , call_count1 } , fn { type , index } , { acc_result , acc_count } ->
1670- { new_result , new_count } =
1517+ |> Enum . reduce_while ( true , fn { type , index } , acc_result ->
1518+ new_result =
16711519 List . update_at ( args , index , fn { _ , arg } -> { true , difference ( arg , type ) } end )
1672- |> phi ( { b , ret } , rest_positive , acc_count + 1 )
1520+ |> phi ( { b , ret } , rest_positive )
16731521
16741522 if new_result do
1675- { :cont , { acc_result and new_result , new_count } }
1523+ { :cont , acc_result and new_result }
16761524 else
1677- { :halt , { false , new_count } }
1525+ { :halt , false }
16781526 end
16791527 end )
16801528
1681- result = { result1 and result2 , call_count2 }
1529+ result = result1 and result2
16821530 Process . put ( :phi_cache , Map . put ( cache , cache_key , result ) )
16831531 result
16841532 end
@@ -2038,7 +1886,6 @@ defmodule Module.Types.Descr do
20381886 end
20391887
20401888 defp list_difference ( dnf1 , dnf2 ) do
2041- # IO.puts("list_difference")
20421889 Enum . reduce ( dnf2 , dnf1 , fn { t2 , last2 , negs2 } , acc_dnf1 ->
20431890 last2 = list_tail_unfold ( last2 )
20441891
@@ -2068,10 +1915,6 @@ defmodule Module.Types.Descr do
20681915 defp list_empty? ( @ non_empty_list_top ) , do: false
20691916
20701917 defp list_empty? ( dnf ) do
2071- # IO.puts("list_empty?")
2072- # IO.puts("on dnf: #{inspect(dnf)}")
2073- # IO.puts("the dnf has #{length(dnf)} elements")
2074- # IO.puts("i count #{Enum.reduce(dnf, 0, fn {_, _, negs}, acc -> acc + length(negs) end)} negations")
20751918 Enum . all? ( dnf , fn { list_type , last_type , negs } ->
20761919 last_type = list_tail_unfold ( last_type )
20771920
@@ -2903,7 +2746,6 @@ defmodule Module.Types.Descr do
29032746 # Since the algorithm is recursive, we implement the short-circuiting
29042747 # as throw/catch.
29052748 defp map_empty? ( dnf ) do
2906- # IO.puts("map_empty?")
29072749 Enum . all? ( dnf , fn { tag , pos , negs } -> map_empty? ( tag , pos , negs ) end )
29082750 end
29092751
0 commit comments