Skip to content
This repository has been archived by the owner on Dec 1, 2022. It is now read-only.

[smt2parser] Add support for name resolution #27

Merged
merged 4 commits into from Jun 4, 2021

Conversation

ma2bd
Copy link

@ma2bd ma2bd commented Jun 3, 2021

Provide a working implementation of name resolution and name normalization for SMT2 files with the following caveats:

  • The old syntax for testers is-Foo is not compatible with name resolution. One needs to replace is-Foo into (_ is Foo) first using the given rewriter renaming::TesterModernizer (see unit tests).
  • Error handling is not fully satisfying yet: visitor APIs do not use Result yet and will panic! in case of unknown symbol. (However, this only affects people using the new name-resolution callbacks, not the parsing.)
  • The LALR parser will attempt to call some of the new callbacks but proper name resolution requires to use SyntaxBuilder first, then visit the concrete syntax again. See the unit test of the utility type renaming::SymbolNormalizer.

@facebook-github-bot facebook-github-bot added the CLA Signed This label is managed by the Facebook bot. Authors need to sign the CLA before a PR can be reviewed. label Jun 3, 2021
@ma2bd ma2bd merged commit d6e35e5 into facebookarchive:master Jun 4, 2021
@ma2bd ma2bd deleted the name_resolution branch June 4, 2021 17:47
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
CLA Signed This label is managed by the Facebook bot. Authors need to sign the CLA before a PR can be reviewed.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants