Safe Haskell	None
Language	Haskell2010

Language.PTS.Pretty

Contents

Class
Convience functons
Symbols
Combinators
Syntax
Hadron
Precedence

Description

TODO The syntax is quite light, so the precedence table is small:

operation	assoc	examples
application	left	`f x y`, `f (g x)`
Pi,arrow	right	`a -> b -> c`, `(a -> b) -> c`
lambda	none	`λx → x`
annotation	right	`a : t`, `a : t : s`, `(a : t) : t'`

%>>> let pp = prettyPut :: Term LambdaStar -> IO () %>>> let pp' = prettyPut :: Value LambdaStar -> IO () %>>> let s = LambdaStar

%>>> pp $ "f" @ "x" @ "y" f x y

%>>> pp $ pi_ "m" (Nat ~> sort_ s) s ("m" @@ "zero" ~> "x") s ∏m : Nat → ⋆. m zero → x

%>>> pp' $ lam_ "x" "x" λx → x

%>>> prettyPut ("x" -:- "t" -:- "s" :: Term LambdaStar) x : t : s

%>>> prettyPut (("x" -:- "t") -:- "s" :: Term LambdaStar) (x : t) : s

Note: we don't rename or disambiguate variables (in pretty-printing), so one have to be careful:

%>>> let latter = lams_ ["x", "x"] "x" :: Value LambdaStar %>>> let former = lams_ ["f", "x"] ("f" valueApp "x") valueApp lams_ ["y", "x"] "y" :: Value LambdaStar

%>>> pp' latter λx x → x

%>>> pp' former λx x → x

but they are different:

%>>> print latter >> print former ValueLam "x" (Scope (ValueLam "x" (Scope (ValueCoerce (ValueVar (B "x")))))) ValueLam "x" (Scope (ValueLam "x" (Scope (ValueCoerce (ValueVar (F (B "x")))))))

Synopsis

class PrettyPrec a where
data PrettyM a
type Doc = Doc ()
ppp0 :: PrettyPrec a => a -> PrettyM Doc
pppParens :: Bool -> PrettyM Doc -> PrettyM Doc
class PrettyPrec1 f where
ppp1 :: (PrettyPrec1 f, PrettyPrec a) => Prec -> f a -> PrettyM Doc
prettyShow :: PrettyPrec a => a -> String
prettyShowWith :: PrettyPrec a => Options () String -> a -> String
prettyPut :: PrettyPrec a => a -> IO ()
prettyPutWith :: PrettyPrec a => Options () String -> a -> IO ()
pppMarkSym :: Sym -> PrettyM Doc
pppFreshSym :: Sym -> PrettyM Doc
pppScopedSym :: Sym -> (Doc -> PrettyM a) -> PrettyM a
pppScopedIrrSym :: IrrSym -> (Doc -> PrettyM a) -> PrettyM a
pppChar :: Char -> PrettyM Doc
pppText :: String -> PrettyM Doc
pppIntegral :: Integral a => a -> PrettyM Doc
pppIntegralSub :: Integral a => a -> PrettyM Doc
(<+>) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc
(</>) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc
($$$) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc
pppHsepPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc
pppSepPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc
pppCatPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc
pppColon :: PrettyM Doc
pppComma_ :: Doc ()
pppHang :: Int -> PrettyM Doc -> PrettyM Doc -> PrettyM Doc
pppApplication :: Prec -> PrettyM Doc -> [PrettyM Doc] -> PrettyM Doc
pppPi :: Prec -> [PPPi] -> PrettyM Doc -> PrettyM Doc
data PPPi
- = PPPi Doc (PrettyM Doc)
- | PPForall Doc
- | PPArrow (PrettyM Doc)
- | PPSigma Doc (PrettyM Doc)
- | PPExists Doc
pppLambda :: Prec -> [Doc] -> PrettyM Doc -> PrettyM Doc
pppAnnotation :: Prec -> PrettyM Doc -> PrettyM Doc -> PrettyM Doc
pppAnnotationPi :: Prec -> PrettyM Doc -> [PPPi] -> PrettyM Doc -> PrettyM Doc
pppHadron :: Set Sym -> PrettyM Doc
pppQuark :: Sym -> PrettyM Doc
pppQuarkElim :: Prec -> IrrSym -> (Doc -> PrettyM Doc) -> Map Sym (PrettyM Doc) -> PrettyM Doc -> PrettyM Doc
data Prec
- = PrecDef
- | PrecAnn
- | PrecLambda
- | PrecPi
- | PrecApp
predPrec :: Prec -> Prec

Class

class PrettyPrec a where Source #

Minimal complete definition

ppp

Methods

ppp :: Prec -> a -> PrettyM Doc Source #

Instances

PrettyPrec () Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> () -> PrettyM Doc Source #
PrettyPrec Void Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Void -> PrettyM Doc Source #
PrettyPrec IrrSym Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> IrrSym -> PrettyM Doc Source #
PrettyPrec Sym Source #	Generates fresh names. Uses `pppMarkSym`, see also `pppFreshSym`, and `pppScopedSym`. `>>>` `prettyPut $ ppp0 ("x" :: Sym)`x `>>>` `prettyPut $ ppp0 ("x2" :: Sym)`x₂
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Sym -> PrettyM Doc Source #
PrettyPrec IntVar Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> IntVar -> PrettyM Doc Source #
PrettyPrec Err Source #
Instance details Defined in Language.PTS.Error Methods ppp :: Prec -> Err -> PrettyM Doc Source #
PrettyPrec SystemU Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> SystemU -> PrettyM Doc Source #
PrettyPrec HOL Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> HOL -> PrettyM Doc Source #
PrettyPrec MartinLof Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> MartinLof -> PrettyM Doc Source #
PrettyPrec CoC Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> CoC -> PrettyM Doc Source #
PrettyPrec HindleyMilner Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> HindleyMilner -> PrettyM Doc Source #
PrettyPrec SystemF Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> SystemF -> PrettyM Doc Source #
PrettyPrec STLC Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> STLC -> PrettyM Doc Source #
PrettyPrec LambdaStar Source #
Instance details Defined in Language.PTS.Systems Methods ppp :: Prec -> LambdaStar -> PrettyM Doc Source #
PrettyPrec a => PrettyPrec (Maybe a) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Maybe a -> PrettyM Doc Source #
a ~ Doc => PrettyPrec (PrettyM a) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> PrettyM a -> PrettyM Doc Source #
(PrettyPrec a, PrettyPrec b) => PrettyPrec (Either a b) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Either a b -> PrettyM Doc Source #
(PrettyPrec a, PrettyPrec b) => PrettyPrec (a, b) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> (a, b) -> PrettyM Doc Source #
PrettyPrec n => PrettyPrec (Name n a) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Name n a -> PrettyM Doc Source #
(PrettyPrec a, PrettyPrec b) => PrettyPrec (Var a b) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Var a b -> PrettyM Doc Source #
(PrettyPrec1 t, PrettyPrec a) => PrettyPrec (UTerm t a) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> UTerm t a -> PrettyM Doc Source #
(Specification s, PrettyPrec a) => PrettyPrec (TermChk s a) Source #
Instance details Defined in Language.PTS.Term Methods ppp :: Prec -> TermChk s a -> PrettyM Doc Source #
(Specification s, PrettyPrec a) => PrettyPrec (TermInf s a) Source #
Instance details Defined in Language.PTS.Term Methods ppp :: Prec -> TermInf s a -> PrettyM Doc Source #
(Specification s, PrettyPrec err, PrettyPrec a) => PrettyPrec (ValueElim err s a) Source #
Instance details Defined in Language.PTS.Value Methods ppp :: Prec -> ValueElim err s a -> PrettyM Doc Source #
(Specification s, PrettyPrec err, PrettyPrec a) => PrettyPrec (ValueIntro err s a) Source #
Instance details Defined in Language.PTS.Value Methods ppp :: Prec -> ValueIntro err s a -> PrettyM Doc Source #

data PrettyM a Source #

A pretty-printing monad, keeping state of binded symbols.

Instances

