Skip to content

feat: KMP matcher#178

Merged
digama0 merged 26 commits intoleanprover-community:mainfrom
fgdorais:kmp
Aug 26, 2023
Merged

feat: KMP matcher#178
digama0 merged 26 commits intoleanprover-community:mainfrom
fgdorais:kmp

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Jul 7, 2023

A versatile implementation of the Knuth-Morris-Pratt matching algorithm.

@fgdorais fgdorais force-pushed the kmp branch 4 times, most recently from b4ea617 to 38a3846 Compare July 7, 2023 16:36
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Jul 7, 2023

Now integrates #172

@fgdorais fgdorais marked this pull request as ready for review July 8, 2023 17:03
Copy link
Copy Markdown
Contributor

@nomeata nomeata left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! In one application of mine I would be interested in a variant of the API where I use .ofStream only once, and can then that to check containsStr multiple time. Of course I can cargo-cult the code in posOfSubstr, but maybe a convenient middle ground works well.

@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 3, 2023

Good idea! Do you think @[specialize] might be enough? Or do you absolutely need a reusable matcher type as in the Array API?

@nomeata
Copy link
Copy Markdown
Contributor

nomeata commented Aug 3, 2023

Hmm, actually, looking close at the functions you provide, I think for my needs I’d be happy with what’s there.

@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 3, 2023

I added a few things that you might find useful. This API would be a lot simpler if there was a coercion from String to Substring.

@nomeata
Copy link
Copy Markdown
Contributor

nomeata commented Aug 3, 2023

Great, thanks!

This API would be a lot simpler if there was a coercion from String to Substring.

Could there be one?

@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Aug 11, 2023
@digama0 digama0 added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Aug 15, 2023
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Aug 21, 2023
fgdorais and others added 3 commits August 20, 2023 22:38
Co-authored-by: Scott Morrison <scott@tqft.net>
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Aug 21, 2023
Copy link
Copy Markdown
Collaborator

@kim-em kim-em left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise, LGTM now.

@digama0 digama0 added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Aug 22, 2023
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Aug 22, 2023
@digama0 digama0 merged commit 8cab876 into leanprover-community:main Aug 26, 2023
fgdorais added a commit to fgdorais/batteries that referenced this pull request Oct 19, 2023
A versatile implementation of the Knuth-Morris-Pratt matching algorithm.

---------

Co-authored-by: James <jamesgallicchio@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-review This PR is ready for review; the author thinks it is ready to be merged.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants