Map from subexpr positions in
e₀to diff points.
A map from subexpr positions in
e₁to 'diff points' which are tags describing how the expression has changed relative to
beforeat the given position.
A description of the differences between a pair of expressions
after : Expr.
The information can be used to display a 'visual diff' for
before, showing the parts of the expression that are about to change,
after showing which parts of the expression have changed.
Computes a diff between
This works by recursively comparing function arguments.
TODO(ed): experiment with a 'greatest common subexpression' design where
e₁, find the greatest common subexpressions
Xs : Array Expr and a congruence
F such that
e₀ = F[A₀[..Xs]] and
e₀ = F[A₁[..Xs]]. Then, we can have fancy diff highlighting where common subexpressions are not highlighted.
Diffing binders #
Two binding domains are identified if they have the same user name and the same type.
The most common tactic that modifies binders is after an
To deal with this case, if
before = (a : α) → β and
after, is not a matching binder (ie: not
(a : α) → _)
then we instantiate the
before variable in a new context and continue diffing
after : Expr, and the rendered
infoAfter : CodeWithInfos for
this function decorates
infoAfter with tags indicating where the expression has changed.
useAfter == false before and after are swapped.
Diffs the given hypothesis bundle against the given local context.
useAfter == true,
ctx₀ is the context before and
h₁ is the bundle after.
useAfter == false, these are swapped.
Decorates the given goal
i₁ with a diff by comparing with goal
useAfter is true then
i₁ is after and
g₀ is before. Otherwise they are swapped.
goalsAfter with additional information about how it is different to
igs₁ is the set of interactive goals after the tactic has been applied.
igs₁ is the set of interactive goals before.