@@ -138,7 +138,7 @@ 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
141+ if false do
142142 domain_clauses =
143143 Enum . reduce ( args_clauses , [ ] , fn { args , return } , acc ->
144144 domain = args |> Enum . map ( & upper_bound / 1 ) |> args_to_domain ( )
@@ -1479,73 +1479,71 @@ defmodule Module.Types.Descr do
14791479 # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
14801480 #
14811481 # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
1482- def descr_size ( :term ) , do: 1
1483-
1484- def descr_size ( % { } = descr ) do
1485- Enum . reduce ( descr , 0 , fn { key , value } , acc ->
1486- acc + descr_size ( key , value )
1487- end )
1488- end
1489-
1490- def descr_size ( :tuple , dnf ) do
1491- Enum . sum ( Enum . map ( dnf , fn { tag , elems } -> length ( elems ) end ) )
1492- end
1493-
1494- def descr_size ( :fun , bdd ) , do: bdd_size ( bdd )
1495-
1496- def descr_size ( :map , dnf ) do
1497- Enum . reduce ( dnf , 0 , fn { tag , pos , negs } , acc ->
1498- acc + 1 + length ( negs )
1499- end )
1500- end
1501-
1502- def descr_size ( :list , dnf ) do
1503- Enum . reduce ( dnf , 0 , fn { _ , last , negs } , acc ->
1504- acc + 1 + length ( negs )
1505- end )
1506- end
1507-
1508- def descr_size ( _ , _ ) , do: 1
1509-
1510- defp bdd_size ( { fun , l , r } ) do
1511- bdd_size ( l ) + bdd_size ( r ) + 1
1512- end
1513-
1514- defp bdd_size ( :fun_top ) , do: 1
1515- defp bdd_size ( :fun_bottom ) , do: 0
1516-
1517- defp list_dnf_size ( dnf ) do
1518- Enum . reduce ( dnf , 0 , fn { _ , _ , negs } , acc ->
1519- 1 + length ( negs )
1520- end )
1521- end
1522-
1523- defp all_distinct_non_empty_domains? ( [ { args , _ret } ] ) do
1524- not empty? ( args_to_domain ( args ) )
1525- end
1526-
1527- defp all_distinct_non_empty_domains? ( positives ) do
1528- # For each two elements of positives, their domains are distinct
1529- for { args1 , _ret1 } <- positives ,
1530- { args2 , _ret2 } <- positives ,
1531- args1 != args2 ,
1532- reduce: true do
1533- acc ->
1534- # 1. check there are no empty args
1535- dom1 = args_to_domain ( args1 )
1536- dom2 = args_to_domain ( args2 )
1537- if empty? ( dom1 ) or empty? ( dom2 ) do
1538- IO . puts ( "We found that #{ to_quoted_string ( dom1 ) } or #{ to_quoted_string ( dom2 ) } is empty" )
1539- false
1540- else
1541- d = disjoint? ( dom1 , dom2 )
1542- if not d do
1543- IO . puts ( "We found that #{ to_quoted_string ( dom1 ) } and #{ to_quoted_string ( dom2 ) } are not disjoint" )
1544- end
1545- acc and d
1546- end
1547- end
1548- end
1482+ # def descr_size(:term), do: 1
1483+
1484+ # def descr_size(%{} = descr) do
1485+ # Enum.reduce(descr, 0, fn {key, value}, acc ->
1486+ # acc + descr_size(key, value)
1487+ # end)
1488+ # end
1489+
1490+ # def descr_size(:tuple, dnf) do
1491+ # Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
1492+ # end
1493+
1494+ # def descr_size(:fun, bdd), do: bdd_size(bdd)
1495+
1496+ # def descr_size(:map, dnf) do
1497+ # Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
1498+ # acc + 1 + length(negs)
1499+ # end)
1500+ # end
1501+
1502+ # def descr_size(:list, dnf) do
1503+ # Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
1504+ # acc + 1 + length(negs)
1505+ # end)
1506+ # end
1507+
1508+ # def descr_size(_, _), do: 1
1509+
1510+ # defp bdd_size({fun, l, r}) do
1511+ # bdd_size(l) + bdd_size(r) + 1
1512+ # end
1513+
1514+ # defp bdd_size(:fun_top), do: 1
1515+ # defp bdd_size(:fun_bottom), do: 0
1516+
1517+ # defp list_dnf_size(dnf) do
1518+ # Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
1519+ # 1 + length(negs)
1520+ # end)
1521+ # end
1522+
1523+ # defp all_distinct_non_empty_domains?([{args, _ret}]) do
1524+ # not empty?(args_to_domain(args))
1525+ # end
1526+
1527+ # defp all_distinct_non_empty_domains?(positives) do
1528+ # # For each two elements of positives, their domains are distinct
1529+ # for {args1, _ret1} <- positives,
1530+ # {args2, _ret2} <- positives,
1531+ # args1 != args2,
1532+ # reduce: true do
1533+ # acc ->
1534+ # # 1. check there are no empty args
1535+ # dom1 = args_to_domain(args1)
1536+ # dom2 = args_to_domain(args2)
1537+ # if empty?(dom1) or empty?(dom2) do
1538+ # false
1539+ # else
1540+ # d = disjoint?(dom1, dom2)
1541+ # if not d do
1542+ # end
1543+ # acc and d
1544+ # end
1545+ # end
1546+ # end
15491547
15501548 defp all_non_empty_domains? ( positives ) do
15511549 Enum . all? ( positives , fn { args , _ret } -> not empty? ( args_to_domain ( args ) ) end )
@@ -1556,42 +1554,18 @@ defmodule Module.Types.Descr do
15561554 # In that case, checking subtyping of it with a single arrow is simply:
15571555 # checking that the union of the domains of the positives is a supertype of the domain of the arrow
15581556 # 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
1559- IO . puts ( "Checking if all the positives have distinct non empty domains..." )
15601557 if all_non_empty_domains? ( positives ) and all_non_empty_domains? ( [ { arguments , return } ] ) do
15611558 return = negation ( return )
1562- IO . puts ( "They DO" )
1563- IO . puts ( "All distinct non empty domains" )
1564- IO . puts ( "The positives are:" )
1565- Enum . each ( positives , fn { args , ret } ->
1566- IO . puts ( "#{ Enum . map ( args , fn arg -> to_quoted_string ( arg ) end ) |> Enum . join ( ", " ) } -> #{ to_quoted_string ( ret ) } " )
1567- end )
1568- IO . puts ( "--------------------------------" )
1569- IO . puts ( "--------------------------------" )
1570- IO . puts ( "Checking if the single arrow" )
1571- IO . puts ( "#{ Enum . map ( arguments , fn arg -> to_quoted_string ( arg ) end ) |> Enum . join ( ", " ) } -> #{ to_quoted_string ( return ) } " )
1572- IO . puts ( "is a supertype of the intersection of these #{ length ( positives ) } positives" )
1573-
15741559 type_positives =
15751560 Enum . map ( positives , fn { args , ret } -> fun ( args , ret ) end ) |> Enum . reduce ( & intersection / 2 )
15761561
15771562 { :ok , _dom , static_arrows } = fun_normalize ( type_positives , length ( arguments ) , :static )
15781563 result = fun_apply_static ( arguments , static_arrows , false )
15791564
1580- IO . puts ( "We are done!" )
1581- IO . puts ( "After applying the intersection of positives" )
1582- IO . puts ( "to the arguments" )
1583- IO . puts ( "(#{ Enum . map ( arguments , fn arg -> to_quoted_string ( arg ) end ) |> Enum . join ( ", " ) } )" )
1584- IO . puts ( "We get result:" )
1585- IO . puts ( "#{ to_quoted_string ( result ) } " )
1586- IO . puts ( "And we are checking if it is a subtype of:" )
1587- IO . puts ( "#{ to_quoted_string ( return ) } " )
1588-
15891565 r = subtype? ( result , return )
15901566 if r do
1591- IO . puts ( "Thus, the single arrow IS a supertype." )
15921567 r
15931568 else
1594- IO . puts ( "Thus, the single arrow IS NOT a supertype." )
15951569 false
15961570 end
15971571
@@ -1614,47 +1588,21 @@ defmodule Module.Types.Descr do
16141588 # end
16151589 else
16161590 # Show the caller of this function
1617- IO . puts ( "They DO NOT" )
1618- IO . puts ( "phi_starter" )
16191591 # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
16201592 # IO.puts("Starting phi starter with return: #{inspect(return)}")
16211593 # IO.puts("Starting phi starter with positives: #{inspect(positives)}")
16221594 # Total size of the descrs in arguments, return, and positives
1623- total_size =
1624- arguments
1625- |> Enum . map ( & descr_size / 1 )
1626- |> Enum . sum ( )
1627- |> Kernel . + ( descr_size ( return ) )
1628- |> Kernel . + (
1629- Enum . reduce ( positives , 0 , fn { args , ret } , acc ->
1630- acc + Enum . sum ( Enum . map ( args , & descr_size / 1 ) ) + descr_size ( ret )
1631- end )
1632- )
1633-
1634- IO . puts ( "Total size: #{ total_size } " )
1635- IO . puts ( "Size decomposition:" )
1636- IO . puts ( "How many arguments: #{ length ( arguments ) } " )
1637- IO . puts ( "arguments: #{ Enum . map ( arguments , & descr_size / 1 ) |> Enum . sum ( ) } " )
1638- IO . puts ( "return: #{ descr_size ( return ) } " )
1639- IO . puts ( "We are checking if this function:" )
1640-
1641- IO . puts (
1642- "#{ Enum . map ( arguments , fn arg -> to_quoted_string ( arg ) end ) |> Enum . join ( ", " ) } -> #{ to_quoted_string ( return ) } "
1643- )
1595+ # total_size =
1596+ # arguments
1597+ # |> Enum.map(&descr_size/1)
1598+ # |> Enum.sum()
1599+ # |> Kernel.+(descr_size(return))
1600+ # |> Kernel.+(
1601+ # Enum.reduce(positives, 0, fn {args, ret}, acc ->
1602+ # acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
1603+ # end)
1604+ # )
16441605
1645- IO . puts (
1646- "positives: #{ Enum . reduce ( positives , 0 , fn { args , ret } , acc -> acc + Enum . sum ( Enum . map ( args , & descr_size / 1 ) ) + descr_size ( ret ) end ) } "
1647- )
1648-
1649- # How many negatives there are
1650- IO . puts ( "Is a supertype of the intersection of these #{ length ( positives ) } positives:" )
1651- IO . puts ( "here are each of them:" )
1652-
1653- Enum . each ( positives , fn { args , ret } ->
1654- IO . puts (
1655- "#{ Enum . map ( args , fn arg -> to_quoted_string ( arg ) end ) |> Enum . join ( ", " ) } -> #{ to_quoted_string ( ret ) } \n "
1656- )
1657- end )
16581606
16591607 # start_time = DateTime.utc_now()
16601608
@@ -1680,9 +1628,6 @@ defmodule Module.Types.Descr do
16801628 { result , call_count } = phi ( arguments , { false , return } , positives , 0 )
16811629 cache_size = map_size ( Process . get ( :phi_cache , % { } ) )
16821630 # Recursive calls
1683- IO . puts ( "phi recursive calls: #{ call_count } " )
1684- # IO.puts("it took #{DateTime.diff(DateTime.utc_now(), start_time, :millisecond)}ms")
1685- IO . puts ( "--------------------------------" )
16861631
16871632 result
16881633 end
0 commit comments