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
• _leftIdiomBrkt :: Doc
• _rightIdiomBrkt :: Doc
• _emptyIdiomBrkt :: Doc

specialCharacters :: SpecialCharacters

braces' :: Doc -> Doc

dbraces :: Doc -> Doc

forallQ :: Doc

leftIdiomBrkt :: Doc

rightIdiomBrkt :: Doc

emptyIdiomBrkt :: 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

prettyQuantity :: LensQuantity a => a -> Doc -> Doc

prettyCohesion :: LensCohesion a => a -> Doc -> Doc

prettyTactic :: BoundName -> Doc -> Doc

prettyTactic' :: TacticAttribute -> Doc -> Doc

data NamedBinding

Constructors

NamedBinding

Fields

• withHiding :: Bool
• namedBinding :: NamedArg Binder

Instances

Pretty NamedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NamedBinding -> Doc

prettyPrec :: Int -> NamedBinding -> Doc

prettyList :: [NamedBinding] -> Doc

isLabeled :: NamedArg Binder -> Maybe ArgName

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

pRecord :: Name -> Maybe (Ranged Induction) -> Maybe HasEta -> Maybe (Name, IsInstance) -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc

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 LamClause

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> 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 BoundName

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

Show LamBinding

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show DoStmt

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> 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

Show ModuleAssignment

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

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 Fixity

Methods

pretty :: Fixity -> Doc

prettyPrec :: Int -> Fixity -> Doc

prettyList :: [Fixity] -> Doc

Pretty Cohesion

Methods

pretty :: Cohesion -> Doc

prettyPrec :: Int -> Cohesion -> Doc

prettyList :: [Cohesion] -> Doc

Pretty Relevance

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

Pretty Quantity

Methods

pretty :: Quantity -> Doc

prettyPrec :: Int -> Quantity -> Doc

prettyList :: [Quantity] -> Doc

Pretty QωOrigin

Methods

pretty :: QωOrigin -> Doc

prettyPrec :: Int -> QωOrigin -> Doc

prettyList :: [QωOrigin] -> Doc

Pretty Q1Origin

Methods

pretty :: Q1Origin -> Doc

prettyPrec :: Int -> Q1Origin -> Doc

prettyList :: [Q1Origin] -> Doc

Pretty Q0Origin

Methods

pretty :: Q0Origin -> Doc

prettyPrec :: Int -> Q0Origin -> Doc

prettyList :: [Q0Origin] -> 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 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

Show a => Show (Binder' a)

Methods

showsPrec :: Int -> Binder' a -> ShowS

show :: Binder' a -> String

showList :: [Binder' a] -> ShowS

Show a => Show (OpApp a)

Methods

showsPrec :: Int -> OpApp a -> ShowS

show :: OpApp a -> String

showList :: [OpApp a] -> ShowS

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 (Binder' a)

Methods

pretty :: Binder' a -> Doc

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

prettyList :: [Binder' a] -> 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

(Show a, Show b) => Show (Renaming' a b)

Methods

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

show :: Renaming' a b -> String

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

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

Methods

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

show :: Using' a b -> String

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

(Show a, Show 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 (Renaming' a b)

Methods

pretty :: Renaming' a b -> Doc

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

prettyList :: [Renaming' 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