WIP: Reference terms

[mattulbrich]

Introduce reference term. They can be used to model reference dependencies over rule applications. They will be removed from the terms before adding them to the sequent. But before they indicate dependencies.

If we apply swapAdd on the sequent

phi |- 0 < x+y

then the proof application would contain the replacement

S.0.1  ---->  y«S.0.1.1» + x«S.0.1.0»

which allows the reference mapping to track that.

Still needs discussion. Not ready for merge yet. @JonasKlamroth

[JonasKlamroth]

i like the basic idea however i am not quite sure if we do in fact need those or if this is already possible to be modeled with the existing TermParameters. As long as those references are only needed after rule applications i feel like TermParameters should already be able to capture this

[mattulbrich]

Ok.

In the above example: How would you resolve the reference for "x" if the substitution read

S.0.1 ---> y+x

From this information alone it is not possible to know the origin of "x". Yes, it may be possible to compute this from the object identities ("x" is the same term which used to be at S.0.1.0 and we can attach it. But this has two drawbacks:

• if anyone uses object sharing (reusing objects for the same term), this mechanism breaks.
• One is restricted to referencing objects which occur verbatim in the sequent.

[JonasKlamroth]

ok now i get it. thats purely for the reference highlighting! The replacement itself could be done anyway but the references could get lost.