Re-enable support for "and" inside function/predicate #147
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
In Gbury#129 support was added for mutually recursive function and predicate definitions using the "and" keyword. However, the keyword "and" can also be used to denote the boolean conjunection, but now the conflicts are resolved in such a way that: ``` predicate X = true and true ``` is now a syntax error (upon seeing the [and] token, [predicate X = true] gets reduced into a [predicate_def], and a recursive [function] or [predicate] definition is expected). This patch fixes the issue by marking the appropriate rules (predicate_def, function_def) as inline, propagating enough context to the conflict that it can be resolved appropriately. Note that we are still not able to parse horrors such as: ``` predicate X = true and true and predicate Y = true ``` but that is OK because those were never supported by Alt-Ergo. (as an aside, I don't think it's even possible by using a %right associative token for AND in Menhir)
|
Fixes #144 |
Gbury
approved these changes
May 2, 2023
|
Actually, this probably deserves a note in the |
Gbury
added a commit
to Gbury/opam-repository
that referenced
this pull request
Jul 4, 2023
…men_bin and dolmen (0.9) CHANGES: ### Doc - Add examples in the doc and tuto for type-checking (including a minimal working example in the tutorial). ### UI - Make the unknown logic fatal by default, and simply enabled in non-strict mode (PR#158) - Add the `--check-flow` option to checks coherence of sequences of statements (PR#135) - Ensure stability of error codes for the `dolmen` binary ### Parsing - Add `attrs` fields for all declarations and definition types, and correctly attach predicate attribute to individual definitions (PR#130) - Restore support for toplevel "and" in non-recursive predicate/function definitions in Alt-Ergo syntax (PR Gbury/dolmen#147, fixes issue Gbury/dolmen#144) - Add support for hexadecimal floats in Alt-Ergo syntax (PR Gbury/dolmen#148, fixes issue Gbury/dolmen#145) - Add local goals to the `Prove` statement (PR#140) - Add a check-sat/prove-sat statement to ae's language (PR#140) ### Typing - Ignore arithmetic restrictions when typing model values. This particularly affects difference logic (PR#141) - Rename theory-specific configuration to `config` (instead of `arith`, `arrays`, etc..) (PR#142) - Add printing function for logics (PR#142) - Attach type definitions to type-defs (PR#157) - Add a proper reason for reserved builtins (PR#155) - Add bitvector builtins for alt-ergo's language (PR#136) ### Loop - Add possibility for users of the loop library to choose the exit/return code for a `Code.t` (PR#134) - Add the `Flow` module for flow checking (PR#135) - Add the `check` function in `typer.ml`/`typer_intf.ml` - Add `update` and `update_opt` in `State` (PR#156) - Print type definitions in the printer of typed statements (PR#157) - Prelude statements have been removed and replaced with prelude files (PR#160) - `Typer.additional_builtins` is now a `State.key` and takes the current state and language as arguments (PR#160) ### Model - Fix bug in bitvector implementation: negative inputs to `bvsmod` would raise an internal error (PR#138) - Remove the "error" keyword and statement from smtlib2 response (model) files (PR#139) - Correctly compare abstract array values (PR#143) - Accept extensions of functions/symbols with only partially defined semantics, for e.g. `fp.to_ubv`, `div`, etc.. (PR#151) - Error out on incremental problems (PR#169)
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.
In #129 support was added for mutually recursive function and predicate definitions using the "and" keyword.
However, the keyword "and" can also be used to denote the boolean conjunection, but now the conflicts are resolved in such a way that:
is now a syntax error (upon seeing the [and] token, [predicate X = true] gets reduced into a [predicate_def], and a recursive [function] or [predicate] definition is expected).
This patch fixes the issue by marking the appropriate rules (predicate_def, function_def) as inline, propagating enough context to the conflict that it can be resolved appropriately.
Note that we are still not able to parse horrors such as:
but that is OK because those were never supported by Alt-Ergo.
(as an aside, I don't think it's even possible by using a %right associative token for AND in Menhir)