de.uka.ilkd.key.taclettranslation.assumptions

Class GenericTranslator

java.lang.Object

de.uka.ilkd.key.taclettranslation.assumptions.GenericTranslator

class GenericTranslator
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.ArrayList<TranslationListener>	listener
private VariablePool	pool
private Services	services

Constructor Summary

Constructors

Constructor and Description
GenericTranslator(VariablePool pool)

Method Summary

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.

Methods inherited from class java.lang.Object

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

Field Detail

pool

private VariablePool pool

services

private Services services

listener

private java.util.ArrayList<TranslationListener> listener

Constructor Detail

GenericTranslator

GenericTranslator(VariablePool pool)

Method Detail

translate

public java.util.Collection<Term> translate(Term term,
                                            ImmutableSet<Sort> sorts,
                                            Taclet t,
                                            TacletConditions conditions,
                                            Services serv,
                                            int maxGeneric)
                                     throws IllegalTacletException

Translates generic variables.

Throws:

IllegalTacletException

sameHierachyBranch

private boolean sameHierachyBranch(Sort sort1,
                                   Sort sort2)

instantiateGeneric

private Term instantiateGeneric(Term term,
                                GenericSort generic,
                                Sort instantiation,
                                Taclet t)
                         throws java.lang.IllegalArgumentException,
                                IllegalTacletException

Instantiates all variables of a generic sort with logic variables. The logic variable has the same name with the prefix [sort]__

Parameters:

term -

generic - the generic sort that should be instantiated.

instantiation - the instantiation sort.

Returns:

returns the new term with instantiated variables. If 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}.

Throws:

java.lang.IllegalArgumentException

IllegalTacletException

doInstantiation

private boolean doInstantiation(GenericSort generic,
                                Sort inst,
                                TacletConditions conditions)

Tests sort of its instantiation ability.

Returns:

true if generic can be instantiated with inst, otherwise false

instantiateGeneric

private ImmutableList<Term> instantiateGeneric(Term term,
                                               java.util.HashSet<GenericSort> genericSorts,
                                               ImmutableSet<Sort> instSorts,
                                               Taclet t,
                                               TacletConditions conditions,
                                               int maxGeneric)
                                        throws IllegalTacletException

Instantiates generic variables of the term. It instantiates the variables using all possibilities.

Parameters:

term - the term to be instantiated.

genericSorts - the generic sorts that should be replaced.

instSorts - the instantiations

Returns:

returns a new term, where all generic variables are instantiated. If there is no generic variable the original term is returned.

Throws:

IllegalTacletException

addListener

public void addListener(TranslationListener list)

removeListener

public void removeListener(TranslationListener list)