🪟 Translucency: semi-abstract definitions and unfolding via extension types

[jonsterling]

OK, I'm running out of steam today but let me record what I need to do:

• [x] Incorporate for each Global.t the list of other global unfolders it requires, and its associated unfolder dimension.
• [x] Make the unfolder imply each requirement
• [x] Make the unfolder imply each unfolding
• [x] Elaborate the type under its requirements
• [x] Elaborate the term under its unfolder
• [x] Add the requirements and unfoldings to the concrete syntax

[jonsterling]

So let me summarize the state of things here. This is a proof of concept PR for a research paper, and I am not requesting that it be merged at this time unless substantial improvements are made. But it is already really cool and suffices to test out the research ideas 😎

What would need to be done for this to be mergeable / usable is:

• [x] Top-level definitions should be printed in a less abstract way. Right now it is just a bunch of axioms of a very complicated type involving sub and (foo : phi) -> bar. It should be possible to print these in a more user friendly language like that conveys this is an abstract definition whose type requires blah-blah-blah, which will unfold to blah-blah-blah when requested. (This is done, but in #375). Incorporated.

• [x] Right now all top-level definitions take a proof argument (for cofibration that governs their requirements, i.e. the unfoldings needed to make their type well-formed). This argument is automatically inserted by the refiner when the definition is used (resulting in an error when the requisite cofibration is not yet true). This argument is shown in the pretty printer: so we have + * x y rather than + x y everywhere. We should work to make this invisible to the user somehow. (This is no longer an issue in #375). Incorporated.

• [x] The new modifiers are only supported on def/axiom. But we need these to be supported on other commands, like #normalize and perhaps even #print.

• [x] I have broken the parsing of !def because I couldn't figure out the conflicts in the parser. I realize the 🧞 has retired, but this would have to get fixed before this PR is merged.

[jonsterling]

The main usability problems with this PR have been addressed and now I think it constitutes a strict improvement on what is in main. Therefore I think it is possible to merge this PR, pending review and whatever changes are suggested.

[favonia]

Following the comments above, if we wish to have keep the current generality, I think we could maybe make the type of unfolder being a list or something. The semantics of [d1; d2; d3] would be meet [eq1 d1; eq1 d2; eq3], and maybe it would be interesting for a top-level def to share the unfolder of another top-level def?

Maybe this is already something easily doable in the current framework.

EDIT: Add the second paragraph.

[jonsterling]

Following the comments above, if we wish to have keep the current generality, I think we could maybe make the type of unfolder being a list or something. The semantics of [d1; d2; d3] would be meet [eq1 d1; eq1 d2; eq3], and maybe it would be interesting for a top-level def to share the unfolder of another top-level def?

Maybe this is already something easily doable in the current framework.

EDIT: Add the second paragraph.

In principle this is possible, but I don't see a compelling use case for it right now... Do you?

[favonia]

In principle this is possible, but I don't see a compelling use case for it right now... Do you?

What could be interesting is to 100% recreate the abstract block in Agda, which is essentially prefixing everything with the same unfolder.

[jonsterling]

@favonia that's a cool idea.

[jonsterling]

In principle this is possible, but I don't see a compelling use case for it right now... Do you?

What could be interesting is to 100% recreate the abstract block in Agda, which is essentially prefixing everything with the same unfolder.

Hmm @favonia I think that prefixing a bunch of definitions under the same unfolder is not a use-case for the generality you are proposing; it in particular does not need a single global to have multiple unfolders.

[favonia]

Hmm @favonia I think that prefixing a bunch of definitions under the same unfolder is not a use-case for the generality you are proposing; it in particular does not need a single global to have multiple unfolders.

That's correct, but this would justify the current (unnecessary imo) generality. The list thing is for composable and resumable abstract regions/blocks.

[jonsterling]

@favonia If you feel the current generality is unnecessary, please feel free to fix the #376 PR where I tried to implement your proposed downgrade ;-) I got stuck and I couldn't figure out what happened, but maybe your knowledge of the units mechanism will help you make progress where I failed.

[favonia]

@favonia If you feel the current generality is unnecessary, please feel free to fix the #376 PR where I tried to implement your proposed downgrade ;-) I got stuck and I couldn't figure out what happened, but maybe your knowledge of the units mechanism will help you make progress where I failed.

BTW the #376 is a bit different from what I imagined, and I realized the unleash_top_level could not be structured in a way I wanted it to be anyways, so maybe we should just give up #376. :laughing: