module Agda.Syntax.Abstract.Pretty where

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

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

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

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

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

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

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

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