Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exporting function in quickcheck; adapting mutabelle script
authorbulwahn
Wed, 20 Jul 2011 08:16:36 +0200
changeset 43912 13e6a4e70219
parent 43911 a1da544e2652
child 43913 003f8c5f3e37
exporting function in quickcheck; adapting mutabelle script
src/HOL/Mutabelle/lib/Tools/mutabelle file | annotate | diff | comparison | revisions
src/Tools/quickcheck.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Jul 20 08:16:35 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Jul 20 08:16:36 2011 +0200
@@ -85,11 +85,11 @@
 
 ML {*
 val mtds = [
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"  
 (*  MutabelleExtra.nitpick_mtd *)
 ]
--- a/src/Tools/quickcheck.ML	Wed Jul 20 08:16:35 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Jul 20 08:16:36 2011 +0200
@@ -23,6 +23,7 @@
   val timeout : real Config.T
   val finite_types : bool Config.T
   val finite_type_size : int Config.T
+  val set_active_testers: string list -> Context.generic -> Context.generic
   datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
   val test_params_of : Proof.context -> test_params
isabelle