Agda.Syntax.Concrete.Pretty

Pretty printer for the concrete syntax.

Documentation

data SpecialCharacters

Picking the appropriate set of special characters depending on whether we are allowed to use unicode or have to limit ourselves to ascii.

Constructors

SpecialCharacters

Fields

• _dbraces :: Doc -> Doc
• _lambda :: Doc
• _arrow :: Doc
• _forallQ :: Doc

specialCharacters :: SpecialCharacters

braces' :: Doc -> Doc

dbraces :: Doc -> Doc

forallQ :: Doc

bracesAndSemicolons :: [Doc] -> Doc

arrow :: Doc

lambda :: Doc

prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc

prettyHiding info visible doc puts the correct braces around doc according to info info and returns visible doc if the we deal with a visible thing.

prettyRelevance :: LensRelevance a => a -> Doc -> Doc

newtype Tel

Constructors

Tel Telescope

Instances

Pretty Tel

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

prettyList :: [Tel] -> Doc

smashTel :: Telescope -> Telescope

prettyOpApp :: forall a. Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]

Orphan instances

Show Pragma

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Show ModuleApplication

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Show Declaration

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Show WhereClause

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

Show RHS

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

Show LHSCore

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Show LHS

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

Show TypedBinding

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Show TypedBindings

Methods

showsPrec :: Int -> TypedBindings -> ShowS

show :: TypedBindings -> String

showList :: [TypedBindings] -> ShowS

Show LamBinding

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show Pattern

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

Show Expr

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Pretty Fixity'

Methods

pretty :: Fixity' -> Doc

prettyPrec :: Int -> Fixity' -> Doc

prettyList :: [Fixity'] -> Doc

Pretty Relevance

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

Pretty Induction

Methods

pretty :: Induction -> Doc

prettyPrec :: Int -> Induction -> Doc

prettyList :: [Induction] -> Doc

Pretty GenPart

Methods

pretty :: GenPart -> Doc

prettyPrec :: Int -> GenPart -> Doc

prettyList :: [GenPart] -> Doc

Pretty Fixity

Methods

pretty :: Fixity -> Doc

prettyPrec :: Int -> Fixity -> Doc

prettyList :: [Fixity] -> Doc

Pretty Pragma

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

Pretty OpenShortHand

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

Pretty ModuleApplication

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

Pretty Declaration

Methods

pretty :: Declaration -> Doc

prettyPrec :: Int -> Declaration -> Doc

prettyList :: [Declaration] -> Doc

Pretty LamClause

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

Pretty WhereClause

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

Pretty RHS

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

Pretty LHSCore

Methods

pretty :: LHSCore -> Doc

prettyPrec :: Int -> LHSCore -> Doc

prettyList :: [LHSCore] -> Doc

Pretty LHS

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

Pretty TypedBinding

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

Pretty BoundName

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

Pretty TypedBindings

Methods

pretty :: TypedBindings -> Doc

prettyPrec :: Int -> TypedBindings -> Doc

prettyList :: [TypedBindings] -> Doc

Pretty LamBinding

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty DoStmt

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

Pretty Pattern

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

Pretty Expr

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

Pretty ModuleAssignment

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

Pretty a => Pretty (MaybePlaceholder a)

Methods

pretty :: MaybePlaceholder a -> Doc

prettyPrec :: Int -> MaybePlaceholder a -> Doc

prettyList :: [MaybePlaceholder a] -> Doc

Pretty e => Pretty (Named_ e)

Methods

pretty :: Named_ e -> Doc

prettyPrec :: Int -> Named_ e -> Doc

prettyList :: [Named_ e] -> Doc

Pretty a => Pretty (Arg a)

Methods

pretty :: Arg a -> Doc

prettyPrec :: Int -> Arg a -> Doc

prettyList :: [Arg a] -> Doc

Pretty a => Pretty (WithHiding a)

Methods

pretty :: WithHiding a -> Doc

prettyPrec :: Int -> WithHiding a -> Doc

prettyList :: [WithHiding a] -> Doc

Pretty (ThingWithFixity Name)

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

Pretty a => Pretty (FieldAssignment' a)

Methods

pretty :: FieldAssignment' a -> Doc

prettyPrec :: Int -> FieldAssignment' a -> Doc

prettyList :: [FieldAssignment' a] -> Doc

Pretty (OpApp Expr)

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

(Pretty a, Pretty b) => Show (ImportDirective' a b)

Methods

showsPrec :: Int -> ImportDirective' a b -> ShowS

show :: ImportDirective' a b -> String

showList :: [ImportDirective' a b] -> ShowS

(Pretty a, Pretty b) => Pretty (Either a b)

Methods

pretty :: Either a b -> Doc

prettyPrec :: Int -> Either a b -> Doc

prettyList :: [Either a b] -> Doc

(Pretty a, Pretty b) => Pretty (a, b)

Methods

pretty :: (a, b) -> Doc

prettyPrec :: Int -> (a, b) -> Doc

prettyList :: [(a, b)] -> Doc

(Pretty a, Pretty b) => Pretty (ImportedName' a b)

Methods

pretty :: ImportedName' a b -> Doc

prettyPrec :: Int -> ImportedName' a b -> Doc

prettyList :: [ImportedName' a b] -> Doc

(Pretty a, Pretty b) => Pretty (Using' a b)

Methods

pretty :: Using' a b -> Doc

prettyPrec :: Int -> Using' a b -> Doc

prettyList :: [Using' a b] -> Doc

(Pretty a, Pretty b) => Pretty (ImportDirective' a b)

Methods

pretty :: ImportDirective' a b -> Doc

prettyPrec :: Int -> ImportDirective' a b -> Doc

prettyList :: [ImportDirective' a b] -> Doc