Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Pretty

Contents

Description

Pretty printer for the concrete syntax.

Synopsis

Documentation

data SpecialCharacters Source #

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

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

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.

getLabel :: NamedArg a -> Maybe String Source #

newtype Tel Source #

Constructors

Tel Telescope 
Instances
Pretty Tel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc Source #

prettyPrec :: Int -> Tel -> Doc Source #

prettyList :: [Tel] -> Doc Source #

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

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

Orphan instances

Show Pragma Source # 
Instance details

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Show ModuleApplication Source # 
Instance details

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Show Declaration Source # 
Instance details

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Show LamClause Source # 
Instance details

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> ShowS

Show LHSCore Source # 
Instance details

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Show LHS Source # 
Instance details

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

Show DoStmt Source # 
Instance details

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> ShowS

Show Pattern Source # 
Instance details

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

Show Expr Source # 
Instance details

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Show ModuleAssignment Source # 
Instance details

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

Pretty Fixity' Source # 
Instance details

Pretty Relevance Source # 
Instance details

Pretty GenPart Source # 
Instance details

Pretty Fixity Source # 
Instance details

Pretty Pragma Source # 
Instance details

Pretty OpenShortHand Source # 
Instance details

Pretty ModuleApplication Source # 
Instance details

Pretty Declaration Source # 
Instance details

Pretty LamClause Source # 
Instance details

Pretty WhereClause Source # 
Instance details

Pretty RHS Source # 
Instance details

Methods

pretty :: RHS -> Doc Source #

prettyPrec :: Int -> RHS -> Doc Source #

prettyList :: [RHS] -> Doc Source #

Pretty LHSCore Source # 
Instance details

Pretty LHS Source # 
Instance details

Methods

pretty :: LHS -> Doc Source #

prettyPrec :: Int -> LHS -> Doc Source #

prettyList :: [LHS] -> Doc Source #

Pretty TypedBinding Source # 
Instance details

Pretty BoundName Source # 
Instance details

Pretty LamBinding Source # 
Instance details

Pretty DoStmt Source # 
Instance details

Pretty Pattern Source # 
Instance details

Pretty Expr Source # 
Instance details

Methods

pretty :: Expr -> Doc Source #

prettyPrec :: Int -> Expr -> Doc Source #

prettyList :: [Expr] -> Doc Source #

Pretty ModuleAssignment Source # 
Instance details

Show (WhereClause' [Declaration]) Source # 
Instance details

Methods

showsPrec :: Int -> WhereClause' [Declaration] -> ShowS

show :: WhereClause' [Declaration] -> String

showList :: [WhereClause' [Declaration]] -> ShowS

Show (RHS' Expr) Source # 
Instance details

Methods

showsPrec :: Int -> RHS' Expr -> ShowS

show :: RHS' Expr -> String

showList :: [RHS' Expr] -> ShowS

Show (TypedBinding' Expr) Source # 
Instance details

Methods

showsPrec :: Int -> TypedBinding' Expr -> ShowS

show :: TypedBinding' Expr -> String

showList :: [TypedBinding' Expr] -> ShowS

Show (LamBinding' TypedBinding) Source # 
Instance details

Show a => Show (OpApp a) Source # 
Instance details

Methods

showsPrec :: Int -> OpApp a -> ShowS

show :: OpApp a -> String

showList :: [OpApp a] -> ShowS

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Pretty e => Pretty (Named_ e) Source # 
Instance details

Methods

pretty :: Named_ e -> Doc Source #

prettyPrec :: Int -> Named_ e -> Doc Source #

prettyList :: [Named_ e] -> Doc Source #

Pretty a => Pretty (Dom a) Source # 
Instance details

Methods

pretty :: Dom a -> Doc Source #

prettyPrec :: Int -> Dom a -> Doc Source #

prettyList :: [Dom a] -> Doc Source #

Pretty a => Pretty (Arg a) Source # 
Instance details

Methods

pretty :: Arg a -> Doc Source #

prettyPrec :: Int -> Arg a -> Doc Source #

prettyList :: [Arg a] -> Doc Source #

Pretty a => Pretty (WithHiding a) Source # 
Instance details

Pretty (ThingWithFixity Name) Source # 
Instance details

Pretty a => Pretty (FieldAssignment' a) Source # 
Instance details

Pretty (OpApp Expr) Source # 
Instance details

(Show a, Show b) => Show (Renaming' a b) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Methods

pretty :: Either a b -> Doc Source #

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

prettyList :: [Either a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (a, b) Source # 
Instance details

Methods

pretty :: (a, b) -> Doc Source #

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

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

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Methods

pretty :: Using' a b -> Doc Source #

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

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

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details