de.uka.ilkd.key.gui.mergerule

Class MergeProcedureCompletion<C extends MergeProcedure>

java.lang.Object

de.uka.ilkd.key.gui.mergerule.MergeProcedureCompletion<C>

Direct Known Subclasses:

PredicateAbstractionCompletion

public abstract class MergeProcedureCompletion<C extends MergeProcedure>
extends java.lang.Object

A completion class for merge procedures. Certain procedures, such as MergeWithPredicateAbstraction, may not be complete initially and need additional input.

Author:

Dominic Scheurer

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	MergeProcedureCompletion() Default constructor is hidden.

Method Summary

Modifier and Type	Method and Description
abstract C	complete(C proc, Pair<Goal,PosInOccurrence> mergeGoalPio, java.util.Collection<MergePartner> partners) Completes the given merge procedure either automatically (if the procedure is already complete) or by demanding input from the user in a GUI.
static <T extends MergeProcedure> MergeProcedureCompletion<T>	create(java.util.function.Function<T,T> completion)
static <T extends MergeProcedure> MergeProcedureCompletion<T>	defaultCompletion()
static MergeProcedureCompletion<? extends MergeProcedure>	getCompletionForClass(java.lang.Class<? extends MergeProcedure> cls) Returns the completion for the given merge procedure class.

Methods inherited from class java.lang.Object

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

Constructor Detail

MergeProcedureCompletion

protected MergeProcedureCompletion()

Default constructor is hidden. Use create(Function) instead.

Method Detail

defaultCompletion

public static <T extends MergeProcedure> MergeProcedureCompletion<T> defaultCompletion()

Returns:

The default completion (identity mapping).

create

public static <T extends MergeProcedure> MergeProcedureCompletion<T> create(java.util.function.Function<T,T> completion)

complete

public abstract C complete(C proc,
                           Pair<Goal,PosInOccurrence> mergeGoalPio,
                           java.util.Collection<MergePartner> partners)

Completes the given merge procedure either automatically (if the procedure is already complete) or by demanding input from the user in a GUI.

Parameters:

proc - MergeProcedure to complete.

mergeGoalPio - The Goal and PosInOccurrence identifying the merge goal.

partners - The MergePartners chosen.

Returns:

The completed MergeProcedure.

getCompletionForClass

public static MergeProcedureCompletion<? extends MergeProcedure> getCompletionForClass(java.lang.Class<? extends MergeProcedure> cls)

Returns the completion for the given merge procedure class.

Returns:

The requested completion.