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 = ConOfAbs a -> String
forall a. Show a => a -> String
show (ConOfAbs a -> String) -> m (ConOfAbs a) -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (ConOfAbs a)
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 = ConOfAbs a -> Doc
forall a. Pretty a => a -> Doc
pretty (ConOfAbs a -> Doc) -> m (ConOfAbs a) -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (ConOfAbs a)
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 = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> ([ce] -> [Doc]) -> [ce] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ce -> Doc) -> [ce] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ce -> Doc
forall a. Pretty a => a -> Doc
pretty ([ce] -> Doc) -> m [ce] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (ConOfAbs a)
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 = ConOfAbs a -> String
forall a. Show a => a -> String
show (ConOfAbs a -> String) -> m (ConOfAbs a) -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> m (ConOfAbs a)
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 = ConOfAbs a -> Doc
forall a. Pretty a => a -> Doc
pretty (ConOfAbs a -> Doc) -> m (ConOfAbs a) -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx Precedence
TopCtx a
x