public class DefaultTacletTranslator extends AbstractSkeletonGenerator
Modifier and Type | Class and Description |
---|---|
private static class |
DefaultTacletTranslator.TacletSections |
Modifier and Type | Field and Description |
---|---|
private static int |
ANTE |
private static int |
SUCC |
DEFAULT_TACLET_TRANSLATOR
Constructor and Description |
---|
DefaultTacletTranslator() |
Modifier and Type | Method and Description |
---|---|
private int |
getPolarity(RewriteTaclet rwTaclet) |
Term |
translate(Taclet taclet,
TermServices services)
Translates a RewriteTaclet to a formula.
|
private Term |
translateEquivalence(Term find,
Term replace,
int polarity,
TermServices services) |
private Term |
translateReplaceAndAddFormula(TacletGoalTemplate template,
Term find,
int polarity,
TermServices services)
Translates the replace and add pattern of a goal template to:
(find<->replace)->add
Use this method if you want to translate a taclet, where the find pattern is a formula. |
private Term |
translateReplaceAndAddSequent(TacletGoalTemplate template,
int type,
TermServices services) |
private Term |
translateReplaceAndAddTerm(TacletGoalTemplate template,
Term find,
TermServices services)
Translates the replace and add pattern of a goal template to:
find=replace->add
Use this method if you want to translate a taclet, where the find pattern is a term. |
translate
private static final int ANTE
private static final int SUCC
private Term translateReplaceAndAddTerm(TacletGoalTemplate template, Term find, TermServices services)
template
- contains the replace and add pattern that are to be
translated.find
- the find pattern of the taclet, already translated.services
- TODOprivate Term translateReplaceAndAddFormula(TacletGoalTemplate template, Term find, int polarity, TermServices services)
template
- contains the replace and add pattern that are to be
translated.find
- the find pattern of the taclet, already translated.polarity
- a value between -1 and 1. describes the expected polarity of
the find clause (-1 antecedent, 0 both, +1 succedent)services
- TODOprivate Term translateEquivalence(Term find, Term replace, int polarity, TermServices services)
private Term translateReplaceAndAddSequent(TacletGoalTemplate template, int type, TermServices services)
public Term translate(Taclet taclet, TermServices services) throws IllegalTacletException
taclet
- taclet to be translated.services
- TODOIllegalTacletException
private int getPolarity(RewriteTaclet rwTaclet)