PrintHOL

label :: Int	Line label
newLn :: Bool	If true, then we're on a new line. Note: binary operators are always on a new line; this tells us whether some other sentence or term is on its own line.
unOp :: Int	How many negations we've seen
absInd :: Int	Indentation after label stuff. Where the line begins.
relInd :: Int	Relative indentation (from last operator)
defaultInd :: Int	Default indendtation (up to the longest label of a formula)
prevSameBinOp :: Bool	Was this binary operator the argument to the same binary operator? (If so, we don't indent.)
splitArgs :: Bool	True: put args to functions & predicates on their own line. The number is the length of the identifier, plus other args and identifiers, up to this term.
innerTerm :: Bool	Is this term inside another term? (The only case in which it is not is if it is an argument to = .)
showLabels :: Bool	Show labels? This is only for whether labels should currently be suppressed (e.g., in let defs). For no labels at all, we set a global flag.
noLabels :: Bool	Are we showing labels at all (or are they globally suppressed)?

mkinitEnv :: Flags -> Env

The initial environment.

resetEnv :: Env -> Env

Resets the environment except for the default indentation (from the length of the longest label).

printTree :: Print a => a -> Flags -> String

type Doc = [ShowS] -> [ShowS]

doc :: ShowS -> Doc

render :: Doc -> String

Takes the final Doc and returns the output. Ideally, the Doc should be considered the logical structure of the pretty-printed formula and the render assigns concrete syntax.

concatS :: [ShowS] -> ShowS

concatD :: [Doc] -> Doc

replicateS :: Int -> ShowS -> ShowS

spaces :: Int -> ShowS

type EnvT = Reader Env Doc

prtList :: Print a => [a] -> [Env] -> [Doc]

class Print a where

The Print class. Each constructor of the grammar instantiates this. The prt function tells how to pretty-print each construct.

Methods

prt :: a -> EnvT

Instances

Print Char

Print Double

Print Int

Print Integer

mkEsc :: Char -> Char -> ShowS

Escape characters for rendering.

maxLabels :: [SENT] -> Env -> [Env]

intersperseTerms :: Env -> [TERM] -> [Doc]

For a list of terms, we intersperse the argument separator string.

binOpDoc :: Env -> SENT -> SENT -> String -> Int -> (SENT -> Bool) -> Doc

Returns the String to bring for binary operator sentences.

quantDoc :: Env -> [TERM] -> SENT -> String -> Int -> (SENT -> Bool) -> Doc

Returns the String to print for a forall/exists sentence.

ifDoc :: Env -> SENT -> SENT -> SENT -> Doc

Returns the string to print for if-then-else sentences.

ifEnv

:: Env
-> Int	length of ifTab
-> Int	extra space needed because if is shorter than then and else
-> Int	operand label
-> Env
New environment for the second argument to a binary operator.

letDoc :: Env -> [DEF] -> SENT -> Doc

Returns the doc for let [defs] in SENT. [DEF] should be nonempty.

letEnv

:: Env
-> Int	length of letTab
-> Int	extra space needed because let is longer than in
-> Bool	whether labels should be shown or suppressed
-> Env

notEnv :: Env -> Int -> Bool -> Env

argSeparators :: Env -> Doc

Takes an environment and returns separators (default is commas) for between lists of variables, terms, etc. and if necessary, it inserts linebreak commands. The Doc returned is interspersed into the list of of variables or terms.

nextLnArgs :: Env -> Doc

Puts either args or curried arguments on the next line with the right indenting.

newSplit :: [TERM] -> Bool

Are the args long enough that we have to split them, or is there a curried function that is a term?

curriedTerm :: [TERM] -> Bool

maxArg :: [TERM] -> Int

termStrLens :: TERM -> Int

numApp

:: Bool	are labels currently suppressed (e.g., in let...in statements).
-> Int	depth
-> Int	which operand
-> Int

showLabel :: Env -> ShowS

predIdLen :: PredId -> Int

functIdLen :: FunctId -> Int

absIndUp :: Env -> Int -> Int

Absolute indentation (for splitting across lines and not splitting).

andSent :: SENT -> Bool

orSent :: SENT -> Bool

impSent :: SENT -> Bool

forallSent :: SENT -> Bool

existsSent :: SENT -> Bool

binEnv1

:: Env
-> Int
-> Bool	is the same operator as we've just seen, so no indentation
-> Int	label
-> Env
Returns the new environment for the first argument to a binary operator.

binEnv2 :: Env -> Int -> Bool -> Int -> Env

Returns the new environment for second argument to a binary operator (see documentation for binEnv1).

checkUnOpArg :: SENT -> String -> Doc

If the next sentence to parse is a binary operator sentence, then don't do anything the not will printed with the next sentence. Otherwise, just do the indenting.

checkQuant :: SENT -> Bool

True if there is a sequence of not sentences followed by a quantified sentence.

checkBinOp :: SENT -> Bool

True if there is a sequence of negated sentences followed by a binary operator sentence.

negInd :: Env -> SENT -> Doc

quantEnv1 :: Env -> Int -> Bool -> Int -> Env

relUpdate

:: Int
-> Int	i==0 menas the environment hasn't been indented yet.
-> Int
If the env has not been indented yet (i==0), then just update according to the operator's tab width (j); otherwise add the old relative indent, the new tab, and an extra space between the strings.

simpInd :: Env -> Doc

Indentation for binary operator sentences.

upIndUnOp

:: Env
-> Int	operator size
-> Int
Returns an absolute indentation depending on the operator size and whether there is a preceding unary operator. Does not indent for operators of the same kind (so there's no precedence to record).

quantOpInd :: Env -> String -> Doc

binaryOpInd :: Env -> String -> Doc

If we're inside a not sentence, then put this sentence right after the nots.

computeSpcs

:: Bool	are there labels
-> Int	spaces before separator
-> Int	spaces after separator
-> ShowS
Compute spaces from beginning of line.

labelInd :: Env -> ShowS

Returns the indentation for directly after a label.

Produced by Haddock version 2.4.1