-- | 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
  , ppTy

  -- * 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 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
                                                         , topPrec
                                                         , funPrec
                                                         , srcSpanStartLine
                                                         , srcSpanStartCol
                                                         )
import           Language.Haskell.Liquid.GHC.Logging
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names (LHName (..), getLHNameSymbol, lhNameToResolvedSymbol)
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.UX.Config
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
(Filter -> Filter -> Bool)
-> (Filter -> Filter -> Bool) -> Eq Filter
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Filter -> Filter -> Bool
== :: Filter -> Filter -> Bool
$c/= :: Filter -> Filter -> Bool
/= :: Filter -> Filter -> Bool
Eq, Eq Filter
Eq Filter =>
(Filter -> Filter -> Ordering)
-> (Filter -> Filter -> Bool)
-> (Filter -> Filter -> Bool)
-> (Filter -> Filter -> Bool)
-> (Filter -> Filter -> Bool)
-> (Filter -> Filter -> Filter)
-> (Filter -> Filter -> Filter)
-> Ord 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
$ccompare :: Filter -> Filter -> Ordering
compare :: Filter -> Filter -> Ordering
$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
>= :: Filter -> Filter -> Bool
$cmax :: Filter -> Filter -> Filter
max :: Filter -> Filter -> Filter
$cmin :: Filter -> Filter -> Filter
min :: Filter -> Filter -> Filter
Ord, Int -> Filter -> ShowS
[Filter] -> ShowS
Filter -> [Char]
(Int -> Filter -> ShowS)
-> (Filter -> [Char]) -> ([Filter] -> ShowS) -> Show Filter
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Filter -> ShowS
showsPrec :: Int -> Filter -> ShowS
$cshow :: Filter -> [Char]
show :: Filter -> [Char]
$cshowList :: [Filter] -> ShowS
showList :: [Filter] -> ShowS
Show)

