Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verified and easy-to-use parser combinators #64

Open
wants to merge 25 commits into
base: master
Choose a base branch
from

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Jan 3, 2023

  • Largely inspired from (Meijer 1996) parsers
  • Each function has some minimal docstring
  • Support for notion of "commitment" and recoverable errors
  • Default Parsers export provides And, Not, Or, OrSeq, Concat, ConcatMap, ConcatL, ConcatR, Lookahead, If, Rep, RepSeq,
    Map, Bind, Recursive, RecursiveMap, RecursiveDef, Debug, Any, Many, BindSucceeds, Succeed Fail, intToString, stringToInt, and failure-compatible ParseResult
  • The Parsers module is abstract as parsers operate on a seq, where C is char in the refining module StringParsers
    StringParsers also export Char, CharTest, Nat, Int, String, Debug
  • Three ways to create parsers: directly as functions: plain combinators, or a nice looking DSL
  • Impossible to create parsers that don't terminate, thanks Dafny. Useful fatal ParseResult in such cases.
  • Possibility to prove that parsers won't return fatal errors and perform progress. Some parser combinators have proofs of progress preservation and absence of fatal errors.
  • Combinators to create recursive and mutually recursive parsers, illustrated in the polynomial parsers example
  • Dual of parsers combinators (Displayers) defined and proved to be the exact inverse in the Concat case. (to discuss: should we just remove them?)
  • Abstract tests currently covering a good portion of the code, including full proofs that intToString and stringToInt are reverse of each other in both ways.
  • Support for multiple error messages
  • For string parsers, a utility to display nice error messages like this:
Error:
1; 1+*   
     ^   
expected '(', or
expected a digit, or
expected 'x'

Missing

  • Integration in the CI and test verification

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@MikaelMayer MikaelMayer changed the title First commit of the parsers combinator Verified and easy-to-use parser combinators Nov 15, 2023
@MikaelMayer MikaelMayer marked this pull request as ready for review November 15, 2023 06:44
@MikaelMayer
Copy link
Member Author

MikaelMayer commented Apr 15, 2024

Note of usability:

  • In the JSON example, extract the function Token?(s: String) whose definition is WS().e_I(S(t)).??()
  • Add a comment to this function explaining what WS() and ??() do
  • More documentation in the README on how to create string-based parsers

@codyroux
Copy link

codyroux commented Apr 17, 2024

Some further minor notes:

  • StringParsersBuilders should be StringParserBuilders, similarly for ParsersBuilders.
  • Minor usability improvements: having an alphanum would be handy, and Space may want to exclude newlines (not sure). Also an EnclosedBy<T>(left: string, p: B<T>, right: string) or something.
  • Some ParsePair, ParseTriple, ParseQuadruple would be nice. A little tedious to write, sadly.
  • A Token("foo", value) implementation which simply does S("foo").M( _ => value) seems convenient.
  • The implementation of Digit can be CharTest(c => '0' <= c <= '9') for efficiency, I think, unless there's some implementation specific reason which would make this incorrect. Or maybe one cannot prove anything about this definition.

None of these are "must haves" though.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants