[commit: ghc] wip/nested-cpr: Note [Termination information and arguments] (b47bd78)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/nested-cpr
Link       : http://ghc.haskell.org/trac/ghc/changeset/b47bd786fd5c7d6b5d885e612619447fcdef2412/ghc

>---------------------------------------------------------------

commit b47bd786fd5c7d6b5d885e612619447fcdef2412
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Wed Jan 15 16:53:31 2014 +0000

    Note [Termination information and arguments]


>---------------------------------------------------------------

b47bd786fd5c7d6b5d885e612619447fcdef2412
 compiler/basicTypes/Demand.lhs  |   30 +++++++++++++++++++++++++++++-
 compiler/prelude/primops.txt.pp |    1 +
 compiler/stranal/DmdAnal.lhs    |    1 +
 3 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/compiler/basicTypes/Demand.lhs b/compiler/basicTypes/Demand.lhs
index 7c38b48..b2e8f6c 100644
--- a/compiler/basicTypes/Demand.lhs
+++ b/compiler/basicTypes/Demand.lhs
@@ -1151,7 +1151,7 @@ postProcessDmdTypeM (Just du) (DmdType fv _ res_ty)
 
 postProcessDmdResult :: DeferAndUse -> DmdResult -> Termination ()
     -- if we use it lazily, there cannot be divergence worrying us
-    -- (Otherwise we'd lose the termination information of constructors in in dmdAnalVarApp, for example)
+    -- See Note [Termination information and arguments]
 postProcessDmdResult (True,_)  _              = Converges ()
 postProcessDmdResult (False,_) (Dunno {})     = Dunno ()
 postProcessDmdResult (False,_) (Converges {}) = Converges ()
@@ -1362,6 +1362,34 @@ and A on the second.
 If this same function is applied to one arg, all we can say is that it
 uses x with <L,U>, and its arg with demand <L,U>.
 
+
+Note [Termination information and arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A strictness signature of <L>t indicates:
+    If you apply me to one argument, I will surely terminate (even if this
+    argument may diverge).
+Therefore, in postProcessDmdResult, we replace the termination info of a lazy
+argument by Converges.
+
+For strict arguments, we do not do that. But usually, <S>t is not possible anyways:
+Assume such a function is applied to undefined. This diverges, because it is strict,
+and it converges, because of the terminating flag.
+
+One exception to this rule are unlifted arguments. These cannot be undefined, so the
+function is (vacuously) strict in them. But moreover, it is important that we treat
+them as strict! Consider I# (or any function with an unlifted argument type). We
+clearly want "I# 1#" to be terminating, and also "I# x" and "I# (x +# 2#)".
+But not "I# (x `quotInt#` 0#)"! Therefore, we need to analyze the argument with a strict
+demand, so that postProcessDmdResult will not hide the termination result of the argument,
+and bothDmdType takes case of erasing the Converges coming from I#.
+
+This is a property not just of primitive operations. Consider
+  f :: Bool -> (Int# -> b) -> b
+  f b g = g (if b then 1# else 0#)
+Is this strict in `b`? Yes, it is! So we want to consider any function with an
+unlifted argument type as strict. Hence we do that conveniently in dmdTransformThunkDmd.
+And therefore we do not have to worry about the strictness on arguments in primops.txt.pp
+
 \begin{code}
 newtype StrictSig = StrictSig DmdType
                   deriving( Eq )
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index f020ae8..b1278af 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -62,6 +62,7 @@ defaults
    commutable       = False
    code_size        = { primOpCodeSizeDefault }
    -- Strictness is turned to terminating in PrimOp.primOpSig, if allowed
+   -- Also see [Termination information and arguments]
    strictness       = { \ arity -> mkClosedStrictSig (replicate arity topDmd) topRes }
    fixity           = Nothing
    llvm_only        = False
diff --git a/compiler/stranal/DmdAnal.lhs b/compiler/stranal/DmdAnal.lhs
index 12215d1..da2a7c3 100644
--- a/compiler/stranal/DmdAnal.lhs
+++ b/compiler/stranal/DmdAnal.lhs
@@ -108,6 +108,7 @@ c) The application rule wouldn't be right either
 --   at most once, so oneify it.
 -- * If e is of an unlifted type, e will be evaluated before the actual call, so
 --   in that sense, the demand on e is strict.
+--   See [Termination information and arguments]
 dmdTransformThunkDmd :: CoreExpr -> Demand -> Demand
 dmdTransformThunkDmd e
   = when (not (exprIsTrivial e))       oneifyDmd .