{-# LANGUAGE UndecidableInstances #-}

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

import Prelude hiding ( null )

import Control.Monad

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

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

import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (equalityUnview)
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute

import Agda.Utils.Except
import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Permutation (Permutation)
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P

import Agda.Utils.Impossible

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

type Doc = P.Doc

comma, colon, equals :: Monad m => m Doc
comma :: m Doc
comma  = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
P.comma
colon :: m Doc
colon  = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
P.colon
equals :: m Doc
equals = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
P.equals

pretty :: (Monad m, P.Pretty a) => a -> m Doc
pretty :: a -> m Doc
pretty a
x = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
P.pretty a
x

prettyA :: (P.Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc
prettyA :: a -> m Doc
prettyA a
x = a -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
AP.prettyA a
x

prettyAs :: (P.Pretty c, ToConcrete a [c], MonadAbsToCon m) => a -> m Doc
prettyAs :: a -> m Doc
prettyAs a
x = a -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a [c], MonadAbsToCon m) =>
a -> m Doc
AP.prettyAs a
x

text :: Monad m => String -> m Doc
text :: String -> m Doc
text String
s = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.text String
s

multiLineText :: Monad m => String -> m Doc
multiLineText :: String -> m Doc
multiLineText String
s = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.multiLineText String
s

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

fwords :: Monad m => String -> m Doc
fwords :: String -> m Doc
fwords String
s = Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.fwords String
s

sep, fsep, hsep, hcat, vcat :: Monad m => [m Doc] -> m Doc
sep :: [m Doc] -> m Doc
sep [m Doc]
ds  = [Doc] -> Doc
P.sep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m Doc]
ds
fsep :: [m Doc] -> m Doc
fsep [m Doc]
ds = [Doc] -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m Doc]
ds
hsep :: [m Doc] -> m Doc
hsep [m Doc]
ds = [Doc] -> Doc
P.hsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m Doc]
ds
hcat :: [m Doc] -> m Doc
hcat [m Doc]
ds = [Doc] -> Doc
P.hcat ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m Doc]
ds
vcat :: [m Doc] -> m Doc
vcat [m Doc]
ds = [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Doc] -> m [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m Doc]
ds

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

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

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

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

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

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

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

-- | 'prettyList' without the brackets.
prettyList_ :: (Monad m, Semigroup (m Doc)) => [m Doc] -> m Doc
prettyList_ :: [m Doc] -> m Doc
prettyList_ [m Doc]
ds = [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma [m Doc]
ds

punctuate :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> [m Doc]
punctuate :: m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
_ [] = []
punctuate m Doc
d [m Doc]
ds = (m Doc -> m Doc -> m Doc) -> [m Doc] -> [m Doc] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
(<>) [m Doc]
ds (Int -> m Doc -> [m Doc]
forall a. Int -> a -> [a]
replicate Int
n m Doc
d [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
forall a. Null a => a
empty])
  where
    n :: Int
n = [m Doc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m Doc]
ds Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

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

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

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

instance PrettyTCM Bool        where prettyTCM :: Bool -> m Doc
prettyTCM = Bool -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM C.Name      where prettyTCM :: Name -> m Doc
prettyTCM = Name -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM C.QName     where prettyTCM :: QName -> m Doc
prettyTCM = QName -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Comparison  where prettyTCM :: Comparison -> m Doc
prettyTCM = Comparison -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Literal     where prettyTCM :: Literal -> m Doc
prettyTCM = Literal -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Nat         where prettyTCM :: Int -> m Doc
prettyTCM = Int -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM ProblemId   where prettyTCM :: ProblemId -> m Doc
prettyTCM = ProblemId -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM Range       where prettyTCM :: Range -> m Doc
prettyTCM = Range -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
instance PrettyTCM CheckpointId where prettyTCM :: CheckpointId -> m Doc
prettyTCM = CheckpointId -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty
-- instance PrettyTCM Interval where prettyTCM = pretty
-- instance PrettyTCM Position where prettyTCM = pretty

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

instance PrettyTCM a => PrettyTCM [a] where
  prettyTCM :: [a] -> m Doc
prettyTCM = [m Doc] -> m Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList ([m Doc] -> m Doc) -> ([a] -> [m Doc]) -> [a] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM

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

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

instance PrettyTCM Term         where prettyTCM :: Term -> m Doc
prettyTCM = Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Term -> m Expr) -> Term -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM Type         where prettyTCM :: Type -> m Doc
prettyTCM = Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Type -> m Expr) -> Type -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM Sort         where prettyTCM :: Sort -> m Doc
prettyTCM = Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Sort -> m Expr) -> Sort -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM DisplayTerm  where prettyTCM :: DisplayTerm -> m Doc
prettyTCM = Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (DisplayTerm -> m Expr) -> DisplayTerm -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< DisplayTerm -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM NamedClause  where prettyTCM :: NamedClause -> m Doc
prettyTCM = Clause -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (NamedClause -> m Clause) -> NamedClause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedClause -> m Clause
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM (QNamed Clause) where prettyTCM :: QNamed Clause -> m Doc
prettyTCM = Clause -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Clause -> m Doc)
-> (QNamed Clause -> m Clause) -> QNamed Clause -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< QNamed Clause -> m Clause
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
instance PrettyTCM Level        where prettyTCM :: Level -> m Doc
prettyTCM = Expr -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> m Doc) -> (Level -> m Expr) -> Level -> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> (Level -> Term) -> Level -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level -> Term
Level
instance PrettyTCM Permutation  where prettyTCM :: Permutation -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc)
-> (Permutation -> String) -> Permutation -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> String
forall a. Show a => a -> String
show
instance PrettyTCM Polarity     where prettyTCM :: Polarity -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> (Polarity -> String) -> Polarity -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> String
forall a. Show a => a -> String
show
instance PrettyTCM IsForced     where prettyTCM :: IsForced -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> (IsForced -> String) -> IsForced -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsForced -> String
forall a. Show a => a -> String
show

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

instance (Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) where
  prettyTCM :: 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. (Monad m, Pretty a) => a -> m Doc
pretty Int
m
  prettyTCM (EmptyS Empty
_) = m Doc
"emptyS"
  prettyTCM Substitution' a
rho = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
forall (m :: * -> *). Monad m => m Doc
comma m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution' a
rho1
    where
      (Substitution' a
rho1, Substitution' a
rho2) = Int -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS Int
1 Substitution' a
rho
      u :: a
u            = Substitution' a -> Int -> a
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' a
rho2 Int
0

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

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

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

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

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Named_ a) where
  prettyTCM :: Named_ a -> m Doc
prettyTCM Named_ a
x = Named (WithOrigin (Ranged String)) e -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Named (WithOrigin (Ranged String)) e -> m Doc)
-> m (Named (WithOrigin (Ranged String)) e) -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Named_ a -> m (Named (WithOrigin (Ranged String)) e)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Named_ a
x

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Arg a) where
  prettyTCM :: Arg a -> m Doc
prettyTCM Arg a
x = Arg e -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg e -> m Doc) -> m (Arg e) -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Arg a -> m (Arg e)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Arg a
x

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Dom a) where
  prettyTCM :: Dom a -> m Doc
prettyTCM Dom a
x = Arg e -> m Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg e -> m Doc) -> m (Arg e) -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Dom a -> m (Arg e)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Dom a
x

instance (PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) where
  prettyTCM :: 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 :: * -> *). Monad m => [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 :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma
    [ m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (k -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM k
k m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=") Int
2 (v -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM v
v) | (k
k, v
v) <- Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m ])

instance {-# OVERLAPPING #-} PrettyTCM ArgName where
  prettyTCM :: String -> m Doc
prettyTCM = String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> m Doc) -> (String -> String) -> String -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. Pretty a => a -> String
P.prettyShow

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

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

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

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

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

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

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

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

instance PrettyTCM ProblemConstraint where
  prettyTCM :: ProblemConstraint -> m Doc
prettyTCM (PConstr Set ProblemId
pids Closure Constraint
c) = Closure Constraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Closure Constraint
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [ProblemId] -> m Doc
forall (m :: * -> *) a.
(Null (m Doc), IsString (m Doc), PrettyTCM a, MonadReduce m,
 MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m,
 HasConstInfo m, HasBuiltins m, MonadStConcreteNames m,
 Semigroup (m Doc)) =>
[a] -> m Doc
prPids (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids)
    where
      prPids :: [a] -> m Doc
prPids []    = m Doc
forall a. Null a => a
empty
      prPids [a
pid] = 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
"problem" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
pid
      prPids [a]
pids  = 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
"problems" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
"," ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [a]
pids)

instance PrettyTCM Constraint where
    prettyTCM :: Constraint -> m Doc
prettyTCM Constraint
c = case Constraint
c of
        ValueCmp Comparison
cmp CompareAs
ty Term
s Term
t -> m Doc -> Term -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> CompareAs -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM CompareAs
ty
        ValueCmpOnFace Comparison
cmp Term
p Type
ty Term
s Term
t ->
            [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
p m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|"
                , m Doc -> Term -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Term
s Term
t ]
            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
<+> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
ty)
        ElimCmp [Polarity]
cmps [IsForced]
fs Type
t Term
v [Elim]
us [Elim]
vs -> m Doc -> [Elim] -> [Elim] -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
"~~" [Elim]
us [Elim]
vs   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
<+> Precedence -> Type -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Type
t)
        LevelCmp Comparison
cmp Level
a Level
b         -> m Doc -> Level -> Level -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Level
a Level
b
        TelCmp Type
a Type
b Comparison
cmp Telescope
tela Telescope
telb -> m Doc -> Telescope -> Telescope -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Telescope
tela Telescope
telb
        SortCmp Comparison
cmp Sort
s1 Sort
s2        -> m Doc -> Sort -> Sort -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp (Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp) Sort
s1 Sort
s2
        Guarded Constraint
c ProblemId
pid            -> Constraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (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
"blocked by problem" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemId
pid)
        UnBlock MetaId
m   -> do
            -- BlockedConst t <- mvInstantiation <$> lookupMeta m
            MetaInstantiation
mi <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> m MetaVariable -> m MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
            case MetaInstantiation
mi of
              BlockedConst Term
t -> m Doc -> MetaId -> Term -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m Term
t
              PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl TCM Bool
_ -> Closure TypeCheckingProblem
-> (TypeCheckingProblem -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> m Doc) -> m Doc)
-> (TypeCheckingProblem -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
p ->
                m Doc -> MetaId -> TypeCheckingProblem -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":=" MetaId
m TypeCheckingProblem
p
              Open{}  -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
              OpenInstance{} -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
              InstV{} -> m Doc
forall a. Null a => a
empty
              -- Andreas, 2017-01-11, issue #2637:
              -- The size solver instantiates some metas with infinity
              -- without cleaning up the UnBlock constraints.
              -- Thus, this case is not IMPOSSIBLE.
              --
              -- InstV args t -> do
              --   reportS "impossible" 10
              --     [ "UnBlock meta " ++ show m ++ " surprisingly has InstV instantiation:"
              --     , show m ++ show args ++ " := " ++ show t
              --     ]
              --   __IMPOSSIBLE__
        FindInstance MetaId
m Maybe MetaId
mb Maybe [Candidate]
mcands -> do
            Type
t <- MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m
            [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ m Doc
"Resolve instance argument" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
blk
                    m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> m Doc -> MetaId -> Type -> m Doc
forall a b (m :: * -> *).
(PrettyTCM a, PrettyTCM b, MonadPretty m) =>
m Doc -> a -> b -> m Doc
prettyCmp m Doc
":" MetaId
m Type
t
                , m Doc
cands
                ]
          where
            blk :: m Doc
blk = case Maybe MetaId
mb of
                    Maybe MetaId
Nothing -> m Doc
forall a. Null a => a
empty
                    Just MetaId
b  -> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"blocked on" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty MetaId
b
            cands :: m Doc
cands =
              case Maybe [Candidate]
mcands of
                Maybe [Candidate]
Nothing -> m Doc
"No candidates yet"
                Just [Candidate]
cnds ->
                  m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang m Doc
"Candidates" Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
                    [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Candidate -> m Doc
forall p. (IsString p, Null p) => Candidate -> p
overlap Candidate
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Candidate -> Term
candidateTerm Candidate
c) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
                            Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Candidate -> Type
candidateType Candidate
c) | Candidate
c <- [Candidate]
cnds ]
              where overlap :: Candidate -> p
overlap Candidate
c | Candidate -> Bool
candidateOverlappable Candidate
c = p
"overlap"
                              | Bool
otherwise               = p
forall a. Null a => a
empty
        IsEmpty Range
r Type
t ->
            m Doc
"Is empty:" 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
t
        CheckSizeLtSat Term
t ->
            m Doc
"Is not empty type of sizes:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Precedence -> Term -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx Term
t
        CheckFunDef Delayed
d DefInfo
i QName
q [Clause]
cs -> do
            Type
t <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            m Doc
"Check definition of" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        HasBiggerSort Sort
a -> m Doc
"Has bigger sort:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
a
        HasPTSRule Dom Type
a Abs Sort
b -> m Doc
"Has PTS rule:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> case Abs Sort
b of
          NoAbs String
_ Sort
b -> (Dom Type, Sort) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Dom Type
a,Sort
b)
          Abs String
x Sort
b   -> m Doc
"(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> (Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
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
<+> String -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext String
x (Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
b)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"
        UnquoteTactic Maybe MetaId
_ Term
v Term
_ Type
_ -> do
          Expr
e <- Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
          Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
A.defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
A.exprNoRange) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e))
        CheckMetaInst MetaId
x -> do
          MetaVariable
m <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
          case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
            HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            IsSort{} -> MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"is a sort"

      where
        prettyCmp
          :: (PrettyTCM a, PrettyTCM b, MonadPretty m)
          => m Doc -> a -> b -> m Doc
        prettyCmp :: m Doc -> a -> b -> m Doc
prettyCmp m Doc
cmp a
x b
y = Precedence -> a -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx a
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
cmp m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Precedence -> b -> m Doc
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
Precedence -> a -> m Doc
prettyTCMCtx Precedence
TopCtx b
y)

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

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

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

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

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

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

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

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

newtype PrettyContext = PrettyContext Context

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

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

instance PrettyTCM a => PrettyTCM (Pattern' a) where
  prettyTCM :: Pattern' a -> m Doc
prettyTCM (IApplyP PatternInfo
_ Term
_ Term
_ a
x)    = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x
  prettyTCM (VarP PatternInfo
_ a
x)    = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x
  prettyTCM (DotP PatternInfo
_ Term
t)    = m Doc
".(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"
  prettyTCM (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
  prettyTCM (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps) = (if Bool
b then m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces else m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> m Doc
forall a. a -> a
prTy (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
        ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
        where
        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 :: MonadPretty m => m Doc
        showRec :: m Doc
showRec = [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ m Doc
"record"
          , [Doc] -> Doc
bracesAndSemicolons ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg QName -> NamedArg (Pattern' a) -> m Doc)
-> [Arg QName] -> [NamedArg (Pattern' a)] -> m [Doc]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Arg QName -> NamedArg (Pattern' a) -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Arg QName -> NamedArg (Pattern' a) -> m Doc
showField (ConHead -> [Arg QName]
conFields ConHead
c) [NamedArg (Pattern' a)]
ps
          ]
        showField :: MonadPretty m => Arg QName -> NamedArg (Pattern' a) -> m Doc
        showField :: Arg QName -> NamedArg (Pattern' a) -> m Doc
showField (Arg ArgInfo
ai QName
x) NamedArg (Pattern' a)
p =
          [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Name
A.qnameName QName
x) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=" , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Pattern' a -> m Doc) -> Pattern' a -> m Doc
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p ]
        showCon :: MonadPretty m => m Doc
        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
forall a. a -> a
prTy (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Pattern' a -> m Doc)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
        prTy :: p -> p
prTy p
d = p
d -- caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> prettyTCM t
  prettyTCM (LitP PatternInfo
_ Literal
l)    = String -> m Doc
forall (m :: * -> *). Monad 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 :: * -> *). Monad m => String -> m Doc
text (String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
q)

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

prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList = [m Doc] -> m Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA ([NamedArg Pattern] -> m Doc)
-> ([NamedArg DeBruijnPattern] -> m [NamedArg Pattern])
-> [NamedArg DeBruijnPattern]
-> m Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
reifyPatterns

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

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

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

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

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

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

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

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

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

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

instance (PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) where
  prettyTCM :: Graph n e -> m Doc
prettyTCM Graph n e
g = [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 n a.
(MonadReduce m, MonadAddContext m, MonadInteractionPoints m,
 MonadFresh NameId m, HasConstInfo m, HasBuiltins m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc), PrettyTCM a, PrettyTCM (WithNode n a)) =>
(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 :: * -> *). Monad m => [m Doc] -> m Doc
sep
        [ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
n
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (WithNode n a -> m Doc)
-> ((n, a) -> WithNode n a) -> (n, a) -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> a -> WithNode n a) -> (n, a) -> WithNode n a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry n -> a -> WithNode n a
forall n a. n -> a -> WithNode n a
WithNode) ([(n, a)] -> [m Doc]) -> [(n, a)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Map n a -> [(n, a)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map n a
es
        ]

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