-- | Provides facilities for pretty-printing 'Nabla's in a way appropriate for
-- user facing pattern match warnings.
module GHC.HsToCore.Pmc.Ppr (
      pprUncovered
    ) where

import GHC.Prelude

import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf
import GHC.Types.Basic
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DFM
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Builtin.Types
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import Control.Monad.Trans.RWS.CPS
import GHC.Data.Maybe
import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)

import GHC.HsToCore.Pmc.Types

-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
-- components and refutable shapes associated to any mentioned variables.
--
-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]])@:
--
-- @
-- (Just p) q
--     where p is not one of {3, 4}
--           q is not one of {0, 5}
-- @
--
-- When the set of refutable shapes contains more than 3 elements, the
-- additional elements are indicated by "...".
pprUncovered :: Nabla -> [Id] -> SDoc
pprUncovered :: Nabla -> [Id] -> SDoc
pprUncovered Nabla
nabla [Id]
vas
  | forall key elt. UniqDFM key elt -> Bool
isNullUDFM DIdEnv (SDoc, [PmAltCon])
refuts = forall doc. IsLine doc => [doc] -> doc
fsep [SDoc]
vec -- there are no refutations
  | Bool
otherwise         = SDoc -> Int -> SDoc -> SDoc
hang (forall doc. IsLine doc => [doc] -> doc
fsep [SDoc]
vec) Int
4 forall a b. (a -> b) -> a -> b
$
                          forall doc. IsLine doc => String -> doc
text String
"where" forall doc. IsLine doc => doc -> doc -> doc
<+> forall doc. IsDoc doc => [doc] -> doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map ((SDoc, [PmAltCon]) -> SDoc
pprRefutableShapes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall key elt. UniqDFM key elt -> [(Unique, elt)]
udfmToList DIdEnv (SDoc, [PmAltCon])
refuts))
  where
    init_prec :: PprPrec
init_prec
      -- No outer parentheses when it's a unary pattern by assuming lowest
      -- precedence
      | [Id
_] <- [Id]
vas   = PprPrec
topPrec
      | Bool
otherwise    = PprPrec
appPrec
    ppr_action :: RWST Nabla () (DIdEnv (Id, SDoc), Infinite SDoc) Identity [SDoc]
ppr_action       = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
init_prec) [Id]
vas
    ([SDoc]
vec, DIdEnv (Id, SDoc)
renamings) = forall a. Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
runPmPpr Nabla
nabla RWST Nabla () (DIdEnv (Id, SDoc), Infinite SDoc) Identity [SDoc]
ppr_action
    refuts :: DIdEnv (SDoc, [PmAltCon])
refuts           = Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
prettifyRefuts Nabla
nabla DIdEnv (Id, SDoc)
renamings

