Feat: Verified and easy-to-use parser combinators #6143

MikaelMayer · 2025-03-07T18:49:31Z

This PR adds to the standard library support for functional parsers and parsers combinators.
A parser is simply a Input -> ParseResult<T> where ParseResult is either a success or a failure that contains the remaining unparsed input. A parsing failure is "committed" if the remaining unparsed input is strictly smaller than the input. Disjunctions can happen only if a failure is not committed. Combinators can help modify the consumption of the input, which makes it possible to create a rich variety of parsers.

The Parsers module is abstract as parsers operate on an Input that can be converted at any time to a seq<C>. In StringParsers, C is a char and Input is a datatype simulating lazy slicing on the input string. That lazy slicing resulted in a +16% speedup on a real benchmark compared to just having seq<char> for Input.

You can browse the example to understand how parsers combinators can be used.

A parser for polynomial expressions like 4*(1+3)*x^3+x
A Tic-tac-toe grid parser

The easiest way to use parsers is to use the parsers builders. Parser builds are a datatype wrapper around parsers to make it possible to have suffix and infix combinators. This allows chaining and avoid nested parentheses. See the following examples:

The same parser for polynomial expressions like 4*(1+3)*x^3+x but the syntax seems better to me.
A JSON-like parser in 70 LoC
A Dafny-like parser that can parse imports, nested modules and declarations
A Parser generator parser that can parse expressions of the type abc((de|f((g))*))ml", create another parser out of that, and apply this parser to an input string like "abcdeml".
A Tic-tac-toe grid parser

Notable features include:

Combinators for repetition do not concatenate sequences with one value at a time. Instead, they build a linked list and when done convert the whole linked list to a sequence. This resulted in a +430% speedup on a benchmark that was using single-character repetition when using the JavaScript version of the parsers.
Debugging utilities and tutorial to explain how to use them in the README.md
It is not possible to create parsers that don't terminate, thanks Dafny for proving it. At worst, a non-terminating parser will always return a "fatal" parsing result that can be still be analyzed at run-time.
It is possible 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 in ParserTheorems.dfy
Dual of parsers combinators (Displayers) defined and proved to be the exact inverse in the Concat case. (to discuss -- should we just remove them as they are immature?)
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 parse error messages
For string parsers, a utility to display nice error messages that includes the line number, the line, a hat to indicate the column where parsing fails, and a detailed error message.

Error:
1; 1+*   
     ^   
expected '(', or
expected a digit, or
expected 'x'

Largely inspired from (Meijer 1996) parsers

How has this been tested?

Main examples in the README.md are checked
Several example illustrate the parsers functionality
I have used this parsers combinators library on a big project.

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

Better names.

robin-aws · 2025-03-25T21:02:18Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/Parsers.dfy

+    A.AboutDrop(input, A.Length(input)-A.Length(remaining1), A.Length(remaining1)-A.Length(remaining2));
+  }
+
+  // Cannot express this predicate if Input is allocated. Add once we accept quantification over unallocated objects


You might be interested in the "proof trait" pattern I used in the Actions library: https://github.com/dafny-lang/dafny/pull/6074/files#diff-cb5145d4b584ea7656360f05c946523c48c5651815cea269b469a855844c3ed2R105

robin-aws

Just some initial thoughts based on the offline demo, will return for a more thorough review.

robin-aws · 2025-03-25T21:10:16Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/Parsers.dfy

+                        FailureData("expected a "+name, input, Option.None))
+  }
+
+  opaque function IntToString(n: int): string


Why not use the existing utilities like Std.Strings.OfInt()?

Excellent suggestion.

I remember why I did not do that. In the project that was using these parsers, I was only import Std.Wrappers and these parsers.
By using Std.Strings.OfInt(), I now need to include all these files

