-- | 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 FlexibleInstances    #-}
{-# LANGUAGE RecordWildCards      #-}
{-# LANGUAGE ScopedTypeVariables  #-}

{-# OPTIONS_GHC -Wno-orphans #-}

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

    -- * Printers
  , rtypeDoc

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

  -- * Printing diagnostics
  , printWarning

  -- * Filtering errors
  , Filter(..)
  , getFilters
  , reduceFilters
  , defaultFilterReporter

  -- * Reporting errors in the typechecking phase
  , FilterReportErrorsArgs(..)
  , filterReportErrorsWith
  , filterReportErrors

  ) where

import           Control.Monad                           (void)
import qualified Data.HashMap.Strict              as M
import qualified Data.List                        as L                               -- (sort)
import qualified Data.Set                         as Set
import           Data.String
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Types          as F
import qualified Liquid.GHC.API  as Ghc
import           Liquid.GHC.API  as Ghc ( Class
                                                         , SrcSpan
                                                         , PprPrec
                                                         , Type
                                                         , Var
                                                         , Name
                                                         , SourceError
                                                         , TyCon
                                                         , topPrec
                                                         , funPrec
                                                         , srcSpanStartLine
                                                         , srcSpanStartCol
                                                         )
import           Language.Haskell.Liquid.GHC.Logging (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 ((<>))


-- | `Filter`s match errors. They are used to ignore classes of errors they
-- match. `AnyFilter` matches all errors. `StringFilter` matches any error whose
-- \"representation\" contains the given `String`. A \"representation\" is
-- pretty-printed String of the error.
data Filter = StringFilter String
            | AnyFilter
  deriving (Filter -> Filter -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Filter -> Filter -> Bool
$c/= :: Filter -> Filter -> Bool
== :: Filter -> Filter -> Bool
$c== :: Filter -> Filter -> Bool
Eq, Eq Filter
Filter -> Filter -> Bool
Filter -> Filter -> Ordering
Filter -> Filter -> Filter
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Filter -> Filter -> Filter
$cmin :: Filter -> Filter -> Filter
max :: Filter -> Filter -> Filter
$cmax :: Filter -> Filter -> Filter
>= :: Filter -> Filter -> Bool
$c>= :: Filter -> Filter -> Bool
> :: Filter -> Filter -> Bool
$c> :: Filter -> Filter -> Bool
<= :: Filter -> Filter -> Bool
$c<= :: Filter -> Filter -> Bool
< :: Filter -> Filter -> Bool
$c< :: Filter -> Filter -> Bool
compare :: Filter -> Filter -> Ordering
$ccompare :: Filter -> Filter -> Ordering
Ord, Int -> Filter -> ShowS
[Filter] -> ShowS
Filter -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Filter] -> ShowS
$cshowList :: [Filter] -> ShowS
show :: Filter -> String
$cshow :: Filter -> String
showsPrec :: Int -> Filter -> ShowS
$cshowsPrec :: Int -> Filter -> ShowS
Show)

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

--------------------------------------------------------------------------------
pprintLongList :: PPrint a => F.Tidy -> [a] -> Doc
--------------------------------------------------------------------------------
pprintLongList :: forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k = Doc -> Doc
brackets forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (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
<-> 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 (Ghc.MsgEnvelope Ghc.DecoratedSDoc) where
  pprintTidy :: Tidy -> MsgEnvelope DecoratedSDoc -> Doc
pprintTidy Tidy
_ = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

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

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

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

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

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

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

instance PPrint Type where
  pprintTidy :: Tidy -> Type -> Doc
pprintTidy Tidy
_ = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> Doc
pprDoc
  pprintTidy Tidy
F.Full  =                forall a. Outputable a => a -> Doc
pprDoc

instance Show Predicate where
  show :: Predicate -> String
show = 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
<+> 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
<+> 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
<+> 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
<+> 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 forall a b. (a -> b) -> a -> b
$ forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a. PPrint a => a -> String
showpp

pprAnnInfoBinds :: (PPrint a, PPrint b) => F.Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds :: forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc
pprAnnInfoBinds Tidy
k (SrcSpan
l, [(Maybe a, b)]
xvs)
  = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
pprAnnInfoBind Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SrcSpan
l,) 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 :: forall a b.
(PPrint a, PPrint b) =>
Tidy -> (SrcSpan, (Maybe a, b)) -> Doc
pprAnnInfoBind Tidy
k (Ghc.RealSrcSpan RealSrcSpan
sp Maybe BufSpan
_, (Maybe a, b)
xv)
  = Doc
xd Doc -> Doc -> Doc
$$ forall a. Outputable a => a -> Doc
pprDoc Int
l Doc -> Doc -> Doc
$$ forall a. Outputable a => a -> Doc
pprDoc Int
c Doc -> Doc -> 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) = forall a a1.
(PPrint a, PPrint a1) =>
Tidy -> (Maybe a, a1) -> (Doc, Doc)
pprXOT Tidy
k (Maybe a, b)
xv
      n :: Int
n        = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ String -> [String]
lines 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 :: forall a a1.
(PPrint a, PPrint a1) =>
Tidy -> (Maybe a, a1) -> (Doc, Doc)
pprXOT Tidy
k (Maybe a
x, a1
v) = (Doc
xd, forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a1
v)
  where
    xd :: Doc
xd          = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"unknown" (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 [forall a. PPrint a => a -> Doc
pprint LocSymbol
x, forall a. PPrint a => a -> Doc
pprint [Symbol]
xs, String -> Doc
text String
"|->", 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 forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"logic-map"
                                 , Int -> Doc -> Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint HashMap Symbol LMap
lm
                                 , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"axiom-map"
                                 , Int -> Doc -> Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ 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
_ = 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 = 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 :: forall tv ty.
(PPrint tv, PPrint ty) =>
Tidy -> RTAlias tv ty -> Doc
ppAlias Tidy
k RTAlias tv ty
a =   forall a. PPrint a => a -> Doc
pprint (forall x a. RTAlias x a -> Symbol
rtName RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
space (forall x a. RTAlias x a -> [x]
rtTArgs RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
space (forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias tv ty
a)
            Doc -> Doc -> Doc
<+> String -> Doc
text String
" = "
            Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint (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 (forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (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 (forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (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 :: forall a. PPrint a => Tidy -> Doc -> [a] -> Doc
pprints Tidy
k Doc
c = [Doc] -> Doc
sep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k)

--------------------------------------------------------------------------------
rtypeDoc :: (OkRT c tv r) => F.Tidy -> RType c tv r -> Doc
--------------------------------------------------------------------------------
rtypeDoc :: forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc Tidy
k      = forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype (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

--------------------------------------------------------------------------------
pprRtype :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc
--------------------------------------------------------------------------------
pprRtype :: forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p t :: RType c tv r
t@(RAllT RTVU c tv
_ RType c tv r
_ r
r)
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprForall PPEnv
bb Prec
p RType c tv r
t
pprRtype PPEnv
bb Prec
p t :: RType c tv r
t@(RAllP PVU c tv
_ RType c tv r
_)
  = forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprForall PPEnv
bb Prec
p RType c tv r
t
pprRtype PPEnv
_ Prec
_ (RVar tv
a r
r)
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint tv
a
pprRtype PPEnv
bb Prec
p t :: RType c tv r
t@RFun{}
  = Prec -> Prec -> Doc -> Doc
maybeParen Prec
p Prec
funPrec (forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Doc -> RType c tv r -> Doc
pprRtyFun PPEnv
bb Doc
empty RType c tv r
t)
pprRtype PPEnv
bb Prec
p (RApp c
c [RType c tv r
t] [Ref (RType c tv ()) (RType c tv r)]
rs r
r)
  | forall c. TyConable c => c -> Bool
isList c
c
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t) Doc -> Doc -> 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 [Ref (RType c tv ()) (RType c tv r)]
rs
pprRtype PPEnv
bb Prec
p (RApp c
c [RType c tv r]
ts [Ref (RType c tv ()) (RType c tv r)]
rs r
r)
  | forall c. TyConable c => c -> Bool
isTuple c
c
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> [Doc] -> Doc
intersperse Doc
comma (forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts)) Doc -> Doc -> 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 [Ref (RType c tv ()) (RType c tv r)]
rs
pprRtype PPEnv
bb Prec
p (RApp c
c [RType c tv r]
ts [Ref (RType c tv ()) (RType c tv r)]
rs r
r)
  | Doc -> Bool
isEmpty Doc
rsDoc Bool -> Bool -> Bool
&& Doc -> Bool
isEmpty Doc
tsDoc
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ c -> Doc
ppT c
c
  | Bool
otherwise
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens 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            = 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 [Ref (RType c tv ()) (RType c tv r)]
rs
    tsDoc :: Doc
tsDoc            = [Doc] -> Doc
hsep (forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts)
    ppT :: c -> Doc
ppT              = forall c. TyConable c => PPEnv -> c -> Doc
ppTyConB PPEnv
bb

pprRtype PPEnv
bb Prec
p t :: RType c tv r
t@REx{}
  = 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
pprRtype PPEnv
bb Prec
p t :: RType c tv r
t@RAllE{}
  = 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
pprRtype PPEnv
_ Prec
_ (RExprArg Located Expr
e)
  = Doc -> Doc
braces forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint Located Expr
e
pprRtype PPEnv
bb Prec
p (RAppTy RType c tv r
t RType c tv r
t' r
r)
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t Doc -> Doc -> Doc
<+> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t'
pprRtype 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 (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
pprRsubtype PPEnv
bb Prec
p [(Symbol, RType c tv r)]
e) Doc -> Doc -> Doc
<+> Doc
"=>", forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t]
pprRtype PPEnv
bb Prec
p (RRTy [(Symbol, RType c tv r)]
e r
r Oblig
o RType c tv r
rt)
  = [Doc] -> Doc
sep [Doc -> Doc
ppp (forall a. PPrint a => a -> Doc
pprint Oblig
o Doc -> Doc -> Doc
<+> Doc
ppe Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint r
r), forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
rt]
  where
    ppe :: Doc
ppe         = [Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Symbol, RType c tv r) -> Doc
ppxt 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) = forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t
pprRtype PPEnv
_ Prec
_ (RHole r
r)
  = forall r. Reftable r => r -> Doc -> Doc
F.ppTy r
r forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"_"

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

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

pprRsubtype
  :: (OkRT c tv r, PPrint a, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Prec -> [(a, RType c tv r)] -> Doc
pprRsubtype :: 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
pprRsubtype PPEnv
bb Prec
p [(a, RType c tv r)]
e
  = Doc
pprint_env Doc -> Doc -> Doc
<+> String -> Doc
text String
"|-" Doc -> Doc -> Doc
<+> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
tl Doc -> Doc -> Doc
<+> Doc
"<:" Doc -> Doc -> Doc
<+> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
tr
  where
    ([(a, RType c tv r)]
el, (a, RType c tv r)
r)  = (forall a. [a] -> [a]
init [(a, RType c tv r)]
e,  forall a. [a] -> a
last [(a, RType c tv r)]
e)
    ([(a, RType c tv r)]
env, (a, RType c tv r)
l) = (forall a. [a] -> [a]
init [(a, RType c tv r)]
el, forall a. [a] -> a
last [(a, RType c tv r)]
el)
    tr :: RType c tv r
tr   = forall a b. (a, b) -> b
snd (a, RType c tv r)
r
    tl :: RType c tv r
tl   = forall a b. (a, b) -> b
snd (a, RType c tv r)
l
    pprint_bind :: (a, RType c tv r) -> Doc
pprint_bind (a
x, RType c tv r
t) = forall a. PPrint a => a -> Doc
pprint a
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<+> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
t
    pprint_env :: Doc
pprint_env         = [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((a, RType c tv r) -> Doc
pprint_bind 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 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 :: 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
rt
  = String -> Doc
text String
"exists" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [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
pprDbind PPEnv
bb Prec
topPrec Symbol
x RType c tv r
t | (Symbol
x, RType c tv r
t) <- [(Symbol, RType c tv r)]
ws]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
rt'
    where ([(Symbol, RType c tv r)]
ws,  RType c tv r
rt')               = 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
rt
          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)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                = (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 :: 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
rt
  = String -> Doc
text String
"forall" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [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
pprDbind PPEnv
bb Prec
topPrec Symbol
x RType c tv r
t | (Symbol
x, RType c tv r
t) <- [(Symbol, RType c tv r)]
ws]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
p RType c tv r
rt'
    where
      ([(Symbol, RType c tv r)]
ws,  RType c tv r
rt')               = 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
rt
      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)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              = (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 :: 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 t
_ t1
_ [Ref (RType c tv ()) (RType c tv r)]
rs
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall a b. (a -> b) -> a -> b
$ forall c tv r.
OkRT c tv r =>
Ref (RType c tv ()) (RType c tv r) -> Doc
pprRef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ref (RType c tv ()) (RType c tv r)]
rs

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



pprRtyFun
  :: ( OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))
  => PPEnv -> Doc -> RType c tv r -> Doc
pprRtyFun :: forall c tv r.
(OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) =>
PPEnv -> Doc -> RType c tv r -> Doc
pprRtyFun PPEnv
bb Doc
prefix RType c tv r
rt = [Doc] -> Doc
hsep (Doc
prefix forall a. a -> [a] -> [a]
: [Doc]
dArgs forall a. [a] -> [a] -> [a]
++ [Doc
dOut])
  where
    dArgs :: [Doc]
dArgs               = 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                = forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype 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)     = [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
pprDbind 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)         = forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun RType c tv r
rt

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

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

brkFun :: RType c tv r -> ([(F.Symbol, RType c tv r, Doc)], RType c tv r)
brkFun :: forall c tv r.
RType c tv r -> ([(Symbol, RType c tv r, Doc)], RType c tv r)
brkFun (RFun Symbol
b RFInfo
_ RType c tv r
t RType c tv r
t' r
_)  = ((Symbol
b, RType c tv r
t, String -> Doc
text String
"->") 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) = 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)




pprForall :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc
pprForall :: forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprForall PPEnv
bb Prec
p RType c tv r
t = Prec -> Prec -> Doc -> Doc
maybeParen Prec
p Prec
funPrec forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [
                      Bool -> [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> Doc
pprForalls (PPEnv -> Bool
ppPs PPEnv
bb) (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars RTypeRep c tv r
trep) (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
pprClss [(c, [RType c tv r])]
cls
                    , forall c tv r. OkRT c tv r => PPEnv -> Prec -> RType c tv r -> Doc
pprRtype PPEnv
bb Prec
topPrec RType c tv r
t'
                    ]
  where
    trep :: RTypeRep c tv r
trep          = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
t
    -- YL: remember to revert back
    ([(c, [RType c tv r])]
cls, RType c tv r
t')     = forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep 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 = []}
    -- t' = fromRTypeRep $ trep {ty_vars = [], ty_preds = []}

    pprForalls :: Bool -> [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> Doc
pprForalls Bool
False [RTVar tv (RType c tv ())]
_ [PVar (RType c tv ())]
_  = Doc
empty
    pprForalls Bool
_    [] [] = Doc
empty
    pprForalls Bool
True [RTVar tv (RType c tv ())]
αs [PVar (RType c tv ())]
πs = String -> Doc
text String
"forall" Doc -> Doc -> 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

    pprClss :: [(c, [RType c tv r])] -> Doc
pprClss []               = Doc
empty
    pprClss [(c, [RType c tv r])]
cs               = Doc -> Doc
parens ([Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (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
pprCls PPEnv
bb Prec
p) 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                    = forall {tv} {c}. PPrint tv => [RTVar tv (RType c tv ())] -> Doc
pprRtvarDef [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 forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
intersperse Doc
comma forall a b. (a -> b) -> a -> b
$ forall c tv.
OkRT c tv () =>
PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
pprPvarDef PPEnv
bb Prec
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar (RType c tv ())]
πs

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

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


pprPvarDef :: (OkRT c tv ()) => PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
pprPvarDef :: forall c tv.
OkRT c tv () =>
PPEnv -> Prec -> PVar (RType c tv ()) -> Doc
pprPvarDef PPEnv
bb Prec
p (PV Symbol
s PVKind (RType c tv ())
t Symbol
_ [(RType c tv (), Symbol, Expr)]
xts)
  = 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
<+> forall c tv.
OkRT c tv () =>
PPEnv -> Prec -> PVKind (RType c tv ()) -> Doc
pprPvarKind PPEnv
bb Prec
p PVKind (RType c tv ())
t
  where
    dargs :: [Doc]
dargs = [forall c tv. OkRT c tv () => PPEnv -> Prec -> RType c tv () -> Doc
pprPvarSort PPEnv
bb Prec
p RType c tv ()
xt | (RType c tv ()
xt,Symbol
_,Expr
_) <- [(RType c tv (), Symbol, Expr)]
xts]


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

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

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

pprRef :: (OkRT c tv r) => Ref (RType c tv ()) (RType c tv r) -> Doc
pprRef :: forall c tv r.
OkRT c tv r =>
Ref (RType c tv ()) (RType c tv r) -> Doc
pprRef  (RProp [(Symbol, RType c tv ())]
ss RType c tv r
s) = [Symbol] -> Doc
ppRefArgs (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint RType c tv r
s
-- pprRef (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 (forall a. (Eq a, IsString a, PPrint a) => a -> Doc
ppRefSym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ss forall a. [a] -> [a] -> [a]
++ [Maybe Integer -> Symbol
F.vv forall a. Maybe a
Nothing]) Doc -> Doc -> Doc
<+> Doc
arrow

ppRefSym :: (Eq a, IsString a, PPrint a) => a -> Doc
ppRefSym :: forall a. (Eq a, IsString a, PPrint a) => a -> Doc
ppRefSym a
"" = String -> Doc
text String
"_"
ppRefSym a
s  = 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)
    | forall r. Reftable r => r -> Bool
F.isTauto r
r  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Predicate
p
    | forall r. Reftable r => r -> Bool
F.isTauto Predicate
p  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k r
r
    | Bool
otherwise  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Predicate
p Doc -> Doc -> Doc
<-> String -> Doc
text String
" & " Doc -> Doc -> Doc
<-> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k r
r

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

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

-- | Similar in spirit to 'reportErrors' from the GHC API, but it uses our
-- pretty-printer and shim functions under the hood. Also filters the errors
-- according to the given `Filter` list.
--
-- @filterReportErrors failure continue filters k@ will call @failure@ if there
-- are unexpected errors, or will call @continue@ otherwise.
--
-- An error is expected if there is any filter that matches it.
filterReportErrors :: forall e' a. (Show e', F.PPrint e') => FilePath -> Ghc.TcRn a -> Ghc.TcRn a -> [Filter] -> F.Tidy -> [TError e'] -> Ghc.TcRn a
filterReportErrors :: forall e' a.
(Show e', PPrint e') =>
String
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
filterReportErrors String
path TcRn a
failure TcRn a
continue [Filter]
filters Tidy
k =
  forall (m :: * -> *) filter msg e a.
(Monad m, Ord filter) =>
FilterReportErrorsArgs m filter msg e a -> [e] -> m a
filterReportErrorsWith
    FilterReportErrorsArgs { msgReporter :: [MsgEnvelope DecoratedSDoc] -> IOEnv (Env TcGblEnv TcLclEnv) ()
msgReporter = [MsgEnvelope DecoratedSDoc] -> IOEnv (Env TcGblEnv TcLclEnv) ()
Ghc.reportErrors
                           , filterReporter :: [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
filterReporter = String -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter String
path
                           , failure :: TcRn a
failure = TcRn a
failure
                           , continue :: TcRn a
continue = TcRn a
continue
                           , pprinter :: TError e'
-> IOEnv (Env TcGblEnv TcLclEnv) (MsgEnvelope DecoratedSDoc)
pprinter = \TError e'
err -> SrcSpan
-> Doc
-> Doc
-> IOEnv (Env TcGblEnv TcLclEnv) (MsgEnvelope DecoratedSDoc)
mkLongErrAt (forall t. TError t -> SrcSpan
pos TError e'
err) (forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty TError e'
err) forall a. Monoid a => a
mempty
                           , matchingFilters :: TError e' -> [Filter]
matchingFilters = forall e. (e -> String) -> [Filter] -> e -> [Filter]
reduceFilters TError e' -> String
renderer [Filter]
filters
                           , filters :: [Filter]
filters = [Filter]
filters
                           }
  where
    renderer :: TError e' -> String
renderer TError e'
e = Doc -> String
render (forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty TError e'
e Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint (forall t. TError t -> SrcSpan
pos TError e'
e))


-- | Retrieve the `Filter`s from the Config.
getFilters :: Config -> [Filter]
getFilters :: Config -> [Filter]
getFilters Config
cfg = [Filter]
anyFilter forall a. Semigroup a => a -> a -> a
<> [Filter]
stringFilters
  where
    anyFilter :: [Filter]
anyFilter = [Filter
AnyFilter | Config -> Bool
expectAnyError Config
cfg]
    stringFilters :: [Filter]
stringFilters = String -> Filter
StringFilter forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> [String]
expectErrorContaining Config
cfg

-- | Return the list of @filters@ that matched the @err@ , given a @renderer@
-- for the @err@ and some @filters@
reduceFilters :: (e -> String) -> [Filter] -> e -> [Filter]
reduceFilters :: forall e. (e -> String) -> [Filter] -> e -> [Filter]
reduceFilters e -> String
renderer [Filter]
fs e
err = forall a. (a -> Bool) -> [a] -> [a]
filter (forall e. (e -> String) -> e -> Filter -> Bool
filterDoesMatchErr e -> String
renderer e
err) [Filter]
fs

filterDoesMatchErr :: (e -> String) -> e -> Filter -> Bool
filterDoesMatchErr :: forall e. (e -> String) -> e -> Filter -> Bool
filterDoesMatchErr e -> String
_        e
_ Filter
AnyFilter = Bool
True
filterDoesMatchErr e -> String
renderer e
e (StringFilter String
filter') = String -> String -> Bool
stringMatch String
filter' (e -> String
renderer e
e)

stringMatch :: String -> String -> Bool
stringMatch :: String -> String -> Bool
stringMatch String
filter' String
str = String
filter' forall a. Eq a => [a] -> [a] -> Bool
`L.isInfixOf` String
str

-- | Used in `filterReportErrorsWith'`
data FilterReportErrorsArgs m filter msg e a =
  FilterReportErrorsArgs
  {
    -- | Report the @msgs@ to the monad (usually IO)
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [msg] -> m ()
msgReporter :: [msg] -> m ()
  ,
    -- | Report unmatched @filters@ to the monad
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter] -> m ()
filterReporter :: [filter] -> m ()
  ,
    -- | Continuation for when there are unmatched filters or unmatched errors
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
failure :: m a
  ,
    -- | Continuation for when there are no unmatched errors or filters
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
continue :: m a
  ,
    -- | Compute a representation of the given error; does not report the error
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> e -> m msg
pprinter :: e -> m msg
  ,
    -- | Yields the filters that map a given error. Must only yield
    -- filters in the @filters@ field.
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> e -> [filter]
matchingFilters :: e -> [filter]
  ,
    -- | List of filters which could have been matched
    forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter]
filters :: [filter]
  }

-- | Calls the continuations in FilterReportErrorsArgs depending on whethere there
-- are unmatched errors, unmatched filters or none.
filterReportErrorsWith :: (Monad m, Ord filter) => FilterReportErrorsArgs m filter msg e a -> [e] -> m a
filterReportErrorsWith :: forall (m :: * -> *) filter msg e a.
(Monad m, Ord filter) =>
FilterReportErrorsArgs m filter msg e a -> [e] -> m a
filterReportErrorsWith FilterReportErrorsArgs {m a
[filter]
e -> m msg
e -> [filter]
[filter] -> m ()
[msg] -> m ()
filters :: [filter]
matchingFilters :: e -> [filter]
pprinter :: e -> m msg
continue :: m a
failure :: m a
filterReporter :: [filter] -> m ()
msgReporter :: [msg] -> m ()
filters :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter]
matchingFilters :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> e -> [filter]
pprinter :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> e -> m msg
continue :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
failure :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
filterReporter :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter] -> m ()
msgReporter :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [msg] -> m ()
..} [e]
errs =
  let
    ([(e, [filter])]
unmatchedErrors, [(e, [filter])]
matchedFilters) =
      forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [ (e
e, [filter]
fs) | e
e <- [e]
errs, let fs :: [filter]
fs = e -> [filter]
matchingFilters e
e ]
    unmatchedFilters :: [filter]
unmatchedFilters = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$
      forall a. Ord a => [a] -> Set a
Set.fromList [filter]
filters forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. Ord a => [a] -> Set a
Set.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [(e, [filter])]
matchedFilters)
  in
    if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(e, [filter])]
unmatchedErrors then
      if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [filter]
unmatchedFilters then
        m a
continue
      else do
        [filter] -> m ()
filterReporter [filter]
unmatchedFilters
        m a
failure
    else do
      [msg]
msgs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (e -> m msg
pprinter forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(e, [filter])]
unmatchedErrors
      forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ [msg] -> m ()
msgReporter [msg]
msgs
      m a
failure

-- | Report errors via GHC's API stating the given `Filter`s did not get
-- matched. Does nothing if the list of filters is empty.
defaultFilterReporter :: FilePath -> [Filter] -> Ghc.TcRn ()
defaultFilterReporter :: String -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter String
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
defaultFilterReporter String
path [Filter]
fs = MsgEnvelope DecoratedSDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
Ghc.reportError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SrcSpan
-> Doc
-> Doc
-> IOEnv (Env TcGblEnv TcLclEnv) (MsgEnvelope DecoratedSDoc)
mkLongErrAt SrcSpan
srcSpan ([Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ Doc
leaderMsg forall a. a -> [a] -> [a]
: (Int -> Doc -> Doc
nest Int
4 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
filterMsgs)) Doc
empty
  where
    leaderMsg :: Doc
    leaderMsg :: Doc
leaderMsg = String -> Doc
text String
"Could not match the following expected errors with actual thrown errors:"

    filterToMsg :: Filter -> Doc
    filterToMsg :: Filter -> Doc
filterToMsg Filter
AnyFilter = String -> Doc
text String
"<Any Liquid error>"
    filterToMsg (StringFilter String
s) = String -> Doc
text String
"String filter: " Doc -> Doc -> Doc
<-> Doc -> Doc
quotes (String -> Doc
text String
s)

    filterMsgs :: [Doc]
    filterMsgs :: [Doc]
filterMsgs = Filter -> Doc
filterToMsg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Filter]
fs

    beginningOfFile :: Ghc.SrcLoc
    beginningOfFile :: SrcLoc
beginningOfFile = FastString -> Int -> Int -> SrcLoc
Ghc.mkSrcLoc (forall a. IsString a => String -> a
fromString String
path) Int
1 Int
1

    srcSpan :: SrcSpan
    srcSpan :: SrcSpan
srcSpan = SrcLoc -> SrcLoc -> SrcSpan
Ghc.mkSrcSpan SrcLoc
beginningOfFile SrcLoc
beginningOfFile