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 Control.Monad.Reader (ReaderT)
import Control.Monad.State  (StateT)

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)
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.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.Permutation (Permutation)
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P

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  = forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.comma
colon :: forall (m :: * -> *). Applicative m => m Doc
colon  = forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.colon
equals :: forall (m :: * -> *). Applicative m => m Doc
equals = forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
P.equals

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

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 = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
AP.prettyA a
x

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 = forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
AP.prettyAs a
x

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

multiLineText :: Applicative m => String -> m Doc
multiLineText :: forall (m :: * -> *). Applicative m => String -> m Doc
multiLineText String
s = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 = forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String -> Doc
P.fwords String
s

sep, fsep, hsep, hcat, vcat :: (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  = forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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 = forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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 = forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hsep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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 = forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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 = forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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
P.hang forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n 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
(P.$$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 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.$+$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 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.<+>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 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.<?>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Doc
d1 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
P.nest Int
n 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 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 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 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 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 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   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         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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. Pretty a => a -> Doc
P.pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (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 = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma t (m Doc)
ds

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

---------------------------------------------------------------------------
-- * 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 <> :: TCM Doc -> TCM Doc -> TCM Doc
(<>) = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 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 = forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence Precedence
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM

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

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

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

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

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

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) = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Applicative m => m Doc
comma forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM b
b forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Applicative m => m Doc
comma forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM c
c

instance PrettyTCM Term               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM Type               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM Sort               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM DisplayTerm        where prettyTCM :: forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM NamedClause        where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (QNamed Clause)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM Level              where prettyTCM :: forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify 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 = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (Arg Term)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (Arg Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (Arg Bool)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (Arg A.Expr)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Expr -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (NamedArg A.Expr)  where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (NamedArg Term)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Term -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM (Dom Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance PrettyTCM ContextEntry       where prettyTCM :: forall (m :: * -> *). MonadPretty m => ContextEntry -> m Doc
prettyTCM = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify

instance PrettyTCM Permutation where prettyTCM :: forall (m :: * -> *). MonadPretty m => Permutation -> m Doc
prettyTCM = forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance PrettyTCM Polarity    where prettyTCM :: forall (m :: * -> *). MonadPretty m => Polarity -> m Doc
prettyTCM = forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance PrettyTCM IsForced    where prettyTCM :: forall (m :: * -> *). MonadPretty m => IsForced -> m Doc
prettyTCM = forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

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 = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => m Doc
comma forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution' a
rho1
    where
      (Substitution' a
rho1, Substitution' a
rho2) = forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS Int
1 Substitution' a
rho
      u :: a
u            = 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_ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"<unnamedclause>" :: String)
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. QName -> a -> QNamed a
QNamed QName
x Clause
cl)

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

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

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

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

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" forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Functor m => m Doc -> m Doc
braces (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma
    [ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM k
k forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=") Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM v
v) | (k
k, v
v) <- forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m ])

-- 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$" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  prettyTCM (Apply Arg Term
v) = m Doc
"$" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Term
v
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

newtype PrettyContext = PrettyContext Context

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

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

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)    = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x
  prettyTCM (VarP PatternInfo
_ a
x)    = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x
  prettyTCM (DotP PatternInfo
_ Term
t)    = m Doc
".(" forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t forall a. Semigroup a => a -> a -> a
<> m Doc
")"
  prettyTCM (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps) = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 $
        forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) forall a. Eq a => a -> a -> Bool
/= PatOrigin
PatOCon
        showRec :: m Doc -- Defined, but currently not used
        showRec :: m Doc
showRec = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ m Doc
"record"
          , forall (t :: * -> *). Foldable t => t Doc -> Doc
bracesAndSemicolons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 =
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Name
A.qnameName QName
x) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=" , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p ]
        showCon :: m Doc -- NB:: Defined but not used
        showCon :: m Doc
showCon = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ m Doc -> m Doc
prTy forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
        prTy :: m Doc -> m Doc
prTy m Doc
d = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i) m Doc
d forall a b. (a -> b) -> a -> b
$ \ Arg Type
t -> m Doc
d  forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
t
  prettyTCM (LitP PatternInfo
_ Literal
l)    = forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Pretty a => a -> String
P.prettyShow Literal
l)
  prettyTCM (ProjP ProjOrigin
_ QName
q)   = forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"." forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
P.prettyShow QName
q)

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

prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList :: forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< 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
"$" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DisplayTerm
v
  prettyTCM (Apply Arg DisplayTerm
v) = m Doc
"$" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg DisplayTerm
v)
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f

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

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

instance PrettyTCM NLPSort where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
prettyTCM = \case
    PType NLPat
l   -> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ m Doc
"Set" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
l
    PProp NLPat
l   -> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ m Doc
"Prop" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
l
    PSSet NLPat
l   -> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ m Doc
"SSet" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
l
    PInf IsFibrant
f Integer
n  -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n :: Sort)
    NLPSort
PSizeUniv -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. Sort' t
SizeUniv :: Sort)
    NLPSort
PLockUniv -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. Sort' t
LockUniv :: Sort)
    NLPSort
PIntervalUniv -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. Sort' t
IntervalUniv :: Sort)

instance PrettyTCM (Elim' NLPat) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
prettyTCM (IApply NLPat
x NLPat
y NLPat
v) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NLPat
v
  prettyTCM (Apply Arg NLPat
v) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg NLPat
v)
  prettyTCM (Proj ProjOrigin
_ QName
f)= m Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f

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

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) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
" |- "
    , forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> PElims -> NLPat
PDef QName
f PElims
ps)
      , m Doc
" --> "
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs
      , m Doc
" : "
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
      ]
    ]

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

-- | 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) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Occurrence
o forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.assocs forall a b. (a -> b) -> a -> b
$ 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) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
n
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a n (m :: * -> *).
(PrettyTCMWithNode a, PrettyTCM n, MonadPretty m) =>
WithNode n a -> m Doc
prettyTCMWithNode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall n a. n -> a -> WithNode n a
WithNode) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.assocs Map n a
es
        ]

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

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) -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
    CandidateKind
LocalCandidate      -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Candidate -> Term
candidateTerm Candidate
c