-- | This module contains a single function that converts a RType -> Doc
--   without using *any* simplifications.

{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TupleSections        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MonoLocalBinds       #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}

module Language.Haskell.Liquid.Types.PrettyPrint
  ( -- * Printable RTypes
    OkRT

    -- * Printers
  , rtypeDoc

  -- * Printing Lists (TODO: move to fixpoint)
  , pprManyOrdered
  , pprintLongList
  , pprintSymbol

  -- * Printing diagnostics
  , printWarning
  , printError

  -- * Reporting errors in the typechecking phase
  , reportErrors

  ) where

import           Control.Monad

import qualified Data.HashMap.Strict              as M
import qualified Data.List                        as L                               -- (sort)
import           Data.String
import qualified TcRnMonad                        as Ghc
import qualified CoreSyn as GHC
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Types          as F
import           Language.Haskell.Liquid.GHC.API  as Ghc hiding (maybeParen, LM)
import           Language.Haskell.Liquid.GHC.Logging (putErrMsg, mkLongErrAt)
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Types.Types
import           Prelude                          hiding (error)
import           Text.PrettyPrint.HughesPJ        hiding ((<>))

--------------------------------------------------------------------------------
pprManyOrdered :: (PPrint a, Ord a) => F.Tidy -> String -> [a] -> [Doc]
--------------------------------------------------------------------------------
pprManyOrdered :: Tidy -> String -> [a] -> [Doc]
pprManyOrdered Tidy
k String
msg = (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Doc
text String
msg Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k) ([a] -> [Doc]) -> ([a] -> [a]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort

--------------------------------------------------------------------------------
pprintLongList :: PPrint a => F.Tidy -> [a] -> Doc
--------------------------------------------------------------------------------
pprintLongList :: Tidy -> [a] -> Doc
pprintLongList Tidy
k = Doc -> Doc
brackets (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k)


--------------------------------------------------------------------------------
pprintSymbol :: F.Symbol -> Doc
--------------------------------------------------------------------------------
pprintSymbol :: Symbol -> Doc
pprintSymbol Symbol
x = Char -> Doc
char Char
'‘' Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<-> Char -> Doc
char Char
'’'


--------------------------------------------------------------------------------
-- | A whole bunch of PPrint instances follow ----------------------------------
--------------------------------------------------------------------------------
instance PPrint ErrMsg where
  pprintTidy :: Tidy -> ErrMsg -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (ErrMsg -> String) -> ErrMsg -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrMsg -> String
forall a. Show a => a -> String
show

instance PPrint SourceError where
  pprintTidy :: Tidy -> SourceError -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (SourceError -> String) -> SourceError -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceError -> String
forall a. Show a => a -> String
show

instance PPrint Var where
  pprintTidy :: Tidy -> Var -> Doc
pprintTidy Tidy
_ = Var -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance PPrint (GHC.Expr Var) where
  pprintTidy :: Tidy -> Expr Var -> Doc
pprintTidy Tidy
_ = Expr Var -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance PPrint (GHC.Bind Var) where
  pprintTidy :: Tidy -> Bind Var -> Doc
pprintTidy Tidy
_ = Bind Var -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance PPrint Name where
  pprintTidy :: Tidy -> Name -> Doc
pprintTidy Tidy
_ = Name -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance PPrint TyCon where
  pprintTidy :: Tidy -> TyCon -> Doc
pprintTidy Tidy
F.Lossy = Doc -> Doc
shortModules (Doc -> Doc) -> (TyCon -> Doc) -> TyCon -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Doc
forall a. Outputable a => a -> Doc
pprDoc
  pprintTidy Tidy
F.Full  =                TyCon -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance PPrint Type where
  pprintTidy :: Tidy -> Type -> Doc
pprintTidy Tidy
_ = Type -> Doc
forall a. Outputable a => a -> Doc
pprDoc -- . tidyType emptyTidyEnv -- WHY WOULD YOU DO THIS???

instance PPrint Class where
  pprintTidy :: Tidy -> Class -> Doc
pprintTidy Tidy
F.Lossy = Doc -> Doc
shortModules (Doc -> Doc) -> (Class -> Doc) -> Class -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> Doc
forall a. Outputable a => a -> Doc
pprDoc
  pprintTidy Tidy
F.Full  =                Class -> Doc
forall a. Outputable a => a -> Doc
pprDoc

instance Show Predicate where
  show :: Predicate -> String
show = Predicate -> String
forall a. PPrint a => a -> String
showpp

instance (PPrint t) => PPrint (Annot t) where
  pprintTidy :: Tidy -> Annot t -> Doc
pprintTidy Tidy
k (AnnUse t
t) = String -> Doc
text String
"AnnUse" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
  pprintTidy Tidy
k (AnnDef t
t) = String -> Doc
text String
"AnnDef" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
  pprintTidy Tidy
k (AnnRDf t
t) = String -> Doc
text String
"AnnRDf" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
  pprintTidy Tidy
_ (AnnLoc SrcSpan
l) = String -> Doc
text String
"AnnLoc" Doc -> Doc -> Doc
<+> SrcSpan -> Doc
forall a. Outputable a => a -> Doc
pprDoc SrcSpan
l

instance PPrint a => PPrint (AnnInfo a) where
  pprintTidy :: Tidy -> AnnInfo a -> Doc
pprintTidy Tidy
k (AI HashMap SrcSpan [(Maybe Text, a)]
m) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> (SrcSpan, [(Maybe Text, a)]) -> Doc
forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds Tidy
k ((SrcSpan, [(Maybe Text, a)]) -> Doc)
-> [(SrcSpan, [(Maybe Text, a)])] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SrcSpan [(Maybe Text, a)] -> [(SrcSpan, [(Maybe Text, a)])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SrcSpan [(Maybe Text, a)]
m

instance PPrint a => Show (AnnInfo a) where
  show :: AnnInfo a -> String
show = AnnInfo a -> String
forall a. PPrint a => a -> String
showpp

pprAnnInfoBinds :: (PPrint a, PPrint b) => F.Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds :: Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds Tidy
k (SrcSpan
l, [(Maybe a, b)]
xvs)
  = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
pprAnnInfoBind Tidy
k ((SrcSpan, (Maybe a, b)) -> Doc)
-> ((Maybe a, b) -> (SrcSpan, (Maybe a, b))) -> (Maybe a, b) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SrcSpan
l,)) ((Maybe a, b) -> Doc) -> [(Maybe a, b)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe a, b)]
xvs

pprAnnInfoBind :: (PPrint a, PPrint b) => F.Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
pprAnnInfoBind :: Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
pprAnnInfoBind Tidy
k (RealSrcSpan RealSrcSpan
sp, (Maybe a, b)
xv)
  = Doc
xd Doc -> Doc -> Doc
$$ Int -> Doc
forall a. Outputable a => a -> Doc
pprDoc Int
l Doc -> Doc -> Doc
$$ Int -> Doc
forall a. Outputable a => a -> Doc
pprDoc Int
c Doc -> Doc -> Doc
$$ Tidy -> Int -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Int
n Doc -> Doc -> Doc
$$ Doc
vd Doc -> Doc -> Doc
$$ String -> Doc
text String
"\n\n\n"
    where
      l :: Int
l        = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
sp
      c :: Int
c        = RealSrcSpan -> Int
srcSpanStartCol RealSrcSpan
sp
      (Doc
xd, Doc
vd) = Tidy -> (Maybe a, b) -> (Doc, Doc)
forall a a1.
(PPrint a, PPrint a1) =>
Tidy -> (Maybe a, a1) -> (Doc, Doc)
pprXOT Tidy
k (Maybe a, b)
xv
      n :: Int
n        = [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([String] -> Int) -> [String] -> Int
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
vd

pprAnnInfoBind Tidy
_ (SrcSpan
_, (Maybe a, b)
_)
  = Doc
empty

pprXOT :: (PPrint a, PPrint a1) => F.Tidy -> (Maybe a, a1) -> (Doc, Doc)
pprXOT :: Tidy -> (Maybe a, a1) -> (Doc, Doc)
pprXOT Tidy
k (Maybe a
x, a1
v) = (Doc
xd, Tidy -> a1 -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a1
v)
  where
    xd :: Doc
xd          = Doc -> (a -> Doc) -> Maybe a -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"unknown" (Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k) Maybe a
x

instance PPrint LMap where
  pprintTidy :: Tidy -> LMap -> Doc
pprintTidy Tidy
_ (LMap LocSymbol
x [Symbol]
xs Expr
e) = [Doc] -> Doc
hcat [LocSymbol -> Doc
forall a. PPrint a => a -> Doc
pprint LocSymbol
x, [Symbol] -> Doc
forall a. PPrint a => a -> Doc
pprint [Symbol]
xs, String -> Doc
text String
"|->", Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e ]

instance PPrint LogicMap where
  pprintTidy :: Tidy -> LogicMap -> Doc
pprintTidy Tidy
_ (LM HashMap Symbol LMap
lm HashMap Var (Maybe Symbol)
am) = [Doc] -> Doc
vcat [ String -> Doc
text String
"Logic Map"
                                 , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"logic-map"
                                 , Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap Symbol LMap -> Doc
forall a. PPrint a => a -> Doc
pprint HashMap Symbol LMap
lm
                                 , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"axiom-map"
                                 , Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ HashMap Var (Maybe Symbol) -> Doc
forall a. PPrint a => a -> Doc
pprint HashMap Var (Maybe Symbol)
am
                                 ]
                    
--------------------------------------------------------------------------------
-- | Pretty Printing RefType ---------------------------------------------------
--------------------------------------------------------------------------------
instance (OkRT c tv r) => PPrint (RType c tv r) where
  -- RJ: THIS IS THE CRUCIAL LINE, the following prints short types.
  pprintTidy :: Tidy -> RType c tv r -> Doc
pprintTidy Tidy
_ = Tidy -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc Tidy
F.Lossy
  -- pprintTidy _ = ppRType topPrec

instance (PPrint tv, PPrint ty) => PPrint (RTAlias tv ty) where
  pprintTidy :: Tidy -> RTAlias tv ty -> Doc
pprintTidy = Tidy -> RTAlias tv ty -> Doc
forall tv ty.
(PPrint tv, PPrint ty) =>
Tidy -> RTAlias tv ty -> Doc
ppAlias

ppAlias :: (PPrint tv, PPrint ty) => F.Tidy -> RTAlias tv ty -> Doc
ppAlias :: Tidy -> RTAlias tv ty -> Doc
ppAlias Tidy
k RTAlias tv ty
a =   Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (RTAlias tv ty -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> Tidy -> Doc -> [tv] -> Doc
forall a. PPrint a => Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
space (RTAlias tv ty -> [tv]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> Tidy -> Doc -> [Symbol] -> Doc
forall a. PPrint a => Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
space (RTAlias tv ty -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> String -> Doc
text String
" = "
            Doc -> Doc -> Doc
<+> ty -> Doc
forall a. PPrint a => a -> Doc
pprint (RTAlias tv ty -> ty
forall x a. RTAlias x a -> a
rtBody RTAlias tv ty
a)

instance (F.PPrint tv, F.PPrint t) => F.PPrint (RTEnv tv t) where 
  pprintTidy :: Tidy -> RTEnv tv t -> Doc
pprintTidy Tidy
k RTEnv tv t
rte 
    =   String -> Doc
text String
"** Type Aliaes *********************" 
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Tidy -> HashMap Symbol (Located (RTAlias tv t)) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases RTEnv tv t
rte)) 
    Doc -> Doc -> Doc
$+$ String -> Doc
text String
"** Expr Aliases ********************" 
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Tidy -> HashMap Symbol (Located (RTAlias Symbol Expr)) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases RTEnv tv t
rte))

