Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Pretty
Contents
Synopsis
- ($$) :: Applicative m => m Doc -> m Doc -> m Doc
- ($+$) :: Applicative m => m Doc -> m Doc -> m Doc
- (<+>) :: Applicative m => m Doc -> m Doc -> m Doc
- (<?>) :: Applicative m => m Doc -> m Doc -> m Doc
- braces :: Functor m => m Doc -> m Doc
- brackets :: Functor m => m Doc -> m Doc
- colon :: Applicative m => m Doc
- comma :: Applicative m => m Doc
- dbraces :: Functor m => m Doc -> m Doc
- defnToNameKind :: Defn -> NameKind
- doubleQuotes :: Functor m => m Doc -> m Doc
- equals :: Applicative m => m Doc
- fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- fwords :: Applicative m => String -> m Doc
- githubIssue :: Applicative m => Int -> m Doc
- hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
- hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- hlArgument :: Functor m => m Doc -> m Doc
- hlBound :: Functor m => m Doc -> m Doc
- hlConstructor :: Functor m => Induction -> m Doc -> m Doc
- hlDatatype :: Functor m => m Doc -> m Doc
- hlField :: Functor m => m Doc -> m Doc
- hlFunction :: Functor m => m Doc -> m Doc
- hlGeneralizable :: Functor m => m Doc -> m Doc
- hlMacro :: Functor m => m Doc -> m Doc
- hlModule :: Functor m => m Doc -> m Doc
- hlPostulate :: Functor m => m Doc -> m Doc
- hlPrimitive :: Functor m => m Doc -> m Doc
- hlRecord :: Functor m => m Doc -> m Doc
- hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- multiLineText :: Applicative m => String -> m Doc
- nest :: Functor m => Int -> m Doc -> m Doc
- parens :: Functor m => m Doc -> m Doc
- parensNonEmpty :: Functor m => m Doc -> m Doc
- pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
- pretty :: (Applicative m, Pretty a) => a -> m Doc
- prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
- prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
- prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
- prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
- prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
- prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
- prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
- pshow :: (Applicative m, Show a) => a -> m Doc
- punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
- pwords :: Applicative m => String -> [m Doc]
- quotes :: Functor m => m Doc -> m Doc
- sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
- superscript :: Applicative m => Int -> m Doc
- text :: Applicative m => String -> m Doc
- url :: Applicative m => String -> m Doc
- vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- type Doc = Doc
- type MonadPretty (m :: Type -> Type) = MonadAbsToCon m
- newtype PrettyContext = PrettyContext Context
- class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> m Doc
- class PrettyTCMWithNode a where
- prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
- data WithNode n a = WithNode n a
- type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))
Documentation
colon :: Applicative m => m Doc Source #
comma :: Applicative m => m Doc Source #
defnToNameKind :: Defn -> NameKind Source #
equals :: Applicative m => m Doc Source #
githubIssue :: Applicative m => Int -> m Doc Source #
Link to an issue on the Agda bug tracker.
multiLineText :: Applicative m => String -> m Doc Source #
prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc Source #
prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc Source #
prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #
Comma-separated list in brackets.
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc Source #
prettyList
without the brackets.
prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc Source #
For unquote.
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc Source #
Pretty print with a given context precedence
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc Source #
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc] Source #
Proper pretty printing of patterns:
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc] Source #
sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a] Source #
sequenceAFoldable == sequenceA . Fold.toList
superscript :: Applicative m => Int -> m Doc Source #
type MonadPretty (m :: Type -> Type) = MonadAbsToCon m Source #
newtype PrettyContext Source #
Constructors
PrettyContext Context |
Instances
PrettyTCM PrettyContext Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source # |
class PrettyTCM a where Source #
Methods
prettyTCM :: MonadPretty m => a -> m Doc Source #
Instances
class PrettyTCMWithNode a where Source #
Pretty-print something paired with a (printable) node. | This intermediate typeclass exists to avoid UndecidableInstances.
Methods
prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc Source #
Instances
PrettyTCMWithNode Occurrence Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc Source # | |
PrettyTCMWithNode (Edge OccursWhere) Source # | |
Defined in Agda.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source # |
Pairing something with a node (for printing only).
Constructors
WithNode n a |
type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #
Preconditions to run the AbstractToConcrete translation.