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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Pretty

Contents

- Orphan instances

Description

Pretty printer for the concrete syntax.

Synopsis

- attributesForModality :: HasOptions m => Modality -> m Doc
- bracesAndSemicolons :: Foldable t => t Doc -> Doc
- prettyTactic :: BoundName -> Doc -> Doc
- prettyTactic' :: TacticAttribute -> Doc -> Doc
- prettyFiniteness :: BoundName -> Doc -> Doc
- prettyOpApp :: Pretty a => Aspect -> QName -> List1 (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

attributesForModality :: HasOptions m => Modality -> m 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.

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

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

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

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

prettyOpApp :: Pretty a => Aspect -> QName -> List1 (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 Fixity' Source # |
Instance details Methods pretty :: Fixity' -> Doc Source # prettyPrec :: Int -> Fixity' -> Doc Source # prettyList :: [Fixity'] -> Doc Source #
Pretty NotationPart Source # |
Instance details Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> 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 Source # show :: BoundName -> String Source # showList :: [BoundName] -> ShowS Source #
Show Declaration Source # |
Instance details Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
Show DoStmt Source # |
Instance details Methods showsPrec :: Int -> DoStmt -> ShowS Source # show :: DoStmt -> String Source # showList :: [DoStmt] -> ShowS Source #
Show Expr Source # |
Instance details Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
Show LHS Source # |
Instance details Methods showsPrec :: Int -> LHS -> ShowS Source # show :: LHS -> String Source # showList :: [LHS] -> ShowS Source #
Show LHSCore Source # |
Instance details Methods showsPrec :: Int -> LHSCore -> ShowS Source # show :: LHSCore -> String Source # showList :: [LHSCore] -> ShowS Source #
Show LamBinding Source # |
Instance details Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
Show LamClause Source # |
Instance details Methods showsPrec :: Int -> LamClause -> ShowS Source # show :: LamClause -> String Source # showList :: [LamClause] -> ShowS Source #
Show Module Source # |
Instance details Methods showsPrec :: Int -> Module -> ShowS Source # show :: Module -> String Source # showList :: [Module] -> ShowS Source #
Show ModuleApplication Source # |
Instance details Methods showsPrec :: Int -> ModuleApplication -> ShowS Source # show :: ModuleApplication -> String Source # showList :: [ModuleApplication] -> ShowS Source #
Show ModuleAssignment Source # |
Instance details Methods showsPrec :: Int -> ModuleAssignment -> ShowS Source # show :: ModuleAssignment -> String Source # showList :: [ModuleAssignment] -> ShowS Source #
Show Pattern Source # |
Instance details Methods showsPrec :: Int -> Pattern -> ShowS Source # show :: Pattern -> String Source # showList :: [Pattern] -> ShowS Source #
Show Pragma Source # |
Instance details Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
Show RHS Source # |
Instance details Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
Show TypedBinding Source # |
Instance details Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
Show WhereClause Source # |
Instance details Methods showsPrec :: Int -> WhereClause -> ShowS Source # show :: WhereClause -> String Source # showList :: [WhereClause] -> ShowS 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 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 Source # show :: Binder' a -> String Source # showList :: [Binder' a] -> ShowS Source #
Show a => Show (OpApp a) Source # |
Instance details Methods showsPrec :: Int -> OpApp a -> ShowS Source # show :: OpApp a -> String Source # showList :: [OpApp a] -> ShowS 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 #