Collapsing computationally irrelevant code

[jkzinzindohoue]

Hi Clement,

How hard would it be to implement a feature in the interactive mode which would collapse all the expressions (assumed on a single statement-like line) which either return Tot unit or Ghost 'a pre post ?
I am assuming it may be feasible since the interactive mode gets type information from F* but I have no clue whether it would be easy or not...
It would be an auditing / readability improvement feature for already written code, the idea being to hide all the lemma and ghost calls to only be left with the real code.

Thanks !

[cpitclaudel]

Hi Jean-Karim,

Thanks for the suggestions! I don't think it's currently feasible (but I'm hoping to be wrong!)

The problem is that we have types for identifiers, but not for expressions — that information is computed by the typechecker, but promptly discarded (we used to store it in .tk fields, but I think we got rid of those recently to reduce our memory footprint)

If we had that information in F*, it would be easy to expose it to fstar-mode — we'd just request a collection of text ranges from F*. On the F* side, we'd need two things:

• A way to keep track of type information; I think this could be recovered by adding a hook in the typechecker that allows the interactive mode to record types for subexpressions.
• Better range annotations. For now we have no way to distinguish real terms from terms that were added during elaboration. For example, if you write f 1 2 and f takes an implicit argument, the elaborated AST will contain that extra inferred argument, with the same range as f. If the extra argument is Ghost, we'd end up hiding f :/ There may be clever heuristics that don't require us to annotate all ranges, though.

I might have missed something though. Maybe there's an easier way?