Add dedicated node and constructor for general custom contracts #1964
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Continue to address #1466.
After introducing a special AST node and constructor for contracts built from a predicate in #1955, this PR introduces another variant for generic custom contracts. For backward compatibility reasons, we still need to support custom contracts given as naked functions, but this PR migrates examples, the stdlib and the documentation to using this new node through the
std.contract.custom
constructor. The only module that isn't migrated is theinternals
module, because it was harder to do without breaking things (it can surely be done, but it requires a bit more changes), and because those primitive contracts aren't really user-facing and thus it's less important for error messages and the like that they follow the new convention. As this PR is already sizeable, this is left for future work (or maybe we don't want to do it at all).The documentation is updated in way that already assumes the as-of-yet nonexistent
std.contract.from_validator
, planned in a follow-up PR, because it was harder to pretend that it won't exist, or put differently, it would have required more effort to update the documentation once again with this new intermediate type of custom contract than to just leave a placeholder and pretend it already exists.#1955 introduced predicates as functions, where the AST node also stores the function's parameter - the idea was to be more typed, and avoid having something else than a function lying in a
CustomContract
node. Unfortunately, I realized while working on this PR that custom contracts as predicates can actually also be match expressions. We could add a variant for things that are either functions or match expressions, but it starts to be verbose and to cause more code duplication. For now, I reverted to using a genericRichTerm
there, where the only hypothesis is that it's a WHNF that can be applied to some arguments.