de.uka.ilkd.key.rule.inst

Class GenericSortInstantiations

java.lang.Object

de.uka.ilkd.key.rule.inst.GenericSortInstantiations

public final class GenericSortInstantiations
extends java.lang.Object

This class handles the instantiation of generic sorts (used for generic taclets), i.e. the class tries to find a solution for the conditions on the generic sorts given by the type hierarchy and the chosen SV instantiations this class is immutable

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	GenericSortInstantiations.FailException

Field Summary

Fields

Modifier and Type	Field and Description
static GenericSortInstantiations	EMPTY_INSTANTIATIONS
private static GenericSortInstantiations.FailException	FAIL_EXCEPTION
private ImmutableMap<GenericSort,Sort>	insts
private static GenericSortException	UNSATISFIABLE_SORT_CONSTRAINTS exception thrown if no solution exists

Constructor Summary

Constructors

Modifier	Constructor and Description
private	GenericSortInstantiations(ImmutableMap<GenericSort,Sort> p_insts)

Method Summary

Modifier and Type	Method and Description
private static ImmutableList<Sort>	addChosenInstantiations(ImmutableMap<GenericSort,Sort> p_curRes, GenericSort p_gs, ImmutableList<Sort> p_subsorts)
private static void	addSortsToSet(java.util.Set<Sort> p_set, ImmutableSet<Sort> p_sorts)
java.lang.Boolean	checkCondition(GenericSortCondition p_condition)
java.lang.Boolean	checkSorts(SchemaVariable sv, InstantiationEntry<?> p_entry)
private static ImmutableList<Sort>	chooseResults(GenericSort p_gs, ImmutableList<GenericSortCondition> p_idConditions)
private static Sort	condSort(java.util.Iterator<GenericSortCondition> itC)
static GenericSortInstantiations	create(ImmutableList<GenericSort> p_sorts, ImmutableList<GenericSortCondition> p_conditions, Services services) Create an object that holds instantiations of the generic sorts "p_sorts" satisfying the conditions "p_conditions"
static GenericSortInstantiations	create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations, ImmutableList<GenericSortCondition> p_conditions, Services services) Create an object that solves the conditions given by the instantiation iterator, i.e. instantiations of the generic sorts used within "p_instantiations" are sought for which are compatible with the instantiations of the SVs
private static ImmutableMap<GenericSort,Sort>	descend(ImmutableList<GenericSort> p_remainingSorts, ImmutableMap<GenericSort,Sort> p_curRes, ImmutableList<GenericSortCondition> p_conditions, ImmutableList<GenericSort> p_pushedBack, GenericSort p_gs, ImmutableList<Sort> p_subsorts, ImmutableList<Sort> p_chosenList, Services services)
private static ImmutableList<Sort>	findMinimalElements(java.util.Set<Sort> p_inside) Find all minimal elements of the given set p_inside
ImmutableMap<GenericSort,Sort>	getAllInstantiations() ONLY FOR JUNIT TESTS
Sort	getInstantiation(GenericSort p_gs)
private static Sort	getOneOf(java.util.Set<Sort> p_set)
Sort	getRealSort(SchemaVariable p_sv, TermServices services)
Sort	getRealSort(Sort p_s, TermServices services)
boolean	isEmpty()
boolean	isInstantiated(GenericSort p_gs)
private static boolean	isPossibleInstantiation(GenericSort p_gs, Sort p_s, ImmutableMap<GenericSort,Sort> p_curRes)
private static boolean	isSupersortOf(Sort p_s, ImmutableList<Sort> p_subsorts)
private static ImmutableList<Sort>	minimalSupersorts(ImmutableList<Sort> p_sorts, Services services) Find all minimal common supersorts of "p_itSorts" PRECONDITION: !
private static ImmutableMap<GenericSort,Sort>	solve(ImmutableList<GenericSort> p_sorts, ImmutableList<GenericSortCondition> p_conditions, Services services) Really solve the conditions given
private static ImmutableMap<GenericSort,Sort>	solveForcedInst(ImmutableList<GenericSort> p_remainingSorts, ImmutableMap<GenericSort,Sort> p_curRes, ImmutableList<GenericSortCondition> p_conditions, Services services) Method which is called by solveHelp and tries to instantiate the generic sorts for which GSCForceInstantiation-conditions (with "maximum" parameter) are contained within "p_conditions"
private static ImmutableMap<GenericSort,Sort>	solveForcedInstHelp(ImmutableList<GenericSort> p_remainingSorts, ImmutableMap<GenericSort,Sort> p_curRes, Services services) Method which is called recursively and tries to instantiate one (the first) generic sort from the "p_remainingSorts"-list
private static ImmutableMap<GenericSort,Sort>	solveHelp(ImmutableList<GenericSort> p_remainingSorts, ImmutableMap<GenericSort,Sort> p_curRes, ImmutableList<GenericSortCondition> p_conditions, ImmutableList<GenericSort> p_pushedBack, Services services) Method which is called recursively and tries to instantiate one (the first) generic sort from the "p_remainingSorts"-list
ImmutableList<GenericSortCondition>	toConditions() Create a list of conditions establishing the instantiations stored by this object (not saying anything about further generic sorts)
private static ImmutableList<Sort>	toList(ImmutableSet<Sort> p_set)
private static ImmutableList<GenericSort>	topology(ImmutableList<GenericSort> p_sorts) Sort generic sorts topologically, i.e. if sort A is a supersort of sort B, then A appears behind B within the return value
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_INSTANTIATIONS

public static final GenericSortInstantiations EMPTY_INSTANTIATIONS

insts

private final ImmutableMap<GenericSort,Sort> insts

UNSATISFIABLE_SORT_CONSTRAINTS

private static final GenericSortException UNSATISFIABLE_SORT_CONSTRAINTS

exception thrown if no solution exists

FAIL_EXCEPTION

private static final GenericSortInstantiations.FailException FAIL_EXCEPTION

Constructor Detail

GenericSortInstantiations

private GenericSortInstantiations(ImmutableMap<GenericSort,Sort> p_insts)

Method Detail

create

public static GenericSortInstantiations create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations,
                                               ImmutableList<GenericSortCondition> p_conditions,
                                               Services services)

Create an object that solves the conditions given by the instantiation iterator, i.e. instantiations of the generic sorts used within "p_instantiations" are sought for which are compatible with the instantiations of the SVs

Parameters:

p_instantiations - list of SV instantiations

p_conditions - additional conditions for sort instantiations

Throws:

GenericSortException - iff the conditions could not be solved

create

public static GenericSortInstantiations create(ImmutableList<GenericSort> p_sorts,
                                               ImmutableList<GenericSortCondition> p_conditions,
                                               Services services)

Create an object that holds instantiations of the generic sorts "p_sorts" satisfying the conditions "p_conditions"

Parameters:

p_sorts - generic sorts to instantiate

p_conditions - conditions the instantiations have to satisfy

Throws:

GenericSortException - if no instantiations has been found

checkSorts

public java.lang.Boolean checkSorts(SchemaVariable sv,
                                    InstantiationEntry<?> p_entry)

Returns:

Boolean.TRUE if the sorts used within "p_entry" are correct, Boolean.FALSE if the sorts are definitely incorrect, null if the sorts could (perhaps) be made correct by choosing the right generic sort instantiations

checkCondition

public java.lang.Boolean checkCondition(GenericSortCondition p_condition)

Returns:

Boolean.TRUE if the generic sort instantiations within "this" satisfy "p_condition", null otherwise (this means, "p_condition" could be satisfied by create a new "GenericSortInstantiations"-object)

isInstantiated

public boolean isInstantiated(GenericSort p_gs)

getInstantiation

public Sort getInstantiation(GenericSort p_gs)

isEmpty

public boolean isEmpty()

toConditions

public ImmutableList<GenericSortCondition> toConditions()

Create a list of conditions establishing the instantiations stored by this object (not saying anything about further generic sorts)

getRealSort

public Sort getRealSort(SchemaVariable p_sv,
                        TermServices services)

Parameters:

services - the Services class

Returns:

p_s iff p_s is not a generic sort, the concrete sort p_s is instantiated with currently otherwise

Throws:

GenericSortException - iff p_s is a generic sort which is not yet instantiated

getRealSort

public Sort getRealSort(Sort p_s,
                        TermServices services)

solve

private static ImmutableMap<GenericSort,Sort> solve(ImmutableList<GenericSort> p_sorts,
                                                    ImmutableList<GenericSortCondition> p_conditions,
                                                    Services services)

Really solve the conditions given

Parameters:

p_sorts - generic sorts that must be instantiated

p_conditions - conditions to be solved

Returns:

the/a found solution

Throws:

GenericSortException - no solution could be found

solveHelp

private static ImmutableMap<GenericSort,Sort> solveHelp(ImmutableList<GenericSort> p_remainingSorts,
                                                        ImmutableMap<GenericSort,Sort> p_curRes,
                                                        ImmutableList<GenericSortCondition> p_conditions,
                                                        ImmutableList<GenericSort> p_pushedBack,
                                                        Services services)

Method which is called recursively and tries to instantiate one (the first) generic sort from the "p_remainingSorts"-list

Parameters:

p_remainingSorts - generic sorts which needs to be instantiated (topologically sorted)

p_curRes - instantiations so far

p_conditions - conditions (see above)

Returns:

a solution if one could be found, null otherwise

descend

private static ImmutableMap<GenericSort,Sort> descend(ImmutableList<GenericSort> p_remainingSorts,
                                                      ImmutableMap<GenericSort,Sort> p_curRes,
                                                      ImmutableList<GenericSortCondition> p_conditions,
                                                      ImmutableList<GenericSort> p_pushedBack,
                                                      GenericSort p_gs,
                                                      ImmutableList<Sort> p_subsorts,
                                                      ImmutableList<Sort> p_chosenList,
                                                      Services services)

chooseResults

private static ImmutableList<Sort> chooseResults(GenericSort p_gs,
                                                 ImmutableList<GenericSortCondition> p_idConditions)
                                          throws GenericSortInstantiations.FailException

Throws:

GenericSortInstantiations.FailException

toList

private static ImmutableList<Sort> toList(ImmutableSet<Sort> p_set)

condSort

private static Sort condSort(java.util.Iterator<GenericSortCondition> itC)

addChosenInstantiations

private static ImmutableList<Sort> addChosenInstantiations(ImmutableMap<GenericSort,Sort> p_curRes,
                                                           GenericSort p_gs,
                                                           ImmutableList<Sort> p_subsorts)

solveForcedInst

private static ImmutableMap<GenericSort,Sort> solveForcedInst(ImmutableList<GenericSort> p_remainingSorts,
                                                              ImmutableMap<GenericSort,Sort> p_curRes,
                                                              ImmutableList<GenericSortCondition> p_conditions,
                                                              Services services)

Method which is called by solveHelp and tries to instantiate the generic sorts for which GSCForceInstantiation-conditions (with "maximum" parameter) are contained within "p_conditions"

Parameters:

p_curRes - instantiations so far

p_conditions - conditions (see above)

Returns:

a solution if one could be found, null otherwise

solveForcedInstHelp

private static ImmutableMap<GenericSort,Sort> solveForcedInstHelp(ImmutableList<GenericSort> p_remainingSorts,
                                                                  ImmutableMap<GenericSort,Sort> p_curRes,
                                                                  Services services)

Method which is called recursively and tries to instantiate one (the first) generic sort from the "p_remainingSorts"-list

Parameters:

p_remainingSorts - generic sorts which needs to be instantiated (topologically sorted, starting with the most general sort)

p_curRes - instantiations so far

Returns:

a solution if one could be found, null otherwise

topology

private static ImmutableList<GenericSort> topology(ImmutableList<GenericSort> p_sorts)

Sort generic sorts topologically, i.e. if sort A is a supersort of sort B, then A appears behind B within the return value

Returns:

sorted sorts

minimalSupersorts

private static ImmutableList<Sort> minimalSupersorts(ImmutableList<Sort> p_sorts,
                                                     Services services)

Find all minimal common supersorts of "p_itSorts" PRECONDITION: !p_sorts.isEmpty ()

findMinimalElements

private static ImmutableList<Sort> findMinimalElements(java.util.Set<Sort> p_inside)

Find all minimal elements of the given set p_inside

getOneOf

private static Sort getOneOf(java.util.Set<Sort> p_set)

addSortsToSet

private static void addSortsToSet(java.util.Set<Sort> p_set,
                                  ImmutableSet<Sort> p_sorts)

isSupersortOf

private static boolean isSupersortOf(Sort p_s,
                                     ImmutableList<Sort> p_subsorts)

Returns:

true iff "p_s" is supersort of every sort of "p_subsorts"

isPossibleInstantiation

private static boolean isPossibleInstantiation(GenericSort p_gs,
                                               Sort p_s,
                                               ImmutableMap<GenericSort,Sort> p_curRes)

Returns:

true iff "p_s" is a valid instantiation of the generic sort "p_gs", and this instantiation is consistent with previously chosen instantiations

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getAllInstantiations

public ImmutableMap<GenericSort,Sort> getAllInstantiations()

ONLY FOR JUNIT TESTS