search

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)
GNU General Public License v3.0
4 stars 0 forks source link

Origin Information in all Processing Phases of Sequenters #115

Open sgrebing opened 5 years ago

sgrebing commented 5 years ago

See branch referenceGraph for improved versions of ReferenceTargets

mattulbrich commented 5 years ago

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

Commit bd56114ed4050f3ea304183c7c1e7194b7043a00 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 commented 5 years ago

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)