net.sourceforge.czt.print.zeves

Class ZEvesPrintVisitor

java.lang.Object

net.sourceforge.czt.parser.util.AbstractVisitor<R>

net.sourceforge.czt.print.z.AbstractPrintVisitor<Object>

net.sourceforge.czt.print.z.ZPrintVisitor

net.sourceforge.czt.print.zeves.ZEvesPrintVisitor

All Implemented Interfaces:

net.sourceforge.czt.base.visitor.ListTermVisitor<Object>, net.sourceforge.czt.base.visitor.TermVisitor<Object>, ApplicationVisitor<Object>, OperatorApplicationVisitor<Object>, PrintExpressionVisitor<Object>, PrintParagraphVisitor<Object>, PrintPredicateVisitor<Object>, PrintPropertiesKeys, net.sourceforge.czt.util.Visitor<Object>, net.sourceforge.czt.z.visitor.AndExprVisitor<Object>, net.sourceforge.czt.z.visitor.AndPredVisitor<Object>, net.sourceforge.czt.z.visitor.ApplExprVisitor<Object>, net.sourceforge.czt.z.visitor.AxParaVisitor<Object>, net.sourceforge.czt.z.visitor.BindExprVisitor<Object>, net.sourceforge.czt.z.visitor.BindSelExprVisitor<Object>, net.sourceforge.czt.z.visitor.BranchVisitor<Object>, net.sourceforge.czt.z.visitor.CompExprVisitor<Object>, net.sourceforge.czt.z.visitor.CondExprVisitor<Object>, net.sourceforge.czt.z.visitor.ConjParaVisitor<Object>, net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>, net.sourceforge.czt.z.visitor.DecorExprVisitor<Object>, net.sourceforge.czt.z.visitor.DirectiveVisitor<Object>, net.sourceforge.czt.z.visitor.Exists1ExprVisitor<Object>, net.sourceforge.czt.z.visitor.Exists1PredVisitor<Object>, net.sourceforge.czt.z.visitor.ExistsExprVisitor<Object>, net.sourceforge.czt.z.visitor.ExistsPredVisitor<Object>, net.sourceforge.czt.z.visitor.ExprPredVisitor<Object>, net.sourceforge.czt.z.visitor.FalsePredVisitor<Object>, net.sourceforge.czt.z.visitor.ForallExprVisitor<Object>, net.sourceforge.czt.z.visitor.ForallPredVisitor<Object>, net.sourceforge.czt.z.visitor.FreeParaVisitor<Object>, net.sourceforge.czt.z.visitor.FreetypeVisitor<Object>, net.sourceforge.czt.z.visitor.GenericTypeVisitor<Object>, net.sourceforge.czt.z.visitor.GenParamTypeVisitor<Object>, net.sourceforge.czt.z.visitor.GivenParaVisitor<Object>, net.sourceforge.czt.z.visitor.GivenTypeVisitor<Object>, net.sourceforge.czt.z.visitor.HideExprVisitor<Object>, net.sourceforge.czt.z.visitor.IffExprVisitor<Object>, net.sourceforge.czt.z.visitor.IffPredVisitor<Object>, net.sourceforge.czt.z.visitor.ImpliesExprVisitor<Object>, net.sourceforge.czt.z.visitor.ImpliesPredVisitor<Object>, net.sourceforge.czt.z.visitor.InclDeclVisitor<Object>, net.sourceforge.czt.z.visitor.InStrokeVisitor<Object>, net.sourceforge.czt.z.visitor.LambdaExprVisitor<Object>, net.sourceforge.czt.z.visitor.LatexMarkupParaVisitor<Object>, net.sourceforge.czt.z.visitor.LetExprVisitor<Object>, net.sourceforge.czt.z.visitor.LocAnnVisitor<Object>, net.sourceforge.czt.z.visitor.MemPredVisitor<Object>, net.sourceforge.czt.z.visitor.MuExprVisitor<Object>, net.sourceforge.czt.z.visitor.NameSectTypeTripleVisitor<Object>, net.sourceforge.czt.z.visitor.NameTypePairVisitor<Object>, net.sourceforge.czt.z.visitor.NarrParaVisitor<Object>, net.sourceforge.czt.z.visitor.NarrSectVisitor<Object>, net.sourceforge.czt.z.visitor.NegExprVisitor<Object>, net.sourceforge.czt.z.visitor.NegPredVisitor<Object>, net.sourceforge.czt.z.visitor.NewOldPairVisitor<Object>, net.sourceforge.czt.z.visitor.NextStrokeVisitor<Object>, net.sourceforge.czt.z.visitor.NumExprVisitor<Object>, net.sourceforge.czt.z.visitor.NumStrokeVisitor<Object>, net.sourceforge.czt.z.visitor.OperandVisitor<Object>, net.sourceforge.czt.z.visitor.OperatorVisitor<Object>, net.sourceforge.czt.z.visitor.OptempParaVisitor<Object>, net.sourceforge.czt.z.visitor.OrExprVisitor<Object>, net.sourceforge.czt.z.visitor.OrPredVisitor<Object>, net.sourceforge.czt.z.visitor.OutStrokeVisitor<Object>, net.sourceforge.czt.z.visitor.ParenAnnVisitor<Object>, net.sourceforge.czt.z.visitor.ParentVisitor<Object>, net.sourceforge.czt.z.visitor.PipeExprVisitor<Object>, net.sourceforge.czt.z.visitor.PowerExprVisitor<Object>, net.sourceforge.czt.z.visitor.PowerTypeVisitor<Object>, net.sourceforge.czt.z.visitor.PreExprVisitor<Object>, net.sourceforge.czt.z.visitor.ProdExprVisitor<Object>, net.sourceforge.czt.z.visitor.ProdTypeVisitor<Object>, net.sourceforge.czt.z.visitor.ProjExprVisitor<Object>, net.sourceforge.czt.z.visitor.RefExprVisitor<Object>, net.sourceforge.czt.z.visitor.RenameExprVisitor<Object>, net.sourceforge.czt.z.visitor.SchemaTypeVisitor<Object>, net.sourceforge.czt.z.visitor.SchExprVisitor<Object>, net.sourceforge.czt.z.visitor.SectTypeEnvAnnVisitor<Object>, net.sourceforge.czt.z.visitor.SetCompExprVisitor<Object>, net.sourceforge.czt.z.visitor.SetExprVisitor<Object>, net.sourceforge.czt.z.visitor.SignatureAnnVisitor<Object>, net.sourceforge.czt.z.visitor.SignatureVisitor<Object>, net.sourceforge.czt.z.visitor.SpecVisitor<Object>, net.sourceforge.czt.z.visitor.ThetaExprVisitor<Object>, net.sourceforge.czt.z.visitor.TruePredVisitor<Object>, net.sourceforge.czt.z.visitor.TupleExprVisitor<Object>, net.sourceforge.czt.z.visitor.TupleSelExprVisitor<Object>, net.sourceforge.czt.z.visitor.TypeAnnVisitor<Object>, net.sourceforge.czt.z.visitor.UnparsedParaVisitor<Object>, net.sourceforge.czt.z.visitor.UnparsedZSectVisitor<Object>, net.sourceforge.czt.z.visitor.VarDeclVisitor<Object>, net.sourceforge.czt.z.visitor.ZBranchListVisitor<Object>, net.sourceforge.czt.z.visitor.ZDeclListVisitor<Object>, net.sourceforge.czt.z.visitor.ZExprListVisitor<Object>, net.sourceforge.czt.z.visitor.ZFreetypeListVisitor<Object>, net.sourceforge.czt.z.visitor.ZNameListVisitor<Object>, net.sourceforge.czt.z.visitor.ZNameVisitor<Object>, net.sourceforge.czt.z.visitor.ZNumeralVisitor<Object>, net.sourceforge.czt.z.visitor.ZParaListVisitor<Object>, net.sourceforge.czt.z.visitor.ZRenameListVisitor<Object>, net.sourceforge.czt.z.visitor.ZSchTextVisitor<Object>, net.sourceforge.czt.z.visitor.ZSectVisitor<Object>, net.sourceforge.czt.z.visitor.ZStrokeListVisitor<Object>, net.sourceforge.czt.z.visitor.ZVisitor<Object>, ApplyCommandVisitor<Object>, CaseAnalysisCommandVisitor<Object>, InstantiationListVisitor<Object>, InstantiationVisitor<Object>, NormalizationCommandVisitor<Object>, ProofCommandInfoListVisitor<Object>, ProofCommandInfoVisitor<Object>, ProofCommandListVisitor<Object>, ProofScriptVisitor<Object>, ProofTypeVisitor<Object>, QuantifiersCommandVisitor<Object>, SimplificationCommandVisitor<Object>, SorryCommandVisitor<Object>, SubstitutionCommandVisitor<Object>, UseCommandVisitor<Object>, WithCommandVisitor<Object>, ZEvesLabelVisitor<Object>, ZEvesNoteVisitor<Object>, ZEvesVisitor<Object>

