Improve behaviour regarding unsupported constructs#468
Open
n-osborne wants to merge 5 commits into
Open
Conversation
n-osborne
force-pushed
the
unsupported
branch
3 times, most recently
from
5ba8c9b to
9dabbbc
Compare
This commit makes Gospel type-checker stop failling when it encounters an unsupported construct. The unsupported constructs are simply filtered out of the untyped ast.
The `Uattr2spec.Unsupported` exception now carries two pieces of information: 1. a description of the construct (polymorphic variant, object...) 2. the location
If an unsupported construct is specified, we raise an `Unsupported` error as the spcifications don't make any sense. If an unsupported construct appears in the module but is not annotated with some Gospel specification, we simply ignore it.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
This patch proposes to improve how unsupported OCaml constructs are handled by the Gospel type-checker.
Fixes #467
The current behaviour is to fail with an
assert falsewhen we encounter an unsupported construct.This is decided when parsing the OCaml attributes containing the Gospel annotation (with the AST traversal).
The proposed behaviour is to fail with an informative error message when an unsupported OCaml contruct is annotated with some Gospel specifications.
Unupported OCaml constructs that are not annotated are simply ignored.
The information carried by the error is the name of the construct and the location so that the incriminated line of code is displayed with the error message.
Caveat:
test/Typechecking/unsupported/variant_as_argument.mlireads as follow:What is happening is that the type declaration is ignored (unsupported but not specified), the type-checker later adds a header to the unspecified value definition and fail to find
tin the typing environment.But this is related to another problem, hence out of scope of this patch.