    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.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Substitute

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

    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

    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

    text :: Applicative m => String -> m Doc
    text :: forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    s = Doc -> m Doc
    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.text String
    s

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

    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 (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 (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList t (m Doc)
    ts
        n :: Int
    n  = [m Doc] -> 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

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

    type MonadPretty m =
      ( MonadReify m
      , MonadAbsToCon m
      , IsString (m Doc)
      , Null (m Doc)
      , Semigroup (m Doc)
      )

    -- 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
    (<>) = (Doc -> Doc -> Doc) -> TCM Doc -> TCM Doc -> TCM Doc
    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
    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 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

    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 :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure a
    cl a -> m Doc
    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 = [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
    prettyTCM

    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
    prettyTCM

    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
    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
    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) = 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
    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
    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
    prettyTCM c
    c

    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
    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 = 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
    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 = 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
    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 = 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
    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 = 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
    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 = 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
    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 = 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
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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)
    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 = 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)
    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 = 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)
    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 = 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)
    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 = 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)
    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 = 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)
    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 = 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)
    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 = 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)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify
    instance PrettyTCM (Dom (Name, Type)) where prettyTCM :: forall (m :: * -> *). MonadPretty m => Dom (Name, Type) -> 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)
    -> (Dom (Name, Type) -> m (Arg (Name, Expr)))
    -> Dom (Name, Type)
    -> m Doc
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Dom (Name, Type) -> m (Arg (Name, Expr))
    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 = 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

    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
    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
    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
    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
    freshName_ (String
    "<unnamedclause>" :: String)
        QNamed Clause -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> Clause -> QNamed Clause
    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) = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, 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
    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
    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
    prettyTCM Type
    t

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

    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
    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
    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" 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
    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
    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 ])

    -- 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
    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
    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
    prettyTCM QName
    f

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

    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
    prettyTCM (Type -> m Doc) -> Type -> m Doc
    forall a b. (a -> b) -> a -> b
    $ EqualityView -> Type
    equalityUnview EqualityView
    v

    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

    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

    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

    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

    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
    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
    prettyTCM (Modality -> Relevance
    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" 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
    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
    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
    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

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

    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
    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
    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
    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
    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 (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) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length List1 (WithHiding Name)
    xs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    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
    prettyTCM (List1 (WithHiding Name) -> [WithHiding Name]
    forall a. NonEmpty a -> [a]
    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
    prettyTCM Type
    a])) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              Doc -> m Doc
    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
    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
    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)
    reify Term
    v
        Expr -> m Doc
    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) (Expr -> NamedArg Expr
    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) = 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
    prettyTCM a
    a

    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

    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

    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

    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
    prettyTCM (QName -> m Doc)
    -> (AbstractName -> QName) -> AbstractName -> m Doc
    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 = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> m Doc) -> (ConHead -> QName) -> ConHead -> m Doc
    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 = [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)
    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 a b.
    ToConcrete a =>
    a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
    bindToConcrete Telescope
    tel ConOfAbs Telescope -> AbsToCon [Maybe TypedBinding]
    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) = Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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

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

    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
    prettyTCM a
    x
      prettyTCM (VarP PatternInfo
    _ a
    x)    = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, 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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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)

    -- | 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)
    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

    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
    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
    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
    prettyTCM QName
    f

    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
    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 (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
    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
    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
    $
        String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String
    "λ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Abs NLPat -> String
    forall a. Abs a -> String
    absName Abs NLPat
    u String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " →") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        String -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs NLPat -> String
    forall a. Abs a -> String
    absName Abs NLPat
    u) (NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    $
        String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Abs NLPType -> String
    forall a. Abs a -> String
    absName Abs NLPType
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " :") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (NLPType -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Dom NLPType -> NLPType
    forall t e. Dom' t e -> e
    unDom Dom NLPType
    a) m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ") →") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        String -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs NLPType -> String
    forall a. Abs a -> String
    absName Abs NLPType
    b) (NLPType -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM NLPSort
    s
      prettyTCM (PBoundVar Int
    i []) = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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
    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
    prettyTCM Term
    t)

    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
    prettyTCM NLPat
    a

    instance PrettyTCM NLPSort where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NLPSort -> m Doc
    prettyTCM = \case
        PType 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
    $ m Doc
    "Set" 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
    prettyTCM NLPat
    l
        PProp 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
    $ m Doc
    "Prop" 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
    prettyTCM NLPat
    l
        PInf IsFibrant
    f Integer
    n  -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    n :: Sort)
        NLPSort
    PSizeUniv -> Sort -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM (Sort
    forall t. Sort' t
    LockUniv :: Sort)

    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
    prettyTCM NLPat
    v
      prettyTCM (Apply Arg NLPat
    v) = NLPat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM QName
    f

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

    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
    prettyTCM QName
    q
        , Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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
    prettyTCM (QName -> PElims -> NLPat
    PDef QName
    f PElims
    ps)
          , m Doc
    " --> "
          , Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    rhs
          , m Doc
    " : "
          , Type -> 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  = 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
    "]->"

    -- | 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
    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
    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}.
    (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames 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
    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
    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
            ]

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