-- | Output refutable shapes of a variable in the form of @var is not one of {2,
-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
-- indicated by an ellipsis.
pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
pprRefutableShapes :: (SDoc, [PmAltCon]) -> SDoc
pprRefutableShapes (SDoc
var, [PmAltCon]
alts)
  = SDoc
var forall doc. IsLine doc => doc -> doc -> doc
<+> forall doc. IsLine doc => String -> doc
text String
"is not one of" forall doc. IsLine doc => doc -> doc -> doc
<+> [PmAltCon] -> SDoc
format_alts [PmAltCon]
alts
  where
    format_alts :: [PmAltCon] -> SDoc
format_alts = forall doc. IsLine doc => doc -> doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => [doc] -> doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate forall doc. IsLine doc => doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. IsLine a => [a] -> [a]
shorten forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map PmAltCon -> SDoc
ppr_alt
    shorten :: [a] -> [a]
shorten (a
a:a
b:a
c:a
_:[a]
_)       = a
aforall a. a -> [a] -> [a]
:a
bforall a. a -> [a] -> [a]
:a
cforall a. a -> [a] -> [a]
:[forall doc. IsLine doc => String -> doc
text String
"..."]
    shorten [a]
xs                = [a]
xs
    ppr_alt :: PmAltCon -> SDoc
ppr_alt (PmAltConLike ConLike
cl) = forall a. Outputable a => a -> SDoc
ppr ConLike
cl
    ppr_alt (PmAltLit PmLit
lit)    = forall a. Outputable a => a -> SDoc
ppr PmLit
lit

{- 1. Literals
~~~~~~~~~~~~~~
Starting with a function definition like:

    f :: Int -> Bool
    f 5 = True
    f 6 = True

The uncovered set looks like:
    { var |> var /= 5, var /= 6 }

Yet, we would like to print this nicely as follows:
   x , where x not one of {5,6}

Since these variables will be shown to the programmer, we give them better names
(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'.

2. Residual Constraints
~~~~~~~~~~~~~~~~~~~~~~~
Unhandled constraints that refer to HsExpr are typically ignored by the solver
(it does not even substitute in HsExpr so they are even printed as wildcards).
Additionally, the oracle returns a substitution if it succeeds so we apply this
substitution to the vectors before printing them out (see function `pprOne' in
"GHC.HsToCore.Pmc") to be more precise.
-}

-- | Extract and assigns pretty names to constraint variables with refutable
-- shapes.
prettifyRefuts :: Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
prettifyRefuts :: Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
prettifyRefuts Nabla
nabla = forall elt key. [(Unique, elt)] -> UniqDFM key elt
listToUDFM_Directly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Unique, (Id, SDoc)) -> (Unique, (SDoc, [PmAltCon]))
attach_refuts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall key elt. UniqDFM key elt -> [(Unique, elt)]
udfmToList
  where
    attach_refuts :: (Unique, (Id, SDoc)) -> (Unique, (SDoc, [PmAltCon]))
attach_refuts (Unique
u, (Id
x, SDoc
sdoc)) = (Unique
u, (SDoc
sdoc, Nabla -> Id -> [PmAltCon]
lookupRefuts Nabla
nabla Id
x))


type PmPprM a = RWS Nabla () (DIdEnv (Id, SDoc), Infinite SDoc) a

-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: Infinite SDoc
nameList :: Infinite SDoc
nameList = forall a b. (a -> b) -> [a] -> [b]
map forall doc. IsLine doc => String -> doc
text [String
"p",String
"q",String
"r",String
"s",String
"t"] forall (f :: * -> *) a.
Foldable f =>
f a -> Infinite a -> Infinite a
Inf.++ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b a. (b -> (a, b)) -> b -> Infinite a
Inf.unfoldr (Int
0 :: Int) (\ Int
u -> (forall doc. IsLine doc => String -> doc
text (Char
't'forall a. a -> [a] -> [a]
:forall a. Show a => a -> String
show Int
u), Int
uforall a. Num a => a -> a -> a
+Int
1))

runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
runPmPpr :: forall a. Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
runPmPpr Nabla
nabla PmPprM a
m = case forall w r s a. Monoid w => RWS r w s a -> r -> s -> (a, s, w)
runRWS PmPprM a
m Nabla
nabla (forall a. DVarEnv a
emptyDVarEnv, Infinite SDoc
nameList) of
  (a
a, (DIdEnv (Id, SDoc)
renamings, Infinite SDoc
_), ()
_) -> (a
a, DIdEnv (Id, SDoc)
renamings)

-- | Allocates a new, clean name for the given 'Id' if it doesn't already have
-- one.
getCleanName :: Id -> PmPprM SDoc
getCleanName :: Id -> PmPprM SDoc
getCleanName Id
x = do
  (DIdEnv (Id, SDoc)
renamings, Infinite SDoc
name_supply) <- forall (m :: * -> *) r w s. Monad m => RWST r w s m s
get
  let Inf SDoc
clean_name Infinite SDoc
name_supply' = Infinite SDoc
name_supply
  case forall a. DVarEnv a -> Id -> Maybe a
lookupDVarEnv DIdEnv (Id, SDoc)
renamings Id
x of
    Just (Id
_, SDoc
nm) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SDoc
nm
    Maybe (Id, SDoc)
Nothing -> do
      forall (m :: * -> *) s r w. Monad m => s -> RWST r w s m ()
put (forall a. DVarEnv a -> Id -> a -> DVarEnv a
extendDVarEnv DIdEnv (Id, SDoc)
renamings Id
x (Id
x, SDoc
clean_name), Infinite SDoc
name_supply')
      forall (f :: * -> *) a. Applicative f => a -> f a
pure SDoc
clean_name

checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached
checkRefuts :: Id -> PmPprM (Maybe SDoc)
checkRefuts Id
x = do
  Nabla
nabla <- forall (m :: * -> *) r w s. Monad m => RWST r w s m r
ask
  case Nabla -> Id -> [PmAltCon]
lookupRefuts Nabla
nabla Id
x of
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing -- Will just be a wildcard later on
    [PmAltCon]
_  -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> PmPprM SDoc
getCleanName Id
x

-- | Pretty print a variable, but remember to prettify the names of the variables
-- that refer to neg-literals. The ones that cannot be shown are printed as
-- underscores.
pprPmVar :: PprPrec -> Id -> PmPprM SDoc
pprPmVar :: PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
prec Id
x = do
  Nabla
nabla <- forall (m :: * -> *) r w s. Monad m => RWST r w s m r
ask
  case Nabla -> Id -> Maybe PmAltConApp
lookupSolution Nabla
nabla Id
x of
    Just (PACA PmAltCon
alt [Id]
_tvs [Id]
args) -> PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc
pprPmAltCon PprPrec
prec PmAltCon
alt [Id]
args
    Maybe PmAltConApp
Nothing                   -> forall a. a -> Maybe a -> a
fromMaybe forall doc. IsLine doc => doc
underscore forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> PmPprM (Maybe SDoc)
checkRefuts Id
x

pprPmAltCon :: PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc
pprPmAltCon :: PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc
pprPmAltCon PprPrec
_prec (PmAltLit PmLit
l)      [Id]
_    = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Outputable a => a -> SDoc
ppr PmLit
l)
pprPmAltCon PprPrec
prec  (PmAltConLike ConLike
cl) [Id]
args = do
  Nabla
nabla <- forall (m :: * -> *) r w s. Monad m => RWST r w s m r
ask
  Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc
pprConLike Nabla
nabla PprPrec
prec ConLike
cl [Id]
args

pprConLike :: Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc
pprConLike :: Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc
pprConLike Nabla
nabla PprPrec
_prec ConLike
cl [Id]
args
  | Just PmExprList
pm_expr_list <- Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList Nabla
nabla (ConLike -> PmAltCon
PmAltConLike ConLike
cl) [Id]
args
  = case PmExprList
pm_expr_list of
      NilTerminated [Id]
list ->
        forall doc. IsLine doc => doc -> doc
brackets forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => [doc] -> doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate forall doc. IsLine doc => doc
comma forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
appPrec) [Id]
list
      WcVarTerminated NonEmpty Id
pref Id
x ->
        forall doc. IsLine doc => doc -> doc
parens   forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate forall doc. IsLine doc => doc
colon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
appPrec) (forall a. NonEmpty a -> [a]
toList NonEmpty Id
pref forall a. [a] -> [a] -> [a]
++ [Id
x])
pprConLike Nabla
_nabla PprPrec
_prec (RealDataCon DataCon
con) [Id]
args
  | DataCon -> Bool
isUnboxedTupleDataCon DataCon
con
  , let hash_parens :: doc -> doc
hash_parens doc
doc = forall doc. IsLine doc => String -> doc
text String
"(#" forall doc. IsLine doc => doc -> doc -> doc
<+> doc
doc forall doc. IsLine doc => doc -> doc -> doc
<+> forall doc. IsLine doc => String -> doc
text String
"#)"
  = forall doc. IsLine doc => doc -> doc
hash_parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => [doc] -> doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate forall doc. IsLine doc => doc
comma forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
appPrec) [Id]
args
  | DataCon -> Bool
isTupleDataCon DataCon
con
  = forall doc. IsLine doc => doc -> doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => [doc] -> doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate forall doc. IsLine doc => doc
comma forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
appPrec) [Id]
args
pprConLike Nabla
_nabla PprPrec
prec ConLike
cl [Id]
args
  | ConLike -> Bool
conLikeIsInfix ConLike
cl = case [Id]
args of
      [Id
x, Id
y] -> do SDoc
x' <- PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
funPrec Id
x
                   SDoc
y' <- PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
funPrec Id
y
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> SDoc -> SDoc
cparen (PprPrec
prec forall a. Ord a => a -> a -> Bool
> PprPrec
opPrec) (SDoc
x' forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr ConLike
cl forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
y'))
      -- can it be infix but have more than two arguments?
      [Id]
list   -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"pprConLike:" (forall a. Outputable a => a -> SDoc
ppr [Id]
list)
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
args = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Outputable a => a -> SDoc
ppr ConLike
cl)
  | Bool
otherwise = do [SDoc]
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PprPrec -> Id -> PmPprM SDoc
pprPmVar PprPrec
appPrec) [Id]
args
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> SDoc -> SDoc
cparen (PprPrec
prec forall a. Ord a => a -> a -> Bool
> PprPrec
funPrec) (forall doc. IsLine doc => [doc] -> doc
fsep (forall a. Outputable a => a -> SDoc
ppr ConLike
cl forall a. a -> [a] -> [a]
: [SDoc]
args')))

-- | The result of 'pmExprAsList'.
data PmExprList
  = NilTerminated [Id]
  | WcVarTerminated (NonEmpty Id) Id

-- | Extract a list of 'Id's out of a sequence of cons cells, optionally
-- terminated by a wildcard variable instead of @[]@. Some examples:
--
-- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular,
--   @[]@-terminated list. Should be pretty-printed as @[1,2]@.
-- * @pmExprAsList (1:2:x) == Just ('WcVarTerminated' [1,2] x)@, a list prefix
--   ending in a wildcard variable x (of list type). Should be pretty-printed as
--   (1:2:_).
-- * @pmExprAsList [] == Just ('NilTerminated' [])@
pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList Nabla
nabla = [Id] -> PmAltCon -> [Id] -> Maybe PmExprList
go_con []
  where
    go_var :: [Id] -> Id -> Maybe PmExprList
go_var [Id]
rev_pref Id
x
      | Just (PACA PmAltCon
alt [Id]
_tvs [Id]
args) <- Nabla -> Id -> Maybe PmAltConApp
lookupSolution Nabla
nabla Id
x
      = [Id] -> PmAltCon -> [Id] -> Maybe PmExprList
go_con [Id]
rev_pref PmAltCon
alt [Id]
args
    go_var [Id]
rev_pref Id
x
      | Just NonEmpty Id
pref <- forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (forall a. [a] -> [a]
reverse [Id]
rev_pref)
      = forall a. a -> Maybe a
Just (NonEmpty Id -> Id -> PmExprList
WcVarTerminated NonEmpty Id
pref Id
x)
    go_var [Id]
_ Id
_
      = forall a. Maybe a
Nothing

    go_con :: [Id] -> PmAltCon -> [Id] -> Maybe PmExprList
go_con [Id]
rev_pref (PmAltConLike (RealDataCon DataCon
c)) [Id]
es
      | DataCon
c forall a. Eq a => a -> a -> Bool
== DataCon
nilDataCon
      = forall a. HasCallStack => Bool -> a -> a
assert (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
es) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([Id] -> PmExprList
NilTerminated (forall a. [a] -> [a]
reverse [Id]
rev_pref))
      | DataCon
c forall a. Eq a => a -> a -> Bool
== DataCon
consDataCon
      = forall a. HasCallStack => Bool -> a -> a
assert (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
es forall a. Eq a => a -> a -> Bool
== Int
2) forall a b. (a -> b) -> a -> b
$ [Id] -> Id -> Maybe PmExprList
go_var ([Id]
es forall a. [a] -> Int -> a
!! Int
0 forall a. a -> [a] -> [a]
: [Id]
rev_pref) ([Id]
es forall a. [a] -> Int -> a
!! Int
1)
    go_con [Id]
_ PmAltCon
_ [Id]
_
      = forall a. Maybe a
Nothing