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.
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
authorbulwahn
Tue, 18 Oct 2011 15:27:17 +0200
changeset 45165 f4896c792316
parent 45164 13dddf30c792
child 45166 861ab6f9eb2b
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
src/HOL/Mutabelle/lib/Tools/mutabelle file | annotate | diff | comparison | revisions
src/HOL/Mutabelle/mutabelle_extra.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Tue Oct 18 11:59:03 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Tue Oct 18 15:27:17 2011 +0200
@@ -89,10 +89,11 @@
 val mtds = [
   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 [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
+  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
   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\"  
+    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
 (*  MutabelleExtra.nitpick_mtd *)
 ]
 *}
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 18 11:59:03 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 18 15:27:17 2011 +0200
@@ -321,7 +321,8 @@
   in
     can (TimeLimit.timeLimit (seconds 2.0)
       (Quickcheck.test_terms
-        ((Config.put Quickcheck.finite_types true #>
+        ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
+          Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.finite_type_size 1 #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
isabelle