--------------------------------------------------------------------------------
pprManyOrdered :: (PPrint a, Ord a) => F.Tidy -> String -> [a] -> [Doc]
--------------------------------------------------------------------------------
pprManyOrdered :: forall a. (PPrint a, Ord a) => Tidy -> [Char] -> [a] -> [Doc]
pprManyOrdered Tidy
k [Char]
msg = (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Doc
text [Char]
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 :: forall a. PPrint a => 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 SourceError where
  pprintTidy :: Tidy -> SourceError -> Doc
pprintTidy Tidy
_ = [Char] -> Doc
text ([Char] -> Doc) -> (SourceError -> [Char]) -> SourceError -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceError -> [Char]
forall a. Show a => a -> [Char]
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 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 -> [Char]
show = Predicate -> [Char]
forall a. PPrint a => a -> [Char]
showpp

instance (PPrint t) => PPrint (Annot t) where
  pprintTidy :: Tidy -> Annot t -> Doc
pprintTidy Tidy
k (AnnUse t
t) = [Char] -> Doc
text [Char]
"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) = [Char] -> Doc
text [Char]
"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) = [Char] -> Doc
text [Char]
"AnnRDf" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k t
t
  pprintTidy Tidy
_ (AnnLoc SrcSpan
l) = [Char] -> Doc
text [Char]
"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 -> [Char]
show = AnnInfo a -> [Char]
forall a. PPrint a => a -> [Char]
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 ([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 :: 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
$$ 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
$$ [Char] -> Doc
text [Char]
"\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        = [[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[Char]] -> Int) -> [[Char]] -> Int
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
lines ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
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, 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 (Ord v, F.Fixpoint v, PPrint v) => PPrint (LMapV v) where
  pprintTidy :: Tidy -> LMapV v -> Doc
pprintTidy Tidy
_ (LMap Located Symbol
x [Symbol]
xs ExprBV Symbol v
e) = [Doc] -> Doc
hcat [Located Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Located Symbol
x, [Symbol] -> Doc
forall a. PPrint a => a -> Doc
pprint [Symbol]
xs, [Char] -> Doc
text [Char]
"|->", ExprBV Symbol v -> Doc
forall a. PPrint a => a -> Doc
pprint ExprBV Symbol v
e ]

instance PPrint LogicMap where
  pprintTidy :: Tidy -> LogicMap -> Doc
pprintTidy Tidy
_ (LM HashMap Symbol LMap
lm HashMap Var (Maybe Symbol)
am) = [Doc] -> Doc
vcat [ [Char] -> Doc
text [Char]
"Logic Map"
                                 , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"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
$ [Char] -> Doc
text [Char]
"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
                                 ]

instance F.Fixpoint LHName where
  toFix :: LHName -> Doc
toFix LHName
lhname = case LHName
lhname of
    LHNUnresolved { }  -> Symbol -> Doc
pprintSymbol (Symbol -> Doc) -> (LHName -> Symbol) -> LHName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Symbol
getLHNameSymbol (LHName -> Doc) -> LHName -> Doc
forall a b. (a -> b) -> a -> b
$ LHName
lhname
    LHNResolved { } -> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> (LHName -> Symbol) -> LHName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Doc) -> LHName -> Doc
forall a b. (a -> b) -> a -> b
$ LHName
lhname

--------------------------------------------------------------------------------
-- | Pretty Printing RefType ---------------------------------------------------
--------------------------------------------------------------------------------
instance (OkRTBV b v c tv r) => PPrint (RTypeBV b v c tv r) where
  -- RJ: THIS IS THE CRUCIAL LINE, the following prints short types.
  pprintTidy :: Tidy -> RTypeBV b v c tv r -> Doc
pprintTidy Tidy
_ = Tidy -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
Tidy -> RTypeBV b v 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 :: forall tv ty.
(PPrint tv, PPrint ty) =>
Tidy -> RTAlias tv ty -> Doc
ppAlias Tidy
k RTAlias tv ty
a =   Located LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (RTAlias tv ty -> Located LHName
forall x a. RTAlias x a -> Located LHName
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
<+> [Char] -> Doc
text [Char]
" = "
            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
    =   [Char] -> Doc
text [Char]
"** Type Aliaes *********************"
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Tidy -> HashMap LHName (RTAlias tv t) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (RTEnv tv t -> HashMap LHName (RTAlias tv t)
forall tv t. RTEnv tv t -> HashMap LHName (RTAlias tv t)
typeAliases RTEnv tv t
rte))
    Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"** Expr Aliases ********************"
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Tidy -> HashMap LHName (RTAlias Symbol Expr) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k (RTEnv tv t -> HashMap LHName (RTAlias Symbol Expr)
forall tv t. RTEnv tv t -> HashMap LHName (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 ([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 :: (OkRTBV b v c tv r) => F.Tidy -> RTypeBV b v c tv r -> Doc
--------------------------------------------------------------------------------
rtypeDoc :: forall b v c tv r.
OkRTBV b v c tv r =>
Tidy -> RTypeBV b v c tv r -> Doc
rtypeDoc Tidy
k      = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype (Tidy -> PPEnv
ppE Tidy
k) PprPrec
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 :: (OkRTBV b v c tv r) => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc
--------------------------------------------------------------------------------
pprRtype :: forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p t :: RTypeBV b v c tv r
t@(RAllT RTVUBV b v c tv
_ RTypeBV b v c tv r
_ r
r)
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprForall PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
pprRtype PPEnv
bb PprPrec
p t :: RTypeBV b v c tv r
t@(RAllP PVUBV b v c tv
_ RTypeBV b v c tv r
_)
  = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprForall PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
pprRtype PPEnv
bb PprPrec
_ (RVar tv
a r
r)
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ tv -> Doc
forall a. PPrint a => a -> Doc
pprint tv
a
pprRtype PPEnv
bb PprPrec
p t :: RTypeBV b v c tv r
t@RFun{}
  = PprPrec -> PprPrec -> Doc -> Doc
maybeParen PprPrec
p PprPrec
funPrec (PPEnv -> Doc -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> Doc -> RTypeBV b v c tv r -> Doc
pprRtyFun PPEnv
bb Doc
empty RTypeBV b v c tv r
t)
pprRtype PPEnv
bb PprPrec
p (RApp c
c [RTypeBV b v c tv r
t] [RTPropBV b v c tv r]
rs r
r)
  | c -> Bool
forall c. TyConable c => c -> Bool
isList c
c
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t) Doc -> Doc -> Doc
<-> PPEnv -> PprPrec -> [RTPropBV b v c tv r] -> Doc
forall b v c tv r t t1.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
t
-> t1
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> Doc
ppReftPs PPEnv
bb PprPrec
p [RTPropBV b v c tv r]
rs
pprRtype PPEnv
bb PprPrec
p (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)
  | c -> Bool
forall c. TyConable c => c -> Bool
isTuple c
c
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> [Doc] -> Doc
intersperse Doc
comma (PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p (RTypeBV b v c tv r -> Doc) -> [RTypeBV b v c tv r] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts)) Doc -> Doc -> Doc
<-> PPEnv -> PprPrec -> [RTPropBV b v c tv r] -> Doc
forall b v c tv r t t1.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
t
-> t1
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> Doc
ppReftPs PPEnv
bb PprPrec
p [RTPropBV b v c tv r]
rs
pprRtype PPEnv
bb PprPrec
p (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)
  | Doc -> Bool
isEmpty Doc
rsDoc Bool -> Bool -> Bool
&& Doc -> Bool
isEmpty Doc
tsDoc
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ c -> Doc
ppT c
c
  | Bool
otherwise
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb 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 -> PprPrec -> [RTPropBV b v c tv r] -> Doc
forall b v c tv r t t1.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
t
-> t1
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> Doc
ppReftPs PPEnv
bb PprPrec
p [RTPropBV b v c tv r]
rs
    tsDoc :: Doc
tsDoc            = [Doc] -> Doc
hsep (PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p (RTypeBV b v c tv r -> Doc) -> [RTypeBV b v c tv r] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts)
    ppT :: c -> Doc
ppT              = PPEnv -> c -> Doc
forall c. TyConable c => PPEnv -> c -> Doc
ppTyConB PPEnv
bb

pprRtype PPEnv
bb PprPrec
p t :: RTypeBV b v c tv r
t@REx{}
  = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint c, PPrint tv,
 PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
ppExists PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
pprRtype PPEnv
bb PprPrec
p t :: RTypeBV b v c tv r
t@RAllE{}
  = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
ppAllExpr PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
pprRtype PPEnv
_ PprPrec
_ (RExprArg Located (ExprBV b v)
e)
  = Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Located (ExprBV b v) -> Doc
forall a. PPrint a => a -> Doc
pprint Located (ExprBV b v)
e
pprRtype PPEnv
bb PprPrec
p (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t Doc -> Doc -> Doc
<+> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t'
pprRtype PPEnv
bb PprPrec
p (RRTy [(b, RTypeBV b v c tv r)]
e r
_ Oblig
OCons RTypeBV b v c tv r
t)
  = [Doc] -> Doc
sep [Doc -> Doc
braces (PPEnv -> PprPrec -> [(b, RTypeBV b v c tv r)] -> Doc
forall b v c tv r a.
(OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> [(a, RTypeBV b v c tv r)] -> Doc
pprRsubtype PPEnv
bb PprPrec
p [(b, RTypeBV b v c tv r)]
e) Doc -> Doc -> Doc
<+> Doc
"=>", PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t]
pprRtype PPEnv
bb PprPrec
p (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
rt)
  = [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 -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
rt]
  where
    ppe :: Doc
ppe         = [Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((b, RTypeBV b v c tv r) -> Doc
ppxt ((b, RTypeBV b v c tv r) -> Doc)
-> [(b, RTypeBV b v c tv r)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv r)]
e)) Doc -> Doc -> Doc
<+> Doc
dcolon
    ppp :: Doc -> Doc
ppp  Doc
doc    = [Char] -> Doc
text [Char]
"<<" Doc -> Doc -> Doc
<+> Doc
doc Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
">>"
    ppxt :: (b, RTypeBV b v c tv r) -> Doc
ppxt (b
x, RTypeBV b v c tv r
t) = b -> Doc
forall a. PPrint a => a -> Doc
pprint b
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
pprRtype PPEnv
bb PprPrec
_ (RHole r
r)
  = PPEnv -> r -> Doc -> Doc
forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"_"

ppTyConB :: TyConable c => PPEnv -> c -> Doc
ppTyConB :: forall c. TyConable c => 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 = [Char] -> Doc
text ([Char] -> Doc) -> (Doc -> [Char]) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString (Symbol -> [Char]) -> (Doc -> Symbol) -> Doc -> [Char]
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
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Doc -> [Char]) -> Doc -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
render

pprRsubtype
  :: (OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Prec -> [(a, RTypeBV b v c tv r)] -> Doc
pprRsubtype :: forall b v c tv r a.
(OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> [(a, RTypeBV b v c tv r)] -> Doc
pprRsubtype PPEnv
bb PprPrec
p [(a, RTypeBV b v c tv r)]
e
  = Doc
pprint_env Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"|-" Doc -> Doc -> Doc
<+> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
tl Doc -> Doc -> Doc
<+> Doc
"<:" Doc -> Doc -> Doc
<+> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
tr
  where
    ([(a, RTypeBV b v c tv r)]
el, (a, RTypeBV b v c tv r)
r)  = ([(a, RTypeBV b v c tv r)] -> [(a, RTypeBV b v c tv r)]
forall a. HasCallStack => [a] -> [a]
init [(a, RTypeBV b v c tv r)]
e,  [(a, RTypeBV b v c tv r)] -> (a, RTypeBV b v c tv r)
forall a. HasCallStack => [a] -> a
last [(a, RTypeBV b v c tv r)]
e)
    ([(a, RTypeBV b v c tv r)]
env, (a, RTypeBV b v c tv r)
l) = ([(a, RTypeBV b v c tv r)] -> [(a, RTypeBV b v c tv r)]
forall a. HasCallStack => [a] -> [a]
init [(a, RTypeBV b v c tv r)]
el, [(a, RTypeBV b v c tv r)] -> (a, RTypeBV b v c tv r)
forall a. HasCallStack => [a] -> a
last [(a, RTypeBV b v c tv r)]
el)
    tr :: RTypeBV b v c tv r
tr   = (a, RTypeBV b v c tv r) -> RTypeBV b v c tv r
forall a b. (a, b) -> b
snd (a, RTypeBV b v c tv r)
r
    tl :: RTypeBV b v c tv r
tl   = (a, RTypeBV b v c tv r) -> RTypeBV b v c tv r
forall a b. (a, b) -> b
snd (a, RTypeBV b v c tv r)
l
    pprint_bind :: (a, RTypeBV b v c tv r) -> Doc
pprint_bind (a
x, RTypeBV b v 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 -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v 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, RTypeBV b v c tv r) -> Doc
pprint_bind ((a, RTypeBV b v c tv r) -> Doc)
-> [(a, RTypeBV b v c tv r)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, RTypeBV b v c tv r)]
env)

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

ppExists
  :: (OkRTBV b v c tv r, PPrint c, PPrint tv, PPrint (RTypeBV b v c tv r),
      PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc
ppExists :: forall b v c tv r.
(OkRTBV b v c tv r, PPrint c, PPrint tv,
 PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
ppExists PPEnv
bb PprPrec
p RTypeBV b v c tv r
rt
  = [Char] -> Doc
text [Char]
"exists" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
pprDbind PPEnv
bb PprPrec
topPrec b
x RTypeBV b v c tv r
t | (b
x, RTypeBV b v c tv r
t) <- [(b, RTypeBV b v c tv r)]
ws]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
rt'
    where ([(b, RTypeBV b v c tv r)]
ws,  RTypeBV b v c tv r
rt')               = [(b, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r)], RTypeBV b v c tv r)
forall {a} {v} {c} {tv} {r}.
[(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split [] RTypeBV b v c tv r
rt
          split :: [(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split [(a, RTypeBV a v c tv r)]
zs (REx a
x RTypeBV a v c tv r
t RTypeBV a v c tv r
t')   = [(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split ((a
x,RTypeBV a v c tv r
t)(a, RTypeBV a v c tv r)
-> [(a, RTypeBV a v c tv r)] -> [(a, RTypeBV a v c tv r)]
forall a. a -> [a] -> [a]
:[(a, RTypeBV a v c tv r)]
zs) RTypeBV a v c tv r
t'
          split [(a, RTypeBV a v c tv r)]
zs RTypeBV a v c tv r
t                = ([(a, RTypeBV a v c tv r)] -> [(a, RTypeBV a v c tv r)]
forall a. [a] -> [a]
reverse [(a, RTypeBV a v c tv r)]
zs, RTypeBV a v c tv r
t)

ppAllExpr
  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc
ppAllExpr :: forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
ppAllExpr PPEnv
bb PprPrec
p RTypeBV b v c tv r
rt
  = [Char] -> Doc
text [Char]
"forall" Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Doc -> [Doc] -> Doc
intersperse Doc
comma [PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
pprDbind PPEnv
bb PprPrec
topPrec b
x RTypeBV b v c tv r
t | (b
x, RTypeBV b v c tv r
t) <- [(b, RTypeBV b v c tv r)]
ws]) Doc -> Doc -> Doc
<-> Doc
dot Doc -> Doc -> Doc
<-> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
rt'
    where
      ([(b, RTypeBV b v c tv r)]
ws,  RTypeBV b v c tv r
rt')               = [(b, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r)], RTypeBV b v c tv r)
forall {a} {v} {c} {tv} {r}.
[(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split [] RTypeBV b v c tv r
rt
      split :: [(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split [(a, RTypeBV a v c tv r)]
zs (RAllE a
x RTypeBV a v c tv r
t RTypeBV a v c tv r
t') = [(a, RTypeBV a v c tv r)]
-> RTypeBV a v c tv r
-> ([(a, RTypeBV a v c tv r)], RTypeBV a v c tv r)
split ((a
x,RTypeBV a v c tv r
t)(a, RTypeBV a v c tv r)
-> [(a, RTypeBV a v c tv r)] -> [(a, RTypeBV a v c tv r)]
forall a. a -> [a] -> [a]
:[(a, RTypeBV a v c tv r)]
zs) RTypeBV a v c tv r
t'
      split [(a, RTypeBV a v c tv r)]
zs RTypeBV a v c tv r
t              = ([(a, RTypeBV a v c tv r)] -> [(a, RTypeBV a v c tv r)]
forall a. [a] -> [a]
reverse [(a, RTypeBV a v c tv r)]
zs, RTypeBV a v c tv r
t)

ppReftPs
  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))
  => t -> t1 -> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)] -> Doc
ppReftPs :: forall b v c tv r t t1.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
t
-> t1
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> Doc
ppReftPs t
_ t1
_ [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
rs
  | (RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)
 -> Bool)
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Bool
RefB
  b (RTypeBV b v c tv (NoReftB b)) (RTypeBV (ReftBind r) v c tv r)
-> Bool
forall {r} {c} {b} {τ} {v} {tv}.
(ToReft r, TyConable c) =>
RefB b τ (RTypeBV (ReftBind r) v c tv r) -> Bool
trivial [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v 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
$ RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc
pprRef (RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc)
-> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
-> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)]
rs
 where
  trivial :: RefB b τ (RTypeBV (ReftBind r) v c tv r) -> Bool
trivial (RProp [(b, τ)]
_ RTypeBV (ReftBind r) v c tv r
t) = RTypeBV (ReftBind r) v c tv r -> Bool
forall r c b v tv.
(ToReft r, TyConable c, Binder b, ReftBind r ~ b) =>
RTypeBV b v c tv r -> Bool
isTrivial RTypeBV (ReftBind r) v c tv r
t

pprDbind
  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Prec -> b -> RTypeBV b v c tv r -> Doc
pprDbind :: forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
pprDbind PPEnv
bb PprPrec
p b
x RTypeBV b v c tv r
t
  | b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall b. Binder b => b
F.wildcard
  = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t
  | Bool
otherwise
  = b -> Doc
forall a. PPrint a => a -> Doc
pprint b
x Doc -> Doc -> Doc
<-> Doc
colon Doc -> Doc -> Doc
<-> PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv r
t



pprRtyFun
  :: ( OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Doc -> RTypeBV b v c tv r -> Doc
pprRtyFun :: forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> Doc -> RTypeBV b v c tv r -> Doc
pprRtyFun PPEnv
bb Doc
prefix RTypeBV b v c tv r
rt = [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               = ((b, RTypeBV b v c tv r, Doc) -> [Doc])
-> [(b, RTypeBV b v c tv r, Doc)] -> [Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (b, RTypeBV b v c tv r, Doc) -> [Doc]
ppArg [(b, RTypeBV b v c tv r, Doc)]
args
    dOut :: Doc
dOut                = PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
topPrec RTypeBV b v c tv r
out
    ppArg :: (b, RTypeBV b v c tv r, Doc) -> [Doc]
ppArg (b
b, RTypeBV b v c tv r
t, Doc
a)     = [PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
(OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> b -> RTypeBV b v c tv r -> Doc
pprDbind PPEnv
bb PprPrec
funPrec b
b RTypeBV b v c tv r
t, Doc
a]
    ([(b, RTypeBV b v c tv r, Doc)]
args, RTypeBV b v c tv r
out)         = RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
forall b v c tv r.
RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
brkFun RTypeBV b v 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 :: RTypeBV b v c tv r -> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
brkFun :: forall b v c tv r.
RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
brkFun (RFun b
b RFInfo
_ RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
_)  = ((b
b, RTypeBV b v c tv r
t, [Char] -> Doc
text [Char]
"->") (b, RTypeBV b v c tv r, Doc)
-> [(b, RTypeBV b v c tv r, Doc)] -> [(b, RTypeBV b v c tv r, Doc)]
forall a. a -> [a] -> [a]
: [(b, RTypeBV b v c tv r, Doc)]
args, RTypeBV b v c tv r
out)
  where ([(b, RTypeBV b v c tv r, Doc)]
args, RTypeBV b v c tv r
out) = RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
forall b v c tv r.
RTypeBV b v c tv r
-> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r)
brkFun RTypeBV b v c tv r
t'
brkFun RTypeBV b v c tv r
out                = ([], RTypeBV b v c tv r
out)




pprForall :: (OkRTBV b v c tv r) => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc
pprForall :: forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprForall PPEnv
bb PprPrec
p RTypeBV b v c tv r
t = PprPrec -> PprPrec -> Doc -> Doc
maybeParen PprPrec
p PprPrec
funPrec (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [
                      Bool
-> [RTVar tv (RTypeBV b v c tv (NoReftB b))]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> Doc
pprForalls (PPEnv -> Bool
ppPs PPEnv
bb) ((RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> RTVar tv (RTypeBV b v c tv (NoReftB b))
forall a b. (a, b) -> a
fst ((RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
 -> RTVar tv (RTypeBV b v c tv (NoReftB b)))
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [RTVar tv (RTypeBV b v c tv (NoReftB b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_vars RTypeRepBV b v c tv r
trep) (RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds RTypeRepBV b v c tv r
trep)
                    , [(c, [RTypeBV b v c tv r])] -> Doc
pprClss [(c, [RTypeBV b v c tv r])]
cls
                    , PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
topPrec RTypeBV b v c tv r
t'
                    ]
  where
    trep :: RTypeRepBV b v c tv r
trep          = RTypeBV b v c tv r -> RTypeRepBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RTypeBV b v c tv r
t
    -- YL: remember to revert back
    ([(c, [RTypeBV b v c tv r])]
cls, RTypeBV b v c tv r
t')     = RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
forall c b v tv r.
(PPrint c, TyConable c) =>
RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass (RTypeBV b v c tv r
 -> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r))
-> RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
forall a b. (a -> b) -> a -> b
$ RTypeRepBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeRepBV b v c tv r -> RTypeBV b v c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRepBV b v c tv r
trep {ty_vars = [], ty_preds = []}
    -- t' = fromRTypeRep $ trep {ty_vars = [], ty_preds = []}

    pprForalls :: Bool
-> [RTVar tv (RTypeBV b v c tv (NoReftB b))]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> Doc
pprForalls Bool
False [RTVar tv (RTypeBV b v c tv (NoReftB b))]
_ [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
_  = Doc
empty
    pprForalls Bool
_    [] [] = Doc
empty
    pprForalls Bool
True [RTVar tv (RTypeBV b v c tv (NoReftB b))]
αs [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs = [Char] -> Doc
text [Char]
"forall" Doc -> Doc -> Doc
<+> [RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc
forall {tv} {b} {v} {c}.
PPrint tv =>
[RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc
dαs [RTVar tv (RTypeBV b v c tv (NoReftB b))]
αs Doc -> Doc -> Doc
<+> Bool -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))] -> Doc
dπs (PPEnv -> Bool
ppPs PPEnv
bb) [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs Doc -> Doc -> Doc
<-> Doc
dot

    pprClss :: [(c, [RTypeBV b v c tv r])] -> Doc
pprClss []               = Doc
empty
    pprClss [(c, [RTypeBV b v c tv r])]
cs               = Doc -> Doc
parens ([Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((c -> [RTypeBV b v c tv r] -> Doc)
-> (c, [RTypeBV b v c tv r]) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (PPEnv -> PprPrec -> c -> [RTypeBV b v c tv r] -> Doc
forall b v c tv r a.
(OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> a -> [RTypeBV b v c tv r] -> Doc
pprCls PPEnv
bb PprPrec
p) ((c, [RTypeBV b v c tv r]) -> Doc)
-> [(c, [RTypeBV b v c tv r])] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(c, [RTypeBV b v c tv r])]
cs)) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"=>"

    dαs :: [RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc
dαs [RTVar tv (RTypeBV b v c tv (NoReftB b))]
αs                    = [RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc
forall {tv} {b} {v} {c}.
PPrint tv =>
[RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc
pprRtvarDef [RTVar tv (RTypeBV b v c tv (NoReftB b))]
αs

    -- dπs :: Bool -> [PVar a] -> Doc
    dπs :: Bool -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))] -> Doc
dπs Bool
_ []                  = Doc
empty
    dπs Bool
False [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
_               = Doc
empty
    dπs Bool
True [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
π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
-> PprPrec -> PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc
forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv
-> PprPrec -> PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc
pprPvarDef PPEnv
bb PprPrec
p (PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc)
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs

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

pprCls
  :: (OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),
      PPrint (RTypeBV b v c tv (NoReftB b)))
  => PPEnv -> Prec -> a -> [RTypeBV b v c tv r] -> Doc
pprCls :: forall b v c tv r a.
(OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),
 PPrint (RTypeBV b v c tv (NoReftB b))) =>
PPEnv -> PprPrec -> a -> [RTypeBV b v c tv r] -> Doc
pprCls PPEnv
bb PprPrec
p a
c [RTypeBV b v c tv r]
ts
  = a -> Doc
pp a
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((RTypeBV b v c tv r -> Doc) -> [RTypeBV b v c tv r] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p) [RTypeBV b v c tv r]
ts)
  where
    pp :: a -> Doc
pp | PPEnv -> Bool
ppShort PPEnv
bb = [Char] -> Doc
text ([Char] -> Doc) -> (a -> [Char]) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString (Symbol -> [Char]) -> (a -> Symbol) -> a -> [Char]
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
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (a -> [Char]) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
render (Doc -> [Char]) -> (a -> Doc) -> a -> [Char]
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


pprPvarDef :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc
pprPvarDef :: forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv
-> PprPrec -> PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc
pprPvarDef PPEnv
bb PprPrec
p (PV b
s RTypeBV b v c tv (NoReftB b)
t b
_ [(RTypeBV b v c tv (NoReftB b), b, ExprBV b v)]
xts)
  = b -> Doc
forall a. PPrint a => a -> Doc
pprint b
s Doc -> Doc -> Doc
<+> Doc
dcolon Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
intersperse Doc
arrow [Doc]
dargs Doc -> Doc -> Doc
<+> PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarKind PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
t
  where
    dargs :: [Doc]
dargs = [PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarSort PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
xt | (RTypeBV b v c tv (NoReftB b)
xt,b
_,ExprBV b v
_) <- [(RTypeBV b v c tv (NoReftB b), b, ExprBV b v)]
xts]


pprPvarKind :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarKind :: forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarKind PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
t = PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarSort PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
t Doc -> Doc -> Doc
<+> Doc
arrow Doc -> Doc -> Doc
<+> Symbol -> Doc
pprName Symbol
F.boolConName

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

pprPvarSort :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarSort :: forall b v c tv.
OkRTBV b v c tv (NoReftB b) =>
PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
pprPvarSort PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
t = PPEnv -> PprPrec -> RTypeBV b v c tv (NoReftB b) -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
PPEnv -> PprPrec -> RTypeBV b v c tv r -> Doc
pprRtype PPEnv
bb PprPrec
p RTypeBV b v c tv (NoReftB b)
t

pprRef :: (OkRTBV b v c tv r) => RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc
pprRef :: forall b v c tv r.
OkRTBV b v c tv r =>
RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc
pprRef  (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss RTypeBV b v c tv r
s) = [b] -> Doc
forall b. (Binder b, PPrint b) => [b] -> Doc
ppRefArgs ((b, RTypeBV b v c tv (NoReftB b)) -> b
forall a b. (a, b) -> a
fst ((b, RTypeBV b v c tv (NoReftB b)) -> b)
-> [(b, RTypeBV b v c tv (NoReftB b))] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv (NoReftB b))]
ss) Doc -> Doc -> Doc
<+> RTypeBV b v c tv r -> Doc
forall a. PPrint a => a -> Doc
pprint RTypeBV b v c tv r
s
-- pprRef (RProp ss s) = ppRefArgs (fst <$> ss) <+> pprint (fromMaybe mempty (stripRTypeBase s))

ppRefArgs :: (F.Binder b, PPrint b) => [b] -> Doc
ppRefArgs :: forall b. (Binder b, PPrint b) => [b] -> Doc
ppRefArgs [] = Doc
empty
ppRefArgs [b]
ss = [Char] -> Doc
text [Char]
"\\" Doc -> Doc -> Doc
<-> [Doc] -> Doc
hsep (b -> Doc
forall b. (Binder b, PPrint b) => b -> Doc
ppRefSym (b -> Doc) -> [b] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
ss [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b
forall b. Binder b => b
F.wildcard]) Doc -> Doc -> Doc
<+> Doc
arrow

ppRefSym :: (F.Binder b, PPrint b) => b -> Doc
ppRefSym :: forall b. (Binder b, PPrint b) => b -> Doc
ppRefSym b
s | b
s b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall b. Binder b => b
F.wildcard = [Char] -> Doc
text [Char]
"_"
ppRefSym b
s                   = b -> Doc
forall a. PPrint a => a -> Doc
pprint b
s

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

ppTy ::
  ( Ord (ReftBind r), F.Fixpoint (ReftBind r), PPrint (ReftBind r)
  , Ord (ReftVar r), F.Fixpoint (ReftVar r), PPrint (ReftVar r)
  , ToReft r
  ) => PPEnv -> r -> Doc -> Doc
ppTy :: forall r.
(Ord (ReftBind r), Fixpoint (ReftBind r), PPrint (ReftBind r),
 Ord (ReftVar r), Fixpoint (ReftVar r), PPrint (ReftVar r),
 ToReft r) =>
PPEnv -> r -> Doc -> Doc
ppTy PPEnv
bb r
r0 Doc
t = Doc
doc
 where
  MkUReft ReftBV (ReftBind r) (ReftVar r)
r PredicateBV (ReftBind r) (ReftVar r)
p = r
-> UReftBV
     (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r))
forall r.
ToReft r =>
r
-> UReftBV
     (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r))
toUReft r
r0
  doc :: Doc
doc
    | ReftBV (ReftBind r) (ReftVar r) -> Bool
forall r. ToReft r => r -> Bool
isTauto ReftBV (ReftBind r) (ReftVar r)
r = Doc
tDoc
    | F.Reft (ReftBind (ReftBV (ReftBind r) (ReftVar r))
v, ExprBV
  (ReftBind (ReftBV (ReftBind r) (ReftVar r)))
  (ReftVar (ReftBV (ReftBind r) (ReftVar r)))
e) <- ReftBV (ReftBind r) (ReftVar r)
-> ReftBV
     (ReftBind (ReftBV (ReftBind r) (ReftVar r)))
     (ReftVar (ReftBV (ReftBind r) (ReftVar r)))
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft ReftBV (ReftBind r) (ReftVar r)
r =
        Doc -> Doc
braces (ReftBind r -> Doc
forall a. PPrint a => a -> Doc
pprint ReftBind r
ReftBind (ReftBV (ReftBind r) (ReftVar r))
v Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Doc
tDoc Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"|" Doc -> Doc -> Doc
<+> ExprBV (ReftBind r) (ReftVar r) -> Doc
forall a. PPrint a => a -> Doc
pprint ExprBV (ReftBind r) (ReftVar r)
ExprBV
  (ReftBind (ReftBV (ReftBind r) (ReftVar r)))
  (ReftVar (ReftBV (ReftBind r) (ReftVar r)))
e)
  tDoc :: Doc
tDoc
    | Pr [] <- PredicateBV (ReftBind r) (ReftVar r)
p    = Doc
t
    | Bool -> Bool
not (PPEnv -> Bool
ppPs PPEnv
bb) = Doc
t
    | Bool
otherwise     = Doc
t Doc -> Doc -> Doc
<-> Doc -> Doc
angleBrackets (PredicateBV (ReftBind r) (ReftVar r) -> Doc
forall a. PPrint a => a -> Doc
pprint PredicateBV (ReftBind r) (ReftVar r)
p)

instance (PPrint (PredicateBV b v), ToReft (PredicateBV b v), PPrint r, ToReft r) => PPrint (UReftBV b v r) where
  pprintTidy :: Tidy -> UReftBV b v r -> Doc
pprintTidy Tidy
k (MkUReft r
r PredicateBV b v
p)
    | r -> Bool
forall r. ToReft r => r -> Bool
isTauto r
r  = Tidy -> PredicateBV b v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k PredicateBV b v
p
    | PredicateBV b v -> Bool
forall r. ToReft r => r -> Bool
isTauto PredicateBV b v
p  = Tidy -> r -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k r
r
    | Bool
otherwise  = Tidy -> PredicateBV b v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k PredicateBV b v
p Doc -> Doc -> Doc
<-> [Char] -> Doc
text [Char]
" & " Doc -> Doc -> Doc
<-> Tidy -> r -> 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') =>
[Char]
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
filterReportErrors [Char]
path TcRn a
failure TcRn a
continue [Filter]
filters Tidy
k =
  FilterReportErrorsArgs
  (IOEnv (Env TcGblEnv TcLclEnv)) Filter (ZonkAny 0) (TError e') a
-> [TError e'] -> TcRn a
forall (m :: * -> *) filter msg e a.
(Monad m, Ord filter) =>
FilterReportErrorsArgs m filter msg e a -> [e] -> m a
filterReportErrorsWith
    FilterReportErrorsArgs { errorReporter :: [TError e'] -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorReporter = \[TError e']
errs ->
                               [(SrcSpan, Doc)] -> IOEnv (Env TcGblEnv TcLclEnv) ()
addTcRnUnknownMessages [(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) | TError e'
err <- [TError e']
errs]
                           , filterReporter :: [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
filterReporter = [Char] -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter [Char]
path
                           , failure :: TcRn a
failure = TcRn a
failure
                           , continue :: TcRn a
continue = TcRn a
continue
                           , matchingFilters :: TError e' -> [Filter]
matchingFilters = (TError e' -> [Char]) -> [Filter] -> TError e' -> [Filter]
forall e. (e -> [Char]) -> [Filter] -> e -> [Filter]
reduceFilters TError e' -> [Char]
renderer [Filter]
filters
                           , filters :: [Filter]
filters = [Filter]
filters
                           }
  where
    renderer :: TError e' -> [Char]
renderer TError e'
e = Doc -> [Char]
render (Tidy -> Doc -> TError e' -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty TError e'
e Doc -> Doc -> Doc
$+$ SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint (TError e' -> SrcSpan
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 [Filter] -> [Filter] -> [Filter]
forall a. Semigroup a => a -> a -> a
<> [Filter]
stringFilters
  where
    anyFilter :: [Filter]
anyFilter = [Filter
AnyFilter | Config -> Bool
expectAnyError Config
cfg]
    stringFilters :: [Filter]
stringFilters = [Char] -> Filter
StringFilter ([Char] -> Filter) -> [[Char]] -> [Filter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> [[Char]]
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 -> [Char]) -> [Filter] -> e -> [Filter]
reduceFilters e -> [Char]
renderer [Filter]
fs e
err = (Filter -> Bool) -> [Filter] -> [Filter]
forall a. (a -> Bool) -> [a] -> [a]
filter ((e -> [Char]) -> e -> Filter -> Bool
forall e. (e -> [Char]) -> e -> Filter -> Bool
filterDoesMatchErr e -> [Char]
renderer e
err) [Filter]
fs

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

stringMatch :: String -> String -> Bool
stringMatch :: [Char] -> [Char] -> Bool
stringMatch [Char]
filter' [Char]
str = [Char]
filter' [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isInfixOf` [Char]
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 -> [e] -> m ()
errorReporter :: [e] -> 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
  ,
    -- | 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 -> [filter]
[filter] -> m ()
[e] -> m ()
errorReporter :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [e] -> m ()
filterReporter :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter] -> m ()
failure :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
continue :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> m a
matchingFilters :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> e -> [filter]
filters :: forall (m :: * -> *) filter msg e a.
FilterReportErrorsArgs m filter msg e a -> [filter]
errorReporter :: [e] -> m ()
filterReporter :: [filter] -> m ()
failure :: m a
continue :: m a
matchingFilters :: e -> [filter]
filters :: [filter]
..} [e]
errs =
  let
    ([(e, [filter])]
unmatchedErrors, [(e, [filter])]
matchedFilters) =
      ((e, [filter]) -> Bool)
-> [(e, [filter])] -> ([(e, [filter])], [(e, [filter])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ([filter] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([filter] -> Bool)
-> ((e, [filter]) -> [filter]) -> (e, [filter]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e, [filter]) -> [filter]
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 = Set filter -> [filter]
forall a. Set a -> [a]
Set.toList (Set filter -> [filter]) -> Set filter -> [filter]
forall a b. (a -> b) -> a -> b
$
      [filter] -> Set filter
forall a. Ord a => [a] -> Set a
Set.fromList [filter]
filters Set filter -> Set filter -> Set filter
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` [filter] -> Set filter
forall a. Ord a => [a] -> Set a
Set.fromList (((e, [filter]) -> [filter]) -> [(e, [filter])] -> [filter]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (e, [filter]) -> [filter]
forall a b. (a, b) -> b
snd [(e, [filter])]
matchedFilters)
  in
    if [(e, [filter])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(e, [filter])]
unmatchedErrors then
      if [filter] -> Bool
forall a. [a] -> Bool
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
      [e] -> m ()
errorReporter ([e] -> m ()) -> [e] -> m ()
forall a b. (a -> b) -> a -> b
$ ((e, [filter]) -> e) -> [(e, [filter])] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map (e, [filter]) -> e
forall a b. (a, b) -> a
fst [(e, [filter])]
unmatchedErrors
      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 :: [Char] -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter [Char]
_ [] = () -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
defaultFilterReporter [Char]
path [Filter]
fs = SrcSpan -> Doc -> IOEnv (Env TcGblEnv TcLclEnv) ()
addTcRnUnknownMessage SrcSpan
srcSpan ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
leaderMsg Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> [Doc] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
filterMsgs))
  where
    leaderMsg :: Doc
    leaderMsg :: Doc
leaderMsg = [Char] -> Doc
text [Char]
"Could not match the following expected errors with actual thrown errors:"

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

    filterMsgs :: [Doc]
    filterMsgs :: [Doc]
filterMsgs = Filter -> Doc
filterToMsg (Filter -> Doc) -> [Filter] -> [Doc]
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 ([Char] -> FastString
forall a. IsString a => [Char] -> a
fromString [Char]
path) Int
1 Int
1

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