de.uka.ilkd.key.strategy.termProjection

Class TermConstructionProjection

java.lang.Object

de.uka.ilkd.key.strategy.termProjection.TermConstructionProjection

All Implemented Interfaces:

ProjectionToTerm

public class TermConstructionProjection
extends java.lang.Object
implements ProjectionToTerm

Term projection for constructing a bigger term from a sequence of direct subterms and an operator. NB: this is a rather restricted version of term construction, one can think of also allowing bound variables, etc to be specified

Field Summary

Fields

Modifier and Type	Field and Description
private Operator	op
private ProjectionToTerm[]	subTerms

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TermConstructionProjection(Operator op, ProjectionToTerm[] subTerms)

Method Summary

Modifier and Type	Method and Description
static ProjectionToTerm	create(Operator op, ProjectionToTerm[] subTerms)
Term	toTerm(RuleApp app, PosInOccurrence pos, Goal goal)

Methods inherited from class java.lang.Object

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

Field Detail

op

private final Operator op

subTerms

private final ProjectionToTerm[] subTerms

Constructor Detail

TermConstructionProjection

private TermConstructionProjection(Operator op,
                                   ProjectionToTerm[] subTerms)

Method Detail

create

public static ProjectionToTerm create(Operator op,
                                      ProjectionToTerm[] subTerms)

toTerm

public Term toTerm(RuleApp app,
                   PosInOccurrence pos,
                   Goal goal)

Specified by:

toTerm in interface ProjectionToTerm