-- Each function here should either have an INLINE or a SPECIALIZE pragma.
--
module Mikan.TypeChecking.Pretty
    ( module Mikan.TypeChecking.Pretty
    , module Reexport
    ) where

import Prelude hiding ( null )

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

import Data.Foldable qualified as Fold
import Data.Map (Map)
import Data.IntMap qualified as IntMap
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Maybe
import Data.String    ()
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS
import Data.Functor

import Mikan.Syntax.Position
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty ( Pretty, prettyShow )
import Mikan.Syntax.Common.Aspect qualified as Asp
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Fixity
import Mikan.Syntax.Internal
import Mikan.Syntax.Literal
import Mikan.Syntax.Translation.InternalToAbstract
import Mikan.Syntax.Translation.ReflectedToAbstract
import Mikan.Syntax.Translation.AbstractToConcrete
import Mikan.Syntax.Translation.AbstractToConcrete qualified as Reexport (MonadAbsToCon)
import Mikan.Syntax.Translation.ReflectedToAbstract qualified as R
import Mikan.Syntax.Abstract.Name (AbstractName (..), AbstractModule (..), KindOfName(..))
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Abstract.Pretty qualified as AP
import Mikan.Syntax.Concrete.Pretty (bracesAndSemicolons)
import Mikan.Syntax.Concrete.Pretty qualified as CP
import Mikan.Syntax.Info qualified as A
import Mikan.Syntax.Scope.Monad (withContextPrecedence)
import Mikan.Syntax.TopLevelModuleName

import Mikan.TypeChecking.Coverage.SplitTree
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Positivity.Occurrence
import Mikan.TypeChecking.DiscrimTree.Types
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Free.Base
import Mikan.TypeChecking.Free.Generic

import Mikan.Utils.BiMap qualified as BiMap
import Mikan.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
import Mikan.Utils.Graph.AdjacencyMap.Unidirectional qualified as Graph
import Mikan.Utils.List1 ( List1, pattern (:|) )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.VarSet qualified as VS
import Mikan.Utils.Maybe
import Mikan.Utils.Null
import Mikan.Utils.Trie
import Mikan.Utils.Permutation ( Permutation )
import Mikan.Utils.Maybe.Strict qualified as S
import Mikan.Utils.Size ( Sized, natSize, size )

import Mikan.Utils.Impossible

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

type Doc = P.Doc

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

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

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

{-# INLINE prettyAs #-}
-- Triggers error: [GHC-69441] RULE left-hand side too complicated to desugar: ...
-- {-# SPECIALIZE prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], P.Pretty ce) => a -> TCM Doc #-}
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 -> m Doc
forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
AP.prettyAs

fwords, text, multiLineText, url :: Applicative m => String -> m Doc
fwords :: forall (m :: * -> *). Applicative m => String -> m Doc
fwords        = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
P.fwords        ; {-# INLINE fwords        #-}
text :: forall (m :: * -> *). Applicative m => String -> m Doc
text          = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
forall a. String -> Doc a
P.text          ; {-# INLINE text          #-}
multiLineText :: forall (m :: * -> *). Applicative m => String -> m Doc
multiLineText = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
P.multiLineText ; {-# INLINE multiLineText #-}
url :: forall (m :: * -> *). Applicative m => String -> m Doc
url           = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (String -> Doc) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
P.url           ; {-# INLINE url           #-}

{-# INLINE pwords #-}
pwords :: Applicative m => String -> [m Doc]
pwords :: forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords = (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Doc] -> [m Doc]) -> (String -> [Doc]) -> String -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc]
P.pwords

-- | Link to an issue on the Agda bug tracker.
{-# INLINE githubIssue #-}
githubIssue :: Applicative m => Int -> m Doc
githubIssue :: forall (m :: * -> *). Applicative m => Int -> m Doc
githubIssue = Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> m Doc) -> (Int -> Doc) -> Int -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc
P.githubIssue

sep, fsep, hsep, hcat, vcat, vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
sep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep  = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep  (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE sep  :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE sep  :: List1 (TCM Doc) -> TCM Doc #-}
fsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE fsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE fsep :: List1 (TCM Doc) -> TCM Doc #-}
hsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE hsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE hsep :: List1 (TCM Doc) -> TCM Doc #-}
hcat :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.hcat (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE hcat :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE hcat :: List1 (TCM Doc) -> TCM Doc #-}
vcat :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE vcat :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE vcat :: List1 (TCM Doc) -> TCM Doc #-}
vsep :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vsep = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
P.vsep (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable  ; {-# SPECIALIZE NOINLINE vsep :: [TCM Doc] -> TCM Doc #-} ; {-# SPECIALIZE NOINLINE vsep :: List1 (TCM Doc) -> TCM Doc #-}

{-# INLINE sequenceAFoldable #-}
-- | @sequenceAFoldable == sequenceA . Fold.toList@
sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
sequenceAFoldable :: forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable = (m a -> m [a] -> m [a]) -> m [a] -> t (m a) -> m [a]
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Fold.foldr ((a -> [a] -> [a]) -> m a -> m [a] -> m [a]
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (:)) ([a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])

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

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

($$), ($+$), (<+>), (<?>) :: Applicative m => m Doc -> m Doc -> m Doc
($$ ) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.$$)   ; {-# INLINE ($$)  #-}
$+$ :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($+$) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.$+$)  ; {-# INLINE ($+$) #-}
<+> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
(<+>) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
(P.<+>)  ; {-# INLINE (<+>) #-}
<?> :: forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
(<?>) = (Doc -> Doc -> Doc) -> m Doc -> m Doc -> m Doc
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Doc -> Doc -> Doc
(P.<?>)  ; {-# INLINE (<?>) #-}

nest :: Functor m => Int -> m Doc -> m Doc
nest :: forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc -> Doc) -> m Doc -> m Doc)
-> (Int -> Doc -> Doc) -> Int -> m Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest    ; {-# INLINE nest  #-}

braces, dbraces, brackets, parens, parensNonEmpty
  , doubleQuotes, quotes :: Functor m => m Doc -> m Doc
braces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
braces         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.braces         ; {-# INLINE braces         #-}
dbraces :: forall (m :: * -> *). Functor m => m Doc -> m Doc
dbraces        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
CP.dbraces       ; {-# INLINE dbraces        #-}
brackets :: forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets       = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.brackets       ; {-# INLINE brackets       #-}
parens :: forall (m :: * -> *). Functor m => m Doc -> m Doc
parens         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.parens         ; {-# INLINE parens         #-}
parensNonEmpty :: forall (m :: * -> *). Functor m => m Doc -> m Doc
parensNonEmpty = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.parensNonEmpty ; {-# INLINE parensNonEmpty #-}
doubleQuotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
doubleQuotes   = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.doubleQuotes   ; {-# INLINE doubleQuotes   #-}
quotes :: forall (m :: * -> *). Functor m => m Doc -> m Doc
quotes         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.quotes         ; {-# INLINE quotes         #-}

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

pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS :: forall (m :: * -> *) a. (Functor m, Sized a) => a -> m Doc -> m Doc
pluralS = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc -> Doc) -> m Doc -> m Doc)
-> (a -> Doc -> Doc) -> a -> m Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc -> Doc
forall a. Sized a => a -> Doc -> Doc
P.pluralS             ; {-# INLINE pluralS        #-}

-- | Comma-separated list in brackets.
{-# INLINE prettyList #-}
prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
prettyList :: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList = ([Doc] -> Doc) -> m [Doc] -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall a. Pretty a => a -> Doc
P.pretty (m [Doc] -> m Doc) -> (t (m Doc) -> m [Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (m Doc) -> m [Doc]
forall (m :: * -> *) (t :: * -> *) a.
(Applicative m, Foldable t) =>
t (m a) -> m [a]
sequenceAFoldable

-- | 'prettyList' without the brackets.
{-# SPECIALIZE prettyList_ :: [TCM Doc]       -> TCM Doc #-}
{-# SPECIALIZE prettyList_ :: List1 (TCM Doc) -> TCM Doc #-}
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_ = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> (t (m Doc) -> [m Doc]) -> t (m Doc) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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

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

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

hlBound, hlGeneralizable, hlDatatype, hlField,
  hlFunction, hlModule, hlPostulate, hlPrimitive, hlRecord, hlArgument,
  hlMacro :: Functor m => m Doc -> m Doc

hlBound :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlBound         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlBound
hlGeneralizable :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlGeneralizable = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlGeneralizable
hlDatatype :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlDatatype      = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlDatatype
hlField :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlField         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlField
hlFunction :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlFunction      = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlFunction
hlModule :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlModule        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlModule
hlPostulate :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlPostulate     = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlPostulate
hlPrimitive :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlPrimitive     = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlPrimitive
hlRecord :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlRecord        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlRecord
hlArgument :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlArgument      = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlArgument
hlMacro :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlMacro         = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlMacro

hlComment, hlSymbol, hlKeyword, hlString, hlNumber, hlHole, hlPrimitiveType, hlPragma
  :: Functor m => m Doc -> m Doc

hlComment :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlComment       = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlComment
hlSymbol :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlSymbol        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlSymbol
hlKeyword :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword       = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlKeyword
hlString :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlString        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlString
hlNumber :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlNumber        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlNumber
hlHole :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlHole          = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlHole
hlPrimitiveType :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlPrimitiveType = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlPrimitiveType
hlPragma :: forall (m :: * -> *). Functor m => m Doc -> m Doc
hlPragma        = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> Doc
P.hlPragma

hlConstructor :: Functor m => Induction -> m Doc -> m Doc
hlConstructor :: forall (m :: * -> *). Functor m => Induction -> m Doc -> m Doc
hlConstructor = (Doc -> Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc -> Doc) -> m Doc -> m Doc)
-> (Induction -> Doc -> Doc) -> Induction -> m Doc -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Induction -> Doc -> Doc
P.hlConstructor

{-# SPECIALISE hlBound         :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlGeneralizable :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlDatatype      :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlField         :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlFunction      :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlModule        :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlPostulate     :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlPrimitive     :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlRecord        :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlArgument      :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlMacro         :: TCM Doc -> TCM Doc #-}
{-# SPECIALISE hlConstructor   :: Induction -> TCM Doc -> TCM Doc #-}

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

type MonadPretty m = MonadAbsToCon m

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

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

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

instance {-# OVERLAPPING #-} PrettyTCM String where prettyTCM :: forall (m :: * -> *). MonadPretty m => String -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text   ; {-# INLINE prettyTCM #-}
instance PrettyTCM ShortText                  where prettyTCM :: forall (m :: * -> *). MonadPretty m => ShortText -> m Doc
prettyTCM = ShortText -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
instance PrettyTCM C.ImportedName             where prettyTCM :: forall (m :: * -> *). MonadPretty m => ImportedName -> m Doc
prettyTCM = ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}
instance PrettyTCM C.LHS                      where prettyTCM :: forall (m :: * -> *). MonadPretty m => LHS -> m Doc
prettyTCM = LHS -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}
instance PrettyTCM TopLevelModuleName         where prettyTCM :: forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM = TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
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 ; {-# INLINE prettyTCM #-}
instance PrettyTCM InteractionId              where prettyTCM :: forall (m :: * -> *). MonadPretty m => InteractionId -> m Doc
prettyTCM = InteractionId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}
instance PrettyTCM MetaSet                    where prettyTCM :: forall (m :: * -> *). MonadPretty m => MetaSet -> m Doc
prettyTCM = MetaSet -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ; {-# INLINE prettyTCM #-}

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

instance PrettyTCM Term               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Term -> m Expr) -> Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify         ; {-# SPECIALIZE prettyTCM :: Term               -> TCM Doc #-}
instance PrettyTCM Teletype           where prettyTCM :: forall (m :: * -> *). MonadPretty m => Teletype -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Teletype -> m Expr) -> Teletype -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Teletype -> m Expr
Teletype -> m (ReifiesTo Teletype)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Teletype -> m (ReifiesTo Teletype)
reify         ; {-# SPECIALIZE prettyTCM :: Teletype           -> TCM Doc #-}
instance PrettyTCM Type               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Type -> m Expr) -> Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify         ; {-# SPECIALIZE prettyTCM :: Type               -> TCM Doc #-}
instance PrettyTCM Sort               where prettyTCM :: forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Sort -> m Expr) -> Sort -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Sort -> m Expr
Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify         ; {-# SPECIALIZE prettyTCM :: Sort               -> TCM Doc #-}
instance PrettyTCM DisplayTerm        where prettyTCM :: forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (DisplayTerm -> m Expr) -> DisplayTerm -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< DisplayTerm -> m Expr
DisplayTerm -> m (ReifiesTo DisplayTerm)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify         ; {-# SPECIALIZE prettyTCM :: DisplayTerm        -> TCM Doc #-}
instance PrettyTCM NamedClause        where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM = Clause -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (NamedClause -> m Clause) -> NamedClause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedClause -> m Clause
NamedClause -> m (ReifiesTo NamedClause)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify         ; {-# SPECIALIZE prettyTCM :: NamedClause        -> TCM Doc #-}
instance PrettyTCM (QNamed Clause)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM = Clause -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (QNamed Clause -> m Clause) -> QNamed Clause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< QNamed Clause -> m Clause
QNamed Clause -> m (ReifiesTo (QNamed Clause))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify         ; {-# SPECIALIZE prettyTCM :: (QNamed Clause)    -> TCM Doc #-}
instance PrettyTCM Level              where prettyTCM :: forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM = Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Level -> m Expr) -> Level -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> m Expr) -> (Level -> Term) -> Level -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level -> Term
Level ; {-# SPECIALIZE prettyTCM :: Level              -> TCM Doc #-}
instance PrettyTCM (Named_ Term)      where prettyTCM :: forall (m :: * -> *). MonadPretty m => Named_ Term -> m Doc
prettyTCM = Named (WithOrigin (Ranged ShortText)) Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Named (WithOrigin (Ranged ShortText)) Expr -> m Doc)
-> (Named_ Term -> m (Named (WithOrigin (Ranged ShortText)) 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 ShortText)) Expr)
Named_ Term -> m (ReifiesTo (Named_ Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Named_ Term -> m (ReifiesTo (Named_ Term))
reify         ; {-# SPECIALIZE prettyTCM :: (Named_ Term)      -> TCM Doc #-}
instance PrettyTCM (Arg Term)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Term -> m (Arg Expr)) -> Arg Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Term -> m (Arg Expr)
Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify         ; {-# SPECIALIZE prettyTCM :: (Arg Term)         -> TCM Doc #-}
instance PrettyTCM (Arg Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Type -> m (Arg Expr)) -> Arg Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Type -> m (Arg Expr)
Arg Type -> m (ReifiesTo (Arg Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Type -> m (ReifiesTo (Arg Type))
reify         ; {-# SPECIALIZE prettyTCM :: (Arg Type)         -> TCM Doc #-}
instance PrettyTCM (Arg Bool)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
prettyTCM = Arg Bool -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Bool -> m Doc)
-> (Arg Bool -> m (Arg Bool)) -> Arg Bool -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Bool -> m (Arg Bool)
Arg Bool -> m (ReifiesTo (Arg Bool))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Bool -> m (ReifiesTo (Arg Bool))
reify         ; {-# SPECIALIZE prettyTCM :: (Arg Bool)         -> TCM Doc #-}
instance PrettyTCM (Arg ShortText)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg ShortText -> m Doc
prettyTCM = Arg ShortText -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg ShortText -> m Doc)
-> (Arg ShortText -> m (Arg ShortText)) -> Arg ShortText -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg ShortText -> m (Arg ShortText)
Arg ShortText -> m (ReifiesTo (Arg ShortText))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg ShortText -> m (ReifiesTo (Arg ShortText))
reify         ; {-# SPECIALIZE prettyTCM :: (Arg ShortText)    -> TCM Doc #-}
instance PrettyTCM (Arg A.Expr)       where prettyTCM :: forall (m :: * -> *). MonadPretty m => Arg Expr -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Arg Expr -> m (Arg Expr)
Arg Expr -> m (ReifiesTo (Arg Expr))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Expr -> m (ReifiesTo (Arg Expr))
reify         ; {-# SPECIALIZE prettyTCM :: (Arg A.Expr)       -> TCM Doc #-}
instance PrettyTCM (NamedArg A.Expr)  where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM = NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (NamedArg Expr -> m Doc)
-> (NamedArg Expr -> m (NamedArg Expr)) -> NamedArg Expr -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedArg Expr -> m (NamedArg Expr)
NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedArg Expr -> m (ReifiesTo (NamedArg Expr))
reify         ; {-# SPECIALIZE prettyTCM :: (NamedArg A.Expr)  -> TCM Doc #-}
instance PrettyTCM (NamedArg Term)    where prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedArg Term -> m Doc
prettyTCM = NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (NamedArg Expr -> m Doc)
-> (NamedArg Term -> m (NamedArg Expr)) -> NamedArg Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedArg Term -> m (NamedArg Expr)
NamedArg Term -> m (ReifiesTo (NamedArg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedArg Term -> m (ReifiesTo (NamedArg Term))
reify         ; {-# SPECIALIZE prettyTCM :: (NamedArg Term)    -> TCM Doc #-}
instance PrettyTCM (Dom Type)         where prettyTCM :: forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM = Arg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> m Doc)
-> (Dom Type -> m (Arg Expr)) -> Dom Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Dom Type -> m (Arg Expr)
Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom Type -> m (ReifiesTo (Dom Type))
reify         ; {-# SPECIALIZE prettyTCM :: (Dom Type)         -> TCM Doc #-}
instance PrettyTCM Context            where prettyTCM :: forall (m :: * -> *). MonadPretty m => Context -> m Doc
prettyTCM = [TypedBinding] -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ([TypedBinding] -> m Doc)
-> (Context -> m [TypedBinding]) -> Context -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Context -> m [TypedBinding]
Context -> m (ReifiesTo Context)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Context -> m (ReifiesTo Context)
reify         ; {-# SPECIALISE prettyTCM :: Context            -> TCM Doc #-}
instance PrettyTCM ContextEntry       where prettyTCM :: forall (m :: * -> *). MonadPretty m => ContextEntry -> m Doc
prettyTCM = TypedBinding -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (TypedBinding -> m Doc)
-> (ContextEntry -> m TypedBinding) -> ContextEntry -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ContextEntry -> m TypedBinding
ContextEntry -> m (ReifiesTo ContextEntry)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ContextEntry -> m (ReifiesTo ContextEntry)
reify         ; {-# SPECIALIZE prettyTCM :: ContextEntry       -> TCM Doc #-}

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               ; {-# SPECIALIZE prettyTCM :: Permutation       -> TCM Doc #-}
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               ; {-# SPECIALIZE prettyTCM :: Polarity          -> TCM Doc #-}
instance PrettyTCM IsForced           where prettyTCM :: forall (m :: * -> *). MonadPretty m => IsForced -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> (IsForced -> String) -> IsForced -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsForced -> String
forall a. Show a => a -> String
show               ; {-# SPECIALIZE prettyTCM :: IsForced          -> TCM Doc #-}

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

instance PrettyTCM AbstractName where prettyTCM :: forall (m :: * -> *). MonadPretty m => AbstractName -> m Doc
prettyTCM = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc)
-> (AbstractName -> QName) -> AbstractName -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName           ; {-# SPECIALIZE prettyTCM :: AbstractName -> TCM Doc #-}
instance PrettyTCM ConHead      where prettyTCM :: forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> (ConHead -> QName) -> ConHead -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName             ; {-# SPECIALIZE prettyTCM :: ConHead      -> TCM Doc #-}
instance PrettyTCM DBPatVar     where prettyTCM :: forall (m :: * -> *). MonadPretty m => DBPatVar -> m Doc
prettyTCM = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (DBPatVar -> Term) -> DBPatVar -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var (Int -> Term) -> (DBPatVar -> Int) -> DBPatVar -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBPatVar -> Int
dbPatVarIndex ; {-# SPECIALIZE prettyTCM :: DBPatVar     -> TCM Doc #-}
instance PrettyTCM EqualityView where prettyTCM :: forall (m :: * -> *). MonadPretty m => EqualityView -> m Doc
prettyTCM = Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> (EqualityView -> Type) -> EqualityView -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqualityView -> Type
forall a. EqualityUnview a => a -> Type
equalityUnview      ; {-# SPECIALIZE prettyTCM :: EqualityView -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (VarOcc' a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => VarOcc' a -> m Doc
prettyTCM (VarOcc FlexRig' a
a) = FlexRig' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => FlexRig' a -> m Doc
prettyTCM FlexRig' a
a
  {-# SPECIALIZE prettyTCM :: PrettyTCM a => VarOcc' a -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (FlexRig' a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => FlexRig' a -> m Doc
prettyTCM = \case
    Flexible a
a    -> m Doc
"FL" 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 (a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a)
    FlexRig' a
WeaklyRigid   -> m Doc
"WR"
    FlexRig' a
StronglyRigid -> m Doc
"SR"
    FlexRig' a
Unguarded     -> m Doc
forall a. Null a => a
empty
  {-# SPECIALIZE prettyTCM :: PrettyTCM a => FlexRig' a -> TCM Doc #-}

instance PrettyTCM ModuleName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
x =
    let
      def :: Doc -> Doc
def = case ModuleName -> [Name]
mnameToList ModuleName
x of
        [] -> Doc -> Doc
forall a. a -> a
id
        [Name]
xs -> (Doc -> Range -> Doc) -> Range -> Doc -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Doc -> Range -> Doc
forall a. HasRange a => Doc -> a -> Doc
P.definedAt (Name -> Range
forall a. HasNameBindingSite a => a -> Range
nameBindingSite ([Name] -> Name
forall a. HasCallStack => [a] -> a
last [Name]
xs))
    in (QName -> Doc) -> m QName -> m Doc
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc -> Doc
P.hlModule (Doc -> Doc) -> (QName -> Doc) -> QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
def (Doc -> Doc) -> (QName -> Doc) -> QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty) (m QName -> m Doc) -> m QName -> m Doc
forall a b. (a -> b) -> a -> b
$ ModuleName -> m (ConOfAbs ModuleName)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ ModuleName
x

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

-- | Automatically highlights the resulting document with the correct
-- name kind.
instance PrettyTCM QName where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x = do
    nk <- QName -> m (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x m (Either SigError Definition)
-> (Either SigError Definition -> Maybe NameKind)
-> m (Maybe NameKind)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Left  SigError
_ -> Maybe NameKind
forall a. Maybe a
Nothing
      Right Definition
d -> NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just (Defn -> NameKind
defnToNameKind (Definition -> Defn
theDef Definition
d))
    fmap (flip P.definedAt (nameBindingSite x) . maybe id P.hlNameKind nk . P.pretty) (abstractToConcrete_ x)

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

defnToNameKind :: Defn -> Asp.NameKind
defnToNameKind :: Defn -> NameKind
defnToNameKind   Axiom{}                      = NameKind
Asp.Postulate
defnToNameKind   DataOrRecSig{}               = NameKind
Asp.Postulate
  -- TODO: ^ maybe break down into Data/Record?
defnToNameKind   GeneralizableVar{}           = NameKind
Asp.Generalizable
defnToNameKind d :: Defn
d@Function{}
  | Defn -> Bool
isProperProjection Defn
d                      = NameKind
Asp.Field
  | Defn -> Bool
isMacro Defn
d                                 = NameKind
Asp.Macro          -- AIM XL, issue #7324
  | Bool
otherwise                                 = NameKind
Asp.Function
defnToNameKind   Datatype{}                   = NameKind
Asp.Datatype
defnToNameKind   Record{}                     = NameKind
Asp.Record
defnToNameKind   Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c } = Induction -> NameKind
Asp.Constructor (Induction -> NameKind) -> Induction -> NameKind
forall a b. (a -> b) -> a -> b
$ ConHead -> Induction
conInductive ConHead
c
defnToNameKind   Primitive{}                  = NameKind
Asp.Primitive
defnToNameKind   PrimitiveSort{}              = NameKind
Asp.Primitive
defnToNameKind   AbstractDefn{}               = NameKind
Asp.Function

-- Functors

instance (PrettyTCM a, Subst a) => PrettyTCM (Abs a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Abs a -> m Doc
prettyTCM Abs a
a = Abs a -> (a -> m Doc) -> m Doc
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
a a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM
{-# SPECIALIZE prettyTCM :: PrettyTCM a => Abs a -> TCM Doc #-}

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

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, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([m Doc] -> m Doc) -> ([a] -> [m Doc]) -> [a] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM
{-# SPECIALIZE prettyTCM :: PrettyTCM a => [a] -> TCM Doc #-}

instance {-# OVERLAPPABLE #-} PrettyTCM a => PrettyTCM (List1 a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => List1 a -> m Doc
prettyTCM = NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList (NonEmpty (m Doc) -> m Doc)
-> (List1 a -> NonEmpty (m Doc)) -> List1 a -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Doc) -> List1 a -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM
{-# SPECIALIZE prettyTCM :: PrettyTCM a => [a] -> TCM Doc #-}

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

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

instance PrettyTCM VS.VarSet where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => VarSet -> m Doc
prettyTCM = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces (m Doc -> m Doc) -> (VarSet -> m Doc) -> VarSet -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ([m Doc] -> m Doc) -> (VarSet -> [m Doc]) -> VarSet -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> m Doc) -> [Int] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (Int -> Term) -> Int -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) ([Int] -> [m Doc]) -> (VarSet -> [Int]) -> VarSet -> [m Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarSet -> [Int]
VS.toAscList
{-# SPECIALIZE prettyTCM :: VS.VarSet -> TCM Doc #-}

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

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

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

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

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

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

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

instance PrettyTCM NamedMeta where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => NamedMeta -> m Doc
prettyTCM (NamedMeta ShortText
s MetaId
m) = do
    current <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
    prefix  <-
      if metaModule m == current
      then return empty
      else do
        modName <- BiMap.invLookup (metaModule m) <$>
                   useR stTopLevelModuleNames
        return $ case modName of
          Maybe RawTopLevelModuleName
Nothing      -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
          Just RawTopLevelModuleName
modName -> RawTopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty RawTopLevelModuleName
modName m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"."
    let inBetween = case ShortText
s of
          ShortText
""  -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
          ShortText
"_" -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
          ShortText
s   -> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ShortText -> String
TS.unpack ShortText
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_"
    prefix <> inBetween <> text (show (metaId m))
{-# SPECIALIZE prettyTCM :: NamedMeta -> TCM Doc #-}

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

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

instance PrettyTCM a => PrettyTCM (VarMap' a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => VarMap' a -> m Doc
prettyTCM (VarMap TheVarMap' a
vars) = m Doc
"VarMap" 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 (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
k) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=") Int
2 (VarOcc' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VarOcc' a -> m Doc
prettyTCM VarOcc' a
v) | (Int
k, VarOcc' a
v) <- TheVarMap' a -> [(Int, VarOcc' a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList TheVarMap' a
vars ])
  {-# SPECIALIZE prettyTCM :: PrettyTCM a => VarMap' a -> TCM Doc #-}

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

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

deriving instance (PrettyTCM x, PrettyTCM a) => PrettyTCM (Boundary' x a)

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

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

instance PrettyTCM TypeCheckingProblem where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (CheckExpr Comparison
cmp Expr
e Type
a) =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":?", Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a ]
  prettyTCM (CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
es Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
_) =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"_ :" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Expr]
es
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
":?" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t1 ]
  prettyTCM (CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_) = TypeCheckingProblem -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t)
  prettyTCM (CheckWithApp Comparison
cmp Type
t WithAppHead
hd QName
_ Elims
_ List1 Expr
es)   = TypeCheckingProblem -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp (ExprInfo -> Expr -> List1 Expr -> Expr
A.WithApp ExprInfo
A.exprNoRange (WithAppHead -> Expr
wahExpr WithAppHead
hd) List1 Expr
es) Type
t)
  prettyTCM (CheckWithAppHead Comparison
cmp Type
t Expr
hd Term
_ List1 Expr
es) = TypeCheckingProblem -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp (ExprInfo -> Expr -> List1 Expr -> Expr
A.WithApp ExprInfo
A.exprNoRange Expr
hd List1 Expr
es) Type
t)
  prettyTCM (DoQuoteTerm Comparison
_ Term
v Type
_) = do
    e <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
    prettyTCM (A.App A.defaultAppInfo_ (A.QuoteTerm A.exprNoRange) (defaultNamedArg e))
  prettyTCM (DisambiguateConstructor (ConstructorDisambiguationData QName
c0 List1 (QName, Type, ConHead)
cands [NamedArg Expr]
args Type
t) ConHead -> TCM Term
_) = do
    let e :: Expr
e = (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
forall a. Null a => a
empty) (AmbiguousQName -> Expr
A.Con (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
c0) [NamedArg Expr]
args
    m Doc
"ambiguous constructor" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
{-# SPECIALIZE prettyTCM :: TypeCheckingProblem -> TCM Doc #-}

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

instance PrettyTCM 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
      [TypedBinding] -> m [Maybe TypedBinding]
forall (m :: * -> *).
MonadAbsToCon m =>
[TypedBinding] -> m [Maybe TypedBinding]
abstractToConcreteTelescope ([TypedBinding] -> m [Maybe TypedBinding])
-> m [TypedBinding] -> m [Maybe TypedBinding]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Telescope -> m (ReifiesTo Telescope)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Telescope -> m (ReifiesTo Telescope)
reify Telescope
tel
{-# SPECIALIZE prettyTCM :: Telescope -> TCM Doc #-}

newtype PrettyContext = PrettyContext Context

instance PrettyTCM PrettyContext where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => PrettyContext -> m Doc
prettyTCM (PrettyContext Context
ctx) = Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> m Doc) -> Telescope -> m Doc
forall a b. (a -> b) -> a -> b
$ Context -> Telescope
contextToTel Context
ctx
{-# SPECIALIZE prettyTCM :: PrettyContext -> TCM Doc #-}

instance PrettyTCM a => PrettyTCM (Pattern' a) where
  prettyTCM :: forall m. MonadPretty m => Pattern' a -> m Doc
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM (IApplyP PatternInfo
_ Term
_ Term
_ a
x) = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
  prettyTCM (VarP PatternInfo
_ a
x)        = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x

  prettyTCM (MaskP Pattern' a
p)  = m Doc
"«" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' a -> m Doc
prettyTCM Pattern' a
p m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"»"
  prettyTCM (DotP PatternInfo
_ Term
t) = m Doc
".(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"

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

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

{-# SPECIALIZE prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc #-}
prettyTCMPatternList :: (MonadPretty m) => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList :: forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, 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

-- | For unquote.
{-# SPECIALIZE prettyR :: (R.ToAbstract r, PrettyTCM (R.AbsOfRef r)) => r -> TCM Doc #-}
prettyR :: (R.ToAbstract r, PrettyTCM (R.AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
prettyR :: forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR = AbsOfRef r -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbsOfRef r -> m Doc
prettyTCM (AbsOfRef r -> m Doc) -> (r -> m (AbsOfRef r)) -> r -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< r -> m (AbsOfRef r)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 ReadTCState m, HasBuiltins m, HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstractWithoutImplicit

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

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

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

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

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

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

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

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

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

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

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