# HG changeset patch
# User haftmann
# Date 1222186303 -7200
# Node ID a8edf4c69a79679e5f8e0df0c839d201285ff56f
# Parent  25326092cf9a15f95ff3fb8f6a91336e20ecaf19
fixed quickcheck parameter syntax

diff -r 25326092cf9a -r a8edf4c69a79 src/HOL/ex/Quickcheck_Examples.thy
--- 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
 
diff -r 25326092cf9a -r a8edf4c69a79 src/Pure/Tools/quickcheck.ML
--- 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));
+fun read_nat s = case (Library.read_int o Symbol.explode) 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 =))
+              (v, ProofContext.read_typ ctxt arg)
+        | _ => (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*)