CN: Separate well-typed and consistency checks #797
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
WellTyped/well-formedness checks were intertwined with the typing monad because they also performed consistency checks. This made running just the well-formedness checks slower, and did not allow users to opt-out of running the consistency check. This commit adds variants `consistent` functions, which are variants on the `welltyped` functions. The latter add variables to scope and check basetypes; the former add variables to scope, constraints and resources. It also tidies up the wellTyped.ml module to clarify and restrict which of the typing monad functions it was using. This will be the first step of many to factor out the logging and the error reporting for different phases. This commit also required an update to the `pure` function in the typing monad, so that it can work without a solver (functionality with a solver initialised should be unaffected). Slightly awkwardly, the reshuffle also required gathering and delaying adding the range constraints for global variables, since adding constraints and resources both require the solver to be initialised. This can and should be tidied up, which will come in subsequent commits, but for now this should pass all tests.
dc-mak
force-pushed
the
cn-separate-bt-consistency
branch
from
f75629f to
40a0164
Compare
dc-mak
added a commit
to dc-mak/cn-tutorial
that referenced
this pull request
Dec 27, 2024
dc-mak
added a commit
to rems-project/cn-tutorial
that referenced
this pull request
Dec 27, 2024
dc-mak
added a commit
to dc-mak/cn-tutorial
that referenced
this pull request
Dec 27, 2024
dc-mak
added a commit
to dc-mak/cn-tutorial
that referenced
this pull request
Dec 27, 2024
dc-mak
added a commit
to rems-project/cn-tutorial
that referenced
this pull request
Dec 27, 2024
dc-mak
added a commit
to dc-mak/cerberus
that referenced
this pull request
Dec 28, 2024
PR rems-project#797 split out the consistency and welltyped checks for a few constructs, but accidentally removed the consistency checks for labels. This commit adds them back. This commit also deletes some code which was made redundant by aba34a0, but was not deleted in that commit.
dc-mak
added a commit
to dc-mak/cerberus
that referenced
this pull request
Dec 29, 2024
PR rems-project#797 split out the consistency and welltyped checks for a few constructs, but accidentally removed the consistency checks for labels. This commit adds them back. This commit also deletes some code which was made redundant by aba34a0, but was not deleted in that commit.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
WellTyped/well-formedness checks were intertwined with the typing monad because they also performed consistency checks. This made running just the well-formedness checks slower, and did not allow users to opt-out of running the consistency check.
This commit adds variants
consistentfunctions, which are variants on thewelltypedfunctions. The latter add variables to scope and check basetypes; the former add variables to scope, constraints and resources.It also tidies up the wellTyped.ml module to clarify and restrict which of the typing monad functions it was using. This will be the first step of many to factor out the logging and the error reporting for different phases.
This commit also required an update to the
purefunction in the typing monad, so that it can work without a solver (functionality with a solver initialised should be unaffected).Slightly awkwardly, the reshuffle also required gathering and delaying adding the range constraints for global variables, since adding constraints and resources both require the solver to be initialised.
This can and should be tidied up, which will come in subsequent commits, but for now this should pass all tests.