Skip to content

add name hint metadata to terms for pretty-printing#3201

Draft
danmatichuk wants to merge 1 commit intomasterfrom
issue3073
Draft

add name hint metadata to terms for pretty-printing#3201
danmatichuk wants to merge 1 commit intomasterfrom
issue3073

Conversation

@danmatichuk
Copy link
Copy Markdown
Contributor

@danmatichuk danmatichuk commented Apr 27, 2026

partially addresses #3073

Attaches some provenance information to subterms that may be used when inventing variable names for memoization.

Currently this data exists as a field in Term, which is a bit wonky because it violates the invariant that terms with the same index must be equal. However, for most purposes this doesn't matter, it (should) only be relevant for printing. The current downside is that term caching can cause some provided name hints to be ignored (instead using the name hints that were present when the cache entry was made).

Update: see comment

@danmatichuk
Copy link
Copy Markdown
Contributor Author

I've re-implemented this in order to make the term metadata a formal TermF constructor. This required some changes to a number of primitives, so that they both ignore the metadata wrappers, and preserve metadata wherever appropriate.

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.

1 participant