module Agda.Syntax.Abstract.Pretty where

import Agda.Syntax.Fixity
import Agda.Syntax.Translation.AbstractToConcrete
import Agda.Utils.Pretty

showA :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String
showA :: forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showA a
x = forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ a
x

prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
prettyA :: forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA a
x = forall a. Pretty a => a -> Doc
pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ a
x

prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
prettyAs :: forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
prettyAs a
x = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ a
x

-- | Variant of 'showA' which does not insert outermost parentheses.

showATop :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String
showATop :: forall a (m :: * -> *).
(ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) =>
a -> m String
showATop a
x = forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx Precedence
TopCtx a
x

-- | Variant of 'prettyA' which does not insert outermost parentheses.

prettyATop :: (ToConcrete a, Pretty (ConOfAbs a),  MonadAbsToCon m) => a -> m Doc
prettyATop :: forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop a
x = forall a. Pretty a => a -> Doc
pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx Precedence
TopCtx a
x