public class ZEvesPrintVisitor
extends ZPrintVisitor
implements ZEvesVisitor<Object>, net.sourceforge.czt.z.visitor.RenameExprVisitor<Object>, net.sourceforge.czt.z.visitor.BindExprVisitor<Object>, net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>

An Circus visitor used for printing.

Author:

Petra Malik, Leo Freitas

Nested Class Summary

Nested classes/interfaces inherited from class net.sourceforge.czt.print.z.ZPrintVisitor

ZPrintVisitor.Utils, ZPrintVisitor.UtilsImpl

Field Summary

Fields inherited from class net.sourceforge.czt.print.z.ZPrintVisitor

ref_

Fields inherited from interface net.sourceforge.czt.print.util.PrintPropertiesKeys

PROP_PRINT_NAME_IDS, PROP_PRINT_NAME_IDS_DEFAULT, PROP_PRINT_ZEVES, PROP_PRINT_ZEVES_DEFAULT, PROP_PRINTING_ONTHEFLY_SECTION_NAME, PROP_PRINTING_ONTHEFLY_SECTION_NAME_DEFAULT, PROP_PRINTING_STRUCTURED_GOAL, PROP_PRINTING_STRUCTURED_GOAL_DEFAULT, PROP_TXT_TAB_SIZE, PROP_TXT_TAB_SIZE_DEFAULT, PROP_TXT_WIDTH, PROP_TXT_WIDTH_DEFAULT

