Derive ArbitrarySuchThat instances using Unification Algorithm from GGG + Generator Schedules from TT#27
Merged
ngernest merged 197 commits intometaprogrammingfrom Aug 7, 2025
Merged
Conversation
…of Strings as args
…chedule-based backend
ArbitrarySuchThat instances using Unification Algorithm from GGG + Generator Schedules from TT
This was referenced Aug 7, 2025
Merged
ngernest
added a commit
that referenced
this pull request
Aug 12, 2025
…ary` instances (#35) * chore: bump toolchain to v4.19.0 * chore: add #guard_msgs to noisy test * chore: add #guard_msgs to noisy test * chore: bump toolchain to v4.20.0-rc1 * chore: bump toolchain to v4.20.0-rc2 * chore: bump toolchain to v4.20.0 * chore: bump toolchain to v4.21.0-rc1 (#26) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.21.0-rc1 --------- Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump toolchain to v4.21.0-rc2 (#27) * chore: bump toolchain to v4.21.0-rc3 (#28) * chore: bump toolchain to v4.21.0 * chore: bump toolchain to v4.22.0-rc1 (#30) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc1 * chore: bump toolchain to v4.22.0-rc2 (#31) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc2 * chore: bump toolchain to v4.22.0-rc3 (#32) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc3 * chore: bump toolchain to v4.22.0-rc4 (#34) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc4 * Derive Arbitrary instances for algebraic data types * Only import linter from Batteries in Testable.lean * Specialize imports (avoid importing Lean directly) * Remove .DS_Store from .gitignore * Remove comment from Plausible.lean * Avoid thunking sub-generators * Update snapshot tests (sub-generators no longer thunked & are now explicitly parenthesized) * Remove mention of "simple inductive types" Co-authored-by: Kyle Miller <kmill31415@gmail.com> * Replace command elaborator with trace class * Update snapshot tests to use trace class instead of command elaborator * Update module docs following Kyle's suggestions * Remove deprecated command elaborator from nolints.json * Remove unused function * Rename ArbitrarySized to ArbitraryFueled following Eric's suggestion * Remove global constants in Idents file * Update snapshot tests to use size' + 1 instead of Nat.succ size' * Rename size function parameter in derived generators to fuel * Add counterexample property to Tree snapshot test * Add module docs for Tree snapshot test * Add counterexample property to Regular Expression snapshot test * Add counterexample property for STLC snapshot test * Add counterexample property for structure test * Fix typo in tests * Add counterexample property for Binop generator test * Add counterexample property for Value generator test * Remove unnecessary equality check for booleans * Add counterexample property for BitVec generator test * Emit error message when target type has no non-recursive constructors * Formatting in Random.lean * Refactor to use same logic as Deriving Repr (handle parameterized types + mutually inductive types) * Update snapshot tests * Add implicit parameters to derived generator for parameterized types * Update tests based on changes to accomodate parameterized types * Add docstrings to make linter happy * Handle mutually recursive types (need to add local let-definitions for Arbitrary instances) * Add snapshot test for mutually recursive types * Add counterexample property for mutually inductive type test * Improve shrinkers for trees * For parameterized types, ArbitraryFueled instances should have inst-implicit Arbitrary binders * Add counterexample property for parameterized type test * Remove Idents file, use Core.mkFreshUserName to produce fresh names instead * Remove mkLetBind (just create let-bind exprs directly using quotations) * Remove mkMatch combinators, just create match-exprs using quotations * Remove TSyntaxCombinators file, combinators are no longer used * Remove unnecessary if-condition * Refactor: move logic for setting ctorIsRecursive flag * Simplify logic for determining if constructors are recursive, remove Utils.lean * Remove spurious instance loop involving SampleableExt -> Arbitrary -> SampleableExt * Simplify logic for parenthesizing sub-generators * Loop fusion when computing sub-generator weights * Clean up nolints.json * Add newline * Replace all instances of LocalContext.getUnusedName w/ Core.mkFreshUserName * Remove mentions of Enum in README * Remove Enum mention * Remove linter & dependency on Batteries * Remove scripts/nolints.json * Fix typo in regular expression test docstring * Moving around definitions so that STLC tests compile * Remove duplicate Arbitrary file, move around definitions some more * Remove mentions of outdated command elaborator #derive_arbitrary in README --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains a rewrite of Chamelean's backend using the unification algorithm described in Generating Good Generators for Inductive Relations (GGG) and the generator schedules from Testing Theorems, Fully Automatically (TT).
We implement the schedule derivation algorithm from TT, but we use a naive well-formed schedule (without any schedule optimizations) for now.
The command
#derive_generatorhas been updated to use this new backend -- there should not be any visible changes in terms of end-user interaction.This PR also addresses most of the outstanding issues re: variable renaming.
Code overview:
UnificationMonad.lean: The unification monad from Fig. 2 of GGG (calledUnifyMin our implementation)UnifyMcombines theState,OptionandMetaMmonads (the latter is Lean's metaprogramming monad, needed for producing terms + error reporting)Schedules.lean: Type definitions for generator schedules, as described in Testing TheoremsDeriveSchedules.lean: Algorithm for deriving generator schedules, as described in Testing TheoremsDeriveScheduledGenerator.lean: Algorithm for deriving constrained generators using the aforementioned unification algorithm & generator schedulesMExp.lean: An intermediate representation for monadic expressions (MExp), used when compiling schedules to Lean codeOther remarks: