public class GenericRemovingLemmaGenerator
extends java.lang.Object
GenericSort
s are replaced to equally named ProxySort
s.
This is done since the resulting term is to be used as a proof obligation in which generic sorts must not appear; proxy sorts, however, may. For every generic sort, precisely one proxy sort is introduced.
Constructor and Description |
---|
GenericRemovingLemmaGenerator() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
checkForIllegalConditions(Taclet taclet) |
static java.lang.String |
checkForIllegalOps(Term formula,
Taclet owner,
boolean schemaVarsAreAllowed) |
static java.lang.String |
checkTaclet(Taclet taclet) |
protected Term |
getInstantiation(Taclet owner,
SchemaVariable var,
TermServices services)
Returns the instantiation for a certain schema variable, i.e.
|
protected Operator |
replaceOp(Operator op,
TermServices services)
Sometimes operators must be replaced during lemma generation.
|
protected Sort |
replaceSort(Sort sort,
TermServices services)
Sometimes sorts must be replaced during lemma generation.
|
TacletFormula |
translate(Taclet taclet,
TermServices services) |
protected Operator replaceOp(Operator op, TermServices services)
By default, this method returns the argument op.
The generic removing implementation replaces sort depending functions if their sort argument is a generic sort.
op
- the operator to be replaced, not null
services
- A services object for lookupsnull
protected Sort replaceSort(Sort sort, TermServices services)
By default, this method returns the argument sort.
The generic removing implementation replaces generic sorts by equally named proxy sorts.
sort
- the sort to be replaced, not null
services
- A services object for lookupsnull
public TacletFormula translate(Taclet taclet, TermServices services)
translate
in interface LemmaGenerator
public static java.lang.String checkTaclet(Taclet taclet)
public static java.lang.String checkForIllegalConditions(Taclet taclet)
public static java.lang.String checkForIllegalOps(Term formula, Taclet owner, boolean schemaVarsAreAllowed)
protected final Term getInstantiation(Taclet owner, SchemaVariable var, TermServices services)
owner
- The taclet the schema variable belongs to.var
- The variable to be instantiated.services
- var
.Copyright © 2003-2019 The KeY-Project.