-{- Never used -- omitting
--- | True of expressions that are guaranteed to diverge upon execution
-exprIsBottom :: CoreExpr -> Bool -- True => definitely bottom
-exprIsBottom e = go 0 e
- where
- -- n is the number of args
- go n (Note _ e) = go n e
- go n (Cast e _) = go n e
- go n (Let _ e) = go n e
- go _ (Case e _ _ _) = go 0 e -- Just check the scrut
- go n (App e _) = go (n+1) e
- go n (Var v) = idAppIsBottom v n
- go _ (Lit _) = False
- go _ (Lam _ _) = False
- go _ (Type _) = False
-
-idAppIsBottom :: Id -> Int -> Bool
-idAppIsBottom id n_val_args = appIsBottom (idNewStrictness id) n_val_args
--}
+-- Note [exprIsHNF]
+-- ~~~~~~~~~~~~~~~~
+-- | exprIsHNF returns true for expressions that are certainly /already/
+-- evaluated to /head/ normal form. This is used to decide whether it's ok
+-- to change:
+--
+-- > case x of _ -> e
+--
+-- into:
+--
+-- > e
+--
+-- and to decide whether it's safe to discard a 'seq'.
+--
+-- So, it does /not/ treat variables as evaluated, unless they say they are.
+-- However, it /does/ treat partial applications and constructor applications
+-- as values, even if their arguments are non-trivial, provided the argument
+-- type is lifted. For example, both of these are values:
+--
+-- > (:) (f x) (map f xs)
+-- > map (...redex...)
+--
+-- because 'seq' on such things completes immediately.
+--
+-- For unlifted argument types, we have to be careful:
+--
+-- > C (f x :: Int#)
+--
+-- Suppose @f x@ diverges; then @C (f x)@ is not a value. However this can't
+-- happen: see "CoreSyn#let_app_invariant". This invariant states that arguments of
+-- unboxed type must be ok-for-speculation (or trivial).
+exprIsHNF :: CoreExpr -> Bool -- True => Value-lambda, constructor, PAP
+exprIsHNF = exprIsHNFlike isDataConWorkId isEvaldUnfolding