Draft
Conversation
This is an implementation of Rocq "quickchick" style constrained generation: for a given inductive predicate `P` over an inductive type `T`, one can derive an `ArbitrarySuchThat` instance, which gives a `Gen (Option T)` capable of generating elements of `T` which always satisfy `P`.
…tances for GenError.
* Schedule Enumeration Working Draft and LazyList made Productive * Hooking in new schedule enumeration, buggy * Efficient schedule enumeration hooked in * Resolving universe constraint error in checker by adding Unit type annotations in checkerBacktrack derivation. * Updated test cases to make them less fragile in the face of changing schedules * Ready for merge, test errors fixed or suppressed * Cleaned up printed messages * Cleaned up unused functions and commented out code, and turned <- into proper arrows * Turned λ into fun * Undo mistaken change to enumerator fuel cap (needed later) and regexp example, and removing unnessecary error log * Suppress result of trying regex enumerator * Responding to comments on merge, cleanup --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
) * Enumeration exponentially improved by only including each enumerator once when combining enumerators with enumerate, and remove fuel cap on enumerations * Cleanup some mistakes from using an older commit * Remove outdated comment on min in enumeration and add test checking that the size of enumeration is appropriate when some branches fail. --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
…sisExp (#7) * Take the WHNF of expressions before turning them into a HypothesisExp. * Nix some stale examples. * Further example cleanup.
…or Literals * feat: Major pruning of equivalent schedules in enumeration using SCC; Supporting Literals; Bugfix (#17) * chore: Turn warnings into trace calls * chore: Well typed cedar test, now works --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
* feat: Partial Order Reduction Major Improvement * chore: fixing typos and adding comment to LazyList.range --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
And make it more flexible: we take in a term of the form (fun x y z .. => exists w, P x y w) and run the elaborator to get somewhat more robust parsing. We now error if an argument to P is not a variable, which we probably wanted to do anyway.
* fix: Function calls in constructor types now supported correctly * Remove dead code and fix name of exprToConstructorExpr * chore: Minor refactors and fixes (biggest being factoring out schedule score) * chore: Added comment describing TyCtor --------- Co-authored-by: Cody Roux <cody.roux@gmail.com> Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
…bug (#45) * fix: type variables should not be linearized * fix: Unknowns generated for multiple flattened functions now have distinct names --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
* feat: Inductive families with Type arguments supported in generator/enum/checker derivation * chore: removing commented code and making targetType underscored as it is unused * chore: Removed commented code and unnecessary import and added doc string * fix: Correctly use Arbitrary for Generator Type arguments and Enum for Enumerator Type arguments --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
* feat: Branch and bound optimizations in schedule enumeration * chore: removing dead code and privating definitions * chore: Replaced $ with <| and made laziness test less inefficient upon failure --------- Co-authored-by: Segev Elazar Mittelman <segevem@amazon.com>
* Pass around constructor names for less cryptic error messages. * chore: make index error message a bit nicer. * chore: minor doc cleanup.
…Add an instance for decidable predicates. (#58)
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
2 participants
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 implements the Chamelean functionality for deriving generators for types
Tconstrained by inductive predicatesP : T -> Prop(or more complex ones).This roughly implements a backtracking search based on unification, guided by the constraints in the constructors of
P.The user interface is a
derive_generatorcommand, which takes syntax of the formwhere all the
param_iandouptutare variables, andPis an inductive family. The form of the constructors ofPis also constrained, only constants, variables and applications are allowed (which to an extent is a silly syntactic restriction).I think this feature is best presented as a "use at your own risk" in progress feature, if it were to be merged in its current state.
There are many issues, for the known ones see here: https://github.com/codyroux/plausible/issues