Monad PrettyM Source #
Instance details Defined in Language.PTS.Pretty Methods (>>=) :: PrettyM a -> (a -> PrettyM b) -> PrettyM b Source # (>>) :: PrettyM a -> PrettyM b -> PrettyM b Source # return :: a -> PrettyM a Source # fail :: String -> PrettyM a Source #
Functor PrettyM Source #
Instance details Defined in Language.PTS.Pretty Methods fmap :: (a -> b) -> PrettyM a -> PrettyM b Source # (<$) :: a -> PrettyM b -> PrettyM a Source #
Applicative PrettyM Source #
Instance details Defined in Language.PTS.Pretty Methods pure :: a -> PrettyM a Source # (<>) :: PrettyM (a -> b) -> PrettyM a -> PrettyM b Source # liftA2 :: (a -> b -> c) -> PrettyM a -> PrettyM b -> PrettyM c Source # (>) :: PrettyM a -> PrettyM b -> PrettyM b Source # (<*) :: PrettyM a -> PrettyM b -> PrettyM a Source #
a ~ Doc => IsString (PrettyM a) Source #
Instance details Defined in Language.PTS.Pretty Methods fromString :: String -> PrettyM a Source #
a ~ Doc => Semigroup (PrettyM a) Source #
Instance details Defined in Language.PTS.Pretty Methods (<>) :: PrettyM a -> PrettyM a -> PrettyM a Source # sconcat :: NonEmpty (PrettyM a) -> PrettyM a Source # stimes :: Integral b => b -> PrettyM a -> PrettyM a Source #
a ~ Doc => Monoid (PrettyM a) Source #
Instance details Defined in Language.PTS.Pretty Methods mempty :: PrettyM a Source # mappend :: PrettyM a -> PrettyM a -> PrettyM a Source # mconcat :: [PrettyM a] -> PrettyM a Source #
a ~ Doc => PrettyPrec (PrettyM a) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> PrettyM a -> PrettyM Doc Source #

type Doc = Doc () Source #

ppp0 :: PrettyPrec a => a -> PrettyM Doc Source #

pppParens :: Bool -> PrettyM Doc -> PrettyM Doc Source #

class PrettyPrec1 f where Source #

Minimal complete definition

liftPpp

Methods

liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> f a -> PrettyM Doc Source #

Instances

PrettyPrec1 Maybe Source #
Instance details Defined in Language.PTS.Pretty Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> Maybe a -> PrettyM Doc Source #
PrettyPrec a => PrettyPrec1 (Var a) Source #
Instance details Defined in Language.PTS.Pretty Methods liftPpp :: (Prec -> a0 -> PrettyM Doc) -> Prec -> Var a a0 -> PrettyM Doc Source #
PrettyPrec1 t => PrettyPrec1 (UTerm t) Source #
Instance details Defined in Language.PTS.Pretty Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> UTerm t a -> PrettyM Doc Source #
Specification s => PrettyPrec1 (TermChk s) Source #
Instance details Defined in Language.PTS.Term Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> TermChk s a -> PrettyM Doc Source #
Specification s => PrettyPrec1 (TermInf s) Source #
Instance details Defined in Language.PTS.Term Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> TermInf s a -> PrettyM Doc Source #
(Specification s, PrettyPrec err) => PrettyPrec1 (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> ValueElim err s a -> PrettyM Doc Source #
(Specification s, PrettyPrec err) => PrettyPrec1 (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> ValueIntro err s a -> PrettyM Doc Source #

ppp1 :: (PrettyPrec1 f, PrettyPrec a) => Prec -> f a -> PrettyM Doc Source #

Helper useful to define PrettyPrec in terms of PrettyPrec1.

Convience functons

prettyShow :: PrettyPrec a => a -> String Source #

prettyShowWith :: PrettyPrec a => Options () String -> a -> String Source #

prettyPut :: PrettyPrec a => a -> IO () Source #

prettyPutWith :: PrettyPrec a => Options () String -> a -> IO () Source #

Symbols

pppMarkSym :: Sym -> PrettyM Doc Source #

Mark symbol name as used, but print it as is

>>> prettyPut' $ pppMarkSym "x" <+> pppMarkSym "x" <+> pppFreshSym "x"
x x x₁

pppFreshSym :: Sym -> PrettyM Doc Source #

Generate fresh name.

>>> prettyPut' $ pppFreshSym "x" <+> pppFreshSym "x" <+> pppFreshSym "x"
x x₁ x₂

pppScopedSym :: Sym -> (Doc -> PrettyM a) -> PrettyM a Source #

Scoped name usage. See 'PrettyPrec

>>> prettyPut $ pppFreshSym "x" <+> pppParens True (pppScopedSym "x" (\x -> "\\" <> return x <> "...")) <+> pppFreshSym "x"
x (\x₁...) x₁

pppScopedIrrSym :: IrrSym -> (Doc -> PrettyM a) -> PrettyM a Source #

Combinators

The pretty-compact combinators wrapped in PrettyM.

pppChar :: Char -> PrettyM Doc Source #

pppText :: String -> PrettyM Doc Source #

pppIntegral :: Integral a => a -> PrettyM Doc Source #

pppIntegralSub :: Integral a => a -> PrettyM Doc Source #

(<+>) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc infixr 6 Source #

(</>) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc infixr 5 Source #

($$$) :: PrettyM Doc -> PrettyM Doc -> PrettyM Doc infixr 5 Source #

pppHsepPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc Source #

pppSepPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc Source #

pppCatPunctuated :: Doc -> [PrettyM Doc] -> PrettyM Doc Source #

pppColon :: PrettyM Doc Source #

pppComma_ :: Doc () Source #

pppHang :: Int -> PrettyM Doc -> PrettyM Doc -> PrettyM Doc Source #

Syntax

Combinators for different syntactical constructs.

pppApplication :: Prec -> PrettyM Doc -> [PrettyM Doc] -> PrettyM Doc Source #

Render application.

>>> prettyPut' $ pppApplication PrecDef "f" ["a", "b", "c", "d"]
f a b c d

>>> prettyPut' $ pppApplication PrecDef "f" ["aaaa", "bbbb", "cccc", "dddd"]
f aaaa
  bbbb
  cccc
  dddd

pppPi :: Prec -> [PPPi] -> PrettyM Doc -> PrettyM Doc Source #

Render (dependent) function space.

>>> prettyPut' $ pppPi PrecDef [PPPi "n" "Nat"] "Vec a n"
∏ (n : Nat) →
Vec a n

>>> prettyPut' $ pppPi PrecDef [PPPi "n" "Nat", PPForall "a"] "Vec a n"
∏ (n : Nat) →
∀ a →
Vec a n

>>> prettyPut' $ pppPi PrecDef [PPPi "n" "Nat", PPForall "a", PPArrow "Vec a n"] "r"
∏ (n : Nat) →
∀ a →
Vec a n →
r

>>> prettyPut' $ pppPi PrecDef [PPArrow (pppPi PrecPi [PPArrow "a"] "b"), PPArrow "a"] "b"
(a → b) → a → b

data PPPi Source #

Specifies how to print (function) types.

Constructors

PPPi Doc (PrettyM Doc)
PPForall Doc
PPArrow (PrettyM Doc)
PPSigma Doc (PrettyM Doc)
PPExists Doc

pppLambda :: Prec -> [Doc] -> PrettyM Doc -> PrettyM Doc Source #

Render lambda abstraction.

>>> prettyPut' $ pppLambda PrecDef [] "x"
x

>>> prettyPut' $ pppLambda PrecDef ["x", "y", "z"] "long body"
λ x y z →
    long body

pppAnnotation :: Prec -> PrettyM Doc -> PrettyM Doc -> PrettyM Doc Source #

Render type annotation.

pppAnnotationPi :: Prec -> PrettyM Doc -> [PPPi] -> PrettyM Doc -> PrettyM Doc Source #

Render type annotation with (possibly) pi-type.

>>> prettyPut' $ pppAnnotationPi PrecDef "x" [] "t"
x : t

>>> prettyPut' $ pppAnnotationPi PrecDef "f" [PPArrow (pppPi PrecPi [PPArrow "a"] "b"), PPArrow "a"] "b"
f : (a → b)
  → a
  → b

>>> prettyPut' $ pppAnnotationPi PrecDef "myfunc" [PPPi "n" "Nat", PPForall "a", PPArrow "Vec a n"] "r"
myfunc
    : ∏ (n : Nat)
    → ∀ a
    → Vec a n
    → r

Hadron

pppHadron :: Set Sym -> PrettyM Doc Source #

pppQuark :: Sym -> PrettyM Doc Source #

pppQuarkElim :: Prec -> IrrSym -> (Doc -> PrettyM Doc) -> Map Sym (PrettyM Doc) -> PrettyM Doc -> PrettyM Doc Source #

Precedence

data Prec Source #

Constructors

PrecDef
PrecAnn
PrecLambda
PrecPi
PrecApp

Instances

Eq Prec Source #
Instance details Defined in Language.PTS.Pretty Methods (==) :: Prec -> Prec -> Bool Source # (/=) :: Prec -> Prec -> Bool Source #
Ord Prec Source #
Instance details Defined in Language.PTS.Pretty Methods compare :: Prec -> Prec -> Ordering Source # (<) :: Prec -> Prec -> Bool Source # (<=) :: Prec -> Prec -> Bool Source # (>) :: Prec -> Prec -> Bool Source # (>=) :: Prec -> Prec -> Bool Source # max :: Prec -> Prec -> Prec Source # min :: Prec -> Prec -> Prec Source #
Show Prec Source #
Instance details Defined in Language.PTS.Pretty Methods showsPrec :: Int -> Prec -> ShowS Source # show :: Prec -> String Source # showList :: [Prec] -> ShowS Source #

predPrec :: Prec -> Prec Source #