public interface TranslationListener
TacletTranslator
.
Use this interface to get information while translating a taclet.Modifier and Type | Method and Description |
---|---|
void |
eventFormulaSV(SchemaVariable formula)
Called when the translator finds a schema variable of type formula.
|
boolean |
eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term)
Called when the translator can not instantiate a generic sort
with a particular sort in the given term.
|
void |
eventQuantifiedVariable(QuantifiableVariable var)
Called when the translator finds a term that has a quantified variable.
|
void |
eventSort(Sort sort)
Called when the translator finds a term that have a sort.
|
void eventSort(Sort sort)
sort
- the sort that has been found.void eventQuantifiedVariable(QuantifiableVariable var)
var
- the quantified variable that has been found.void eventFormulaSV(SchemaVariable formula)
formula
- boolean eventInstantiationFailure(GenericSort dest, Sort sort, Taclet t, Term term)
dest
- the generic sort to instantiatesort
- the instantiation sort.t
- the taclet thats belongs to the termterm
- the term to be instantiatedtrue
if you want to terminate the translation
of the taclet, otherwise false.