Origin Information in all Processing Phases of Sequenters

[sgrebing]

• Keep origin information in all Sequenters and in all phases. especially in the post processing phase.
• Generate qualitative ReferenceTargets for origins from skolemization, anonymization, ...

See branch referenceGraph for improved versions of ReferenceTargets

[mattulbrich]

It's not 100% clear what the goal of this issue is.

Commit bd56114 makes the inline sequenter remember all references.

@JonasKlamroth, the LetInliner class can now do book keeping about references for subterm selectors. It might be a possibility to knit a rule expandAllLets around that which.

What is meant by phases?

For the second bullet point, the concept of reference targets needs to be moved to the core. Should be discussed.

[sgrebing]

What is meant by phases?

The sequenter has a Post processing phase in which reference information gets lost

For the second bullet point, the concept of reference targets needs to be moved to the core. Should be discussed.

ReferenceTargets is just the new name for References (currently on master). A ReferenceTarget It is the endpoint of a reference which is stored in the reference graph. In the new implementation we may have CodeReferenceTargets (code elemenst are the endpoints), ProofTermReferenceTargets (proof terms in proofnodes are the endpoints), ScriptReferenceTargets (script AST Nodes are the end points), DescriptionReferenceTarget ( a descuription in natural language is the endpoint, to display it e.g., as tooltip) and UserInputReferenceTarget (endpoint is a userinput)