public class TacletPrefixBuilder
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
TacletPrefixBuilder.InvalidPrefixException |
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<SchemaVariable> |
currentlyBoundVars
set of all schemavariables that are only allowed to be matched
with quantifiable variables.
|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
prefixMap |
private TacletBuilder<? extends Taclet> |
tacletBuilder |
Constructor and Description |
---|
TacletPrefixBuilder(TacletBuilder<? extends Taclet> tacletBuilder) |
Modifier and Type | Method and Description |
---|---|
private void |
addVarsBoundHere(Term visited,
int subTerm) |
private boolean |
atMostOneRepl() |
void |
build() |
private void |
checkPrefixInAddRules(Taclet addRule) |
private void |
considerContext() |
ImmutableMap<SchemaVariable,TacletPrefix> |
getPrefixMap() |
private boolean |
occurrsOnlyInFindOrRepl(SchemaVariable sv) |
private ImmutableSet<SchemaVariable> |
removeNotFreeIn(SchemaVariable sv)
removes all variables x that are declared as x not free in sv from the
currently bound vars set.
|
private void |
setPrefixOfOccurrence(SchemaVariable sv,
ImmutableSet<SchemaVariable> relevantBoundVars) |
private void |
visit(Sequent s) |
private void |
visit(TacletGoalTemplate templ) |
private void |
visit(Term t) |
private ImmutableSet<SchemaVariable> currentlyBoundVars
private TacletBuilder<? extends Taclet> tacletBuilder
protected ImmutableMap<SchemaVariable,TacletPrefix> prefixMap
public TacletPrefixBuilder(TacletBuilder<? extends Taclet> tacletBuilder)
private void addVarsBoundHere(Term visited, int subTerm)
private void setPrefixOfOccurrence(SchemaVariable sv, ImmutableSet<SchemaVariable> relevantBoundVars)
private ImmutableSet<SchemaVariable> removeNotFreeIn(SchemaVariable sv)
private void visit(Term t)
private void visit(Sequent s)
private void visit(TacletGoalTemplate templ)
public void build()
private void checkPrefixInAddRules(Taclet addRule)
private boolean atMostOneRepl()
private boolean occurrsOnlyInFindOrRepl(SchemaVariable sv)
private void considerContext()
public ImmutableMap<SchemaVariable,TacletPrefix> getPrefixMap()