    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