agda icon indicating copy to clipboard operation
agda copied to clipboard

Remove indirections to builtins/primitives in `QName`

Open andreasabel opened this issue 3 months ago • 1 comments

We currently share the QName between abstract and internal syntax. However, after scope checking we could resolve all the BUILTINs and primitives to their special identifier, so that I.QName could directly tell us which builtin we deal with (if any). This would have the advantage that we could work with builtins in pure code, e.g. in smart level constructors. We would also shave off some cycles by not always having to call getBuiltin.

I expect such refactoring could fix the following issue without performance penalty:

  • #8100

andreasabel avatar Oct 13 '25 10:10 andreasabel

Agda dev meeting 2025-10-15: Alternative: have nicifier lift BUILTINs so that we can already in the scope checker resolve builtins. However, we have a problem with BUILTIN NATURAL / MAYBE as the constructors are resolved to the ZERO/SUC etc builtins by type. Suggestion: bring back BUILTIN NATZERO etc.

andreasabel avatar Oct 15 '25 13:10 andreasabel