Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Pretty

Contents

Orphan instances

Description

Pretty printer for the concrete syntax.

Synopsis

prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
attributesForModality :: Modality -> Doc
prettyRelevance :: LensRelevance a => a -> Doc -> Doc
bracesAndSemicolons :: Foldable t => t Doc -> Doc
prettyQuantity :: LensQuantity a => a -> Doc -> Doc
prettyLock :: LensLock a => a -> Doc -> Doc
prettyErased :: Erased -> Doc -> Doc
prettyCohesion :: LensCohesion a => a -> Doc -> Doc
prettyTactic :: BoundName -> Doc -> Doc
prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyFiniteness :: BoundName -> Doc -> Doc
prettyOpApp :: Pretty a => Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
newtype Tel = Tel Telescope
smashTel :: Telescope -> Telescope
data NamedBinding = NamedBinding {
- withHiding :: Bool
- namedBinding :: NamedArg Binder
}
isLabeled :: NamedArg Binder -> Maybe ArgName
pRecord :: Erased -> Name -> [RecordDirective] -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc
pHasEta0 :: HasEta0 -> Doc
pRecordDirective :: RecordDirective -> Doc
module Agda.Syntax.Concrete.Glyph

Documentation

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.

attributesForModality :: Modality -> Doc Source #

Show the attributes necessary to recover a modality, in long-form (e.g. using at-syntax rather than dots). For the default modality, the result is at-ω (rather than the empty document). Suitable for showing modalities outside of binders.

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

bracesAndSemicolons :: Foldable t => t Doc -> Doc Source #

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

prettyLock :: LensLock a => a -> Doc -> Doc Source #

prettyErased :: Erased -> Doc -> Doc Source #

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

prettyTactic :: BoundName -> Doc -> Doc Source #

prettyTactic' :: TacticAttribute -> Doc -> Doc Source #

prettyFiniteness :: BoundName -> Doc -> Doc Source #

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

newtype Tel Source #

Constructors

Tel Telescope

Instances

Instances details

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 #

smashTel :: Telescope -> Telescope Source #

data NamedBinding Source #

Constructors

NamedBinding
Fields withHiding :: Bool namedBinding :: NamedArg Binder

Instances

Instances details

Pretty NamedBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: NamedBinding -> Doc Source # prettyPrec :: Int -> NamedBinding -> Doc Source # prettyList :: [NamedBinding] -> Doc Source #

isLabeled :: NamedArg Binder -> Maybe ArgName Source #

pRecord :: Erased -> Name -> [RecordDirective] -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc Source #

pHasEta0 :: HasEta0 -> Doc Source #

pRecordDirective :: RecordDirective -> Doc Source #

module Agda.Syntax.Concrete.Glyph

Orphan instances

Pretty Associativity Source #
Instance details Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source #
Pretty Cohesion Source #
Instance details Methods pretty :: Cohesion -> Doc Source # prettyPrec :: Int -> Cohesion -> Doc Source # prettyList :: [Cohesion] -> Doc Source #
Pretty Erased Source #
Instance details Methods pretty :: Erased -> Doc Source # prettyPrec :: Int -> Erased -> Doc Source # prettyList :: [Erased] -> Doc Source #
Pretty Fixity Source #
Instance details Methods pretty :: Fixity -> Doc Source # prettyPrec :: Int -> Fixity -> Doc Source # prettyList :: [Fixity] -> Doc Source #
Pretty Fixity' Source #
Instance details Methods pretty :: Fixity' -> Doc Source # prettyPrec :: Int -> Fixity' -> Doc Source # prettyList :: [Fixity'] -> Doc Source #
Pretty FixityLevel Source #
Instance details Methods pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> Doc Source #
Pretty Lock Source #
Instance details Methods pretty :: Lock -> Doc Source # prettyPrec :: Int -> Lock -> Doc Source # prettyList :: [Lock] -> Doc Source #
Pretty Modality Source #
Instance details Methods pretty :: Modality -> Doc Source # prettyPrec :: Int -> Modality -> Doc Source # prettyList :: [Modality] -> Doc Source #
Pretty NotationPart Source #
Instance details Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source #
Pretty Q0Origin Source #
Instance details Methods pretty :: Q0Origin -> Doc Source # prettyPrec :: Int -> Q0Origin -> Doc Source # prettyList :: [Q0Origin] -> Doc Source #
Pretty Q1Origin Source #
Instance details Methods pretty :: Q1Origin -> Doc Source # prettyPrec :: Int -> Q1Origin -> Doc Source # prettyList :: [Q1Origin] -> Doc Source #
Pretty Quantity Source #
Instance details Methods pretty :: Quantity -> Doc Source # prettyPrec :: Int -> Quantity -> Doc Source # prettyList :: [Quantity] -> Doc Source #
Pretty QωOrigin Source #
Instance details Methods pretty :: QωOrigin -> Doc Source # prettyPrec :: Int -> QωOrigin -> Doc Source # prettyList :: [QωOrigin] -> Doc Source #
Pretty Relevance Source #
Instance details Methods pretty :: Relevance -> Doc Source # prettyPrec :: Int -> Relevance -> Doc Source # prettyList :: [Relevance] -> Doc Source #
Pretty BoundName Source #
Instance details Methods pretty :: BoundName -> Doc Source # prettyPrec :: Int -> BoundName -> Doc Source # prettyList :: [BoundName] -> Doc Source #
Pretty Declaration Source #
Instance details Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source #
Pretty DoStmt Source #
Instance details Methods pretty :: DoStmt -> Doc Source # prettyPrec :: Int -> DoStmt -> Doc Source # prettyList :: [DoStmt] -> Doc Source #
Pretty Expr Source #
Instance details Methods pretty :: Expr -> Doc Source # prettyPrec :: Int -> Expr -> Doc Source # prettyList :: [Expr] -> Doc Source #
Pretty LHS Source #
Instance details Methods pretty :: LHS -> Doc Source # prettyPrec :: Int -> LHS -> Doc Source # prettyList :: [LHS] -> Doc Source #
Pretty LHSCore Source #
Instance details Methods pretty :: LHSCore -> Doc Source # prettyPrec :: Int -> LHSCore -> Doc Source # prettyList :: [LHSCore] -> Doc Source #
Pretty LamBinding Source #
Instance details Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
Pretty LamClause Source #
Instance details Methods pretty :: LamClause -> Doc Source # prettyPrec :: Int -> LamClause -> Doc Source # prettyList :: [LamClause] -> Doc Source #
Pretty ModuleApplication Source #
Instance details Methods pretty :: ModuleApplication -> Doc Source # prettyPrec :: Int -> ModuleApplication -> Doc Source # prettyList :: [ModuleApplication] -> Doc Source #
Pretty ModuleAssignment Source #
Instance details Methods pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source #
Pretty OpenShortHand Source #
Instance details Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source #
Pretty Pattern Source #
Instance details Methods pretty :: Pattern -> Doc Source # prettyPrec :: Int -> Pattern -> Doc Source # prettyList :: [Pattern] -> Doc Source #
Pretty Pragma Source #
Instance details Methods pretty :: Pragma -> Doc Source # prettyPrec :: Int -> Pragma -> Doc Source # prettyList :: [Pragma] -> Doc Source #
Pretty RHS Source #
Instance details Methods pretty :: RHS -> Doc Source # prettyPrec :: Int -> RHS -> Doc Source # prettyList :: [RHS] -> Doc Source #
Pretty RecordDirective Source #
Instance details Methods pretty :: RecordDirective -> Doc Source # prettyPrec :: Int -> RecordDirective -> Doc Source # prettyList :: [RecordDirective] -> Doc Source #
Pretty TypedBinding Source #
Instance details Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source #
Pretty WhereClause Source #
Instance details Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
Show BoundName Source #
Instance details Methods showsPrec :: Int -> BoundName -> ShowS show :: BoundName -> String showList :: [BoundName] -> ShowS
Show Declaration Source #
Instance details Methods showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS
Show DoStmt Source #
Instance details Methods showsPrec :: Int -> DoStmt -> ShowS show :: DoStmt -> String showList :: [DoStmt] -> ShowS
Show Expr Source #
Instance details Methods showsPrec :: Int -> Expr -> ShowS show :: Expr -> String showList :: [Expr] -> ShowS
Show LHS Source #
Instance details Methods showsPrec :: Int -> LHS -> ShowS show :: LHS -> String showList :: [LHS] -> ShowS
Show LHSCore Source #
Instance details Methods showsPrec :: Int -> LHSCore -> ShowS show :: LHSCore -> String showList :: [LHSCore] -> ShowS
Show LamBinding Source #
Instance details Methods showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS
Show LamClause Source #
Instance details Methods showsPrec :: Int -> LamClause -> ShowS show :: LamClause -> String showList :: [LamClause] -> ShowS
Show Module Source #
Instance details Methods showsPrec :: Int -> Module -> ShowS show :: Module -> String showList :: [Module] -> ShowS
Show ModuleApplication Source #
Instance details Methods showsPrec :: Int -> ModuleApplication -> ShowS show :: ModuleApplication -> String showList :: [ModuleApplication] -> ShowS
Show ModuleAssignment Source #
Instance details Methods showsPrec :: Int -> ModuleAssignment -> ShowS show :: ModuleAssignment -> String showList :: [ModuleAssignment] -> ShowS
Show Pattern Source #
Instance details Methods showsPrec :: Int -> Pattern -> ShowS show :: Pattern -> String showList :: [Pattern] -> ShowS
Show Pragma Source #
Instance details Methods showsPrec :: Int -> Pragma -> ShowS show :: Pragma -> String showList :: [Pragma] -> ShowS
Show RHS Source #
Instance details Methods showsPrec :: Int -> RHS -> ShowS show :: RHS -> String showList :: [RHS] -> ShowS
Show TypedBinding Source #
Instance details Methods showsPrec :: Int -> TypedBinding -> ShowS show :: TypedBinding -> String showList :: [TypedBinding] -> ShowS
Show WhereClause Source #
Instance details Methods showsPrec :: Int -> WhereClause -> ShowS show :: WhereClause -> String showList :: [WhereClause] -> ShowS
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 (MaybePlaceholder a) Source #
Instance details Methods pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source #
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 (WithHiding a) Source #
Instance details Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source #
Pretty a => Pretty (Binder' a) Source #
Instance details Methods pretty :: Binder' a -> Doc Source # prettyPrec :: Int -> Binder' a -> Doc Source # prettyList :: [Binder' a] -> Doc Source #
Pretty a => Pretty (FieldAssignment' a) Source #
Instance details Methods pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source #
Pretty (OpApp Expr) Source #
Instance details Methods pretty :: OpApp Expr -> Doc Source # prettyPrec :: Int -> OpApp Expr -> Doc Source # prettyList :: [OpApp Expr] -> Doc Source #
Pretty a => Pretty (TacticAttribute' a) Source #
Instance details Methods pretty :: TacticAttribute' a -> Doc Source # prettyPrec :: Int -> TacticAttribute' a -> Doc Source # prettyList :: [TacticAttribute' a] -> Doc Source #
Pretty (ThingWithFixity Name) Source #
Instance details Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
Show a => Show (Binder' a) Source #
Instance details Methods showsPrec :: Int -> Binder' a -> ShowS show :: Binder' a -> String showList :: [Binder' a] -> ShowS
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 b) => Pretty (ImportDirective' a b) Source #
Instance details Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> Doc Source #
(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source #
Instance details Methods pretty :: ImportedName' a b -> Doc Source # prettyPrec :: Int -> ImportedName' a b -> Doc Source # prettyList :: [ImportedName' a b] -> Doc Source #
(Pretty a, Pretty b) => Pretty (Renaming' a b) Source #
Instance details Methods pretty :: Renaming' a b -> Doc Source # prettyPrec :: Int -> Renaming' a b -> Doc Source # prettyList :: [Renaming' a b] -> Doc Source #
(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 (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 #
(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
(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