pprints :: (PPrint a) => F.Tidy -> Doc -> [a] -> Doc
pprints :: Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
c = [Doc] -> Doc
sep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
c ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k)

--------------------------------------------------------------------------------
rtypeDoc :: (OkRT c tv r) => F.Tidy -> RType c tv r -> Doc
--------------------------------------------------------------------------------
rtypeDoc :: Tidy -> RType c tv r -> Doc
rtypeDoc Tidy
k      = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype (Tidy -> PPEnv
ppE Tidy
k) Prec
topPrec
  where
    ppE :: Tidy -> PPEnv
ppE Tidy
F.Lossy = PPEnv -> PPEnv
ppEnvShort PPEnv
ppEnv
    ppE Tidy
F.Full  = PPEnv
ppEnv

instance PPrint F.Tidy where
  pprintTidy :: Tidy -> Tidy -> Doc
pprintTidy Tidy
_ Tidy
F.Full  = Doc
"Full"
  pprintTidy Tidy
_ Tidy
F.Lossy = Doc
"Lossy"

type Prec = PprPrec 

--------------------------------------------------------------------------------
ppr_rtype :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc
--------------------------------------------------------------------------------
ppr_rtype :: PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(RAllT RTVU c tv
_ RType c tv r
_ r
r)
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_forall PPEnv
bb Prec
p RType c tv r
t
ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(RAllP PVU c tv
_ RType c tv r
_)
  = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_forall PPEnv
bb Prec
p RType c tv r
t
ppr_rtype PPEnv
_ Prec
_ (RVar tv
a r
r)
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ tv -> Doc
forall a. PPrint a => a -> Doc
pprint tv
a
ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(RImpF Symbol
_ RType c tv r
_ RType c tv r
_ r
_)
  = Prec -> Prec -> Doc -> Doc
maybeParen Prec
p Prec
funPrec (PPEnv -> Doc -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Doc -> RType c tv r -> Doc
ppr_rty_fun PPEnv
bb Doc
empty RType c tv r
t)
ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(RFun Symbol
_ RType c tv r
_ RType c tv r
_ r
_)
  = Prec -> Prec -> Doc -> Doc
maybeParen Prec
p Prec
funPrec (PPEnv -> Doc -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Doc -> RType c tv r -> Doc
ppr_rty_fun PPEnv
bb Doc
empty RType c tv r
t)
ppr_rtype PPEnv
bb Prec
p (RApp c
c [RType c tv r
t] [RTProp c tv r]
rs r
r)
  | c -> Bool
forall c. TyConable c => c -> Bool
isList c
c
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t) Doc -> Doc -> Doc
<-> PPEnv -> Prec -> [RTProp c tv r] -> Doc
forall c tv r t t1.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()),
 Reftable (Ref (RType c tv ()) (RType c tv r))) =>
t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc
ppReftPs PPEnv
bb Prec
p [RTProp c tv r]
rs
ppr_rtype PPEnv
bb Prec
p (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r)
  | c -> Bool
forall c. TyConable c => c -> Bool
isTuple c
c
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> [Doc] -> Doc
intersperse Doc
comma (PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p (RType c tv r -> Doc) -> [RType c tv r] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts)) Doc -> Doc -> Doc
<-> PPEnv -> Prec -> [RTProp c tv r] -> Doc
forall c tv r t t1.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()),
 Reftable (Ref (RType c tv ()) (RType c tv r))) =>
t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc
ppReftPs PPEnv
bb Prec
p [RTProp c tv r]
rs
ppr_rtype PPEnv
bb Prec
p (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r)
  | Doc -> Bool
isEmpty Doc
rsDoc Bool -> Bool -> Bool
&& Doc -> Bool
isEmpty Doc
tsDoc
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ c -> Doc
ppT c
c
  | Bool
otherwise
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ c -> Doc
ppT c
c Doc -> Doc -> Doc
<+> Doc
rsDoc Doc -> Doc -> Doc
<+> Doc
tsDoc
  where
    rsDoc :: Doc
rsDoc            = PPEnv -> Prec -> [RTProp c tv r] -> Doc
forall c tv r t t1.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()),
 Reftable (Ref (RType c tv ()) (RType c tv r))) =>
t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc
ppReftPs PPEnv
bb Prec
p [RTProp c tv r]
rs
    tsDoc :: Doc
tsDoc            = [Doc] -> Doc
hsep (PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p (RType c tv r -> Doc) -> [RType c tv r] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts)
    ppT :: c -> Doc
ppT              = PPEnv -> c -> Doc
forall c. TyConable c => PPEnv -> c -> Doc
ppTyConB PPEnv
bb

ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(REx Symbol
_ RType c tv r
_ RType c tv r
_)
  = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint c, PPrint tv, PPrint (RType c tv r),
 PPrint (RType c tv ()), Reftable (RTProp c tv r),
 Reftable (RTProp c tv ())) =>
PPEnv -> Prec -> RType c tv r -> Doc
ppExists PPEnv
bb Prec
p RType c tv r
t
ppr_rtype PPEnv
bb Prec
p t :: RType c tv r
t@(RAllE Symbol
_ RType c tv r
_ RType c tv r
_)
  = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Prec -> RType c tv r -> Doc
ppAllExpr PPEnv
bb Prec
p RType c tv r
t
ppr_rtype PPEnv
_ Prec
_ (RExprArg Located Expr
e)
  = Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Located Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Located Expr
e
ppr_rtype PPEnv
bb Prec
p (RAppTy RType c tv r
t RType c tv r
t' r
r)
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t Doc -> Doc -> Doc
<+> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t'
ppr_rtype PPEnv
bb Prec
p (RRTy [(Symbol, RType c tv r)]
e r
_ Oblig
OCons RType c tv r
t)
  = [Doc] -> Doc
sep [Doc -> Doc
braces (PPEnv -> Prec -> [(Symbol, RType c tv r)] -> Doc
forall c tv r a.
(OkRT c tv r, PPrint a, PPrint (RType c tv r),
 PPrint (RType c tv ())) =>
PPEnv -> Prec -> [(a, RType c tv r)] -> Doc
ppr_rsubtype PPEnv
bb Prec
p [(Symbol, RType c tv r)]
e) Doc -> Doc -> Doc
<+> Doc
"=>", PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t]
ppr_rtype PPEnv
bb Prec
p (RRTy [(Symbol, RType c tv r)]
e r
r Oblig
o RType c tv r
t)
  = [Doc] -> Doc
sep [Doc -> Doc
ppp (Oblig -> Doc
forall a. PPrint a => a -> Doc
pprint Oblig
o Doc -> Doc -> Doc
<+> Doc
ppe Doc -> Doc -> Doc
<+> r -> Doc
forall a. PPrint a => a -> Doc
pprint r
r), PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t]
  where
    ppe :: Doc
ppe  = ([Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Symbol, RType c tv r) -> Doc
ppxt ((Symbol, RType c tv r) -> Doc)
-> [(Symbol, RType c tv r)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
e)) Doc -> Doc -> Doc
<+> Doc
dcolon
    ppp :: Doc -> Doc
ppp  = \Doc
doc -> String -> Doc
text String
"<<" Doc -> Doc -> Doc
<+> Doc
doc Doc -> Doc -> Doc
<+> String -> Doc
text String
">>"
    ppxt :: (Symbol, RType c tv r) -> Doc
ppxt = \(Symbol
x, RType c tv r
t) -> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t
ppr_rtype PPEnv
_ Prec
_ (RHole r
r)
  = r -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"_"

ppTyConB :: TyConable c => PPEnv -> c -> Doc
ppTyConB :: PPEnv -> c -> Doc
ppTyConB PPEnv
bb
  | PPEnv -> Bool
ppShort PPEnv
bb = {- shortModules . -} c -> Doc
forall c. TyConable c => c -> Doc
ppTycon
  | Bool
otherwise  = c -> Doc
forall c. TyConable c => c -> Doc
ppTycon

shortModules :: Doc -> Doc
shortModules :: Doc -> Doc
shortModules = String -> Doc
text (String -> Doc) -> (Doc -> String) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
F.symbolString (Symbol -> String) -> (Doc -> Symbol) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> (Doc -> Symbol) -> Doc -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> (Doc -> String) -> Doc -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render

