de.uka.ilkd.key.taclettranslation

Class DefaultTacletTranslator

java.lang.Object

de.uka.ilkd.key.taclettranslation.AbstractSkeletonGenerator

de.uka.ilkd.key.taclettranslation.DefaultTacletTranslator

All Implemented Interfaces:

SkeletonGenerator

public class DefaultTacletTranslator
extends AbstractSkeletonGenerator

Translates a rewrite taclet to a formula.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	DefaultTacletTranslator.TacletSections

Field Summary

Fields

Modifier and Type	Field and Description
private static int	ANTE
private static int	SUCC

Fields inherited from interface de.uka.ilkd.key.taclettranslation.SkeletonGenerator

DEFAULT_TACLET_TRANSLATOR

Constructor Summary

Constructors

Constructor and Description
DefaultTacletTranslator()

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.taclettranslation.AbstractSkeletonGenerator

translate

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ANTE

private static final int ANTE

See Also:

Constant Field Values

SUCC

private static final int SUCC

See Also:

Constant Field Values

Constructor Detail

DefaultTacletTranslator

public DefaultTacletTranslator()

Method Detail

translateReplaceAndAddTerm

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.

Parameters:

template - contains the replace and add pattern that are to be translated.

find - the find pattern of the taclet, already translated.

services - TODO

Returns:

translation

translateReplaceAndAddFormula

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.

Parameters:

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 - TODO

Returns:

translation

translateEquivalence

private Term translateEquivalence(Term find,
                                  Term replace,
                                  int polarity,
                                  TermServices services)

translateReplaceAndAddSequent

private Term translateReplaceAndAddSequent(TacletGoalTemplate template,
                                           int type,
                                           TermServices services)

translate

public Term translate(Taclet taclet,
                      TermServices services)
               throws IllegalTacletException

Translates a RewriteTaclet to a formula.

Parameters:

taclet - taclet to be translated.

services - TODO

Returns:

returns the translation of the taclet.

Throws:

IllegalTacletException

getPolarity

private int getPolarity(RewriteTaclet rwTaclet)