Constructor Summary

Constructors

Constructor and Description
ZEvesPrintVisitor(net.sourceforge.czt.session.SectionInfo si, ZPrinter printer, Properties properties, net.sourceforge.czt.z.util.WarningManager wm)
ZEvesPrintVisitor(net.sourceforge.czt.session.SectionInfo si, ZPrinter printer, net.sourceforge.czt.z.util.WarningManager wm) Creates a new Object-Z print visitor.

Method Summary

Modifier and Type	Method and Description
protected net.sourceforge.czt.z.util.WarningManager	getWarningManager()
protected void	print(Token token)
Object	visitApplyCommand(ApplyCommand term)
Object	visitBindExpr(net.sourceforge.czt.z.ast.BindExpr bindExpr)
Object	visitCaseAnalysisCommand(CaseAnalysisCommand term)
Object	visitConjPara(net.sourceforge.czt.z.ast.ConjPara conjPara)
Object	visitConstDecl(net.sourceforge.czt.z.ast.ConstDecl constDecl)
String	visitInstantiation(Instantiation term)
String	visitInstantiationList(InstantiationList term)
Object	visitNormalizationCommand(NormalizationCommand term)
Object	visitProofCommandInfo(ProofCommandInfo term)
Object	visitProofCommandInfoList(ProofCommandInfoList term)
Object	visitProofCommandList(ProofCommandList term)
Object	visitProofScript(ProofScript term)
Object	visitProofType(ProofType term)
Object	visitQuantifiersCommand(QuantifiersCommand term)
Object	visitRenameExpr(net.sourceforge.czt.z.ast.RenameExpr renameExpr)
Object	visitSimplificationCommand(SimplificationCommand term)
Object	visitSorryCommand(SorryCommand term)
Object	visitSubstitutionCommand(SubstitutionCommand term)
Object	visitUseCommand(UseCommand term)
Object	visitWithCommand(WithCommand term)
Object	visitZEvesLabel(ZEvesLabel term)
Object	visitZEvesNote(ZEvesNote term)

