public class TacletPBuilder extends ExpressionBuilder
javaSchemaModeAllowed, NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE
LIMIT_SUFFIX, nss, services
Constructor and Description |
---|
TacletPBuilder(Services services,
NamespaceSet nss) |
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Method and Description |
---|---|
<T> T |
accept(org.antlr.v4.runtime.RuleContext ctx)
Helper function for avoiding cast.
|
protected <T> T |
accept(org.antlr.v4.runtime.RuleContext ctx,
java.lang.Object... args) |
protected <T> T |
acceptFirst(java.util.Collection<? extends org.antlr.v4.runtime.RuleContext> seq) |
protected BuildingIssue |
addWarning(org.antlr.v4.runtime.ParserRuleContext node,
java.lang.String description) |
protected BuildingIssue |
addWarning(java.lang.String description) |
protected T |
aggregateResult(T aggregate,
T nextResult) |
java.lang.Object |
buildTypeResolver(KeYParser.Varexp_argumentContext ctx) |
protected void |
declareSchemaVariable(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String name,
Sort s,
boolean makeVariableSV,
boolean makeSkolemTermSV,
boolean makeTermLabelSV,
SchemaVariableModifierSet mods) |
protected void |
each(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument) |
protected void |
each(org.antlr.v4.runtime.RuleContext... ctx) |
java.util.List<BuildingIssue> |
getBuildingIssues() |
java.util.List<Taclet> |
getTopLevelTaclets() |
protected <T2> java.util.List<T2> |
mapMapOf(java.util.List<? extends org.antlr.v4.runtime.RuleContext>... ctxss) |
protected <T> java.util.List<T> |
mapOf(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument) |
protected <T> T |
oneOf(org.antlr.v4.runtime.ParserRuleContext... ctxs) |
protected <T> T |
peek() |
protected <T> T |
pop() |
protected void |
push(java.lang.Object... obj) |
protected void |
semanticError(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String format,
java.lang.Object... args)
Throws a semanticError for the given ast node and message.
|
protected void |
throwEx(java.lang.Throwable e)
Wraps an exception into a
BuildingException |
java.lang.Object |
visitAdd(KeYParser.AddContext ctx)
Visit a parse tree produced by
KeYParser.add() . |
ImmutableSet<SchemaVariable> |
visitAddprogvar(KeYParser.AddprogvarContext ctx)
Visit a parse tree produced by
KeYParser.addprogvar() . |
java.lang.Object |
visitAddrules(KeYParser.AddrulesContext ctx)
Visit a parse tree produced by
KeYParser.addrules() . |
java.lang.Object |
visitDecls(KeYParser.DeclsContext ctx)
Visit a parse tree produced by
KeYParser.decls() . |
java.lang.Object |
visitGoalspec(KeYParser.GoalspecContext ctx)
Visit a parse tree produced by
KeYParser.goalspec() . |
java.lang.Object |
visitGoalspecs(KeYParser.GoalspecsContext ctx)
Visit a parse tree produced by
KeYParser.goalspecs() . |
java.lang.Object |
visitGoalspecwithoption(KeYParser.GoalspecwithoptionContext ctx)
Visit a parse tree produced by
KeYParser.goalspecwithoption() . |
java.lang.Object |
visitModifiers(KeYParser.ModifiersContext ctx)
Visit a parse tree produced by
KeYParser.modifiers() . |
java.lang.Object |
visitOne_schema_modal_op_decl(KeYParser.One_schema_modal_op_declContext ctx)
Visit a parse tree produced by
KeYParser.one_schema_modal_op_decl() . |
java.lang.Object |
visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx)
Visit a parse tree produced by
KeYParser.one_schema_var_decl() . |
java.util.List<Choice> |
visitOption_list(KeYParser.Option_listContext ctx)
Visit a parse tree produced by
KeYParser.option_list() . |
Choice |
visitOption(KeYParser.OptionContext ctx)
Visit a parse tree produced by
KeYParser.option() . |
java.lang.Object |
visitReplacewith(KeYParser.ReplacewithContext ctx)
Visit a parse tree produced by
KeYParser.replacewith() . |
java.lang.Object |
visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx)
Visit a parse tree produced by
KeYParser.rulesOrAxioms() . |
java.lang.Object |
visitSchema_modifiers(KeYParser.Schema_modifiersContext ctx)
Visit a parse tree produced by
KeYParser.schema_modifiers() . |
java.lang.Object |
visitSchema_var_decls(KeYParser.Schema_var_declsContext ctx)
Visit a parse tree produced by
KeYParser.schema_var_decls() . |
Taclet |
visitTaclet(KeYParser.TacletContext ctx)
Visit a parse tree produced by
KeYParser.taclet() . |
ImmutableList<Taclet> |
visitTacletlist(KeYParser.TacletlistContext ctx)
Visit a parse tree produced by
KeYParser.tacletlist() . |
TacletBuilder |
visitTriggers(KeYParser.TriggersContext ctx)
Visit a parse tree produced by
KeYParser.triggers() . |
java.lang.Object |
visitVarexp(KeYParser.VarexpContext ctx)
Visit a parse tree produced by
KeYParser.varexp() . |
java.lang.Object |
visitVarexplist(KeYParser.VarexplistContext ctx)
Visit a parse tree produced by
KeYParser.varexplist() . |
Operator |
visitVarId(KeYParser.VarIdContext ctx)
Visit a parse tree produced by
KeYParser.varId() . |
capsulateTf, createAttributeTerm, defaultOnException, disableJavaSchemaMode, enableJavaSchemaMode, getAbbrevMap, getTermFactory, heapSelectionSuffix, isClass, isHeapTerm, operatorOfJavaBlock, opSVHelper, setAbbrevMap, trimJavaBlock, updateOrigin, visitAbbreviation, visitAccessterm, visitArgument_list, visitBoolean_literal, visitBound_variables, visitBracket_access_heap_term, visitBracket_access_heap_update, visitBracket_access_indexrange, visitBracket_access_star, visitBracket_term, visitCast_term, visitChar_literal, visitComparison_term, visitConjunction_term, visitDisjunction_term, visitElementary_update_term, visitEquality_term, visitEquivalence_term, visitFuncpred_name, visitIfExThenElseTerm, visitIfThenElseTerm, visitImplication_term, visitLabel, visitLocation_term, visitLocset_term, visitMetaId, visitMetaTerm, visitModality_term, visitNegation_term, visitNumber, visitOne_bound_variable, visitParallel_term, visitPrimitive_labeled_term, visitQuantifierterm, visitSemisequent, visitSeq, visitSeqEOF, visitSingle_label, visitString_literal, visitStrong_arith_term_1, visitStrong_arith_term_2, visitSubstitution_term, visitTermEOF, visitTermorseq, visitTermParen, visitUnary_minus_term, visitUpdate_term, visitWeak_arith_term
choices, doLookup, functions, getJavaInfo, getServices, lookup, lookupSort, lookupVarfuncId, namespaces, programVariables, ruleSets, schemaVariables, semanticErrorMsg, setSchemaVariables, sorts, toArraySort, unbindVars, variables, visitArg_sorts_or_formula_helper, visitArg_sorts_or_formula, visitArg_sorts, visitKeyjavatype, visitPvset, visitRuleset, visitRulesets, visitSimple_ident_comma_list, visitSimple_ident_dots_comma_list, visitSimple_ident_dots, visitSimple_ident, visitSortId, visitString_value, visitVarIds, visitWhere_to_bind
visitActivated_choice, visitArrayopid, visitAtom_prefix, visitAttribute_complex, visitAttribute_simple, visitAttribute_star, visitBootClassPath, visitBracket_suffix_heap, visitCall, visitChoice, visitClassPaths, visitContracts, visitExtends_sorts, visitFile, visitFunc_decl, visitFunc_decls, visitId_declaration, visitInvariants, visitJavaSource, visitLiterals, visitOne_contract, visitOne_include_statement, visitOne_include, visitOne_invariant, visitOne_sort_decl, visitOneJavaSource, visitOneof_sorts, visitOption_decls, visitOptionDecl, visitOptions_choice, visitPred_decl, visitPred_decls, visitPreferences, visitPrimitive_term, visitProblem, visitProfile, visitProg_var_decls, visitProof, visitProofScript, visitRuleset_decls, visitSort_decls, visitTerm, visitTerm60, visitTransform_decl, visitTransform_decls, visitVarexp_argument, visitVarexpId
defaultResult, shouldVisitNextChild, visit, visitChildren, visitErrorNode, visitTerminal
public TacletPBuilder(Services services, NamespaceSet nss)
public TacletPBuilder(Services services, NamespaceSet namespaces, java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder)
public java.lang.Object visitDecls(KeYParser.DeclsContext ctx)
KeYParserBaseVisitor
KeYParser.decls()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitDecls
in interface KeYParserVisitor<java.lang.Object>
visitDecls
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx)
KeYParserBaseVisitor
KeYParser.rulesOrAxioms()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitRulesOrAxioms
in interface KeYParserVisitor<java.lang.Object>
visitRulesOrAxioms
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitOne_schema_modal_op_decl(KeYParser.One_schema_modal_op_declContext ctx)
KeYParserBaseVisitor
KeYParser.one_schema_modal_op_decl()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitOne_schema_modal_op_decl
in interface KeYParserVisitor<java.lang.Object>
visitOne_schema_modal_op_decl
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic TacletBuilder visitTriggers(KeYParser.TriggersContext ctx)
KeYParserBaseVisitor
KeYParser.triggers()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTriggers
in interface KeYParserVisitor<java.lang.Object>
visitTriggers
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Taclet visitTaclet(KeYParser.TacletContext ctx)
KeYParserBaseVisitor
KeYParser.taclet()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTaclet
in interface KeYParserVisitor<java.lang.Object>
visitTaclet
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitModifiers(KeYParser.ModifiersContext ctx)
KeYParserBaseVisitor
KeYParser.modifiers()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitModifiers
in interface KeYParserVisitor<java.lang.Object>
visitModifiers
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitVarexplist(KeYParser.VarexplistContext ctx)
KeYParserBaseVisitor
KeYParser.varexplist()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitVarexplist
in interface KeYParserVisitor<java.lang.Object>
visitVarexplist
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitVarexp(KeYParser.VarexpContext ctx)
KeYParserBaseVisitor
KeYParser.varexp()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitVarexp
in interface KeYParserVisitor<java.lang.Object>
visitVarexp
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object buildTypeResolver(KeYParser.Varexp_argumentContext ctx)
public java.lang.Object visitGoalspecs(KeYParser.GoalspecsContext ctx)
KeYParserBaseVisitor
KeYParser.goalspecs()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitGoalspecs
in interface KeYParserVisitor<java.lang.Object>
visitGoalspecs
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitGoalspecwithoption(KeYParser.GoalspecwithoptionContext ctx)
KeYParserBaseVisitor
KeYParser.goalspecwithoption()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitGoalspecwithoption
in interface KeYParserVisitor<java.lang.Object>
visitGoalspecwithoption
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Choice visitOption(KeYParser.OptionContext ctx)
KeYParserBaseVisitor
KeYParser.option()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitOption
in interface KeYParserVisitor<java.lang.Object>
visitOption
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<Choice> visitOption_list(KeYParser.Option_listContext ctx)
KeYParserBaseVisitor
KeYParser.option_list()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitOption_list
in interface KeYParserVisitor<java.lang.Object>
visitOption_list
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitGoalspec(KeYParser.GoalspecContext ctx)
KeYParserBaseVisitor
KeYParser.goalspec()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitGoalspec
in interface KeYParserVisitor<java.lang.Object>
visitGoalspec
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitReplacewith(KeYParser.ReplacewithContext ctx)
KeYParserBaseVisitor
KeYParser.replacewith()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitReplacewith
in interface KeYParserVisitor<java.lang.Object>
visitReplacewith
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitAdd(KeYParser.AddContext ctx)
KeYParserBaseVisitor
KeYParser.add()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitAdd
in interface KeYParserVisitor<java.lang.Object>
visitAdd
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitAddrules(KeYParser.AddrulesContext ctx)
KeYParserBaseVisitor
KeYParser.addrules()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitAddrules
in interface KeYParserVisitor<java.lang.Object>
visitAddrules
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic ImmutableSet<SchemaVariable> visitAddprogvar(KeYParser.AddprogvarContext ctx)
KeYParserBaseVisitor
KeYParser.addprogvar()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitAddprogvar
in interface KeYParserVisitor<java.lang.Object>
visitAddprogvar
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic ImmutableList<Taclet> visitTacletlist(KeYParser.TacletlistContext ctx)
KeYParserBaseVisitor
KeYParser.tacletlist()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitTacletlist
in interface KeYParserVisitor<java.lang.Object>
visitTacletlist
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Operator visitVarId(KeYParser.VarIdContext ctx)
KeYParserBaseVisitor
KeYParser.varId()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitVarId
in interface KeYParserVisitor<java.lang.Object>
visitVarId
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx)
KeYParserBaseVisitor
KeYParser.one_schema_var_decl()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitOne_schema_var_decl
in interface KeYParserVisitor<java.lang.Object>
visitOne_schema_var_decl
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitSchema_modifiers(KeYParser.Schema_modifiersContext ctx)
KeYParserBaseVisitor
KeYParser.schema_modifiers()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSchema_modifiers
in interface KeYParserVisitor<java.lang.Object>
visitSchema_modifiers
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitSchema_var_decls(KeYParser.Schema_var_declsContext ctx)
KeYParserBaseVisitor
KeYParser.schema_var_decls()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSchema_var_decls
in interface KeYParserVisitor<java.lang.Object>
visitSchema_var_decls
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treeprotected void declareSchemaVariable(org.antlr.v4.runtime.ParserRuleContext ctx, java.lang.String name, Sort s, boolean makeVariableSV, boolean makeSkolemTermSV, boolean makeTermLabelSV, SchemaVariableModifierSet mods)
public java.util.List<Taclet> getTopLevelTaclets()
@Nullable public <T> T accept(@Nullable org.antlr.v4.runtime.RuleContext ctx)
T
- ctx
- protected T aggregateResult(T aggregate, T nextResult)
aggregateResult
in class org.antlr.v4.runtime.tree.AbstractParseTreeVisitor<T>
protected <T> T peek()
T
- protected <T> T acceptFirst(java.util.Collection<? extends org.antlr.v4.runtime.RuleContext> seq)
protected <T> T pop()
protected void push(java.lang.Object... obj)
@Nullable protected <T> T accept(@Nullable org.antlr.v4.runtime.RuleContext ctx, java.lang.Object... args)
protected <T> T oneOf(org.antlr.v4.runtime.ParserRuleContext... ctxs)
protected <T> java.util.List<T> mapOf(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument)
protected void each(org.antlr.v4.runtime.RuleContext... ctx)
protected void each(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument)
protected <T2> java.util.List<T2> mapMapOf(java.util.List<? extends org.antlr.v4.runtime.RuleContext>... ctxss)
@Nonnull public java.util.List<BuildingIssue> getBuildingIssues()
protected BuildingIssue addWarning(org.antlr.v4.runtime.ParserRuleContext node, java.lang.String description)
protected BuildingIssue addWarning(java.lang.String description)
protected void semanticError(org.antlr.v4.runtime.ParserRuleContext ctx, java.lang.String format, java.lang.Object... args)
ctx
- format
- args
- protected void throwEx(java.lang.Throwable e)
BuildingException
e
- Copyright © 2003-2019 The KeY-Project.