Skip to content

Conversation

@Gbury
Copy link
Owner

@Gbury Gbury commented May 22, 2025

This PR adds some hierarchy in the typed builtins. Previously all the builtins lived in a flat namespace, but now there is (most of the time) one extensible constructor builtin by theory, which wraps a dedicated (regular) type for the builtins of that theory. This brings a few benefits:

  • We can have an exhaustivity check for functions operating on the primitives of one theory
  • we can have more freedom in the naming of builtins, since we have different namespaces for the builtins of each theory
  • This may result in a slight speedup, since matching on extensible variants is not very optimized

Note that this is a rather large breaking change, since it will likely require to update any pattern matching on builtins, but the translation should be rather mechanical. It is not completely mechanical because I took the opportunity to rename some builtins, taking advantage of the now different namespaces for builtins of different theories (and also to avoid repetitions like | Builtin.Float Fp_foo -> ...).

cc @bobot , in particular for the new names of primitives in the Float theory.

Copy link
Contributor

@bobot bobot left a comment

Choose a reason for hiding this comment

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

Just typos, thanks!

@Gbury Gbury merged commit ce4b789 into master Aug 5, 2025
20 checks passed
@Gbury Gbury mentioned this pull request Aug 7, 2025
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.

3 participants