de.uka.ilkd.key.taclettranslation.lemma

Class UserDefinedSymbols

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.UserDefinedSymbols

public class UserDefinedSymbols
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	UserDefinedSymbols.NamedComparator

Field Summary

Fields

Modifier and Type	Field and Description
(package private) ImmutableSet<Taclet>	axioms
(package private) UserDefinedSymbols	parent
private NamespaceSet	referenceNamespaces
private java.lang.String	ruleHeader
(package private) java.util.Set<Function>	usedExtraFunctions
(package private) java.util.Set<Function>	usedExtraPredicates
(package private) java.util.Set<Sort>	usedExtraSorts
(package private) java.util.Set<QuantifiableVariable>	usedExtraVariables
(package private) java.util.Set<Named>	usedSchemaVariables

Constructor Summary

Constructors

Constructor and Description
UserDefinedSymbols(NamespaceSet referenceNamespaces, ImmutableSet<Taclet> axioms)
UserDefinedSymbols(UserDefinedSymbols parent)

Method Summary

Modifier and Type	Method and Description
void	addFunction(Function symbol)
void	addPredicate(Function symbol)
void	addSchemaVariable(SchemaVariable symbol)
void	addSort(Named symbol)
private <T extends Named> void	addSymbolsToNamespace(Namespace<T> namespace, java.util.Collection<T> symbols)
void	addSymbolsToNamespaces(NamespaceSet namespaces)
private <T extends Named> void	addUserDefiniedSymbol(T symbol, java.util.Set<T> set, Namespace<T> excludeNamespace)
void	addVariable(QuantifiableVariable symbol)
private <T extends Named> boolean	contains(T symbol, java.util.Set<T> set)
java.lang.String	createHeader(Services services)
private java.lang.StringBuffer	createHeaderFor(Taclet taclet, Services services)
private void	createHeaderForFunctions(java.lang.StringBuffer result)
private void	createHeaderForPredicates(java.lang.StringBuffer result)
private void	createHeaderForSchemaVariables(java.lang.StringBuffer result)
private void	createHeaderForSorts(java.lang.StringBuffer result)
private java.lang.String	createRuleHeader(Services services)
private java.lang.String	createSignature(Function op)
private java.util.LinkedList<Named>	ensureRightOrderOfSorts(java.util.LinkedList<Named> list)
private void	getAllSorts(java.util.LinkedList<Named> resultingSorts)
java.util.Map<Name,Sort>	getExtraSorts()
java.lang.String	getRuleHeader(Services services)
void	replaceGenericByProxySorts()
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

parent

final UserDefinedSymbols parent

usedExtraFunctions

final java.util.Set<Function> usedExtraFunctions

usedExtraPredicates

final java.util.Set<Function> usedExtraPredicates

usedExtraSorts

final java.util.Set<Sort> usedExtraSorts

usedExtraVariables

final java.util.Set<QuantifiableVariable> usedExtraVariables

usedSchemaVariables

final java.util.Set<Named> usedSchemaVariables

axioms

final ImmutableSet<Taclet> axioms

referenceNamespaces

private final NamespaceSet referenceNamespaces

ruleHeader

private java.lang.String ruleHeader

Constructor Detail

UserDefinedSymbols

public UserDefinedSymbols(NamespaceSet referenceNamespaces,
                          ImmutableSet<Taclet> axioms)

UserDefinedSymbols

public UserDefinedSymbols(UserDefinedSymbols parent)

Method Detail

addUserDefiniedSymbol

private <T extends Named> void addUserDefiniedSymbol(T symbol,
                                                     java.util.Set<T> set,
                                                     Namespace<T> excludeNamespace)

contains

private <T extends Named> boolean contains(T symbol,
                                           java.util.Set<T> set)

addFunction

public void addFunction(Function symbol)

addPredicate

public void addPredicate(Function symbol)

addSort

public void addSort(Named symbol)

addVariable

public void addVariable(QuantifiableVariable symbol)

addSchemaVariable

public void addSchemaVariable(SchemaVariable symbol)

addSymbolsToNamespaces

public void addSymbolsToNamespaces(NamespaceSet namespaces)

addSymbolsToNamespace

private <T extends Named> void addSymbolsToNamespace(Namespace<T> namespace,
                                                     java.util.Collection<T> symbols)

getRuleHeader

public java.lang.String getRuleHeader(Services services)

createRuleHeader

private java.lang.String createRuleHeader(Services services)

createHeaderFor

private java.lang.StringBuffer createHeaderFor(Taclet taclet,
                                               Services services)

replaceGenericByProxySorts

public void replaceGenericByProxySorts()

createHeader

public java.lang.String createHeader(Services services)

ensureRightOrderOfSorts

private java.util.LinkedList<Named> ensureRightOrderOfSorts(java.util.LinkedList<Named> list)

getAllSorts

private void getAllSorts(java.util.LinkedList<Named> resultingSorts)

getExtraSorts

public java.util.Map<Name,Sort> getExtraSorts()

createHeaderForSorts

private void createHeaderForSorts(java.lang.StringBuffer result)

createHeaderForFunctions

private void createHeaderForFunctions(java.lang.StringBuffer result)

createHeaderForPredicates

private void createHeaderForPredicates(java.lang.StringBuffer result)

createHeaderForSchemaVariables

private void createHeaderForSchemaVariables(java.lang.StringBuffer result)

createSignature

private java.lang.String createSignature(Function op)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object