public class SequentChangeInfo
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private SemisequentChangeInfo |
antecedent
change information related to the antecedent, this means the
there added and removed formulas
|
private Sequent |
originalSequent
the sequent before the changes
|
private Sequent |
resultingSequent
the sequent after the changes
|
private SemisequentChangeInfo |
succedent
change information related to the antecedent, this means the
there added and removed formulas
|
Modifier | Constructor and Description |
---|---|
private |
SequentChangeInfo(SemisequentChangeInfo antecedent,
SemisequentChangeInfo succedent,
Sequent resultingSequent,
Sequent originalSequent)
creates a new sequent change information object.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentFormula> |
addedFormulas()
The formulas added to the sequent are returned as a concatenated list of
the formulas added to each semisequent.
|
ImmutableList<SequentFormula> |
addedFormulas(boolean antec)
The formulas added to one of the semisequents are returned.
|
void |
combine(SequentChangeInfo succ)
This method combines the change information from this info and its successor.
|
private <T> ImmutableList<T> |
concatenateHelper(ImmutableList<T> antecList,
ImmutableList<T> succList)
concatenates the two lists in arbitrary but deterministic order
|
static SequentChangeInfo |
createSequentChangeInfo(boolean antec,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by the
value of the selector antec (true selects antecedent; false selects
succedent) has changed.
|
static SequentChangeInfo |
createSequentChangeInfo(PosInOccurrence pos,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by position
pos has changed.
|
static SequentChangeInfo |
createSequentChangeInfo(SemisequentChangeInfo anteCI,
SemisequentChangeInfo sucCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequents have changed.
|
Sequent |
getOriginalSequent() |
SemisequentChangeInfo |
getSemisequentChangeInfo(boolean antec) |
boolean |
hasChanged()
returns true iff the sequent has been changed by the operation
|
boolean |
hasChanged(boolean antec)
returns true if the selected part of sequent has changed.
|
ImmutableList<FormulaChangeInfo> |
modifiedFormulas()
The formulas modified within the sequent are returned as a
concatenated list of the formulas modified within each each
semisequent.
|
ImmutableList<FormulaChangeInfo> |
modifiedFormulas(boolean antec)
The formulas modified within one of the semisequents are
returned.
|
ImmutableList<SequentFormula> |
rejectedFormulas()
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
rejectedFormulas(boolean antec)
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
removedFormulas()
The formulas removed from the sequent are returned as a
concatenated list of the formulas removed from each semisequent.
|
ImmutableList<SequentFormula> |
removedFormulas(boolean antec)
The formulas removed from one of the semisequents are returned.
|
Sequent |
sequent()
returns the resulting sequent
|
java.lang.String |
toString()
toString
|
private java.lang.String |
toStringHelp(boolean antec)
toString helper
|
private SemisequentChangeInfo antecedent
private SemisequentChangeInfo succedent
private Sequent originalSequent
private Sequent resultingSequent
private SequentChangeInfo(SemisequentChangeInfo antecedent, SemisequentChangeInfo succedent, Sequent resultingSequent, Sequent originalSequent)
antecedent
- the SemisequentChangeInfo describing the changes of
the antecedentsuccedent
- the SemisequentChangeInfo describing the changes of
the succedentresultingSequent
- the Sequent being the result of the changesoriginalSequent
- the Sequent that has been transformedpublic static SequentChangeInfo createSequentChangeInfo(PosInOccurrence pos, SemisequentChangeInfo semiCI, Sequent result, Sequent original)
pos
- the PosInOccurrence describing the semisequent where
the changes took placesemiCI
- the SemisequentChangeInfo describing the changes in
detail (which formulas have been added/removed)public static SequentChangeInfo createSequentChangeInfo(boolean antec, SemisequentChangeInfo semiCI, Sequent result, Sequent original)
antec
- a boolean indicating if the given semisequent change information
describes the changes of the antecedent or succedentsemiCI
- the SemisequentChangeInfo describing the
changes in detail (which formulas have been added/removed)result
- the Sequent which is the result of the changesoriginal
- the Sequent to which the described changes have been
appliedpublic static SequentChangeInfo createSequentChangeInfo(SemisequentChangeInfo anteCI, SemisequentChangeInfo sucCI, Sequent result, Sequent original)
anteCI
- the SemisequentChangeInfo describing the changes of the
antecedent in detail (which formulas have been added/removed)sucCI
- the SemisequentChangeInfo describing the changes of the
succedent detail (which formulas have been added/removed)public boolean hasChanged()
public boolean hasChanged(boolean antec)
public SemisequentChangeInfo getSemisequentChangeInfo(boolean antec)
public ImmutableList<SequentFormula> addedFormulas(boolean antec)
antec
- a boolean used to select one of the two semisequents
of a sequent (true means antecedent; false means succedent)public ImmutableList<SequentFormula> addedFormulas()
public ImmutableList<SequentFormula> removedFormulas(boolean antec)
antec
- a boolean used to select one of the two semisequents
of a sequent (true means antecedent; false means succedent)public ImmutableList<SequentFormula> removedFormulas()
public ImmutableList<FormulaChangeInfo> modifiedFormulas(boolean antec)
antec
- a boolean used to select one of the two semisequents
of a sequent (true means antecedent; false means succedent)public ImmutableList<FormulaChangeInfo> modifiedFormulas()
public ImmutableList<SequentFormula> rejectedFormulas(boolean antec)
antec
- a boolean used to select one of the two semisequents
of a sequent (true means antecedent; false means succedent)public ImmutableList<SequentFormula> rejectedFormulas()
private <T> ImmutableList<T> concatenateHelper(ImmutableList<T> antecList, ImmutableList<T> succList)
antecList
- the list of antecedent elementssuccList
- the list of succeden elementspublic void combine(SequentChangeInfo succ)
succ
and does not release it. This means
when invoking the method it must be ensured that succ
is never used afterwards.public Sequent getOriginalSequent()
public Sequent sequent()
private java.lang.String toStringHelp(boolean antec)
public java.lang.String toString()
toString
in class java.lang.Object