Methods inherited from class net.sourceforge.czt.print.z.ZPrintVisitor

print, printDecorword, printDecorword, printGenericFormals, printLPAREN, printRPAREN, printTermList, printTermList, printTermList, printTermList, setVisitor, visit, visitAndExpr, visitAndPred, visitApplExpr, visitApplication, visitAxPara, visitBindSelExpr, visitBranch, visitCompExpr, visitCondExpr, visitDecorExpr, visitDirective, visitExists1Expr, visitExists1Pred, visitExistsExpr, visitExistsPred, visitExprPred, visitFalsePred, visitForallExpr, visitForallPred, visitFreePara, visitFreetype, visitGenericType, visitGenParamType, visitGivenPara, visitGivenType, visitHideExpr, visitIffExpr, visitIffPred, visitImpliesExpr, visitImpliesPred, visitInclDecl, visitInStroke, visitLambdaExpr, visitLatexMarkupPara, visitLetExpr, visitListTerm, visitLocAnn, visitMemPred, visitMuExpr, visitNameSectTypeTriple, visitNameTypePair, visitNarrPara, visitNarrSect, visitNegExpr, visitNegPred, visitNewOldPair, visitNextStroke, visitNumExpr, visitNumStroke, visitOperand, visitOperator, visitOperatorApplication, visitOptempPara, visitOrExpr, visitOrPred, visitOutStroke, visitParenAnn, visitParent, visitPipeExpr, visitPowerExpr, visitPowerType, visitPreExpr, visitPrintExpression, visitPrintParagraph, visitPrintPredicate, visitProdExpr, visitProdType, visitProjExpr, visitRefExpr, visitSchemaType, visitSchExpr, visitSectTypeEnvAnn, visitSetCompExpr, visitSetExpr, visitSignature, visitSignatureAnn, visitSpec, visitTerm, visitThetaExpr, visitTruePred, visitTupleExpr, visitTupleSelExpr, visitTypeAnn, visitUnparsedPara, visitUnparsedZSect, visitVarDecl, visitZBranchList, visitZDeclList, visitZExprList, visitZFreetypeList, visitZName, visitZNameList, visitZNumeral, visitZParaList, visitZRenameList, visitZSchText, visitZSect, visitZStrokeList

Methods inherited from class net.sourceforge.czt.print.z.AbstractPrintVisitor

getPrinter, setPrinter

Methods inherited from class net.sourceforge.czt.parser.util.AbstractVisitor

get, getSectionInfo, run

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ZEvesPrintVisitor

public ZEvesPrintVisitor(net.sourceforge.czt.session.SectionInfo si,
                         ZPrinter printer,
                         net.sourceforge.czt.z.util.WarningManager wm)

Creates a new Object-Z print visitor. The section information should be able to provide information of type net.sourceforge.czt.parser.util.OpTable.class.

Parameters:

printer -

wm -

ZEvesPrintVisitor

public ZEvesPrintVisitor(net.sourceforge.czt.session.SectionInfo si,
                         ZPrinter printer,
                         Properties properties,
                         net.sourceforge.czt.z.util.WarningManager wm)

Method Detail

getWarningManager

protected net.sourceforge.czt.z.util.WarningManager getWarningManager()

visitRenameExpr

public Object visitRenameExpr(net.sourceforge.czt.z.ast.RenameExpr renameExpr)

Specified by:

visitRenameExpr in interface net.sourceforge.czt.z.visitor.RenameExprVisitor<Object>

Overrides:

visitRenameExpr in class ZPrintVisitor

