src/HOL/Tools/Quickcheck/exhaustive_generators.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-19 wenzelm 2014-12-19 just one data slot per program unit;
2014-12-19 wenzelm 2014-12-19 proper exception for internal program failure, not user-error;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-08 blanchet 2014-09-08 use compatibility layer
2014-09-05 blanchet 2014-09-05 pretend code generation is a ctr_sugar plugin
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-03 blanchet 2014-09-03 ported Quickcheck to support new datatypes better
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-08-19 blanchet 2014-08-19 reduced dependency on 'Datatype' theory and ML module
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-11-11 haftmann 2012-11-11 dropped dead code; tuned theory text
2012-07-21 bulwahn 2012-07-21 handling partiality in the case where the equality optimisation is applied
2012-07-17 bulwahn 2012-07-17 improved equality optimisation in Quickcheck
2012-07-02 bulwahn 2012-07-02 exporting important function for the "many conjecture refutation" compilation of quickcheck
2012-05-29 bulwahn 2012-05-29 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
2012-02-21 bulwahn 2012-02-21 subtype preprocessing in Quickcheck; adding option use_subtype; tuned
2012-01-25 bulwahn 2012-01-25 generalizing check if size matters because it is different for random and exhaustive testing
2012-01-20 bulwahn 2012-01-20 tuned
2011-12-29 wenzelm 2011-12-29 comments;
2011-12-20 bulwahn 2011-12-20 exporting instantiation functions in quickcheck for their usage in abstract generators
2011-12-20 bulwahn 2011-12-20 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;
2011-12-05 bulwahn 2011-12-05 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
2011-12-05 bulwahn 2011-12-05 exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
2011-12-05 bulwahn 2011-12-05 dynamic genuine_flag in compilation of random and exhaustive
2011-12-05 bulwahn 2011-12-05 indicating where the restart should occur; making safe_if dynamic
2011-12-01 bulwahn 2011-12-01 removing catch_match' now that catch_match is polymorphic
2011-12-01 bulwahn 2011-12-01 compilations return genuine flag to quickcheck framework
2011-12-01 bulwahn 2011-12-01 the simple exhaustive compilation also indicates if counterexample is potentially spurious;
2011-12-01 bulwahn 2011-12-01 changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier
2011-12-01 bulwahn 2011-12-01 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
2011-12-01 bulwahn 2011-12-01 quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;
2011-11-30 bulwahn 2011-11-30 also potential counterexamples in the simple exhaustive testing in quickcheck
2011-11-30 bulwahn 2011-11-30 adding a exception-safe term reification step in quickcheck; adding examples
2011-11-30 bulwahn 2011-11-30 quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions
2011-11-14 bulwahn 2011-11-14 setting up exhaustive generators which are used for the smart generators
2011-11-09 bulwahn 2011-11-09 more precise messages with the tester's name in quickcheck; tuned
2011-10-17 bulwahn 2011-10-17 moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-07-18 bulwahn 2011-07-18 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
2011-07-18 bulwahn 2011-07-18 removing generator registration
2011-07-18 bulwahn 2011-07-18 parametrized test_term functions in quickcheck
2011-07-18 bulwahn 2011-07-18 adding random, exhaustive and SML quickcheck as testers
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-18 bulwahn 2011-04-18 adding bounded_forall tester
2011-04-18 bulwahn 2011-04-18 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-09 wenzelm 2011-04-09 made SML/NJ happy;
2011-04-08 bulwahn 2011-04-08 deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
2011-04-08 bulwahn 2011-04-08 generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
2011-04-08 bulwahn 2011-04-08 correcting constant name in exhaustive_generators