public class DefaultBuilder extends KeYParserBaseVisitor<T>
ParserRuleContext
s.
This builder provides lookup functions for the namespace set and also namespace for SchemaVariable
.
But it does not evaluate schemaVariables, or other declarations.Modifier and Type | Field and Description |
---|---|
static java.lang.String |
LIMIT_SUFFIX |
protected NamespaceSet |
nss |
protected Services |
services |
Constructor and Description |
---|
DefaultBuilder(Services services,
NamespaceSet nss) |
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) |
protected Namespace<Choice> |
choices() |
protected <T> T |
doLookup(Name n,
Namespace... lookups) |
protected void |
each(java.util.Collection<? extends org.antlr.v4.runtime.ParserRuleContext> argument) |
protected void |
each(org.antlr.v4.runtime.RuleContext... ctx) |
protected Namespace<Function> |
functions() |
java.util.List<BuildingIssue> |
getBuildingIssues() |
JavaInfo |
getJavaInfo() |
Services |
getServices() |
protected Named |
lookup(Name n) |
protected Sort |
lookupSort(java.lang.String name)
looks up and returns the sort of the given name or null if none has been found.
|
protected Operator |
lookupVarfuncId(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String varfuncName,
java.lang.String sortName,
Sort sort)
looks up a function, (program) variable or static query of the
given name varfunc_id and the argument terms args in the namespaces
and java info.
|
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) |
NamespaceSet |
namespaces() |
protected <T> T |
oneOf(org.antlr.v4.runtime.ParserRuleContext... ctxs) |
protected <T> T |
peek() |
protected <T> T |
pop() |
protected Namespace<IProgramVariable> |
programVariables() |
protected void |
push(java.lang.Object... obj) |
protected Namespace<RuleSet> |
ruleSets() |
Namespace<SchemaVariable> |
schemaVariables() |
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 |
semanticErrorMsg(java.lang.String label,
org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.Object... args) |
void |
setSchemaVariables(Namespace<SchemaVariable> ns) |
protected Namespace<Sort> |
sorts() |
protected void |
throwEx(java.lang.Throwable e)
Wraps an exception into a
BuildingException |
Sort |
toArraySort(Pair<Sort,Type> p,
int numOfDimensions) |
protected void |
unbindVars(Namespace<QuantifiableVariable> orig) |
protected Namespace<QuantifiableVariable> |
variables() |
Sort |
visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_helperContext ctx)
Visit a parse tree produced by
KeYParser.arg_sorts_or_formula_helper() . |
java.util.List<Sort> |
visitArg_sorts_or_formula(KeYParser.Arg_sorts_or_formulaContext ctx)
Visit a parse tree produced by
KeYParser.arg_sorts_or_formula() . |
java.util.List<Sort> |
visitArg_sorts(KeYParser.Arg_sortsContext ctx)
Visit a parse tree produced by
KeYParser.arg_sorts() . |
java.lang.Object |
visitFuncpred_name(KeYParser.Funcpred_nameContext ctx)
Visit a parse tree produced by
KeYParser.funcpred_name() . |
KeYJavaType |
visitKeyjavatype(KeYParser.KeyjavatypeContext ctx)
Visit a parse tree produced by
KeYParser.keyjavatype() . |
java.util.List<java.lang.String> |
visitPvset(KeYParser.PvsetContext ctx)
Visit a parse tree produced by
KeYParser.pvset() . |
RuleSet |
visitRuleset(KeYParser.RulesetContext ctx)
Visit a parse tree produced by
KeYParser.ruleset() . |
java.util.List<RuleSet> |
visitRulesets(KeYParser.RulesetsContext ctx)
Visit a parse tree produced by
KeYParser.rulesets() . |
java.util.List<java.lang.String> |
visitSimple_ident_comma_list(KeYParser.Simple_ident_comma_listContext ctx)
Visit a parse tree produced by
KeYParser.simple_ident_comma_list() . |
java.lang.Object |
visitSimple_ident_dots_comma_list(KeYParser.Simple_ident_dots_comma_listContext ctx)
Visit a parse tree produced by
KeYParser.simple_ident_dots_comma_list() . |
java.lang.String |
visitSimple_ident_dots(KeYParser.Simple_ident_dotsContext ctx)
Visit a parse tree produced by
KeYParser.simple_ident_dots() . |
java.lang.String |
visitSimple_ident(KeYParser.Simple_identContext ctx)
Visit a parse tree produced by
KeYParser.simple_ident() . |
Sort |
visitSortId(KeYParser.SortIdContext ctx)
Visit a parse tree produced by
KeYParser.sortId() . |
java.lang.String |
visitString_value(KeYParser.String_valueContext ctx)
Visit a parse tree produced by
KeYParser.string_value() . |
java.lang.Object |
visitVarIds(KeYParser.VarIdsContext ctx)
Visit a parse tree produced by
KeYParser.varIds() . |
java.util.List<java.lang.Boolean> |
visitWhere_to_bind(KeYParser.Where_to_bindContext ctx)
Visit a parse tree produced by
KeYParser.where_to_bind() . |
visitAbbreviation, visitAccessterm, visitActivated_choice, visitAdd, visitAddprogvar, visitAddrules, visitArgument_list, visitArrayopid, visitAtom_prefix, visitAttribute_complex, visitAttribute_simple, visitAttribute_star, visitBoolean_literal, visitBootClassPath, visitBound_variables, visitBracket_access_heap_term, visitBracket_access_heap_update, visitBracket_access_indexrange, visitBracket_access_star, visitBracket_suffix_heap, visitBracket_term, visitCall, visitCast_term, visitChar_literal, visitChoice, visitClassPaths, visitComparison_term, visitConjunction_term, visitContracts, visitDecls, visitDisjunction_term, visitElementary_update_term, visitEquality_term, visitEquivalence_term, visitExtends_sorts, visitFile, visitFunc_decl, visitFunc_decls, visitGoalspec, visitGoalspecs, visitGoalspecwithoption, visitId_declaration, visitIfExThenElseTerm, visitIfThenElseTerm, visitImplication_term, visitInvariants, visitJavaSource, visitLabel, visitLiterals, visitLocation_term, visitLocset_term, visitMetaId, visitMetaTerm, visitModality_term, visitModifiers, visitNegation_term, visitNumber, visitOne_bound_variable, visitOne_contract, visitOne_include_statement, visitOne_include, visitOne_invariant, visitOne_schema_modal_op_decl, visitOne_schema_var_decl, visitOne_sort_decl, visitOneJavaSource, visitOneof_sorts, visitOption_decls, visitOption_list, visitOption, visitOptionDecl, visitOptions_choice, visitParallel_term, visitPred_decl, visitPred_decls, visitPreferences, visitPrimitive_labeled_term, visitPrimitive_term, visitProblem, visitProfile, visitProg_var_decls, visitProof, visitProofScript, visitQuantifierterm, visitReplacewith, visitRuleset_decls, visitRulesOrAxioms, visitSchema_modifiers, visitSchema_var_decls, visitSemisequent, visitSeq, visitSeqEOF, visitSingle_label, visitSort_decls, visitString_literal, visitStrong_arith_term_1, visitStrong_arith_term_2, visitSubstitution_term, visitTaclet, visitTacletlist, visitTerm, visitTerm60, visitTermEOF, visitTermorseq, visitTermParen, visitTransform_decl, visitTransform_decls, visitTriggers, visitUnary_minus_term, visitUpdate_term, visitVarexp_argument, visitVarexp, visitVarexpId, visitVarexplist, visitVarId, visitWeak_arith_term
defaultResult, shouldVisitNextChild, visit, visitChildren, visitErrorNode, visitTerminal
public static final java.lang.String LIMIT_SUFFIX
protected final Services services
protected final NamespaceSet nss
public DefaultBuilder(Services services, NamespaceSet nss)
protected void semanticErrorMsg(java.lang.String label, org.antlr.v4.runtime.ParserRuleContext ctx, java.lang.Object... args)
public java.util.List<java.lang.String> visitPvset(KeYParser.PvsetContext ctx)
KeYParserBaseVisitor
KeYParser.pvset()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitPvset
in interface KeYParserVisitor<java.lang.Object>
visitPvset
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<RuleSet> visitRulesets(KeYParser.RulesetsContext ctx)
KeYParserBaseVisitor
KeYParser.rulesets()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitRulesets
in interface KeYParserVisitor<java.lang.Object>
visitRulesets
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic RuleSet visitRuleset(KeYParser.RulesetContext ctx)
KeYParserBaseVisitor
KeYParser.ruleset()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitRuleset
in interface KeYParserVisitor<java.lang.Object>
visitRuleset
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.String visitSimple_ident_dots(KeYParser.Simple_ident_dotsContext ctx)
KeYParserBaseVisitor
KeYParser.simple_ident_dots()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSimple_ident_dots
in interface KeYParserVisitor<java.lang.Object>
visitSimple_ident_dots
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treeprotected void unbindVars(Namespace<QuantifiableVariable> orig)
public java.util.List<Sort> visitArg_sorts_or_formula(KeYParser.Arg_sorts_or_formulaContext ctx)
KeYParserBaseVisitor
KeYParser.arg_sorts_or_formula()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitArg_sorts_or_formula
in interface KeYParserVisitor<java.lang.Object>
visitArg_sorts_or_formula
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_helperContext ctx)
KeYParserBaseVisitor
KeYParser.arg_sorts_or_formula_helper()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitArg_sorts_or_formula_helper
in interface KeYParserVisitor<java.lang.Object>
visitArg_sorts_or_formula_helper
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treeprotected Operator lookupVarfuncId(org.antlr.v4.runtime.ParserRuleContext ctx, java.lang.String varfuncName, java.lang.String sortName, Sort sort)
varfuncName
- the String with the symbols nameprotected Sort lookupSort(java.lang.String name)
public NamespaceSet namespaces()
protected Namespace<QuantifiableVariable> variables()
protected Namespace<IProgramVariable> programVariables()
public java.lang.String visitString_value(KeYParser.String_valueContext ctx)
KeYParserBaseVisitor
KeYParser.string_value()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitString_value
in interface KeYParserVisitor<java.lang.Object>
visitString_value
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic JavaInfo getJavaInfo()
public Services getServices()
public Namespace<SchemaVariable> schemaVariables()
public void setSchemaVariables(Namespace<SchemaVariable> ns)
public java.lang.Object visitVarIds(KeYParser.VarIdsContext ctx)
KeYParserBaseVisitor
KeYParser.varIds()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitVarIds
in interface KeYParserVisitor<java.lang.Object>
visitVarIds
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitSimple_ident_dots_comma_list(KeYParser.Simple_ident_dots_comma_listContext ctx)
KeYParserBaseVisitor
KeYParser.simple_ident_dots_comma_list()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSimple_ident_dots_comma_list
in interface KeYParserVisitor<java.lang.Object>
visitSimple_ident_dots_comma_list
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.String visitSimple_ident(KeYParser.Simple_identContext ctx)
KeYParserBaseVisitor
KeYParser.simple_ident()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSimple_ident
in interface KeYParserVisitor<java.lang.Object>
visitSimple_ident
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<java.lang.String> visitSimple_ident_comma_list(KeYParser.Simple_ident_comma_listContext ctx)
KeYParserBaseVisitor
KeYParser.simple_ident_comma_list()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSimple_ident_comma_list
in interface KeYParserVisitor<java.lang.Object>
visitSimple_ident_comma_list
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<java.lang.Boolean> visitWhere_to_bind(KeYParser.Where_to_bindContext ctx)
KeYParserBaseVisitor
KeYParser.where_to_bind()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitWhere_to_bind
in interface KeYParserVisitor<java.lang.Object>
visitWhere_to_bind
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.util.List<Sort> visitArg_sorts(KeYParser.Arg_sortsContext ctx)
KeYParserBaseVisitor
KeYParser.arg_sorts()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitArg_sorts
in interface KeYParserVisitor<java.lang.Object>
visitArg_sorts
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic Sort visitSortId(KeYParser.SortIdContext ctx)
KeYParserBaseVisitor
KeYParser.sortId()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitSortId
in interface KeYParserVisitor<java.lang.Object>
visitSortId
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx)
KeYParserBaseVisitor
KeYParser.keyjavatype()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitKeyjavatype
in interface KeYParserVisitor<java.lang.Object>
visitKeyjavatype
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse treepublic java.lang.Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx)
KeYParserBaseVisitor
KeYParser.funcpred_name()
.
The default implementation returns the result of calling
AbstractParseTreeVisitor.visitChildren(org.antlr.v4.runtime.tree.RuleNode)
on ctx
.
visitFuncpred_name
in interface KeYParserVisitor<java.lang.Object>
visitFuncpred_name
in class KeYParserBaseVisitor<java.lang.Object>
ctx
- the parse tree@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.