de.uka.ilkd.key.taclettranslation.lemma

Class LemmaFormula

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.LemmaFormula

All Implemented Interfaces:

TacletFormula

class LemmaFormula
extends java.lang.Object
implements TacletFormula

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.LinkedList<Term>	formula
private Taclet	taclet

Constructor Summary

Constructors

Constructor and Description
LemmaFormula(Taclet taclet, Term formula)

Method Summary

Modifier and Type	Method and Description
Term	getFormula(TermServices services)
java.util.Collection<Term>	getInstantiations() It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated.
java.lang.String	getStatus()
Taclet	getTaclet()

Methods inherited from class java.lang.Object

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

Field Detail

taclet

private Taclet taclet

formula

private java.util.LinkedList<Term> formula

Constructor Detail

LemmaFormula

public LemmaFormula(Taclet taclet,
                    Term formula)

Method Detail

getTaclet

public Taclet getTaclet()

Specified by:

getTaclet in interface TacletFormula

Returns:

the taclet of the instance.

getFormula

public Term getFormula(TermServices services)

Specified by:

getFormula in interface TacletFormula

Parameters:

services - TODO

Returns:

the formula of the instance if the taclet is translatable otherwise null. If the translation of the taclet consists of several instantiations (e.g. the taclet has some generic sorts) the returned term is a conjunction of these instantiations.

getStatus

public java.lang.String getStatus()

Specified by:

getStatus in interface TacletFormula

Returns:

if the taclet can not be translated the reason why. Otherwise a empty string.

getInstantiations

public java.util.Collection<Term> getInstantiations()

Description copied from interface: TacletFormula

It can be that a taclet is translated into several formulas, i.e. in the case that the generics are instantiated. This method returns the set of resulting formulas.

Specified by:

getInstantiations in interface TacletFormula