author haftmann Tue, 23 Sep 2008 18:11:43 +0200 changeset 28336 a8edf4c69a79 parent 28335 25326092cf9a child 28337 93964076e7b8
fixed quickcheck parameter syntax
 src/HOL/ex/Quickcheck_Examples.thy file | annotate | diff | comparison | revisions src/Pure/Tools/quickcheck.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Sep 23 18:11:42 2008 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Tue Sep 23 18:11:43 2008 +0200
@@ -20,27 +20,27 @@
subsection {* Lists *}

theorem "map g (map f xs) = map (g o f) xs"
-  quickcheck []
+  quickcheck
oops

theorem "map g (map f xs) = map (f o g) xs"
-  quickcheck []
+  quickcheck
oops

theorem "rev (xs @ ys) = rev ys @ rev xs"
-  quickcheck []
+  quickcheck
oops

theorem "rev (xs @ ys) = rev xs @ rev ys"
-  quickcheck []
+  quickcheck
oops

theorem "rev (rev xs) = xs"
-  quickcheck []
+  quickcheck
oops

theorem "rev xs = xs"
-  quickcheck []
+  quickcheck
oops

text {* An example involving functions inside other data structures *}
@@ -50,11 +50,11 @@
| "app (f # fs) x = app fs (f x)"

lemma "app (fs @ gs) x = app gs (app fs x)"
-  quickcheck []
+  quickcheck
by (induct fs arbitrary: x) simp_all

lemma "app (fs @ gs) x = app fs (app gs x)"
-  quickcheck []
+  quickcheck
oops

primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -68,16 +68,16 @@
text {* A lemma, you'd think to be true from our experience with delAll *}
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
-- {* Wrong. Precondition needed.*}
-  quickcheck []
+  quickcheck
oops

lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck []
+  quickcheck
-- {* Also wrong.*}
oops

lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck []
+  quickcheck
by (induct xs) auto

primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -86,12 +86,12 @@
else (x#(replace a b xs)))"

lemma "occurs a xs = occurs b (replace a b xs)"
-  quickcheck []
+  quickcheck
-- {* Wrong. Precondition needed.*}
oops

lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
-  quickcheck []
+  quickcheck
by (induct xs) simp_all

@@ -114,12 +114,12 @@
| "mirror (Branch l r) = Branch (mirror r) (mirror l)"

theorem "plant (rev (leaves xt)) = mirror xt"
-  quickcheck []
+  quickcheck
--{* Wrong! *}
oops

theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
-  quickcheck []
+  quickcheck
--{* Wrong! *}
oops

@@ -134,7 +134,7 @@
| "root (Node f x y) = f"

theorem "hd (inOrder xt) = root xt"
-  quickcheck []
+  quickcheck
--{* Wrong! *}
oops
```
```--- a/src/Pure/Tools/quickcheck.ML	Tue Sep 23 18:11:42 2008 +0200
+++ b/src/Pure/Tools/quickcheck.ML	Tue Sep 23 18:11:43 2008 +0200
@@ -170,61 +170,62 @@

(* Isar interfaces *)

-val arg_nat = Args.name #-> (fn s => case (Library.read_int o Symbol.explode) s
- of (k, []) => if k >= 0 then pair k
-      else Scan.fail ("Not a natural number: " ^ s)
-  | (_, _ :: _) => Scan.fail ("Not a natural number: " ^ s));
+ of (k, []) => if k >= 0 then k
+      else error ("Not a natural number: " ^ s)
+  | (_, _ :: _) => error ("Not a natural number: " ^ s);

-val parse_test_param =
-  Scan.lift (Args.\$\$\$ "size" -- Args.\$\$\$ "=" |-- arg_nat) >> (apfst o apfst o K)
-  || Scan.lift (Args.\$\$\$ "iterations" -- Args.\$\$\$ "=" |-- arg_nat) >> (apfst o apsnd o K)
-  || Scan.lift (Args.\$\$\$ "default_type" -- Args.\$\$\$ "=") |-- Args.typ >> (apsnd o K o SOME);
+fun parse_test_param ctxt ("size", arg) =
+      (apfst o apfst o K) (read_nat arg)
+  | parse_test_param ctxt ("iterations", arg) =
+      (apfst o apsnd o K) (read_nat arg)
+  | parse_test_param ctxt ("default_type", arg) =
+      (apsnd o K o SOME) (ProofContext.read_typ ctxt arg)
+  | parse_test_param ctxt (name, _) =
+      error ("Bad test parameter: " ^ name);

-val parse_test_param_inst =
-  Scan.lift (Args.\$\$\$ "generator" -- Args.\$\$\$ "=" |-- Args.name)
-      >> (apsnd o apfst o K o SOME)
-  || parse_test_param >> apfst
-  || Args.tyname --| Scan.lift (Args.\$\$\$ "=") -- Args.typ
-      >> (apsnd o apsnd o AList.update (op =));
+fun parse_test_param_inst ctxt ("generator", arg) =
+      (apsnd o apfst o K o SOME) arg
+  | parse_test_param_inst ctxt (name, arg) =
+      case try (ProofContext.read_typ ctxt) name
+       of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
+        | _ => (apfst o parse_test_param ctxt) (name, arg);

-fun quickcheck_params_cmd pos args thy =
+fun quickcheck_params_cmd args thy =
let
val ctxt = ProofContext.init thy;
-    val src = Args.src (("quickcheck_params", args), pos);
-    val (fs, _) = Args.context_syntax "quickcheck_params"
-      (Scan.repeat parse_test_param) src ctxt;
+    val f = fold (parse_test_param ctxt) args;
in
thy
-    |> (Data.map o apsnd o map_test_params) (Library.apply fs)
+    |> (Data.map o apsnd o map_test_params) f
end;

-fun quickcheck_cmd pos args i state =
+fun quickcheck_cmd args i state =
let
val prf = Toplevel.proof_of state;
val thy = Toplevel.theory_of state;
val ctxt = Toplevel.context_of state;
val default_params = (dest_test_params o snd o Data.get) thy;
-    val src = Args.src (("quickcheck", args), pos);
-    val (fs, _) = Args.context_syntax "quickcheck"
-      (Scan.repeat parse_test_param_inst) src ctxt;
+    val f = fold (parse_test_param_inst ctxt) args;
val (((size, iterations), default_type), (generator_name, insts)) =
-      Library.apply fs (default_params, (NONE, []));
+      f (default_params, (NONE, []));
val counterex = test_goal false generator_name size iterations
default_type insts i [] prf;
in (Pretty.writeln o pretty_counterex ctxt) counterex end;

local structure P = OuterParse and K = OuterKeyword in

+val parse_arg = P.name --| P.\$\$\$ "=" -- P.name;
+val parse_args = P.\$\$\$ "[" |-- P.list1 parse_arg --| P.\$\$\$ "]"
+  || Scan.succeed [];
+
val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
-  (P.\$\$\$ "[" |-- P.position (OuterParse.enum "," Args.parse) --| P.\$\$\$ "]"
-    >> (fn (args, pos) => Toplevel.theory
-         (quickcheck_params_cmd pos (flat args))));
+  (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));

val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag
-  (P.position (Scan.optional (P.\$\$\$ "[" |-- OuterParse.enum "," Args.parse --| P.\$\$\$ "]") [])
-    -- Scan.optional P.nat 1
-    >> (fn ((args, pos), i) => Toplevel.no_timing o Toplevel.keep
-          (quickcheck_cmd pos (flat args) i)));
+  (parse_args -- Scan.optional P.nat 1
+    >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));

end; (*local*)
```