Skip to content

Refactor Demand lattice so that it has less semantic equalities

Since !4371 (closed), Demand is defined pretty simply as data Demand = Card :* SubDemand. But for absent demands (e.g. when Card is C_00 or C_10), the SubDemand doesn't actually make sense because it describes how the thing is evaluated nestedly, if it is evaluated at all. If the premise is never satisfied, as for absent demands, that information is never useful. We should make use sites aware of that fact, so they pick whatever SubDemand they want for absent demands.

More concretely, this ticket is about assessing whether we can bring back some of the demand structure we had before !4371 (closed) and refactor to:

data Card = C_01 | C_0N | C_11 | C_1N -- NB: C_00 and C_10 are gone!
data Demand = Absent | Bottom | Card :* SubDemand
data SubDemand = Poly Card | Prod [Demand] | Call Demand

Note that Call now takes a Demand instead of a Card and a SubDemand separately. The interpretation of that demand is a little different than those demands inside a product, particularly around plusSubDmd, because call demands are relative, whereas product demands are ... at least in part absolute (cf. #18885 (closed)). Nevertheless, the analogy is fitting: The demand 1C(A) then says "evaluated once and called with one argument, but not called further". Edit: No, really it is not: 1C(A) means "evaluated once but never called", because the Card of the Demand expresses how often the thing is called. Better use Poly C_00 here. UC(1C(1U) means "evaluted multiple times, but called exactly one with two arguments" and so on.

Let's see whether that works.

Edited by Sebastian Graf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information