"Std/Strings.dfy", "Std/Arithmetic/Power.dfy", "Std/Arithmetic/Mul.dfy", "Std/Arithmetic/DivMod.dfy", "Std/Arithmetic/Logarithm.dfy", "Std/Arithmetic/Internal/DivInternals.dfy", "Std/Arithmetic/Internal/GeneralInternals.dfy", "Std/Arithmetic/Internal/ModInternals.dfy", "Std/Arithmetic/Internal/MulInternalsNonlinear.dfy", "Std/Arithmetic/Internal/ModInternalsNonlinear.dfy", "Std/Arithmetic/Internal/DivInternalsNonlinear.dfy", "Std/Arithmetic/Internal/MulInternals.dfy", "Std/Arithmetic/LittleEndianNat.dfy",

much of which is useless to my application. Looking forward being able to just enable standard libraries soon :-)

Ah sure, but as you move this code in here it will become part of the project/pre-built doo file, so there's no need for includes anywhere!

robin-aws · 2025-04-02T16:57:24Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/ParsersBuilders.dfy

+            a.e_I(b.e_I(c))  
+
+        will parse a, b, c but only return the result of `c`. */
+    function e_I<U>(other: B<U>): (p: B<U>)


How about just _I and I_, since the "e" can be inferred by the lack of "I"?

_I is not a valid user-defined Dafny identifier because it starts with underscore. I also wanted that initially. That's also why I made the e lowercase. Also, the e lowercase makes me think of the interdiction sign on the road, a bit bended :-)

Ah right, damn. I suppose you could also do '_I and I_'? :)

You could but then that means the resulting generated code will look like _q__I and I___q in most backends, and even __q__I and _I___q in Rust, which does not look as symmetrical. Plus, quotes make it hard to select the entire identifier in any regular IDE. So no, I don't think I want to add quotes in identifiers in a builder pattern.

robin-aws · 2025-04-02T17:03:08Z

Source/DafnyStandardLibraries/examples/Parsers/Tutorial.dfy

+    expect r.ParseFailure?;
+    var failureMessage := P.FailureToString(input, r);
+    expect failureMessage
+        == "Error:"           + "\n" +


You could use @"..." verbatim strings for multi-line constants in a few places.

