RFE: Improvement on "last derivation in sequence does not match"

[Daniel Spiewak]

Consider the following simple example (assume the obvious syntax and
judgments have been defined):

_: s t > t by case analysis on p:
case rule
...
is
p2: ...
_: s t' > t by case analysis on p2: // note the
typo!
case rule
...
is
...
_: s t > t by rule obvious
end case
end case analysis
end case
end case analysis

In this nested series of case analyses, the final (inner-most)
derivation matches the original target. However, one of the
intermediate steps has a typo, meaning that it does not match either
the first or the final derivation. This pattern of nested case
analyses seems to be extremely common, particularly with more
complicated judgments.

At the moment, SASyLF will correctly take issue with this proof in the
form of a "last derivation in sequence..." error. However, this error
will be flagged *on the inner-most* derivation. This derivation is
actually correct w.r.t. the final derivation, making errors like these
somewhat confusing to diagnose and fix.

I think the problem is that SASyLF checks matching derivations
starting from the inside-out. Thus, it sees that (s t > t) does not
match (s t' > t) before it would have seen that (s t' > t) does not
match (s t > t). I think that these errors would be significantly
easier to deal with if the checker were to start at the outer-most
level and work its way inwards, checking that derivations match along
the way. If this were implemented, the checker would have flagged the
actual offending derivation in my example, rather than the unwittingly-
correct inner derivation.

Daniel