Try to make "<S>t" meaningful
by giving it the meaning: "Assuming my first argument is terminating, then I am terminating". In pictures: This is the lattice, which is not a simple product lattice any more: ------ <L><L>------ / | \ \ / | <L><L>t \ <S><L> | <S><L> | \ \ | | | \ | \ <S><L>t | / | <S><L>t | \ | / | \ \ | / | \ ----- <S><S>----- | \ | \ | \ | <S><S>t / \ | / ---------⊥-------------/ This means that we need to be careful when lub’ing: If one branch is lazy, but not absent in an argument or free variable, and the other branch is strict, then even if both branches claim to terminate, we need to remove the termination flag (as one had the termination under a stronger hypothesis as the hole result) (Feels inelegant.) There is no unit for lubDmdType any more. So for case, use we use botDmdType for no alternatives, and foldr1 if there are multiple. Unlifted variables (e.g. Int#) are tricky. Everything is strict in them, so for an *unlifted* argument, <L>t implies <S>t and hence <S>t ⊔ <L>t = <S>t, and we really want to make use of that stronger equation. But when lub’ing, we don’t know any more if this is the demand for an unlifted type. So instead, the demand type of x :: Int# itself is {x ↦ <L>} t, while x :: Int continues to have type {x ↦ <S>} t. It is important that functions (including primitive operations and constructors like I#) have a strict demand on their unlifted argument. But it turned out to be easier to enforce this in the demand analyser: So even if f claims to have a lazy demand on a argument of unlifted type, we make this demand strict before feeding it into the argument.
Showing
- compiler/basicTypes/Demand.lhs 50 additions, 13 deletionscompiler/basicTypes/Demand.lhs
- compiler/prelude/PrimOp.lhs 3 additions, 1 deletioncompiler/prelude/PrimOp.lhs
- compiler/prelude/primops.txt.pp 1 addition, 0 deletionscompiler/prelude/primops.txt.pp
- compiler/stranal/DmdAnal.lhs 28 additions, 10 deletionscompiler/stranal/DmdAnal.lhs
Loading
Please register or sign in to comment