ppr_rsubtype
  :: (OkRT c tv r, PPrint a, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Prec -> [(a, RType c tv r)] -> Doc
ppr_rsubtype :: PPEnv -> Prec -> [(a, RType c tv r)] -> Doc
ppr_rsubtype PPEnv
bb Prec
p [(a, RType c tv r)]
e
  = Doc
pprint_env Doc -> Doc -> Doc
<+> String -> Doc
text String
"|-" Doc -> Doc -> Doc
<+> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
tl Doc -> Doc -> Doc
<+> Doc
"<:" Doc -> Doc -> Doc
<+> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
tr
  where
    ([(a, RType c tv r)]
el, (a, RType c tv r)
r)  = ([(a, RType c tv r)] -> [(a, RType c tv r)]
forall a. [a] -> [a]
init [(a, RType c tv r)]
e,  [(a, RType c tv r)] -> (a, RType c tv r)
forall a. [a] -> a
last [(a, RType c tv r)]
e)
    ([(a, RType c tv r)]
env, (a, RType c tv r)
l) = ([(a, RType c tv r)] -> [(a, RType c tv r)]
forall a. [a] -> [a]
init [(a, RType c tv r)]
el, [(a, RType c tv r)] -> (a, RType c tv r)
forall a. [a] -> a
last [(a, RType c tv r)]
el)
    tr :: RType c tv r
tr   = (a, RType c tv r) -> RType c tv r
forall a b. (a, b) -> b
snd ((a, RType c tv r) -> RType c tv r)
-> (a, RType c tv r) -> RType c tv r
forall a b. (a -> b) -> a -> b
$ (a, RType c tv r)
r
    tl :: RType c tv r
tl   = (a, RType c tv r) -> RType c tv r
forall a b. (a, b) -> b
snd ((a, RType c tv r) -> RType c tv r)
-> (a, RType c tv r) -> RType c tv r
forall a b. (a -> b) -> a -> b
$ (a, RType c tv r)
l
    pprint_bind :: (a, RType c tv r) -> Doc
pprint_bind (a
x, RType c tv r
t) = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<+> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t
    pprint_env :: Doc
pprint_env         = [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((a, RType c tv r) -> Doc
pprint_bind ((a, RType c tv r) -> Doc) -> [(a, RType c tv r)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, RType c tv r)]
env)

-- | From GHC: TypeRep
maybeParen :: Prec -> Prec -> Doc -> Doc
maybeParen :: Prec -> Prec -> Doc -> Doc
maybeParen Prec
ctxt_prec Prec
inner_prec Doc
pretty
  | Prec
ctxt_prec Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
< Prec
inner_prec = Doc
pretty
  | Bool
otherwise                  = Doc -> Doc
parens Doc
pretty

ppExists
  :: (OkRT c tv r, PPrint c, PPrint tv, PPrint (RType c tv r),
      PPrint (RType c tv ()), F.Reftable (RTProp c tv r),
      F.Reftable (RTProp c tv ()))
  => PPEnv -> Prec -> RType c tv r -> Doc
ppExists :: PPEnv -> Prec -> RType c tv r -> Doc
ppExists PPEnv
bb Prec
p RType c tv r
t
  = String -> Doc
text String
"exists" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
ppr_dbind PPEnv
bb Prec
topPrec Symbol
x RType c tv r
t | (Symbol
x, RType c tv r
t) <- [(Symbol, RType c tv r)]
zs]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t'
    where ([(Symbol, RType c tv r)]
zs,  RType c tv r
t')               = [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
forall c tv r.
[(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split [] RType c tv r
t
          split :: [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split [(Symbol, RType c tv r)]
zs (REx Symbol
x RType c tv r
t RType c tv r
t')   = [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split ((Symbol
x,RType c tv r
t)(Symbol, RType c tv r)
-> [(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall a. a -> [a] -> [a]
:[(Symbol, RType c tv r)]
zs) RType c tv r
t'
          split [(Symbol, RType c tv r)]
zs RType c tv r
t                = ([(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall a. [a] -> [a]
reverse [(Symbol, RType c tv r)]
zs, RType c tv r
t)

ppAllExpr
  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Prec -> RType c tv r -> Doc
ppAllExpr :: PPEnv -> Prec -> RType c tv r -> Doc
ppAllExpr PPEnv
bb Prec
p RType c tv r
t
  = String -> Doc
text String
"forall" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
ppr_dbind PPEnv
bb Prec
topPrec Symbol
x RType c tv r
t | (Symbol
x, RType c tv r
t) <- [(Symbol, RType c tv r)]
zs]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t'
    where 
      ([(Symbol, RType c tv r)]
zs,  RType c tv r
t')               = [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
forall c tv r.
[(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split [] RType c tv r
t
      split :: [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split [(Symbol, RType c tv r)]
zs (RAllE Symbol
x RType c tv r
t RType c tv r
t') = [(Symbol, RType c tv r)]
-> RType c tv r -> ([(Symbol, RType c tv r)], RType c tv r)
split ((Symbol
x,RType c tv r
t)(Symbol, RType c tv r)
-> [(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall a. a -> [a] -> [a]
:[(Symbol, RType c tv r)]
zs) RType c tv r
t'
      split [(Symbol, RType c tv r)]
zs RType c tv r
t              = ([(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall a. [a] -> [a]
reverse [(Symbol, RType c tv r)]
zs, RType c tv r
t)

ppReftPs
  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()),
      F.Reftable (Ref (RType c tv ()) (RType c tv r)))
  => t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc
ppReftPs :: t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc
ppReftPs t
_ t1
_ [Ref (RType c tv ()) (RType c tv r)]
rs
  | (Ref (RType c tv ()) (RType c tv r) -> Bool)
-> [Ref (RType c tv ()) (RType c tv r)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ref (RType c tv ()) (RType c tv r) -> Bool
forall r. Reftable r => r -> Bool
F.isTauto [Ref (RType c tv ()) (RType c tv r)]
rs   = Doc
empty
  | Bool -> Bool
not (PPEnv -> Bool
ppPs PPEnv
ppEnv) = Doc
empty
  | Bool
otherwise        = Doc -> Doc
angleBrackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Ref (RType c tv ()) (RType c tv r) -> Doc
forall c tv r.
OkRT c tv r =>
Ref (RType c tv ()) (RType c tv r) -> Doc
ppr_ref (Ref (RType c tv ()) (RType c tv r) -> Doc)
-> [Ref (RType c tv ()) (RType c tv r)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ref (RType c tv ()) (RType c tv r)]
rs

ppr_dbind
  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Prec -> F.Symbol -> RType c tv r -> Doc
ppr_dbind :: PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
ppr_dbind PPEnv
bb Prec
p Symbol
x RType c tv r
t
  | Symbol -> Bool
F.isNonSymbol Symbol
x Bool -> Bool -> Bool
|| (Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol)
  = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t
  | Bool
otherwise
  = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<-> PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv r
t



ppr_rty_fun
  :: ( OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Doc -> RType c tv r -> Doc
ppr_rty_fun :: PPEnv -> Doc -> RType c tv r -> Doc
ppr_rty_fun PPEnv
bb Doc
prefix RType c tv r
t = [Doc] -> Doc
hsep (Doc
prefix Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
dArgs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
dOut])
  where
    dArgs :: [Doc]
dArgs               = ((Symbol, RType c tv r, Doc) -> [Doc])
-> [(Symbol, RType c tv r, Doc)] -> [Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, RType c tv r, Doc) -> [Doc]
ppArg [(Symbol, RType c tv r, Doc)]
args
    dOut :: Doc
dOut                = PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
topPrec RType c tv r
out
    ppArg :: (Symbol, RType c tv r, Doc) -> [Doc]
ppArg (Symbol
b, RType c tv r
t, Doc
a)     = [PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Prec -> Symbol -> RType c tv r -> Doc
ppr_dbind PPEnv
bb Prec
funPrec Symbol
b RType c tv r
t, Doc
a]
    ([(Symbol, RType c tv r, Doc)]
args, RType c tv r
out)         = RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun RType c tv r
t

{- 
ppr_rty_fun bb prefix t
  = prefix <+> ppr_rty_fun' bb t

ppr_rty_fun'
  :: ( OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> RType c tv r -> Doc
ppr_rty_fun' bb (RImpF b t t' r)
  = F.ppTy r $ ppr_dbind bb funPrec b t $+$ ppr_rty_fun bb (text "~>") t'
ppr_rty_fun' bb (RFun b t t' r)
  = F.ppTy r $ ppr_dbind bb funPrec b t $+$ ppr_rty_fun bb arrow t'
ppr_rty_fun' bb t
  = ppr_rtype bb topPrec t
-}

brkFun :: RType c tv r -> ([(F.Symbol, RType c tv r, Doc)], RType c tv r) 
brkFun :: RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun (RImpF Symbol
b RType c tv r
t RType c tv r
t' r
_) = ((Symbol
b, RType c tv r
t, (String -> Doc
text String
"~>")) (Symbol, RType c tv r, Doc)
-> [(Symbol, RType c tv r, Doc)] -> [(Symbol, RType c tv r, Doc)]
forall a. a -> [a] -> [a]
: [(Symbol, RType c tv r, Doc)]
args, RType c tv r
out)   where ([(Symbol, RType c tv r, Doc)]
args, RType c tv r
out)     = RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun RType c tv r
t'  
brkFun (RFun Symbol
b RType c tv r
t RType c tv r
t' r
_)  = ((Symbol
b, RType c tv r
t, (String -> Doc
text String
"->")) (Symbol, RType c tv r, Doc)
-> [(Symbol, RType c tv r, Doc)] -> [(Symbol, RType c tv r, Doc)]
forall a. a -> [a] -> [a]
: [(Symbol, RType c tv r, Doc)]
args, RType c tv r
out)   where ([(Symbol, RType c tv r, Doc)]
args, RType c tv r
out)     = RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun RType c tv r
t'  
brkFun RType c tv r
out              = ([], RType c tv r
out) 




ppr_forall :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc
ppr_forall :: PPEnv -> Prec -> RType c tv r -> Doc
ppr_forall PPEnv
bb Prec
p RType c tv r
t = Prec -> Prec -> Doc -> Doc
maybeParen Prec
p Prec
funPrec (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [
                      Bool -> [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> Doc
ppr_foralls (PPEnv -> Bool
ppPs PPEnv
bb) ((RTVar tv (RType c tv ()), r) -> RTVar tv (RType c tv ())
forall a b. (a, b) -> a
fst ((RTVar tv (RType c tv ()), r) -> RTVar tv (RType c tv ()))
-> [(RTVar tv (RType c tv ()), r)] -> [RTVar tv (RType c tv ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars RTypeRep c tv r
trep) (RTypeRep c tv r -> [PVar (RType c tv ())]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds RTypeRep c tv r
trep)
                    , [(c, [RType c tv r])] -> Doc
ppr_clss [(c, [RType c tv r])]
cls
                    , PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
topPrec RType c tv r
t'
                    ]
  where
    trep :: RTypeRep c tv r
trep          = RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
t
    ([(c, [RType c tv r])]
cls, RType c tv r
t')     = RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass (RType c tv r -> ([(c, [RType c tv r])], RType c tv r))
-> RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep c tv r -> RType c tv r)
-> RTypeRep c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r
trep {ty_vars :: [(RTVar tv (RType c tv ()), r)]
ty_vars = [], ty_preds :: [PVar (RType c tv ())]
ty_preds = []}

    ppr_foralls :: Bool -> [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> Doc
ppr_foralls Bool
False [RTVar tv (RType c tv ())]
_ [PVar (RType c tv ())]
_  = Doc
empty
    ppr_foralls Bool
_    [] [] = Doc
empty
    ppr_foralls Bool
True [RTVar tv (RType c tv ())]
αs [PVar (RType c tv ())]
πs = String -> Doc
text String
"forall" Doc -> Doc -> Doc
<+> [RTVar tv (RType c tv ())] -> Doc
forall tv c. PPrint tv => [RTVar tv (RType c tv ())] -> Doc
dαs [RTVar tv (RType c tv ())]
αs Doc -> Doc -> Doc
<+> Bool -> [PVar (RType c tv ())] -> Doc
dπs (PPEnv -> Bool
ppPs PPEnv
bb) [PVar (RType c tv ())]
πs Doc -> Doc -> Doc
<-> Doc
dot

    ppr_clss :: [(c, [RType c tv r])] -> Doc
ppr_clss []               = Doc
empty
    ppr_clss [(c, [RType c tv r])]
cs               = (Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((c -> [RType c tv r] -> Doc) -> (c, [RType c tv r]) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (PPEnv -> Prec -> c -> [RType c tv r] -> Doc
forall c tv r a.
(OkRT c tv r, PPrint a, PPrint (RType c tv r),
 PPrint (RType c tv ())) =>
PPEnv -> Prec -> a -> [RType c tv r] -> Doc
ppr_cls PPEnv
bb Prec
p) ((c, [RType c tv r]) -> Doc) -> [(c, [RType c tv r])] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(c, [RType c tv r])]
cs)) Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>"

    dαs :: [RTVar tv (RType c tv ())] -> Doc
dαs [RTVar tv (RType c tv ())]
αs                    = [RTVar tv (RType c tv ())] -> Doc
forall tv c. PPrint tv => [RTVar tv (RType c tv ())] -> Doc
ppr_rtvar_def [RTVar tv (RType c tv ())]
αs

    -- dπs :: Bool -> [PVar a] -> Doc
    dπs :: Bool -> [PVar (RType c tv ())] -> Doc
dπs Bool
_ []                  = Doc
empty
    dπs Bool
False [PVar (RType c tv ())]
_               = Doc
empty
    dπs Bool
True [PVar (RType c tv ())]
πs               = Doc -> Doc
angleBrackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
intersperse Doc
comma ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
forall c tv.
OkRT c tv () =>
PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
ppr_pvar_def PPEnv
bb Prec
p (PVar (RType c tv ()) -> Doc) -> [PVar (RType c tv ())] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar (RType c tv ())]
πs

ppr_rtvar_def :: (PPrint tv) => [RTVar tv (RType c tv ())] -> Doc
ppr_rtvar_def :: [RTVar tv (RType c tv ())] -> Doc
ppr_rtvar_def = [Doc] -> Doc
sep ([Doc] -> Doc)
-> ([RTVar tv (RType c tv ())] -> [Doc])
-> [RTVar tv (RType c tv ())]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTVar tv (RType c tv ()) -> Doc)
-> [RTVar tv (RType c tv ())] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (tv -> Doc
forall a. PPrint a => a -> Doc
pprint (tv -> Doc)
-> (RTVar tv (RType c tv ()) -> tv)
-> RTVar tv (RType c tv ())
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar tv (RType c tv ()) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value)

ppr_cls
  :: (OkRT c tv r, PPrint a, PPrint (RType c tv r),
      PPrint (RType c tv ()))
  => PPEnv -> Prec -> a -> [RType c tv r] -> Doc
ppr_cls :: PPEnv -> Prec -> a -> [RType c tv r] -> Doc
ppr_cls PPEnv
bb Prec
p a
c [RType c tv r]
ts
  = a -> Doc
pp a
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((RType c tv r -> Doc) -> [RType c tv r] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPEnv -> Prec -> RType c tv r -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p) [RType c tv r]
ts)
  where
    pp :: a -> Doc
pp | PPEnv -> Bool
ppShort PPEnv
bb = String -> Doc
text (String -> Doc) -> (a -> String) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
F.symbolString (Symbol -> String) -> (a -> Symbol) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> (a -> Symbol) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> (a -> String) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. PPrint a => a -> Doc
pprint
       | Bool
otherwise  = a -> Doc
forall a. PPrint a => a -> Doc
pprint


ppr_pvar_def :: (OkRT c tv ()) => PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
ppr_pvar_def :: PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
ppr_pvar_def PPEnv
bb Prec
p (PV Symbol
s PVKind (RType c tv ())
t Symbol
_ [(RType c tv (), Symbol, Expr)]
xts)
  = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
s Doc -> Doc -> Doc
<+> Doc
dcolon Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
intersperse Doc
arrow [Doc]
dargs Doc -> Doc -> Doc
<+> PPEnv -> Prec -> PVKind (RType c tv ()) -> Doc
forall c tv.
OkRT c tv () =>
PPEnv -> Prec -> PVKind (RType c tv ()) -> Doc
ppr_pvar_kind PPEnv
bb Prec
p PVKind (RType c tv ())
t
  where
    dargs :: [Doc]
dargs = [PPEnv -> Prec -> RType c tv () -> Doc
forall c tv. OkRT c tv () => PPEnv -> Prec -> RType c tv () -> Doc
ppr_pvar_sort PPEnv
bb Prec
p RType c tv ()
xt | (RType c tv ()
xt,Symbol
_,Expr
_) <- [(RType c tv (), Symbol, Expr)]
xts]


ppr_pvar_kind :: (OkRT c tv ()) => PPEnv -> Prec -> PVKind (RType c tv ()) -> Doc
ppr_pvar_kind :: PPEnv -> Prec -> PVKind (RType c tv ()) -> Doc
ppr_pvar_kind PPEnv
bb Prec
p (PVProp RType c tv ()
t) = PPEnv -> Prec -> RType c tv () -> Doc
forall c tv. OkRT c tv () => PPEnv -> Prec -> RType c tv () -> Doc
ppr_pvar_sort PPEnv
bb Prec
p RType c tv ()
t Doc -> Doc -> Doc
<+> Doc
arrow Doc -> Doc -> Doc
<+> Symbol -> Doc
ppr_name Symbol
F.boolConName -- propConName
ppr_pvar_kind PPEnv
_ Prec
_ (PVKind (RType c tv ())
PVHProp)   = Maybe SrcSpan -> String -> Doc
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"TODO: ppr_pvar_kind:hprop" -- ppr_name hpropConName

ppr_name :: F.Symbol -> Doc
ppr_name :: Symbol -> Doc
ppr_name                      = String -> Doc
text (String -> Doc) -> (Symbol -> String) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
F.symbolString

ppr_pvar_sort :: (OkRT c tv ()) => PPEnv -> Prec -> RType c tv () -> Doc
ppr_pvar_sort :: PPEnv -> Prec -> RType c tv () -> Doc
ppr_pvar_sort PPEnv
bb Prec
p RType c tv ()
t = PPEnv -> Prec -> RType c tv () -> Doc
forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
ppr_rtype PPEnv
bb Prec
p RType c tv ()
t

ppr_ref :: (OkRT c tv r) => Ref (RType c tv ()) (RType c tv r) -> Doc
ppr_ref :: Ref (RType c tv ()) (RType c tv r) -> Doc
ppr_ref  (RProp [(Symbol, RType c tv ())]
ss RType c tv r
s) = [Symbol] -> Doc
ppRefArgs ((Symbol, RType c tv ()) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RType c tv ()) -> Symbol)
-> [(Symbol, RType c tv ())] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) Doc -> Doc -> Doc
<+> RType c tv r -> Doc
forall a. PPrint a => a -> Doc
pprint RType c tv r
s
-- ppr_ref (RProp ss s) = ppRefArgs (fst <$> ss) <+> pprint (fromMaybe mempty (stripRTypeBase s))

ppRefArgs :: [F.Symbol] -> Doc
ppRefArgs :: [Symbol] -> Doc
ppRefArgs [] = Doc
empty
ppRefArgs [Symbol]
ss = String -> Doc
text String
"\\" Doc -> Doc -> Doc
<-> [Doc] -> Doc
hsep (Symbol -> Doc
forall a. (Eq a, IsString a, PPrint a) => a -> Doc
ppRefSym (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ss [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing]) Doc -> Doc -> Doc
<+> Doc
arrow 

ppRefSym :: (Eq a, IsString a, PPrint a) => a -> Doc
ppRefSym :: a -> Doc
ppRefSym a
"" = String -> Doc
text String
"_"
ppRefSym a
s  = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
s

dot :: Doc
dot :: Doc
dot                = Char -> Doc
char Char
'.'

instance (PPrint r, F.Reftable r) => PPrint (UReft r) where
  pprintTidy :: Tidy -> UReft r -> Doc
pprintTidy Tidy
k (MkUReft r
r Predicate
p)
    | r -> Bool
forall r. Reftable r => r -> Bool
F.isTauto r
r  = Tidy -> Predicate -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Predicate
p
    | Predicate -> Bool
forall r. Reftable r => r -> Bool
F.isTauto Predicate
p  = Tidy -> r -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k r
r
    | Bool
otherwise  = Tidy -> Predicate -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Predicate
p Doc -> Doc -> Doc
<-> String -> Doc
text String
" & " Doc -> Doc -> Doc
<-> Tidy -> r -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k r
r

--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- | Pretty-printing errors ----------------------------------------------------
--------------------------------------------------------------------------------

printError :: (Show e, F.PPrint e) => F.Tidy -> DynFlags -> TError e -> IO ()
printError :: Tidy -> DynFlags -> TError e -> IO ()
printError Tidy
k DynFlags
dyn TError e
err = DynFlags -> SrcSpan -> Doc -> IO ()
putErrMsg DynFlags
dyn (TError e -> SrcSpan
forall t. TError t -> SrcSpan
pos TError e
err) (Tidy -> Doc -> TError e -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty TError e
err)

-- | Similar in spirit to 'reportErrors' from the GHC API, but it uses our pretty-printer
-- and shim functions under the hood.
reportErrors :: (Show e, F.PPrint e) => F.Tidy -> [TError e] -> Ghc.TcRn ()
reportErrors :: Tidy -> [TError e] -> TcRn ()
reportErrors Tidy
k [TError e]
errs =
  [TError e]
-> (TError e -> IOEnv (Env TcGblEnv TcLclEnv) ErrMsg)
-> IOEnv (Env TcGblEnv TcLclEnv) [ErrMsg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TError e]
errs (\TError e
err -> SrcSpan -> Doc -> Doc -> IOEnv (Env TcGblEnv TcLclEnv) ErrMsg
mkLongErrAt (TError e -> SrcSpan
forall t. TError t -> SrcSpan
pos TError e
err) (Tidy -> Doc -> TError e -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty TError e
err) Doc
forall a. Monoid a => a
mempty) IOEnv (Env TcGblEnv TcLclEnv) [ErrMsg]
-> ([ErrMsg] -> TcRn ()) -> TcRn ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [ErrMsg] -> TcRn ()
Ghc.reportErrors