Skip to content

feat: add a backtrack combinator to Gen.#53

Merged
hargoniX merged 2 commits intoleanprover-community:mainfrom
codyroux:backtrack-combinator
Dec 16, 2025
Merged

feat: add a backtrack combinator to Gen.#53
hargoniX merged 2 commits intoleanprover-community:mainfrom
codyroux:backtrack-combinator

Conversation

@codyroux
Copy link
Contributor

@codyroux codyroux commented Dec 5, 2025

Because we are in meta, we now need to add an inhabited instance to Gen before defining recursive functions which is possible with exceptions.

Backtracking is only useful when generators can fail, but this is quite useful in "guess and check" situations. There may be some redundancy with functionality provided later in Testable.

I've also made pick public since it can be quite useful.

Copy link
Collaborator

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

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

Looks reasonable to me, I'll wait on Sebastian's remark regarding meta to merge.

One thing: What's the idea behind calling this combinator backtrack? It doesn't really feel like there is backtracking going on to me?

@codyroux
Copy link
Contributor Author

codyroux commented Dec 8, 2025

The tryCatch at line 153 (would this be nicer as a try ... catch ...?) is doing the actual backtracking, trying a given generator, dropping it from the pool if it fails, and retrying with the remaining generators.

@codyroux
Copy link
Contributor Author

codyroux commented Dec 8, 2025

I guess whether this is "actual" backtracking can be debated.

@codyroux
Copy link
Contributor Author

Oops, @hargoniX I noticed that backtrack was only polymorphic at Type 0. Fixed now but you might want to take a second glance.

@hargoniX hargoniX merged commit ad75dc5 into leanprover-community:main Dec 16, 2025
1 check passed
@codyroux codyroux deleted the backtrack-combinator branch December 16, 2025 23:20
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