public class LogicPrinter
extends java.lang.Object
The actual layouting/formatting is done using the
Layouter
class. The concrete syntax for
operators is given by an instance of NotationInfo
. The LogicPrinter
is responsible for the concrete layout, e.g. how terms with infix
operators are indented, and it binds the various needed components together.
NotationInfo
,
Notation
,
Layouter
Modifier and Type | Field and Description |
---|---|
static int |
DEFAULT_LINE_WIDTH
The default and minimal value of the max.
|
protected Layouter |
layouter
This chooses the layout.
|
protected NotationInfo |
notationInfo
Contains information on the concrete syntax of operators.
|
protected Services |
services
the services object
|
Constructor and Description |
---|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Backend backend,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services)
Creates a LogicPrinter.
|
LogicPrinter(ProgramPrinter prgPrinter,
NotationInfo notationInfo,
Services services,
boolean purePrint)
Creates a LogicPrinter.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
escapeHTML(java.lang.String text,
boolean escapeWhitespace)
escapes special characters by their HTML encoding
|
protected HeapLDT |
getHeapLDT() |
InitialPositionTable |
getInitialPositionTable()
returns the PositionTable representing position information on the sequent of
this LogicPrinter.
|
SVInstantiations |
getInstantiations() |
protected Layouter |
getLayouter()
Returns the Layouter
|
NotationInfo |
getNotationInfo() |
PositionTable |
getPositionTable()
returns the PositionTable representing position information on the sequent of
this LogicPrinter.
|
protected ImmutableArray<TermLabel> |
getVisibleTermLabels(Term t)
Determine the Set of labels that will be printed out for a specific
Term . |
protected Layouter |
mark(de.uka.ilkd.key.pp.LogicPrinter.MarkType type) |
protected Layouter |
mark(de.uka.ilkd.key.pp.LogicPrinter.MarkType type,
int parameter) |
protected void |
markEndJavaBlock()
Called after java block is printed and marks current position.
|
protected void |
markEndKeyword()
Called after keyword is printed and marks current position.
|
protected void |
markEndSub()
Called after a substring is printed that has its own entry in a position
table.
|
protected void |
markStartJavaBlock()
Called before java block is printed and marks current position.
|
protected void |
markStartKeyword()
Called before keyword is printed and marks current position.
|
protected void |
markStartSub()
Called before a substring is printed that has its own entry in a position
table.
|
protected void |
markStartSub(int subterm)
TODO
|
protected void |
maybeParens(Term t,
int ass)
Prints a subterm, if needed with parentheses.
|
protected void |
printAddProgVars(ImmutableSet<SchemaVariable> apv) |
protected void |
printAttribs(Taclet taclet) |
void |
printCast(java.lang.String pre,
java.lang.String post,
Term t,
int ass) |
void |
printClassName(java.lang.String className) |
void |
printConstant(java.lang.String s)
Print a constant.
|
void |
printConstant(Term t,
java.lang.String s)
Print a constant.
|
void |
printConstrainedFormula(SequentFormula cfma)
Pretty-prints a constrained formula.
|
protected void |
printDisplayName(Taclet taclet) |
void |
printElementaryUpdate(java.lang.String asgn,
Term t,
int ass2)
Print an elementary update.
|
void |
printElementOf(Term t) |
void |
printElementOf(Term t,
java.lang.String symbol) |
protected boolean |
printEmbeddedHeapConstructorTerm(Term t) |
protected void |
printEmbeddedObserver(Term heapTerm,
Term objectTerm) |
protected void |
printFind(Taclet taclet) |
void |
printFunctionTerm(Term t)
Print a term in
f(t1,...tn) style. |
protected void |
printGoalTemplate(TacletGoalTemplate tgt) |
protected void |
printGoalTemplates(Taclet taclet) |
void |
printHeapConstructor(Term t,
boolean closingBrace) |
protected void |
printHeuristic(RuleSet sv) |
protected void |
printHeuristics(Taclet taclet) |
void |
printIfThenElseTerm(Term t,
java.lang.String keyword) |
void |
printInfixTerm(Term l,
int assLeft,
java.lang.String name,
Term t,
Term r,
int assRight)
Print a binary term in infix style.
|
void |
printInfixTermContinuingBlock(Term l,
int assLeft,
java.lang.String name,
Term t,
Term r,
int assRight)
Print a binary term in infix style, continuing a containing block.
|
boolean |
printInShortForm(java.lang.String programName,
Sort sort)
tests if the program name together with the prefix sort determines the
attribute in a unique way
|
static boolean |
printInShortForm(java.lang.String programName,
Sort sort,
Services services)
tests if the program name together with the prefix sort determines the
attribute in a unique way
|
boolean |
printInShortForm(java.lang.String attributeProgramName,
Term t)
returns true if an attribute term shall be printed in short form.
|
void |
printJavaBlock(JavaBlock j)
Print a Java block.
|
void |
printLabels(Term t) |
void |
printModalityTerm(java.lang.String left,
JavaBlock jb,
java.lang.String right,
Term phi,
int ass)
Print a DL modality formula.
|
protected void |
printNewVarcond(NewVarcond sv) |
protected void |
printNotFreeIn(NotFreeIn sv) |
void |
printObserver(Term t,
Term tacitHeap) |
void |
printParallelUpdate(java.lang.String separator,
Term t,
int ass) |
void |
printPostfix(Term t,
java.lang.String postfix) |
void |
printPostfixTerm(Term t,
int ass,
java.lang.String name)
Print a unary term in postfix style.
|
void |
printPrefixTerm(java.lang.String name,
Term t,
Term sub,
int ass)
Print a unary term in prefix style.
|
void |
printProgramElement(ProgramElement pe)
Pretty-prints a ProgramElement.
|
void |
printProgramSV(ProgramSV pe)
Pretty-prints a ProgramSV.
|
void |
printProgramVariable(ProgramVariable pv)
Pretty-Prints a ProgramVariable in the logic, not in Java blocks.
|
void |
printQuantifierTerm(java.lang.String name,
ImmutableArray<QuantifiableVariable> vars,
Term phi,
int ass)
Print a quantified term.
|
protected void |
printRewrite(Term t) |
protected void |
printRewriteAttributes(RewriteTaclet taclet) |
protected void |
printRules(ImmutableList<Taclet> rules) |
protected void |
printSchemaVariable(SchemaVariable sv) |
void |
printSelect(Term t,
Term tacitHeap) |
void |
printSemisequent(ImmutableList<SequentPrintFilterEntry> formulas) |
void |
printSemisequent(Semisequent semiseq)
Pretty-prints a Semisequent.
|
void |
printSeqGet(Term t) |
void |
printSeqSingleton(Term t,
java.lang.String lDelimiter,
java.lang.String rDelimiter) |
void |
printSequent(Sequent seq)
Pretty-print a sequent.
|
void |
printSequent(Sequent seq,
boolean finalbreak) |
void |
printSequent(SequentPrintFilter filter)
Pretty-print a sequent.
|
void |
printSequent(SequentPrintFilter filter,
boolean finalbreak) |
protected void |
printSequentArrow() |
void |
printSingleton(Term t) |
void |
printStore(Term t,
boolean closingBrace) |
void |
printSubstTerm(java.lang.String l,
QuantifiableVariable v,
Term t,
int ass2,
java.lang.String r,
Term phi,
int ass3)
Print a substitution term.
|
void |
printTaclet(Taclet taclet)
Pretty-print a taclet.
|
void |
printTaclet(Taclet taclet,
SVInstantiations sv,
boolean showWholeTaclet,
boolean declareSchemaVars)
Pretty-print a taclet.
|
void |
printTerm(ImmutableSet<Term> terms)
Pretty-prints a set of terms.
|
void |
printTerm(Term t)
Pretty-prints a term or formula.
|
void |
printTermContinuingBlock(Term t)
Pretty-prints a term or formula in the same block.
|
protected void |
printTextSequent(Sequent seq,
java.lang.String text,
boolean frontbreak) |
void |
printUpdateApplicationTerm(java.lang.String l,
java.lang.String r,
Term t,
int ass3)
Print a term with an update.
|
protected void |
printVarCond(Taclet taclet) |
protected void |
printVariableCondition(VariableCondition sv) |
ProgramPrinter |
programPrinter()
Returns the ProgramPrinter
|
static java.lang.String |
quickPrintSemisequent(Semisequent s,
Services services)
Converts a semisequent to a string.
|
static java.lang.String |
quickPrintSequent(Sequent s,
Services services)
Converts a sequent to a string.
|
static java.lang.String |
quickPrintTerm(Term t,
Services services)
Converts a term to a string.
|
static java.lang.String |
quickPrintTerm(Term t,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols)
Converts a term to a string.
|
void |
reset()
Resets the Backend, the Layouter and (if applicable) the ProgramPrinter of
this Object.
|
java.lang.StringBuffer |
result()
Returns the pretty-printed sequent in a StringBuffer.
|
void |
setInstantiation(SVInstantiations instantiations)
sets instantiations of schema variables
|
int |
setLineWidth(int lineWidth)
sets the line width to the new value but does not reprint the
sequent.
|
protected void |
startTerm(int size)
Start a term with subterms.
|
java.lang.String |
toString()
Returns the pretty-printed sequent.
|
void |
update(SequentPrintFilter filter,
int lineWidth)
Reprints the sequent.
|
public static final int DEFAULT_LINE_WIDTH
protected final NotationInfo notationInfo
protected final Services services
protected Layouter layouter
public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Backend backend, Services services, boolean purePrint)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxbackend
- the Backend for the outputservices
- services.purePrint
- if true the PositionTable will not be calculated
(simulates the behaviour of the former
PureSequentPrinter)public LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxservices
- The Services objectpublic LogicPrinter(ProgramPrinter prgPrinter, NotationInfo notationInfo, Services services, boolean purePrint)
prgPrinter
- the ProgramPrinter that pretty-prints Java programsnotationInfo
- the NotationInfo for the concrete syntaxpurePrint
- if true the PositionTable will not be calculated
(simulates the behaviour of the former
PureSequentPrinter)services
- the Services objectpublic static java.lang.String quickPrintTerm(Term t, Services services)
t
- a term.services
- services.public static java.lang.String quickPrintTerm(Term t, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
t
- a term.services
- services.usePrettyPrinting
- whether or not to use pretty-printing.useUnicodeSymbols
- whether or not to use unicode symbols.public static java.lang.String quickPrintSemisequent(Semisequent s, Services services)
s
- a semisequent.services
- services.public static java.lang.String quickPrintSequent(Sequent s, Services services)
s
- a sequent.services
- services.public NotationInfo getNotationInfo()
public void reset()
public int setLineWidth(int lineWidth)
DEFAULT_LINE_WIDTH
and the given valuelineWidth
- the max. number of character to put on one linepublic void update(SequentPrintFilter filter, int lineWidth)
filter
- The SequentPrintFilter for seqlineWidth
- the max. number of character to put on one line (the actual
taken linewidth is the max of
DEFAULT_LINE_WIDTH
and the given valuepublic void setInstantiation(SVInstantiations instantiations)
public void printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet, boolean declareSchemaVars)
taclet
- The Taclet to be pretty-printed.sv
- The instantiations of the SchemaVariablesshowWholeTaclet
- Should the find, varcond and heuristic part be
pretty-printed?declareSchemaVars
- Should declarations for the schema variables used in
the taclet be pretty-printed?public void printTaclet(Taclet taclet)
taclet
- The Taclet to be pretty-printed.protected HeapLDT getHeapLDT()
protected void printAttribs(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printDisplayName(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printRewriteAttributes(RewriteTaclet taclet) throws java.io.IOException
java.io.IOException
protected void printVarCond(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printNewVarcond(NewVarcond sv) throws java.io.IOException
java.io.IOException
protected void printNotFreeIn(NotFreeIn sv) throws java.io.IOException
java.io.IOException
protected void printVariableCondition(VariableCondition sv) throws java.io.IOException
java.io.IOException
protected void printHeuristics(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printHeuristic(RuleSet sv) throws java.io.IOException
java.io.IOException
protected void printFind(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printTextSequent(Sequent seq, java.lang.String text, boolean frontbreak) throws java.io.IOException
java.io.IOException
protected void printGoalTemplates(Taclet taclet) throws java.io.IOException
java.io.IOException
protected void printGoalTemplate(TacletGoalTemplate tgt) throws java.io.IOException
java.io.IOException
protected void printRules(ImmutableList<Taclet> rules) throws java.io.IOException
java.io.IOException
protected void printAddProgVars(ImmutableSet<SchemaVariable> apv) throws java.io.IOException
java.io.IOException
protected void printSchemaVariable(SchemaVariable sv) throws java.io.IOException
java.io.IOException
public void printProgramElement(ProgramElement pe) throws java.io.IOException
pe
- You've guessed it, the ProgramElement to be pretty-printedjava.io.IOException
public void printProgramVariable(ProgramVariable pv) throws java.io.IOException
pv
- The ProgramVariable in the logicjava.io.IOException
public void printProgramSV(ProgramSV pe) throws java.io.IOException
pe
- the ProgramSV to be pretty-printed.java.io.IOException
- if the ProgramSV cannot be printed.protected void printRewrite(Term t) throws java.io.IOException
java.io.IOException
public void printSequent(SequentPrintFilter filter, boolean finalbreak)
public void printSequent(Sequent seq, boolean finalbreak)
public void printSequent(SequentPrintFilter filter)
=>
.
If the sequent doesn't fit in one line, a line break is inserted after each
formula, the sequent arrow is on a line of its own, and formulae are indented
w.r.t. the arrow. A line-break is printed after the Sequent.filter
- The SequentPrintFilter for seqpublic void printSequent(Sequent seq)
=>
.
If the sequent doesn't fit in one line, a line break is inserted after each
formula, the sequent arrow is on a line of its own, and formulae are indented
w.r.t. the arrow. A line-break is printed after the Sequent. No filtering is
done.seq
- The Sequent to be pretty-printedpublic void printSemisequent(Semisequent semiseq) throws java.io.IOException
semiseq
- the semisequent to be printedjava.io.IOException
- if the semisequent cannot be printed.public void printSemisequent(ImmutableList<SequentPrintFilterEntry> formulas) throws java.io.IOException
java.io.IOException
public void printConstrainedFormula(SequentFormula cfma) throws java.io.IOException
cfma
- the constrained formula to be printedjava.io.IOException
- if the formula cannot be printed.public void printTerm(Term t) throws java.io.IOException
t
- the Term to be printedjava.io.IOException
- if the term cannot be printed.protected ImmutableArray<TermLabel> getVisibleTermLabels(Term t)
Term
. The class SequentViewLogicPrinter
overrides this
method. TermLabel
visibility can be configured via GUI, see
TermLabelMenu
. Default is to print all
TermLabels.public void printLabels(Term t) throws java.io.IOException
java.io.IOException
public void printTerm(ImmutableSet<Term> terms) throws java.io.IOException
terms
- the terms to be printedjava.io.IOException
public void printTermContinuingBlock(Term t) throws java.io.IOException
a & (b
& c)
would print a & b & c
, omitting the
redundant parentheses. The subformula b & c
is printed using
this method to get a layout of
a & b & cinstead of
a & b & c
t
- the Term to be printedjava.io.IOException
public void printFunctionTerm(Term t) throws java.io.IOException
f(t1,...tn)
style. If the operator has arity 0,
no parentheses are printed, i.e. f
instead of f()
.
If the term doesn't fit on one line, t2...tn
are aligned below
t1
.t
- the term to be printed.java.io.IOException
public void printCast(java.lang.String pre, java.lang.String post, Term t, int ass) throws java.io.IOException
java.io.IOException
protected boolean printEmbeddedHeapConstructorTerm(Term t) throws java.io.IOException
java.io.IOException
public void printClassName(java.lang.String className) throws java.io.IOException
java.io.IOException
public void printHeapConstructor(Term t, boolean closingBrace) throws java.io.IOException
java.io.IOException
protected void printEmbeddedObserver(Term heapTerm, Term objectTerm) throws java.io.IOException
java.io.IOException
public void printSelect(Term t, Term tacitHeap) throws java.io.IOException
java.io.IOException
public void printStore(Term t, boolean closingBrace) throws java.io.IOException
java.io.IOException
public void printSeqGet(Term t) throws java.io.IOException
java.io.IOException
public void printPostfix(Term t, java.lang.String postfix) throws java.io.IOException
java.io.IOException
public void printObserver(Term t, Term tacitHeap) throws java.io.IOException
java.io.IOException
public void printSingleton(Term t) throws java.io.IOException
java.io.IOException
public void printSeqSingleton(Term t, java.lang.String lDelimiter, java.lang.String rDelimiter) throws java.io.IOException
java.io.IOException
public void printElementOf(Term t) throws java.io.IOException
java.io.IOException
public void printElementOf(Term t, java.lang.String symbol) throws java.io.IOException
java.io.IOException
public void printPrefixTerm(java.lang.String name, Term t, Term sub, int ass) throws java.io.IOException
!a
. No line
breaks are possible.name
- the prefix operatort
- whole termsub
- the subterm to be printedass
- the associativity for the subtermjava.io.IOException
- if the term cannot be printed.public void printPostfixTerm(Term t, int ass, java.lang.String name) throws java.io.IOException
t.a
, where
.a
is the postfix operator. No line breaks are possible.name
- the postfix operatort
- the subterm to be printedass
- the associativity for the subtermjava.io.IOException
- if the term cannot be printed.public void printInfixTerm(Term l, int assLeft, java.lang.String name, Term t, Term r, int assRight) throws java.io.IOException
p
& q
, where &
is the infix operator. If line
breaks are necessary, the format is like
p & qThe subterms are printed using
printTermContinuingBlock(Term)
.l
- the left subtermassLeft
- associativity for left subtermname
- the infix operatort
- whole termr
- the right subtermassRight
- associativity for right subtermjava.io.IOException
- if the term cannot be printed.public void printInfixTermContinuingBlock(Term l, int assLeft, java.lang.String name, Term t, Term r, int assRight) throws java.io.IOException
printTermContinuingBlock(Term)
for the idea. Otherwise like
#printInfixTerm(Term,int,String,Term,int)
.l
- the left subtermassLeft
- associativity for left subtermname
- the infix operatort
- whole termr
- the right subtermassRight
- associativity for right subtermjava.io.IOException
- if the term cannot be printed.public void printUpdateApplicationTerm(java.lang.String l, java.lang.String r, Term t, int ass3) throws java.io.IOException
{u} t
. If line
breaks are necessary, the format is
{u} t
l
- the left bracer
- the right bracet
- the update termass3
- associativity for phijava.io.IOException
- if the term cannot be printed.public void printElementaryUpdate(java.lang.String asgn, Term t, int ass2) throws java.io.IOException
loc := val
asgn
- the assignment operator (including spaces)ass2
- associativity for the new valuesjava.io.IOException
- if the term cannot be printed.public void printParallelUpdate(java.lang.String separator, Term t, int ass) throws java.io.IOException
java.io.IOException
public void printIfThenElseTerm(Term t, java.lang.String keyword) throws java.io.IOException
java.io.IOException
public void printSubstTerm(java.lang.String l, QuantifiableVariable v, Term t, int ass2, java.lang.String r, Term phi, int ass3) throws java.io.IOException
{var/t}s
. If line
breaks are necessary, the format is
{var/t} s
l
- the String used as left brace symbolv
- the QuantifiableVariable
to be substitutedt
- the Term to be used as new valueass2
- the int defining the associativity for the new valuer
- the String used as right brace symbolphi
- the substituted term/formulaass3
- the int defining the associativity for phijava.io.IOException
public void printQuantifierTerm(java.lang.String name, ImmutableArray<QuantifiableVariable> vars, Term phi, int ass) throws java.io.IOException
all x:s.phi
.
If line breaks are necessary, the format is
all x:s. phiNote that the parameter
var
has to contain the variable name
with colon and sort.name
- the name of the quantifiervars
- the quantified variables (+colon and sort)phi
- the quantified formulaass
- associativity for phijava.io.IOException
public void printConstant(java.lang.String s) throws java.io.IOException
s
and marks it as
a nullary term.s
- the constantjava.io.IOException
public void printConstant(Term t, java.lang.String s) throws java.io.IOException
s
and marks it as
a nullary term.t
- constant as term to be printeds
- name of the constantjava.io.IOException
- in case the layout printing failspublic void printJavaBlock(JavaBlock j) throws java.io.IOException
j
- the Java block to be printedjava.io.IOException
public void printModalityTerm(java.lang.String left, JavaBlock jb, java.lang.String right, Term phi, int ass) throws java.io.IOException
phi
is the whole modality formula,
not just the subformula inside the modality. Normally, this looks like
<Program>psi
, where psi = phi.sub(0)
. No line
breaks are inserted, as the program itself is always broken. In case of a
program modality with arity greater than 1, the subformulae are listed
between parens, like <Program>(psi1,psi2)
java.io.IOException
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.StringBuffer result()
protected Layouter mark(de.uka.ilkd.key.pp.LogicPrinter.MarkType type)
protected Layouter mark(de.uka.ilkd.key.pp.LogicPrinter.MarkType type, int parameter)
public PositionTable getPositionTable()
public InitialPositionTable getInitialPositionTable()
public ProgramPrinter programPrinter()
protected Layouter getLayouter()
protected void maybeParens(Term t, int ass) throws java.io.IOException
If prio and associativity are equal, the subterm is printed using
printTermContinuingBlock(Term)
. This currently only makes a
difference for infix operators.
t
- the the subterm to printass
- the associativity for this subtermjava.io.IOException
protected void printSequentArrow() throws java.io.IOException
java.io.IOException
public SVInstantiations getInstantiations()
protected void markStartSub()
protected void markStartSub(int subterm)
protected void markEndSub()
protected void markStartKeyword()
protected void markStartJavaBlock()
protected void markEndJavaBlock()
protected void markEndKeyword()
protected void startTerm(int size)
size
- the number of rows of the new position tablepublic boolean printInShortForm(java.lang.String attributeProgramName, Term t)
attributeProgramName
- the String of the attribute's program namet
- the Term used as reference prefixpublic boolean printInShortForm(java.lang.String programName, Sort sort)
programName
- the String denoting the program name of the attributesort
- the ObjectSort in whose reachable hierarchy we test for
uniquenesspublic static java.lang.String escapeHTML(java.lang.String text, boolean escapeWhitespace)
text
- the String to be displayed as part of an HTML sidepublic static boolean printInShortForm(java.lang.String programName, Sort sort, Services services)
programName
- the String denoting the program name of the attributesort
- the ObjectSort specifying the hierarchy where to test for
uniquenessservices
- the Services class used to access the type hierarchyCopyright © 2003-2019 The KeY-Project.