No nesting inside RangeToken.StartToken

[keyboardDrummer]

What was changed?

• Replace wrapping RangeToken.StartToken with wrapping the entire RangeToken. This means:

  • Many functions that only took a RangeToken before must now take an IOrigin instead, to also accept wrapped RangeTokens
  • Since the constructor of RangeToken now only takes Token values, locations that constructed RangeTokens had to be updated to use the correct type.
  • Locations that checked for X is RangeToken now check the virtual method X.IncludesRange. This has the side-effect that error reporting more often detects that a range is available, so it reports "Could not prove <printed expression>" instead of "this proposition could not be proved"

• Let NonglobalVariable and its subclasses (Formal and BoundVar) carry a Name instead of a string, so it's clear what the IOrigin is that contains the name.

• Replace RefinementOrigin.IsInherited, which did unwrapping of tokens to find a RefinementToken, with a virtual method IsInherited.

How has this been tested?

• There are a handful of small changes to expected files. I have inspected each one and they're all improvements.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[ssomayyajula]

I understand the RangeToken -> IOrigin generally, but why IOrigin -> Token in some places (e.g., ApplyExpr.cs)? Is that because you are expecting to construct a RangeToken and need a Token as an argument?

Thanks for making the other refactors!

[keyboardDrummer]

I understand the RangeToken -> IOrigin generally, but why IOrigin -> Token in some places (e.g., ApplyExpr.cs)? Is that because you are expecting to construct a RangeToken and need a Token as an argument?

That is correct.