Record Class BadVDiff<L extends Label>

java.lang.Object
java.lang.Record
org.variantsync.diffdetective.variation.diff.bad.BadVDiff<L>
Record Components:
diff - The variation tree that models the tree diff.
matching - Memorization of which nodes are clones and can be safely merged when converting back to a variation diff.
coloring - Memorization of the diff types of all nodes.
lines - Memorization of line ranges within text diffs.

public record BadVDiff<L extends Label>(VariationTree<L extends Label> diff, Map<VariationTreeNode<L extends Label>,VariationTreeNode<L extends Label>> matching, Map<VariationTreeNode<L extends Label>,DiffType> coloring, Map<VariationTreeNode<L extends Label>,DiffLineNumberRange> lines) extends Record
A bad variation diff is a variation diff that has no subtree sharing. This means that the diff is a tree. We thus can store the diff as a variation tree with some extra information. This allows us to prove the variation diff being a tree at the type level.

When converting a variation diff to a bad one, cycles

    .
   / \
  /   \
 .     .
 \    /
  \  /
   x
 
are resolved by cloning the deepest subtree x in the cycle.
    .
   / \
  /   \
 .     .
 |     |
 |     |
 x     x
 
The matching in a bad variation diff stores which nodes have been cloned.

As variation trees do not store any diff-specific information, we remember the nodes difftype in the original variation diff in a coloring map.

(Unproven) Invariants: for all VariationDiff d: fromGood(d).toGood() equals d

Author:
Paul Bittner