Class RefineOperator

java.lang.Object

ca.mcscert.jpipe.operators.CompositionOperator

ca.mcscert.jpipe.operators.builtin.RefineOperator

public final class RefineOperator
extends CompositionOperator

Built-in refine composition operator.

Syntax:

justification result is refine(base, refinement) {
    hook: "elementId"
}

Semantics: the hook element (identified by its id in the first source model) and the conclusion of the second source (refinement) are merged into a single SubConclusion named "hook". All other elements are kept with their source model name as id prefix (e.g. base:c, refinement:s).

The hook id is resolved through the unit alias map, so it can refer to an element that was renamed by a prior composition step (e.g. unification after assemble).

Field Summary

Fields

Modifier and Type	Field	Description
static final String	HOOK_ID	The fixed id of the merged SubConclusion in the result model.

Constructor Summary

Constructors

Constructor	Description
RefineOperator()

Method Summary

Modifier and Type	Method	Description
protected Command	createResultModel(String name, SourceLocation location, List<JustificationModel<?>> sources, Map<String,String> arguments)	Returns the command that creates the result model (typically CreateJustification or CreateTemplate).
protected EquivalenceRelation	equivalenceRelation(List<JustificationModel<?>> sources, Map<String,String> arguments, Map<String,String> knownAliases)	Returns the equivalence relation to use for partitioning elements from sources and arguments.
protected MergeFunction	mergeFunction(List<JustificationModel<?>> sources, Map<String,String> arguments)	Returns the merge function to use for creating result elements from sources and arguments.
protected Set<String>	requiredArguments()	Declares which argument keys this operator requires.

Methods inherited from class CompositionOperator

additionalCommands, apply, apply, apply, apply, resultKind

Methods inherited from class Object

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

Field Details

HOOK_ID

public static final String HOOK_ID

The fixed id of the merged SubConclusion in the result model.

See Also:

• Constant Field Values

Constructor Details

RefineOperator

public RefineOperator()

Method Details

requiredArguments

protected Set<String> requiredArguments()

Description copied from class: CompositionOperator

Declares which argument keys this operator requires. The framework validates their presence at the start of CompositionOperator.apply(String, List, Map) and throws InvalidOperatorCallException listing any missing keys. Default: empty set (no required arguments).

Overrides:

requiredArguments in class CompositionOperator

createResultModel

protected Command createResultModel(String name,
 SourceLocation location,
 List<JustificationModel<?>> sources,
 Map<String,String> arguments)

Description copied from class: CompositionOperator

Returns the command that creates the result model (typically CreateJustification or CreateTemplate).

Specified by:

createResultModel in class CompositionOperator

Parameters:

location - the source location of the operator call; forwarded to the creation command so the result model appears in the symbol table.

sources - the source models being composed; provided so operators can choose the result model type (e.g. Template vs Justification) based on the source types.

equivalenceRelation

protected EquivalenceRelation equivalenceRelation(List<JustificationModel<?>> sources,
 Map<String,String> arguments,
 Map<String,String> knownAliases)

Description copied from class: CompositionOperator

Returns the equivalence relation to use for partitioning elements from sources and arguments.

Specified by:

equivalenceRelation in class CompositionOperator

Parameters:

knownAliases - alias registry of the compilation unit (keyed as "modelName/oldId"); operators may use this to resolve element ids that were renamed by a prior composition step.

mergeFunction

protected MergeFunction mergeFunction(List<JustificationModel<?>> sources,
 Map<String,String> arguments)

Description copied from class: CompositionOperator

Returns the merge function to use for creating result elements from sources and arguments.

Specified by:

mergeFunction in class CompositionOperator