module Agda.TypeChecking.Pretty
    ( module Agda.TypeChecking.Pretty
    , module Data.Semigroup -- This re-export can be removed once <GHC-8.4 is dropped.
    , module Reexport
    ) where

import Prelude hiding ( null )

import Control.Applicative  (liftA2)
import Control.Monad
import Control.Monad.Except

import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.String    ()
import Data.Semigroup (Semigroup((<>)))
import qualified Data.Foldable as Fold

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.ReflectedToAbstract
import Agda.Syntax.Translation.AbstractToConcrete
import qualified Agda.Syntax.Translation.AbstractToConcrete as Reexport (MonadAbsToCon)
import qualified Agda.Syntax.Translation.ReflectedToAbstract as R
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract.Pretty as AP
import Agda.Syntax.Concrete.Pretty (bracesAndSemicolons, prettyHiding)
import qualified Agda.Syntax.Concrete.Pretty as CP
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Scope.Base  (AbstractName(..))
import Agda.Syntax.Scope.Monad (withContextPrecedence)
import Agda.Syntax.TopLevelModuleName

import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.DiscrimTree.Types
import Agda.TypeChecking.Substitute

import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Trie
import Agda.Utils.Permutation ( Permutation )
import Agda.Syntax.Common.Pretty      ( Pretty, prettyShow )
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Utils.Maybe.Strict as S
import Agda.Utils.Size        ( natSize )

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Wrappers for pretty printing combinators
---------------------------------------------------------------------------

type Doc = P.Doc

comma, colon, equals :: Applicative m => m Doc
comma :: forall (m :: * -> *). Applicative m => m Doc
comma  = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.comma
colon :: forall (m :: * -> *). Applicative m => m Doc
colon  = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.colon
equals :: forall (m :: * -> *). Applicative m => m Doc
equals = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.equals

{-# INLINE pretty #-}
pretty :: (Applicative m, P.Pretty a) => a -> m Doc
pretty :: forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
P.pretty a
x

{-# INLINE prettyA #-}
prettyA :: (ToConcrete a, P.Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
prettyA :: forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA a
x = a -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
AP.prettyA a
x

{-# INLINE prettyAs #-}
prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], P.Pretty ce, MonadAbsToCon m) => a -> m Doc
prettyAs :: forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
prettyAs a
x = a -> m Doc
forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
AP.prettyAs a
x

{-# INLINE text #-}
text :: Applicative m => String -> m Doc
text :: forall (m :: * -> *). Applicative m => String -> m Doc
text String
s = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text String
s

multiLineText :: Applicative m => String -> m Doc
multiLineText :: forall (m :: * -> *). Applicative m => String -> m Doc
multiLineText String
s = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.multiLineText String
s

pwords :: Applicative m => String -> [m Doc]
pwords :: forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
s = (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Doc] -> [m Doc]) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
P.pwords String
s

fwords :: Applicative m => String -> m Doc
fwords :: forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
s = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.fwords String
s

sep, fsep, hsep, hcat, vcat, vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
sep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep t (m Doc)
ds  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep  ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)
fsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep t (m Doc)
ds = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)
hsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep t (m Doc)
ds = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)
hcat :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat t (m Doc)
ds = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hcat ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)
vcat :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat t (m Doc)
ds = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)
vsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vsep t (m Doc)
ds = [Doc] -> Doc
P.vsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)

hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
hang :: forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang m Doc
p Int
n m Doc
q = Doc -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
P.hang (Doc -> Int -> Doc -> Doc) -> m Doc -> m (Int -> Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
p m (Int -> Doc -> Doc) -> m Int -> m (Doc -> Doc)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m Int
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n m (Doc -> Doc) -> m Doc -> m Doc
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Doc
q

infixl 6 <+>, <?>
infixl 5 $$, $+$

($$), ($+$), (<+>), (<?>) :: Applicative m => m Doc -> m Doc -> m Doc
m Doc
d1 $$ :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ m Doc
d2  = Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.$$) (Doc -> Doc -> Doc) -> m Doc -> m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 m (Doc -> Doc) -> m Doc -> m Doc
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Doc
d2
m Doc
d1 $+$ :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ m Doc
d2 = Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.$+$) (Doc -> Doc -> Doc) -> m Doc -> m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 m (Doc -> Doc) -> m Doc -> m Doc
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Doc
d2
m Doc
d1 <+> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
d2 = Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.<+>) (Doc -> Doc -> Doc) -> m Doc -> m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 m (Doc -> Doc) -> m Doc -> m Doc
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Doc
d2
m Doc
d1 <?> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> m Doc
d2 = Doc -> Doc -> Doc
(P.<?>) (Doc -> Doc -> Doc) -> m Doc -> m (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 m (Doc -> Doc) -> m Doc -> m Doc
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Doc
d2

nest :: Functor m => Int -> m Doc -> m Doc
nest :: forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
n m Doc
d   = Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest Int
n (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d

braces, dbraces, brackets, parens, parensNonEmpty
  , doubleQuotes, quotes :: Functor m => m Doc -> m Doc
braces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
braces m Doc
d   = Doc -> Doc
P.braces (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
dbraces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
dbraces m Doc
d  = Doc -> Doc
CP.dbraces (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
brackets :: forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets m Doc
d = Doc -> Doc
P.brackets (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
parens :: forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
d   = Doc -> Doc
P.parens (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
parensNonEmpty :: forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty m Doc
d = Doc -> Doc
P.parensNonEmpty (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
doubleQuotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
doubleQuotes   m Doc
d = Doc -> Doc
P.doubleQuotes   (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d
quotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
quotes         m Doc
d = Doc -> Doc
P.quotes         (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d

pshow :: (Applicative m, Show a) => a -> m Doc
pshow :: forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (a -> Doc) -> a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Show a => a -> Doc
P.pshow

-- | Comma-separated list in brackets.
prettyList :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
prettyList :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList t (m Doc)
ds = [Doc] -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ds)

-- | 'prettyList' without the brackets.
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
prettyList_ :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ t (m Doc)
ds = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> t (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma t (m Doc)
ds

{-# INLINABLE punctuate #-}
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
punctuate :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
d t (m Doc)
ts
  | [m Doc] -> Bool
forall a. Null a => a -> Bool
null [m Doc]
ds   = []
  | Bool
otherwise = (m Doc -> m Doc -> m Doc) -> [m Doc] -> [m Doc] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
(<>) [m Doc]
ds (Int -> m Doc -> [m Doc]
forall a. Int -> a -> [a]
replicate Int
n m Doc
d [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
forall a. Null a => a
empty])
  where
    ds :: [m Doc]
ds = t (m Doc) -> [m Doc]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t (m Doc)
ts
    n :: Int
n  = [m Doc] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m Doc]
ds Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

superscript :: Applicative m => Int -> m Doc
superscript :: forall (m :: * -> *). Applicative m => Int -> m Doc
superscript = String -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (String -> m Doc) -> (Int -> String) -> Int -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
go where
  digit :: Int -> Char
digit = (String
"⁰¹²³⁴⁵⁶⁷⁸⁹" String -> Int -> Char
forall a. HasCallStack => [a] -> Int -> a
!!)
  go :: Int -> String
go Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
9    = [Int -> Char
digit Int
k]
    | Bool
otherwise = Int -> Char
digit (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
10)Char -> String -> String
forall a. a -> [a] -> [a]
:Int -> String
go (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
10)

---------------------------------------------------------------------------
-- * The PrettyTCM class
---------------------------------------------------------------------------

type MonadPretty m = MonadAbsToCon m

-- This instance is to satify the constraints of superclass MonadPretty:
-- | This instance is more specific than a generic instance
-- @Semigroup a => Semigroup (TCM a)@.
instance {-# OVERLAPPING #-} Semigroup (TCM Doc)         where <> :: TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
(<>) = (Doc -> Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a b c. (a -> b -> c) -> TCMT IO a -> TCMT IO b -> TCMT IO c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>)


class PrettyTCM a where
  prettyTCM :: MonadPretty m => a -> m Doc

-- | Pretty print with a given context precedence
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
prettyTCMCtx :: forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
p = Precedence -> m Doc -> m Doc
forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence Precedence
p (m Doc -> m Doc) -> (a -> m Doc) -> a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM

instance {-# OVERLAPPING #-} PrettyTCM String where prettyTCM :: forall (m :: * -> *). MonadPretty m => String -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text
instance PrettyTCM Bool                       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM = Bool -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM C.Name                     where prettyTCM :: forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM = Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM C.QName                    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM = QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM TopLevelModuleName         where prettyTCM :: forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM = TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Comparison                 where prettyTCM :: forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM = Comparison -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Literal                    where prettyTCM :: forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM = Literal -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Nat                        where prettyTCM :: forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM = Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM ProblemId                  where prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemId -> m Doc
prettyTCM = ProblemId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Range                      where prettyTCM :: forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM = Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM CheckpointId               where prettyTCM :: forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
prettyTCM = CheckpointId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty
-- instance PrettyTCM Interval where prettyTCM = pretty
-- instance PrettyTCM Position where prettyTCM = pretty

{-# SPECIALIZE prettyTCM :: String             -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Bool               -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: C.Name             -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: C.QName            -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: TopLevelModuleName -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Comparison         -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Literal            -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Nat                -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: ProblemId          -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Range              -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: CheckpointId       -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Closure a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Closure a -> m Doc
prettyTCM Closure a
cl = Closure a -> (a -> m Doc) -> m Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure a
cl a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM

instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM [a] where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => [a] -> m Doc
prettyTCM = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([m Doc] -> m Doc) -> ([a] -> [m Doc]) -> [a] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM

{-# SPECIALIZE prettyTCM :: PrettyTCM a => [a] -> TCM Doc #-}

instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM (Maybe a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Maybe a -> m Doc
prettyTCM = m Doc -> (a -> m Doc) -> Maybe a -> m Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Doc
forall a. Null a => a
empty a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM

{-# SPECIALIZE prettyTCM :: PrettyTCM a => Maybe a -> TCM Doc #-}

instance (PrettyTCM a, PrettyTCM b) => PrettyTCM (a,b) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => (a, b) -> m Doc
prettyTCM (a
a, b
b) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> b -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => b -> m Doc
prettyTCM b
b

{-# SPECIALIZE prettyTCM :: (PrettyTCM a, PrettyTCM b) => (a, b) -> TCM Doc #-}

instance (PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a,b,c) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => (a, b, c) -> m Doc
prettyTCM (a
a, b
b, c
c) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
    a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> b -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => b -> m Doc
prettyTCM b
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> c -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => c -> m Doc
prettyTCM c
c

{-# SPECIALIZE prettyTCM :: (PrettyTCM a, PrettyTCM b, PrettyTCM c) => (a, b, c) -> TCM Doc #-}

instance PrettyTCM Term               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Term -> m Expr) -> Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify
instance PrettyTCM Type               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Type -> m Expr) -> Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify
instance PrettyTCM Sort               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Sort -> m Expr) -> Sort -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Sort -> m Expr
Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify
instance PrettyTCM DisplayTerm        where prettyTCM :: forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (DisplayTerm -> m Expr) -> DisplayTerm -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< DisplayTerm -> m Expr
DisplayTerm -> m (ReifiesTo DisplayTerm)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify
instance PrettyTCM NamedClause        where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM = Clause -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (NamedClause -> m Clause) -> NamedClause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedClause -> m Clause
NamedClause -> m (ReifiesTo NamedClause)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify
instance PrettyTCM (QNamed Clause)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM = Clause -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (QNamed Clause -> m Clause) -> QNamed Clause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< QNamed Clause -> m Clause
QNamed Clause -> m (ReifiesTo (QNamed Clause))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify
instance PrettyTCM Level              where prettyTCM :: forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Level -> m Expr) -> Level -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> m Expr) -> (Level -> Term) -> Level -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level -> Term
Level
instance PrettyTCM (Named_ Term)      where prettyTCM :: forall (m :: * -> *). MonadPretty m => Named_ Term -> m Doc
prettyTCM = Named (WithOrigin (Ranged String)) Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Named (WithOrigin (Ranged String)) Expr -> m Doc)
-> (Named_ Term -> m (Named (WithOrigin (Ranged String)) Expr))
-> Named_ Term
-> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Named_ Term -> m (Named (WithOrigin (Ranged String)) Expr)
Named_ Term -> m (ReifiesTo (Named_ Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Named_ Term -> m (ReifiesTo (Named_ Term))
reify
instance PrettyTCM (Arg Term)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Term -> m (Arg Expr)) -> Arg Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Term -> m (Arg Expr)
Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify
instance PrettyTCM (Arg Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Type -> m (Arg Expr)) -> Arg Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Type -> m (Arg Expr)
Arg Type -> m (ReifiesTo (Arg Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Type -> m (ReifiesTo (Arg Type))
reify
instance PrettyTCM (Arg Bool)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
prettyTCM = Arg Bool -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Bool -> m Doc)
-> (Arg Bool -> m (Arg Bool)) -> Arg Bool -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Bool -> m (Arg Bool)
Arg Bool -> m (ReifiesTo (Arg Bool))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Bool -> m (ReifiesTo (Arg Bool))
reify
instance PrettyTCM (Arg String)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg String -> m Doc
prettyTCM = Arg String -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg String -> m Doc)
-> (Arg String -> m (Arg String)) -> Arg String -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg String -> m (Arg String)
Arg String -> m (ReifiesTo (Arg String))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg String -> m (ReifiesTo (Arg String))
reify
instance PrettyTCM (Arg A.Expr)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Expr -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Expr -> m (Arg Expr)
Arg Expr -> m (ReifiesTo (Arg Expr))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Expr -> m (ReifiesTo (Arg Expr))
reify
instance PrettyTCM (NamedArg A.Expr)  where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM = NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (NamedArg Expr -> m Doc)
-> (NamedArg Expr -> m (NamedArg Expr)) -> NamedArg Expr -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedArg Expr -> m (NamedArg Expr)
NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
reify
instance PrettyTCM (NamedArg Term)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Term -> m Doc
prettyTCM = NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (NamedArg Expr -> m Doc)
-> (NamedArg Term -> m (NamedArg Expr)) -> NamedArg Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedArg Term -> m (NamedArg Expr)
NamedArg Term -> m (ReifiesTo (NamedArg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedArg Term -> m (ReifiesTo (NamedArg Term))
reify
instance PrettyTCM (Dom Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Dom Type -> m (Arg Expr)) -> Dom Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Dom Type -> m (Arg Expr)
Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom Type -> m (ReifiesTo (Dom Type))
reify
instance PrettyTCM ContextEntry       where prettyTCM :: forall (m :: * -> *). MonadPretty m => ContextEntry -> m Doc
prettyTCM = Arg (Name, Expr) -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg (Name, Expr) -> m Doc)
-> (ContextEntry -> m (Arg (Name, Expr))) -> ContextEntry -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ContextEntry -> m (Arg (Name, Expr))
ContextEntry -> m (ReifiesTo ContextEntry)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ContextEntry -> m (ReifiesTo ContextEntry)
reify
instance PrettyTCM Permutation        where prettyTCM :: forall (m :: * -> *). MonadPretty m => Permutation -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc)
-> (Permutation -> String) -> Permutation -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> String
forall a. Show a => a -> String
show
instance PrettyTCM Polarity           where prettyTCM :: forall (m :: * -> *). MonadPretty m => Polarity -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> (Polarity -> String) -> Polarity -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> String
forall a. Show a => a -> String
show
instance PrettyTCM IsForced           where prettyTCM :: forall (m :: * -> *). MonadPretty m => IsForced -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> (IsForced -> String) -> IsForced -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsForced -> String
forall a. Show a => a -> String
show

{-# SPECIALIZE prettyTCM :: Term              -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Type              -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Sort              -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: DisplayTerm       -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: NamedClause       -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (QNamed Clause)   -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Level             -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Named_ Term)     -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Arg Term)        -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Arg Type)        -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Arg Bool)        -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Arg A.Expr)      -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (NamedArg A.Expr) -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (NamedArg Term)   -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: (Dom Type)        -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: ContextEntry      -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Permutation       -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: Polarity          -> TCM Doc #-}
{-# SPECIALIZE prettyTCM :: IsForced          -> TCM Doc #-}

prettyR
  :: (R.ToAbstract r, PrettyTCM (R.AbsOfRef r), MonadPretty m, MonadError TCErr m)
  => r -> m Doc
prettyR :: forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR = AbsOfRef r -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbsOfRef r -> m Doc
prettyTCM (AbsOfRef r -> m Doc) -> (r -> m (AbsOfRef r)) -> r -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< r -> m (AbsOfRef r)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstractWithoutImplicit

instance (Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Substitution' a -> m Doc
prettyTCM Substitution' a
IdS        = m Doc
"idS"
  prettyTCM (Wk Int
m Substitution' a
IdS) = m Doc
"wkS" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
m
  prettyTCM (EmptyS Impossible
_) = m Doc
"emptyS"
  prettyTCM Substitution' a
rho = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution' a -> m Doc
prettyTCM Substitution' a
rho1
    where
      (Substitution' a
rho1, Substitution' a
rho2) = Int -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS Int
1 Substitution' a
rho
      u :: a
u            = Substitution' a -> Int -> a
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' a
rho2 Int
0

instance PrettyTCM Clause where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Clause -> m Doc
prettyTCM Clause
cl = do
    QName
x <- Name -> QName
qualify_ (Name -> QName) -> m Name -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ (String
"<unnamedclause>" :: String)
    QNamed Clause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
x Clause
cl)
{-# SPECIALIZE prettyTCM :: Clause -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Judgement a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Judgement a -> m Doc
prettyTCM (HasType a
a Comparison
cmp Type
t) = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
  prettyTCM (IsSort  a
a Type
t) = m Doc
"Sort" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
{-# SPECIALIZE prettyTCM :: PrettyTCM a => Judgement a -> TCM Doc #-}

instance PrettyTCM MetaId where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x = do
    String
mn <- MetaId -> m String
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m String
getMetaNameSuggestion MetaId
x
    NamedMeta -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedMeta -> m Doc
prettyTCM (NamedMeta -> m Doc) -> NamedMeta -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> MetaId -> NamedMeta
NamedMeta String
mn MetaId
x
{-# SPECIALIZE prettyTCM :: MetaId -> TCM Doc #-}

instance PrettyTCM NamedMeta where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedMeta -> m Doc
prettyTCM (NamedMeta String
s MetaId
m) = do
    ModuleNameHash
current <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
    m Doc
prefix  <-
      if MetaId -> ModuleNameHash
metaModule MetaId
m ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
current
      then m Doc -> m (m Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return m Doc
forall a. Null a => a
empty
      else do
        Maybe RawTopLevelModuleName
modName <- Tag ModuleNameHash
-> BiMap RawTopLevelModuleName ModuleNameHash
-> Maybe RawTopLevelModuleName
forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup (MetaId -> ModuleNameHash
metaModule MetaId
m) (BiMap RawTopLevelModuleName ModuleNameHash
 -> Maybe RawTopLevelModuleName)
-> m (BiMap RawTopLevelModuleName ModuleNameHash)
-> m (Maybe RawTopLevelModuleName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                   Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
-> m (BiMap RawTopLevelModuleName ModuleNameHash)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (BiMap RawTopLevelModuleName ModuleNameHash
 -> f (BiMap RawTopLevelModuleName ModuleNameHash))
-> TCState -> f TCState
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames
        m Doc -> m (m Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (m Doc -> m (m Doc)) -> m Doc -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ case Maybe RawTopLevelModuleName
modName of
          Maybe RawTopLevelModuleName
Nothing      -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
          Just RawTopLevelModuleName
modName -> RawTopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RawTopLevelModuleName
modName m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"."
    let inBetween :: m Doc
inBetween = case String
s of
          String
""  -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
          String
"_" -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
          String
s   -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_"
    m Doc
prefix m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
inBetween m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Word64 -> String
forall a. Show a => a -> String
show (MetaId -> Word64
metaId MetaId
m))
{-# SPECIALIZE prettyTCM :: NamedMeta -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Blocked a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Blocked a -> m Doc
prettyTCM (Blocked Blocker
x a
a) = (m Doc
"[" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"]") m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Blocker -> String
forall a. Pretty a => a -> String
P.prettyShow Blocker
x)
  prettyTCM (NotBlocked NotBlocked' Term
_ a
x) = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
{-# SPECIALIZE prettyTCM :: PrettyTCM a => Blocked a -> TCM Doc #-}

instance (PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Map k v -> m Doc
prettyTCM Map k v
m = m Doc
"Map" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma
    [ m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (k -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => k -> m Doc
prettyTCM k
k m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=") Int
2 (v -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => v -> m Doc
prettyTCM v
v) | (k
k, v
v) <- Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m ])
{-# SPECIALIZE prettyTCM :: (PrettyTCM k, PrettyTCM v) => Map k v -> TCM Doc  #-}

-- instance {-# OVERLAPPING #-} PrettyTCM ArgName where
--   prettyTCM = text . P.prettyShow

-- instance (Reify a e, ToConcrete e c, P.Pretty c, PrettyTCM a) => PrettyTCM (Elim' a) where
instance PrettyTCM Elim where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM (IApply Term
x Term
y Term
v) = m Doc
"I$" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
  prettyTCM (Apply Arg Term
v) = m Doc
"$" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
v
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
{-# SPECIALIZE prettyTCM :: Elim -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (MaybeReduced a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => MaybeReduced a -> m Doc
prettyTCM = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM (a -> m Doc) -> (MaybeReduced a -> a) -> MaybeReduced a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeReduced a -> a
forall a. MaybeReduced a -> a
ignoreReduced
{-# SPECIALIZE prettyTCM :: PrettyTCM a => MaybeReduced a -> TCM Doc #-}

instance PrettyTCM EqualityView where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => EqualityView -> m Doc
prettyTCM EqualityView
v = Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ EqualityView -> Type
forall a. EqualityUnview a => a -> Type
equalityUnview EqualityView
v
{-# SPECIALIZE prettyTCM :: EqualityView -> TCM Doc #-}

instance PrettyTCM A.Expr where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA; {-# INLINE prettyTCM #-}

instance PrettyTCM A.TypedBinding where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
prettyTCM = TypedBinding -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA; {-# INLINE prettyTCM #-}

instance PrettyTCM A.Pattern where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Pattern -> m Doc
prettyTCM = Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA; {-# INLINE prettyTCM #-}

instance PrettyTCM Relevance where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Relevance -> m Doc
prettyTCM = Relevance -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty; {-# INLINE prettyTCM #-}

instance PrettyTCM Quantity where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Quantity -> m Doc
prettyTCM = Quantity -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty; {-# INLINE prettyTCM #-}

instance PrettyTCM Erased where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Erased -> m Doc
prettyTCM = Erased -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty; {-# INLINE prettyTCM #-}

instance PrettyTCM Modality where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Modality -> m Doc
prettyTCM Modality
mod = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
    [ Quantity -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Quantity -> m Doc
prettyTCM (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod)
    , Relevance -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Relevance -> m Doc
prettyTCM (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod)
    ]
{-# SPECIALIZE prettyTCM :: Modality -> TCM Doc #-}

instance PrettyTCM Blocker where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM (UnblockOnAll Set Blocker
us) = m Doc
"all" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (Blocker -> m Doc) -> [Blocker] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM ([Blocker] -> [m Doc]) -> [Blocker] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  prettyTCM (UnblockOnAny Set Blocker
us) = m Doc
"any" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (Blocker -> m Doc) -> [Blocker] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM ([Blocker] -> [m Doc]) -> [Blocker] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  prettyTCM (UnblockOnMeta MetaId
m) = MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
  prettyTCM (UnblockOnProblem ProblemId
p) = m Doc
"problem" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ProblemId
p
  prettyTCM (UnblockOnDef QName
q) = m Doc
"definition" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
q
{-# SPECIALIZE prettyTCM :: Blocker -> TCM Doc #-}

instance PrettyTCM CompareAs where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM (AsTermsOf Type
a) = m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
a
  prettyTCM CompareAs
AsSizes       = m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> m Type -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  prettyTCM CompareAs
AsTypes       = m Doc
forall a. Null a => a
empty
{-# SPECIALIZE prettyTCM :: CompareAs -> TCM Doc #-}

instance PrettyTCM TypeCheckingProblem where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (CheckExpr Comparison
cmp Expr
e Type
a) =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":?", Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a ]
  prettyTCM (CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
es Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
_) =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"_ :" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Expr]
es
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
":?" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t1 ]
  prettyTCM (CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_) = TypeCheckingProblem -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t)
  prettyTCM (CheckLambda Comparison
cmp (Arg ArgInfo
ai (List1 (WithHiding Name)
xs, Maybe Type
mt)) Expr
e Type
t) =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
CP.lambda m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          (ArgInfo -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
CP.prettyRelevance ArgInfo
ai (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
           ArgInfo -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
CP.prettyHiding ArgInfo
ai (if Maybe Type -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Type
mt Bool -> Bool -> Bool
&& List1 (WithHiding Name) -> Peano
forall a. Sized a => a -> Peano
natSize List1 (WithHiding Name)
xs Peano -> Peano -> Bool
forall a. Eq a => a -> a -> Bool
== Peano
1 then Doc -> Doc
forall a. a -> a
id
                               else Doc -> Doc
P.parens) (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
              (WithHiding Name -> m Doc) -> [WithHiding Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => WithHiding Name -> m Doc
prettyTCM (List1 (WithHiding Name) -> [Item (List1 (WithHiding Name))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (WithHiding Name)
xs) [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
              Maybe Type -> [m Doc] -> (Type -> [m Doc]) -> [m Doc]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Type
mt [] (\ Type
a -> [m Doc
":", Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a])) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
CP.arrow m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          m Doc
":?"
        , Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]
  prettyTCM (DoQuoteTerm Comparison
_ Term
v Type
_) = do
    Expr
e <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
    Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
A.defaultAppInfo_ (ExprInfo -> Expr
A.QuoteTerm ExprInfo
A.exprNoRange) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e))
{-# SPECIALIZE prettyTCM :: TypeCheckingProblem -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (WithHiding a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => WithHiding a -> m Doc
prettyTCM (WithHiding Hiding
h a
a) = Hiding -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
CP.prettyHiding Hiding
h Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a
{-# SPECIALIZE prettyTCM :: PrettyTCM a => WithHiding a -> TCM Doc #-}

instance PrettyTCM Name where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x = Name -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Name -> Doc) -> m Name -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> m (ConOfAbs Name)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
x
{-# SPECIALIZE prettyTCM :: Name -> TCM Doc #-}

instance PrettyTCM QName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x = QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty (QName -> Doc) -> m QName -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (ConOfAbs QName)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ QName
x
{-# SPECIALIZE prettyTCM :: Name -> TCM Doc #-}

instance PrettyTCM ModuleName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
x = QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty (QName -> Doc) -> m QName -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (ConOfAbs ModuleName)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ ModuleName
x
{-# SPECIALIZE prettyTCM :: ModuleName -> TCM Doc #-}

instance PrettyTCM AbstractName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc)
-> (AbstractName -> QName) -> AbstractName -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName
{-# SPECIALIZE prettyTCM :: AbstractName -> TCM Doc #-}

instance PrettyTCM ConHead where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> (ConHead -> QName) -> ConHead -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName
{-# SPECIALIZE prettyTCM :: ConHead -> TCM Doc #-}

instance PrettyTCM Telescope where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc)
-> ([Maybe TypedBinding] -> [Doc]) -> [Maybe TypedBinding] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe TypedBinding -> Doc) -> [Maybe TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Maybe TypedBinding -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([Maybe TypedBinding] -> Doc) -> m [Maybe TypedBinding] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Telescope
tel <- Telescope -> m (ReifiesTo Telescope)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Telescope -> m (ReifiesTo Telescope)
reify Telescope
tel
      AbsToCon [Maybe TypedBinding] -> m [Maybe TypedBinding]
forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon (AbsToCon [Maybe TypedBinding] -> m [Maybe TypedBinding])
-> AbsToCon [Maybe TypedBinding] -> m [Maybe TypedBinding]
forall a b. (a -> b) -> a -> b
$ Telescope
-> (ConOfAbs Telescope -> AbsToCon [Maybe TypedBinding])
-> AbsToCon [Maybe TypedBinding]
forall b.
Telescope -> (ConOfAbs Telescope -> AbsToCon b) -> AbsToCon b
forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete Telescope
tel [Maybe TypedBinding] -> AbsToCon [Maybe TypedBinding]
ConOfAbs Telescope -> AbsToCon [Maybe TypedBinding]
forall a. a -> AbsToCon a
forall (m :: * -> *) a. Monad m => a -> m a
return
{-# SPECIALIZE prettyTCM :: Telescope -> TCM Doc #-}

newtype PrettyContext = PrettyContext Context

instance PrettyTCM PrettyContext where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => PrettyContext -> m Doc
prettyTCM (PrettyContext Context
ctx) = Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> m Doc) -> Telescope -> m Doc
forall a b. (a -> b) -> a -> b
$ (Name -> String) -> Context -> Telescope
forall a. (a -> String) -> ListTel' a -> Telescope
telFromList' Name -> String
nameToArgName (Context -> Telescope) -> Context -> Telescope
forall a b. (a -> b) -> a -> b
$ Context -> Context
forall a. [a] -> [a]
reverse Context
ctx
{-# SPECIALIZE prettyTCM :: PrettyContext -> TCM Doc #-}

instance PrettyTCM DBPatVar where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DBPatVar -> m Doc
prettyTCM = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (DBPatVar -> Term) -> DBPatVar -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var (Int -> Term) -> (DBPatVar -> Int) -> DBPatVar -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBPatVar -> Int
dbPatVarIndex
{-# SPECIALIZE prettyTCM :: DBPatVar -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Pattern' a) where
  prettyTCM :: forall m. MonadPretty m => Pattern' a -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (IApplyP PatternInfo
_ Term
_ Term
_ a
x)    = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
  prettyTCM (VarP PatternInfo
_ a
x)    = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
  prettyTCM (DotP PatternInfo
_ Term
t)    = m Doc
".(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"
  prettyTCM (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
  prettyTCM (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps) = -- (if b then braces else parens) $ prTy $
        m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
      where
        -- NONE OF THESE BINDINGS IS USED AT THE MOMENT:
        b :: Bool
b = ConPatternInfo -> Bool
conPRecord ConPatternInfo
i Bool -> Bool -> Bool
&& PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i) PatOrigin -> PatOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= PatOrigin
PatOCon
        showRec :: m Doc -- Defined, but currently not used
        showRec :: m Doc
showRec = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ m Doc
"record"
          , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
bracesAndSemicolons ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg QName -> NamedArg (Pattern' a) -> m Doc)
-> [Arg QName] -> [NamedArg (Pattern' a)] -> m [Doc]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Arg QName -> NamedArg (Pattern' a) -> m Doc
showField (ConHead -> [Arg QName]
conFields ConHead
c) [NamedArg (Pattern' a)]
ps
          ]
        showField :: Arg QName -> NamedArg (Pattern' a) -> m Doc -- NB:: Defined but not used
        showField :: Arg QName -> NamedArg (Pattern' a) -> m Doc
showField (Arg ArgInfo
ai QName
x) NamedArg (Pattern' a)
p =
          [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM (QName -> Name
A.qnameName QName
x) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=" , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (Pattern' a -> m Doc) -> Pattern' a -> m Doc
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p ]
        showCon :: m Doc -- NB:: Defined but not used
        showCon :: m Doc
showCon = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> m Doc
prTy (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
        prTy :: m Doc -> m Doc
prTy m Doc
d = Maybe (Arg Type) -> m Doc -> (Arg Type -> m Doc) -> m Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i) m Doc
d ((Arg Type -> m Doc) -> m Doc) -> (Arg Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Arg Type
t -> m Doc
d  m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
prettyTCM Arg Type
t
  prettyTCM (LitP PatternInfo
_ Literal
l)    = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Literal -> String
forall a. Pretty a => a -> String
P.prettyShow Literal
l)
  prettyTCM (ProjP ProjOrigin
_ QName
q)   = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q)
{-# SPECIALIZE prettyTCM :: PrettyTCM a => Pattern' a -> TCM Doc #-}

{-# SPECIALIZE prettyTCMPatterns :: [NamedArg DeBruijnPattern] -> TCM [Doc] #-}
-- | Proper pretty printing of patterns:
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns :: forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns = (NamedArg Pattern -> m Doc) -> [NamedArg Pattern] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern] -> m [Doc])
-> ([NamedArg DeBruijnPattern] -> m [NamedArg Pattern])
-> [NamedArg DeBruijnPattern]
-> m [Doc]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
reifyPatterns

{-# SPECIALIZE prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc #-}
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList :: forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([m Doc] -> m Doc)
-> ([NamedArg Pattern] -> [m Doc]) -> [NamedArg Pattern] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg Pattern -> m Doc) -> [NamedArg Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern] -> m Doc)
-> ([NamedArg DeBruijnPattern] -> m [NamedArg Pattern])
-> [NamedArg DeBruijnPattern]
-> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
reifyPatterns

instance PrettyTCM (Elim' DisplayTerm) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim' DisplayTerm -> m Doc
prettyTCM (IApply DisplayTerm
x DisplayTerm
y DisplayTerm
v) = m Doc
"$" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DisplayTerm -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM DisplayTerm
v
  prettyTCM (Apply Arg DisplayTerm
v) = m Doc
"$" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DisplayTerm -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM (Arg DisplayTerm -> DisplayTerm
forall e. Arg e -> e
unArg Arg DisplayTerm
v)
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
{-# SPECIALIZE prettyTCM :: Elim' DisplayTerm -> TCM Doc #-}

instance PrettyTCM NLPat where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (PVar Int
x [Arg Int]
bvs) = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Elims -> Term
Var Int
x ((Arg Int -> Elim) -> [Arg Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Arg Int -> Arg Term) -> Arg Int -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Term) -> Arg Int -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
bvs))
  prettyTCM (PDef QName
f PElims
es) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
    QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((Elim' NLPat -> m Doc) -> PElims -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM PElims
es)
  prettyTCM (PLam ArgInfo
i Abs NLPat
u)  = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ m Doc
"λ"
    , ArgInfo -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
i Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Abs NLPat -> String
forall a. Abs a -> String
absName Abs NLPat
u)
    , m Doc
"→"
    , String -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
addContext (Abs NLPat -> String
forall a. Abs a -> String
absName Abs NLPat
u) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (NLPat -> m Doc) -> NLPat -> m Doc
forall a b. (a -> b) -> a -> b
$ Abs NLPat -> NLPat
forall a. Subst a => Abs a -> a
absBody Abs NLPat
u
    ]
  prettyTCM (PPi Dom NLPType
a Abs NLPType
b)   = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Dom NLPType -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Dom NLPType
a Doc -> Doc
P.parens (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ Abs NLPType -> String
forall a. Abs a -> String
absName Abs NLPType
b, m Doc
":", NLPType -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
prettyTCM (NLPType -> m Doc) -> NLPType -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom NLPType -> NLPType
forall t e. Dom' t e -> e
unDom Dom NLPType
a ]
    , m Doc
"→"
    , String -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
addContext (Abs NLPType -> String
forall a. Abs a -> String
absName Abs NLPType
b) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NLPType -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
prettyTCM (NLPType -> m Doc) -> NLPType -> m Doc
forall a b. (a -> b) -> a -> b
$ Abs NLPType -> NLPType
forall a. Abs a -> a
unAbs Abs NLPType
b
    ]
  prettyTCM (PSort NLPSort
s)        = NLPSort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
prettyTCM NLPSort
s
  prettyTCM (PBoundVar Int
i []) = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)
  prettyTCM (PBoundVar Int
i PElims
es) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((Elim' NLPat -> m Doc) -> PElims -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM PElims
es)
  prettyTCM (PTerm Term
t)   = m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t)
{-# SPECIALIZE prettyTCM :: NLPat -> TCM Doc #-}

instance PrettyTCM NLPType where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPType -> m Doc
prettyTCM (NLPType NLPSort
s NLPat
a) = NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
a
{-# SPECIALIZE prettyTCM :: NLPType -> TCM Doc #-}

instance PrettyTCM NLPSort where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
prettyTCM = \case
    PUniv Univ
u NLPat
l -> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Univ -> String
showUniv Univ
u) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
l
      -- Andreas, 2023-05-11, preserving Jesper's printing hack for now...
    PInf Univ
u Integer
n  -> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n :: Sort)
    NLPSort
PSizeUniv -> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Sort
forall t. Sort' t
SizeUniv :: Sort)
    NLPSort
PLockUniv -> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Sort
forall t. Sort' t
LockUniv :: Sort)
    NLPSort
PLevelUniv -> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Sort
forall t. Sort' t
LevelUniv :: Sort)
    NLPSort
PIntervalUniv -> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Sort
forall t. Sort' t
IntervalUniv :: Sort)
{-# SPECIALIZE prettyTCM :: NLPSort -> TCM Doc #-}

instance PrettyTCM (Elim' NLPat) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM (IApply NLPat
x NLPat
y NLPat
v) = NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM NLPat
v
  prettyTCM (Apply Arg NLPat
v) = Arg NLPat -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Arg NLPat
v Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> m Doc -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (Arg NLPat -> NLPat
forall e. Arg e -> e
unArg Arg NLPat
v)
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
{-# SPECIALIZE prettyTCM :: Elim' NLPat -> TCM Doc #-}

instance PrettyTCM (Type' NLPat) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Type' NLPat -> m Doc
prettyTCM = NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (NLPat -> m Doc) -> (Type' NLPat -> NLPat) -> Type' NLPat -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type' NLPat -> NLPat
forall t a. Type'' t a -> a
unEl
{-# SPECIALIZE prettyTCM :: Type' NLPat -> TCM Doc #-}

instance PrettyTCM RewriteRule where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => RewriteRule -> m Doc
prettyTCM (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
b Bool
c) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
    , Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
gamma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" |- "
    , Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ NLPat -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
prettyTCM (QName -> PElims -> NLPat
PDef QName
f PElims
ps)
      , m Doc
" --> "
      , Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
rhs
      , m Doc
" : "
      , Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b
      ]
    ]
{-# SPECIALIZE prettyTCM :: RewriteRule -> TCM Doc #-}

instance PrettyTCM Occurrence where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Occurrence -> m Doc
prettyTCM Occurrence
occ  = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"-[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Occurrence -> String
forall a. Pretty a => a -> String
prettyShow Occurrence
occ String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]->"
{-# SPECIALIZE prettyTCM :: Occurrence -> TCM Doc #-}

-- | Pairing something with a node (for printing only).
data WithNode n a = WithNode n a

-- | Pretty-print something paired with a (printable) node.
-- | This intermediate typeclass exists to avoid UndecidableInstances.
class PrettyTCMWithNode a where
  prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc

instance PrettyTCMWithNode Occurrence where
  prettyTCMWithNode :: forall n (m :: * -> *).
(PrettyTCM n, MonadPretty m) =>
WithNode n Occurrence -> m Doc
prettyTCMWithNode (WithNode n
n Occurrence
o) = Occurrence -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Occurrence -> m Doc
prettyTCM Occurrence
o m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> n -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => n -> m Doc
prettyTCM n
n

instance (PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Graph n e -> m Doc
prettyTCM Graph n e
g = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((n, Map n e) -> m Doc) -> [(n, Map n e)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (n, Map n e) -> m Doc
forall {m :: * -> *} {a} {a} {n}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCMWithNode a, PrettyTCM a,
 PrettyTCM n) =>
(a, Map n a) -> m Doc
pr ([(n, Map n e)] -> [m Doc]) -> [(n, Map n e)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Map n (Map n e) -> [(n, Map n e)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Map n (Map n e) -> [(n, Map n e)])
-> Map n (Map n e) -> [(n, Map n e)]
forall a b. (a -> b) -> a -> b
$ Graph n e -> Map n (Map n e)
forall n e. Graph n e -> Map n (Map n e)
Graph.graph Graph n e
g
    where
      pr :: (a, Map n a) -> m Doc
pr (a
n, Map n a
es) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
n
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((n, a) -> m Doc) -> [(n, a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (WithNode n a -> m Doc
forall a n (m :: * -> *).
(PrettyTCMWithNode a, PrettyTCM n, MonadPretty m) =>
WithNode n a -> m Doc
forall n (m :: * -> *).
(PrettyTCM n, MonadPretty m) =>
WithNode n a -> m Doc
prettyTCMWithNode (WithNode n a -> m Doc)
-> ((n, a) -> WithNode n a) -> (n, a) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> a -> WithNode n a) -> (n, a) -> WithNode n a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry n -> a -> WithNode n a
forall n a. n -> a -> WithNode n a
WithNode) ([(n, a)] -> [m Doc]) -> [(n, a)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Map n a -> [(n, a)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map n a
es
        ]
{-# SPECIALIZE prettyTCM :: (PrettyTCM n, PrettyTCMWithNode e) => (Graph n e) -> TCM Doc #-}

instance PrettyTCM SplitTag where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitTag -> m Doc
prettyTCM (SplitCon QName
c)  = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c
  prettyTCM (SplitLit Literal
l)  = Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
l
  prettyTCM SplitTag
SplitCatchall = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Underscore a => a
underscore
{-# SPECIALIZE prettyTCM :: SplitTag -> TCM Doc #-}

instance PrettyTCM Candidate where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Candidate -> m Doc
prettyTCM Candidate
c = case Candidate -> CandidateKind
candidateKind Candidate
c of
    (GlobalCandidate QName
q) -> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
    CandidateKind
LocalCandidate      -> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> Term -> m Doc
forall a b. (a -> b) -> a -> b
$ Candidate -> Term
candidateTerm Candidate
c
{-# SPECIALIZE prettyTCM :: Candidate -> TCM Doc #-}

instance PrettyTCM Key where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Key -> m Doc
prettyTCM = \case
    RigidK QName
q Int
a -> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Int -> m Doc
forall (m :: * -> *). Applicative m => Int -> m Doc
superscript Int
a
    LocalK Int
i Int
a -> m Doc
"@" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
i m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Int -> m Doc
forall (m :: * -> *). Applicative m => Int -> m Doc
superscript Int
a
    Key
PiK        -> m Doc
"Pi"
    Key
ConstK     -> m Doc
"Const"
    Key
SortK      -> m Doc
"Sort"
    Key
FlexK      -> m Doc
"_"

{-# SPECIALIZE prettyTCM :: Key -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Set.Set a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Set a -> m Doc
prettyTCM = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces (m Doc -> m Doc) -> (Set a -> m Doc) -> Set a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ([m Doc] -> m Doc) -> (Set a -> [m Doc]) -> Set a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM ([a] -> [m Doc]) -> (Set a -> [a]) -> Set a -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

instance PrettyTCM a => PrettyTCM (DiscrimTree a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
prettyTCM = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc)
-> (DiscrimTree a -> [m Doc]) -> DiscrimTree a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Doc -> DiscrimTree a -> [m Doc]
forall {m :: * -> *} {a}.
(IsString (m Doc), PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 Null (m Doc), Semigroup (m Doc)) =>
m Doc -> DiscrimTree a -> [m Doc]
go m Doc
"  " where
    go :: m Doc -> DiscrimTree a -> [m Doc]
go m Doc
ind DiscrimTree a
EmptyDT     = [m Doc
"fail"]
    go m Doc
ind (DoneDT Set a
it) = [m Doc
"done" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Set a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set a -> m Doc
prettyTCM Set a
it]
    go m Doc
ind (CaseDT Int
var Map Key (DiscrimTree a)
branches DiscrimTree a
fallthrough) =
      [m Doc
"case" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
var m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"of"]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ ((Key, DiscrimTree a) -> [m Doc])
-> [(Key, DiscrimTree a)] -> [m Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Key
k, DiscrimTree a
v) -> m Doc -> m Doc -> DiscrimTree a -> [m Doc]
abduct m Doc
ind (Key -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Key -> m Doc
prettyTCM Key
k m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
" →") DiscrimTree a
v) (Map Key (DiscrimTree a) -> [(Key, DiscrimTree a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Key (DiscrimTree a)
branches)
      [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (DiscrimTree a -> Bool
forall a. Null a => a -> Bool
null DiscrimTree a
fallthrough)) [()] -> [m Doc] -> [m Doc]
forall a b. [a] -> [b] -> [b]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m Doc -> m Doc -> DiscrimTree a -> [m Doc]
abduct m Doc
ind (m Doc
"* →") DiscrimTree a
fallthrough)

    abduct :: m Doc -> m Doc -> DiscrimTree a -> [m Doc]
abduct m Doc
ind m Doc
f DiscrimTree a
v | (m Doc
l:[m Doc]
ls) <- m Doc -> DiscrimTree a -> [m Doc]
go m Doc
ind DiscrimTree a
v = ((m Doc
ind m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
f) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
l)m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:(m Doc -> m Doc) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (m Doc
ind m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<>) [m Doc]
ls
    abduct m Doc
ind m Doc
_ DiscrimTree a
_ = [m Doc]
forall a. HasCallStack => a
__IMPOSSIBLE__