src/HOL/Tools/Quickcheck/narrowing_generators.ML
Mon, 23 Jan 2012 15:23:02 +0100 bulwahn support for Ex1 in quickcheck-narrowing
Fri, 20 Jan 2012 09:28:54 +0100 bulwahn catching code generation errors in quickcheck-narrowing
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Thu, 29 Dec 2011 15:54:37 +0100 wenzelm comments;
Tue, 20 Dec 2011 17:22:31 +0100 bulwahn generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
Thu, 15 Dec 2011 18:08:40 +0100 wenzelm clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
Mon, 05 Dec 2011 12:36:22 +0100 bulwahn making the default behaviour of quickcheck a little bit less verbose;
Mon, 05 Dec 2011 12:36:05 +0100 bulwahn inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
Mon, 05 Dec 2011 12:36:00 +0100 bulwahn renaming potential flag to genuine_only flag with an inverse semantics
Mon, 05 Dec 2011 12:35:58 +0100 bulwahn quickcheck narrowing continues searching after found a potentially spurious counterexample
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn compilations return genuine flag to quickcheck framework
Thu, 01 Dec 2011 22:14:35 +0100 bulwahn the narrowing also indicates if counterexample is potentially spurious
Wed, 30 Nov 2011 09:21:11 +0100 bulwahn quickcheck narrowing also shows potential counterexamples
Wed, 09 Nov 2011 11:35:09 +0100 bulwahn more precise messages with the tester's name in quickcheck; tuned
Wed, 09 Nov 2011 11:34:59 +0100 bulwahn quickcheck fails with code generator errors only if one tester is invoked
Wed, 09 Nov 2011 11:34:57 +0100 bulwahn removing extra arguments
Sat, 05 Nov 2011 15:00:49 +0100 wenzelm added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
Mon, 17 Oct 2011 10:19:01 +0200 bulwahn 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
Thu, 22 Sep 2011 07:26:53 +0200 bulwahn adding post-processing of terms to narrowing-based Quickcheck
Mon, 19 Sep 2011 16:18:33 +0200 bulwahn removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
Wed, 14 Sep 2011 10:24:22 +0200 noschinl create central list for language extensions used by the haskell code generator
Thu, 08 Sep 2011 12:23:11 +0200 noschinl call ghc with -XEmptyDataDecls
Tue, 06 Sep 2011 16:40:22 +0200 bulwahn avoid "Code" as structure name (cf. 3bc39cfe27fe)
Thu, 18 Aug 2011 13:37:41 +0200 noschinl do not call ghc with -fglasgow-exts
Thu, 18 Aug 2011 12:06:17 +0200 bulwahn activating narrowing-based quickcheck by default
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 20 Jul 2011 08:16:41 +0200 bulwahn removing inner time limits in quickcheck
Wed, 20 Jul 2011 08:16:35 +0200 bulwahn more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
Wed, 20 Jul 2011 08:16:33 +0200 bulwahn making messages more informative
Mon, 18 Jul 2011 13:49:26 +0200 bulwahn unactivating narrowing-based quickcheck by default
Mon, 18 Jul 2011 13:48:35 +0200 bulwahn making active configuration public in narrowing-based quickcheck
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
Sat, 16 Jul 2011 20:52:41 +0200 wenzelm moved bash operations to Isabelle_System (cf. Scala version);
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
Thu, 30 Jun 2011 13:21:41 +0200 wenzelm standardized use of Path operations;
Tue, 28 Jun 2011 14:36:43 +0200 bulwahn adding timeout to quickcheck narrowing
Tue, 14 Jun 2011 08:30:19 +0200 bulwahn quickcheck_narrowing returns some timing information
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 09:07:13 +0200 bulwahn fixing code generation test
Thu, 09 Jun 2011 08:32:19 +0200 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
Thu, 09 Jun 2011 08:32:13 +0200 bulwahn compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
Tue, 07 Jun 2011 11:11:01 +0200 bulwahn adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
Tue, 07 Jun 2011 11:10:42 +0200 bulwahn adding compilation that allows existentials in Quickcheck_Narrowing
Tue, 31 May 2011 15:45:27 +0200 bulwahn Quickcheck Narrowing only requires one compilation with GHC now
Mon, 30 May 2011 17:55:34 +0200 bulwahn improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
Mon, 30 May 2011 13:57:59 +0200 bulwahn automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 06 Apr 2011 10:58:18 +0200 bulwahn changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
Mon, 04 Apr 2011 14:44:11 +0200 bulwahn refactoring generator definition in quickcheck and removing clone
Thu, 31 Mar 2011 11:17:52 +0200 bulwahn adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
Wed, 30 Mar 2011 09:44:16 +0200 bulwahn generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
Wed, 23 Mar 2011 08:50:39 +0100 bulwahn changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
Mon, 21 Mar 2011 16:38:28 +0100 wenzelm another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn extending the test data generators to take the evaluation terms as arguments
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
less more (0) -60 tip