Skip to content

Render List.append as @ and keep functions fully qualified in goal state - #87

Closed
grantpassmore wants to merge 1 commit into
christoph/new-goal-statefrom
grant/fix-append
Closed

Render List.append as @ and keep functions fully qualified in goal state#87
grantpassmore wants to merge 1 commit into
christoph/new-goal-statefrom
grant/fix-append

Conversation

@grantpassmore

Copy link
Copy Markdown
Member

The goal-state term formatter mapped List.append to @ and computed the proper operator name, but a subsequent module-stripping step overwrote it, turning @ back into infix append and shortening List.length to length.

Drop the module-stripping so operator aliases (@, <==>, ==>) survive and ordinary functions stay fully qualified (List.length). The full id remains available in the hover.

i.e., PR for going from this:

image

to this:

image

The goal-state term formatter mapped List.append to @ and computed the
proper operator name, but a subsequent module-stripping step overwrote it,
turning @ back into infix append and shortening List.length to length.

Drop the module-stripping so operator aliases (@, <==>, ==>) survive and
ordinary functions stay fully qualified (List.length). The full id remains
available in the hover.
// Map operator names to their visual form if different, e.g. `iff` vs `<==>`
// Map operator names to their visual form if different, e.g. `iff` vs
// `<==>`, or `List.append` vs `@`. Names that don't have a special visual
// form are kept fully qualified (e.g. `List.length`).

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I absolutely have to keep module name stripping, because otherwise my entire screen is filled with module names and I can't see what the code means. The fully qualified name is always in the hover if you need to see it.

@wintersteiger

Copy link
Copy Markdown
Collaborator

After losing a bunch of sleep over this last night, I am now surer than ever that my gut feeling was right all along: this is not a "UI" issue at all, but an operator design issue, and this is the wrong place to fix it.

Here's my reasoning: If we like the @ operator, then why do we throw all of its occurrences away as literally the first step of everything we do, and then try to patch it back at the very end? That's not right. If we prefer @, we should never throw it away and always use it internally as well. Therefore, List.append should be a macro for @ and not the other way around. That's a trivial fix and we can remove a whole bunch of special casing in a number of printers.

(Also, less important, but in a user-defined List module, users could never do something like patching the goal state formatter, but they can trivially design their own operators in the same fashion.)

(Some time in the not too distant future, I'll add a @@render_as or similar attribute that lets the user specify how to render a function/operator in other languages and that could also include the goal state language.)

@wintersteiger

Copy link
Copy Markdown
Collaborator

(Implemented as discussed via #85)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants