class GenericTranslator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private java.util.ArrayList<TranslationListener> |
listener |
private VariablePool |
pool |
private Services |
services |
Constructor and Description |
---|
GenericTranslator(VariablePool pool) |
Modifier and Type | Method and Description |
---|---|
void |
addListener(TranslationListener list) |
private boolean |
doInstantiation(GenericSort generic,
Sort inst,
TacletConditions conditions)
Tests sort of its instantiation ability.
|
private Term |
instantiateGeneric(Term term,
GenericSort generic,
Sort instantiation,
Taclet t)
Instantiates all variables of a generic sort with logic variables.
|
private ImmutableList<Term> |
instantiateGeneric(Term term,
java.util.HashSet<GenericSort> genericSorts,
ImmutableSet<Sort> instSorts,
Taclet t,
TacletConditions conditions,
int maxGeneric)
Instantiates generic variables of the term.
|
void |
removeListener(TranslationListener list) |
private boolean |
sameHierachyBranch(Sort sort1,
Sort sort2) |
java.util.Collection<Term> |
translate(Term term,
ImmutableSet<Sort> sorts,
Taclet t,
TacletConditions conditions,
Services serv,
int maxGeneric)
Translates generic variables.
|
private VariablePool pool
private Services services
private java.util.ArrayList<TranslationListener> listener
GenericTranslator(VariablePool pool)
public java.util.Collection<Term> translate(Term term, ImmutableSet<Sort> sorts, Taclet t, TacletConditions conditions, Services serv, int maxGeneric) throws IllegalTacletException
IllegalTacletException
private Term instantiateGeneric(Term term, GenericSort generic, Sort instantiation, Taclet t) throws java.lang.IllegalArgumentException, IllegalTacletException
term
- generic
- the generic sort that should be instantiated.instantiation
- the instantiation sort.term
can not be instantiated the method returns
null
, e.g. this can occur, when
term
is of type SortDependingFunction
and instantiation
is of type
{PrimitiveSort}.java.lang.IllegalArgumentException
IllegalTacletException
private boolean doInstantiation(GenericSort generic, Sort inst, TacletConditions conditions)
true
if generic
can be instantiated
with inst
, otherwise false
private ImmutableList<Term> instantiateGeneric(Term term, java.util.HashSet<GenericSort> genericSorts, ImmutableSet<Sort> instSorts, Taclet t, TacletConditions conditions, int maxGeneric) throws IllegalTacletException
term
- the term to be instantiated.genericSorts
- the generic sorts that should be replaced.instSorts
- the instantiationsIllegalTacletException
public void addListener(TranslationListener list)
public void removeListener(TranslationListener list)