| Tue, 07 Jun 2011 11:11:01 +0200 |
bulwahn |
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:10:42 +0200 |
bulwahn |
adding compilation that allows existentials in Quickcheck_Narrowing
|
file |
diff |
annotate
|
| Tue, 31 May 2011 15:45:27 +0200 |
bulwahn |
Quickcheck Narrowing only requires one compilation with GHC now
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:55:34 +0200 |
bulwahn |
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 10:58:18 +0200 |
bulwahn |
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
|
file |
diff |
annotate
|
| Mon, 04 Apr 2011 14:44:11 +0200 |
bulwahn |
refactoring generator definition in quickcheck and removing clone
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:17:52 +0200 |
bulwahn |
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 08:50:39 +0100 |
bulwahn |
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
|
file |
diff |
annotate
|
| Mon, 21 Mar 2011 16:38:28 +0100 |
wenzelm |
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending the test data generators to take the evaluation terms as arguments
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding size as static argument in quickcheck_narrowing compilation
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 12:34:10 +0100 |
bulwahn |
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 19:27:39 +0100 |
wenzelm |
slightly more robust bash exec, which fails on empty executable;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 19:16:19 +0100 |
wenzelm |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:30:02 +0100 |
wenzelm |
proper File.shell_path;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 14:51:38 +0100 |
wenzelm |
allow spaces in executable names;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 13:53:54 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
renaming tester from lazy_exhaustive to narrowing
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adapting Main file generation for Quickcheck_Narrowing
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adapting Quickcheck_Narrowing and example file to new names
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
renaming lazysmallcheck ML file to Quickcheck_Narrowing
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
|
file |
diff |
annotate
| base
|