visitBindExpr

public Object visitBindExpr(net.sourceforge.czt.z.ast.BindExpr bindExpr)

Specified by:

visitBindExpr in interface net.sourceforge.czt.z.visitor.BindExprVisitor<Object>

Overrides:

visitBindExpr in class ZPrintVisitor

visitConstDecl

public Object visitConstDecl(net.sourceforge.czt.z.ast.ConstDecl constDecl)

Specified by:

visitConstDecl in interface net.sourceforge.czt.z.visitor.ConstDeclVisitor<Object>

Overrides:

visitConstDecl in class ZPrintVisitor

visitConjPara

public Object visitConjPara(net.sourceforge.czt.z.ast.ConjPara conjPara)

Specified by:

visitConjPara in interface net.sourceforge.czt.z.visitor.ConjParaVisitor<Object>

Overrides:

visitConjPara in class ZPrintVisitor

visitProofScript

public Object visitProofScript(ProofScript term)

Specified by:

visitProofScript in interface ProofScriptVisitor<Object>

visitProofCommandList

public Object visitProofCommandList(ProofCommandList term)

Specified by:

visitProofCommandList in interface ProofCommandListVisitor<Object>

visitInstantiationList

public String visitInstantiationList(InstantiationList term)

Specified by:

visitInstantiationList in interface InstantiationListVisitor<Object>

visitProofCommandInfoList

public Object visitProofCommandInfoList(ProofCommandInfoList term)

Specified by:

visitProofCommandInfoList in interface ProofCommandInfoListVisitor<Object>

visitNormalizationCommand

public Object visitNormalizationCommand(NormalizationCommand term)

Specified by:

visitNormalizationCommand in interface NormalizationCommandVisitor<Object>

visitUseCommand

public Object visitUseCommand(UseCommand term)

Specified by:

visitUseCommand in interface UseCommandVisitor<Object>

print

protected void print(Token token)

Overrides:

print in class AbstractPrintVisitor<Object>

visitWithCommand

public Object visitWithCommand(WithCommand term)

Specified by:

visitWithCommand in interface WithCommandVisitor<Object>

visitSubstitutionCommand

public Object visitSubstitutionCommand(SubstitutionCommand term)

Specified by:

visitSubstitutionCommand in interface SubstitutionCommandVisitor<Object>

visitSimplificationCommand

public Object visitSimplificationCommand(SimplificationCommand term)

Specified by:

visitSimplificationCommand in interface SimplificationCommandVisitor<Object>

visitCaseAnalysisCommand

public Object visitCaseAnalysisCommand(CaseAnalysisCommand term)

Specified by:

visitCaseAnalysisCommand in interface CaseAnalysisCommandVisitor<Object>

visitQuantifiersCommand

public Object visitQuantifiersCommand(QuantifiersCommand term)

Specified by:

visitQuantifiersCommand in interface QuantifiersCommandVisitor<Object>

visitApplyCommand

public Object visitApplyCommand(ApplyCommand term)

Specified by:

visitApplyCommand in interface ApplyCommandVisitor<Object>

visitInstantiation

public String visitInstantiation(Instantiation term)

Specified by:

visitInstantiation in interface InstantiationVisitor<Object>

visitSorryCommand

public Object visitSorryCommand(SorryCommand term)

Specified by:

visitSorryCommand in interface SorryCommandVisitor<Object>

visitProofType

public Object visitProofType(ProofType term)

Specified by:

visitProofType in interface ProofTypeVisitor<Object>

visitZEvesLabel

public Object visitZEvesLabel(ZEvesLabel term)

Specified by:

visitZEvesLabel in interface ZEvesLabelVisitor<Object>

visitZEvesNote

public Object visitZEvesNote(ZEvesNote term)

Specified by:

visitZEvesNote in interface ZEvesNoteVisitor<Object>

visitProofCommandInfo

public Object visitProofCommandInfo(ProofCommandInfo term)

Specified by:

visitProofCommandInfo in interface ProofCommandInfoVisitor<Object>