The problem with @"..." is that indentation is treated as part of the constant, the first line requires two more characters than the remaining lines (because of the @" initial) and, because of the way Windows checks out lines, the expect would automatically fail if it expects "\r\n" instead of "\n".
The format I used above makes it possible to preserve the indentation while still having a visual about what the output should look like, and having control over all the characters.
Alternatively, I could use @" and still have the right indentation, by writing something like:

StripIdent(@" FirstLine() SecondLine()");

where strip ident would

Be a method in the standard library, somewhere?

Remove the first newline

Detect the indentation of the first line

Erase the indentation on all subsequent lines

Erase Windows' carriage return \r.

I would prefer the current approach because it does not require any special handling of the string.
I'm personally using @"" mostly for regular expressions, to avoid escaping backslashes, not to avoid newlines.

Fair that this is well out of scope for this PR at least. But those stripping utilities definitely sound like great things to add to Std.Strings in the future, so all Dafny users can get more value out of verbatim strings.

robin-aws · 2025-04-02T17:05:43Z

Source/DafnyStandardLibraries/examples/dfyconfig.toml

@@ -5,7 +5,7 @@ standard-libraries = true
 # but consumers don't have to have this option set
 # to use the standard libraries in general.
 reads-clauses-on-methods = true
-enforce-determinism = true
+#enforce-determinism = true


I don't think we should change this as it means we won't catch cases of libraries that accidentally can't be used in this mode. Is the Parsers library fundamentally non-deterministic or is this something fixable?

The good news is my PR creates a separate examples project with this off since I hit this as well: https://github.com/dafny-lang/dafny/pull/6074/files#diff-8ae9e889ff28306ca6c425716f35f7ef20201f4c15d7128363b49411e724bb3b :)

I think this was accidentally committed. Thanks for pointing it out.

robin-aws · 2025-04-02T17:07:35Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/Parsers.dfy

@@ -0,0 +1,756 @@
+abstract module Std.Parsers.AbstractInput {


Make sure you add the license header to each source file.

robin-aws · 2025-04-02T17:22:29Z

Source/DafnyStandardLibraries/src/Std/Parsers/README.md

+It's expecting a digit where it should have just accepted the end of the string. To figure out what went wrong,
+let's first define two debug functions like below - they can't be defined in the library because they have print effects. You could change the type of the output of string if you were to customize them.


This is a decent solution given the current constraints, but I definitely wish it was easier to flip on for users somehow, and it's not great that it just plain doesn't work if users have --track-print-effects on.

Would it be possible to have an alternate evaluation mode that also carries a separate debugging information type in parallel, so you could do something like:

var r, log := ApplyWithLog(p, input); print log;

(I'll know better myself how feasible that is once I review this more deeply)

I think the way we could do it would be to define a new module ParserBuildersLog that would keep track of everything like this

datatype B = B(p: Parser<(P, string)>) = { ... All operators but adding a log to it } ... All operators but taking into account the log

Then, to import these, one could simply replace import Std.Parsers.StringParsersBuilders by adding Log at the end of the last one.
However, it would have the extra hassle that it has to be maintained separately.
To avoid the separation, one would have to create another abstract module

abstract module StringBuildersAbstract refines ParserBuilders { type Returning function Extract(r: Returning): P function Combine(a: Returning, r: Returning<Q>): Returning } module StringBuilders StringBuildersAbstract { type Returning = P } module StringBuildersLog StringBuildersAbstract { type Returning = (P, string) }

Let me know if it's important for you that we do it this way.

Indeed, that solution would have a lot of overhead. I'll keep this in mind when I review the implementation to see if I can think of a simpler solution.

robin-aws

Reviewed README and examples as requested, will start reviewing the rest next week.

robin-aws · 2025-04-04T17:48:19Z

Source/DafnyStandardLibraries/src/Std/Parsers/README.md

@@ -0,0 +1,336 @@
+# Verified Parser Combinators
+
+Parser combinators in Dafny, inspired from the model (Meijer&Hutton 1996).


Hyperlink to paper perhaps?

robin-aws · 2025-04-04T17:49:11Z

Source/DafnyStandardLibraries/src/Std/Parsers/README.md

+
+This library offers two styles of functional parser combinators.
+
+- The first parsers style is a synonym for `seq<character> -> ParseResult<Result>` that supports monadic styles, is straightforward to use, but results in lots of closing parentheses.


Should that be literally char, or is character more like a type parameter here?

Source/DafnyStandardLibraries/src/Std/Parsers/README.md

robin-aws · 2025-04-04T17:51:28Z

Source/DafnyStandardLibraries/src/Std/Parsers/README.md

+
+  /** Tic tac toe using string parsers */
+  method Main() {
+    var x := OrSeq([


Consider var cell instead of var x

robin-aws · 2025-04-04T21:56:19Z

Source/DafnyStandardLibraries/examples/Parsers/ParsersTheorems.dfy

+    // A parser is valid iff for any input, it never returns a fatal error
+    // and always returns a suffix of its input


How many parsers are NOT valid? (Begs the question again of what a fatal error is)

Reformulated to:

// A parser is NeverFatal iff for any input, it never returns a fatal error // Since fatal errors occur only when a parser returns more characters than it was given, // NeverFatal means the remaining unparsed must be smaller or equal to the input

robin-aws · 2025-04-04T22:01:25Z

Source/DafnyStandardLibraries/examples/Parsers/PolynomialParser.dfy

I really like that you're showing this example with both styles of constructing parsers, but since the rest is identical, I'd say combine them into one file and just run the tests on both copies.

robin-aws · 2025-04-04T22:02:54Z

Source/DafnyStandardLibraries/examples/Parsers/Tutorial.dfy

+    expect r.ParseFailure?;
+    var failureMessage := P.FailureToString(input, r);
+    expect failureMessage
+        == "Error:"           + "\n" +


Fair that this is well out of scope for this PR at least. But those stripping utilities definitely sound like great things to add to Std.Strings in the future, so all Dafny users can get more value out of verbatim strings.

robin-aws · 2025-04-04T22:09:21Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/Parsers.dfy

+                        FailureData("expected a "+name, input, Option.None))
+  }
+
+  opaque function IntToString(n: int): string


Ah sure, but as you move this code in here it will become part of the project/pre-built doo file, so there's no need for includes anywhere!

robin-aws · 2025-04-04T22:10:55Z

Source/DafnyStandardLibraries/src/Std/Parsers/Core/ParsersBuilders.dfy

+            a.e_I(b.e_I(c))  
+
+        will parse a, b, c but only return the result of `c`. */
+    function e_I<U>(other: B<U>): (p: B<U>)


Ah right, damn. I suppose you could also do '_I and I_'? :)

Co-authored-by: Robin Salkeld <[email protected]>

MikaelMayer added 4 commits March 6, 2025 11:39

First commit

54cf8fe

Better perser performance

84569b7

Documentation for all builder constructs.

03cfd82

Better names.

Merge branch 'master' into feat-parsers-in-standard-library

9517f02

MikaelMayer requested a review from robin-aws March 7, 2025 18:52

MikaelMayer and others added 11 commits March 7, 2025 12:53

Adding missing file

9b0215c

Updated tutorial

21be4a9

Fixed proofs

808f5d9

Fixed verification

04dec19

Parsers updated and examples fixed

65cf6b3

Latest version of the standard libraries

52e69ba

Fixed the tests

49a957d

Fixed verification error

dc4d752

Merge branch 'master' into feat-parsers-in-standard-library

677fb2e

Regenerated files

ffe8d36

Fixed documentation and generation of code.

3875495

robin-aws reviewed Mar 25, 2025

View reviewed changes

robin-aws requested changes Apr 2, 2025

View reviewed changes

robin-aws reviewed Apr 4, 2025

View reviewed changes

MikaelMayer and others added 6 commits April 7, 2025 14:32

Review suggestions

0cbd64e

Apply suggestions from code review

62bac3f

Co-authored-by: Robin Salkeld <[email protected]>

Added tail recursive recursive parsers

fcff599

Merge branch 'master' into feat-parsers-in-standard-library

1e2350a

Updated libraries + formatting + new example + tail recursive

9466257

Final review remarks

5fa7d36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Verified and easy-to-use parser combinators #6143

Feat: Verified and easy-to-use parser combinators #6143

MikaelMayer commented Mar 7, 2025 •

edited

Loading

robin-aws Mar 25, 2025

robin-aws left a comment

robin-aws Mar 25, 2025

MikaelMayer Apr 2, 2025

MikaelMayer Apr 2, 2025

robin-aws Apr 4, 2025

robin-aws Apr 2, 2025

MikaelMayer Apr 2, 2025

robin-aws Apr 4, 2025

MikaelMayer Apr 18, 2025

robin-aws Apr 2, 2025

MikaelMayer Apr 2, 2025

robin-aws Apr 4, 2025

robin-aws Apr 2, 2025

MikaelMayer Apr 2, 2025

robin-aws Apr 2, 2025

robin-aws Apr 2, 2025

MikaelMayer Apr 3, 2025

robin-aws Apr 4, 2025

robin-aws left a comment

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

MikaelMayer Apr 17, 2025

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

robin-aws Apr 4, 2025

		@@ -0,0 +1,756 @@
		abstract module Std.Parsers.AbstractInput {

		It's expecting a digit where it should have just accepted the end of the string. To figure out what went wrong,
		let's first define two debug functions like below - they can't be defined in the library because they have print effects. You could change the type of the output of string if you were to customize them.

		@@ -0,0 +1,336 @@
		# Verified Parser Combinators

		Parser combinators in Dafny, inspired from the model (Meijer&Hutton 1996).


		This library offers two styles of functional parser combinators.

		- The first parsers style is a synonym for `seq<character> -> ParseResult<Result>` that supports monadic styles, is straightforward to use, but results in lots of closing parentheses.

		// A parser is valid iff for any input, it never returns a fatal error
		// and always returns a suffix of its input

Feat: Verified and easy-to-use parser combinators #6143

Are you sure you want to change the base?

Feat: Verified and easy-to-use parser combinators #6143

Conversation

MikaelMayer commented Mar 7, 2025 • edited Loading

How has this been tested?

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Mar 7, 2025 •

edited

Loading