--- a/src/HOL/ex/Quickcheck.thy Mon Sep 22 13:56:03 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Mon Sep 22 13:56:04 2008 +0200
@@ -285,99 +285,124 @@
subsection {* Examples *}
-(*lemma
- fixes n m :: nat
- shows "n + m \<le> n * m"
-;test_goal [code];
-oops*)
+theorem "map g (map f xs) = map (g o f) xs"
+ quickcheck [generator = code]
+ by (induct xs) simp_all
-ML {* val f = Quickcheck.compile_generator_expr @{theory}
- @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} *}
+theorem "map g (map f xs) = map (f o g) xs"
+ quickcheck [generator = code]
+ oops
+
+theorem "rev (xs @ ys) = rev ys @ rev xs"
+ quickcheck [generator = code]
+ by simp
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+theorem "rev (xs @ ys) = rev xs @ rev ys"
+ quickcheck [generator = code]
+ oops
+
+theorem "rev (rev xs) = xs"
+ quickcheck [generator = code]
+ by simp
+
+theorem "rev xs = xs"
+ quickcheck [generator = code]
+ oops
+
+primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "app [] x = x"
+ | "app (f # fs) x = app fs (f x)"
-ML {* val f = Quickcheck.compile_generator_expr @{theory}
- @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} *}
+lemma "app (fs @ gs) x = app gs (app fs x)"
+ quickcheck [generator = code]
+ by (induct fs arbitrary: x) simp_all
+
+lemma "app (fs @ gs) x = app fs (app gs x)"
+ quickcheck [generator = code]
+ oops
+
+primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+ "occurs a [] = 0"
+ | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "del1 a [] = []"
+ | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
+
+lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
+ -- {* Wrong. Precondition needed.*}
+ quickcheck [generator = code]
+ oops
-ML {* val f = Quickcheck.compile_generator_expr @{theory}
- @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"} *}
+lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck [generator = code]
+ -- {* Also wrong.*}
+ oops
+
+lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck [generator = code]
+ by (induct xs) auto
-ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 88 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "replace a b [] = []"
+ | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
+ else (x#(replace a b xs)))"
+
+lemma "occurs a xs = occurs b (replace a b xs)"
+ quickcheck [generator = code]
+ -- {* Wrong. Precondition needed.*}
+ oops
+
+lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
+ quickcheck [generator = code]
+ by (induct xs) simp_all
+
+
+subsection {* Trees *}
+
+datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
+
+primrec leaves :: "'a tree \<Rightarrow> 'a list" where
+ "leaves Twig = []"
+ | "leaves (Leaf a) = [a]"
+ | "leaves (Branch l r) = (leaves l) @ (leaves r)"
+
+primrec plant :: "'a list \<Rightarrow> 'a tree" where
+ "plant [] = Twig "
+ | "plant (x#xs) = Branch (Leaf x) (plant xs)"
-ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 6 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
+ "mirror (Twig) = Twig "
+ | "mirror (Leaf a) = Leaf a "
+ | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
-ML {* val f = Quickcheck.compile_generator_expr @{theory}
- @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} *}
+theorem "plant (rev (leaves xt)) = mirror xt"
+ quickcheck [generator = code]
+ --{* Wrong! *}
+ oops
+
+theorem "plant (leaves xt @ leaves yt) = Branch xt yt"
+ quickcheck [generator = code]
+ --{* Wrong! *}
+ oops
+
+datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
+ "inOrder (Tip a)= [a]"
+ | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
+
+primrec root :: "'a ntree \<Rightarrow> 'a" where
+ "root (Tip a) = a"
+ | "root (Node f x y) = f"
-ML {* val f = Quickcheck.compile_generator_expr @{theory}
- @{term "\<lambda>f k. int (f k) = k"} *}
+theorem "hd (inOrder xt) = root xt"
+ quickcheck [generator = code]
+ --{* Wrong! *}
+ oops
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
-ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+lemma "int (f k) = k"
+ quickcheck [generator = code]
+ oops
end
--- a/src/Pure/ProofGeneral/preferences.ML Mon Sep 22 13:56:03 2008 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Sep 22 13:56:04 2008 +0200
@@ -143,10 +143,10 @@
bool_pref Toplevel.debug
"debugging"
"Whether to enable debugging.",
- bool_pref Codegen.auto_quickcheck
+ bool_pref Quickcheck.auto
"auto-quickcheck"
"Whether to enable quickcheck automatically.",
- nat_pref Codegen.auto_quickcheck_time_limit
+ nat_pref Quickcheck.auto_time_limit
"auto-quickcheck-time-limit"
"Time limit for automatic quickcheck (in milliseconds).",
thm_deps_pref]
--- a/src/Pure/Tools/quickcheck.ML Mon Sep 22 13:56:03 2008 +0200
+++ b/src/Pure/Tools/quickcheck.ML Mon Sep 22 13:56:04 2008 +0200
@@ -7,16 +7,22 @@
signature QUICKCHECK =
sig
- val test_term: string option -> Proof.context -> bool -> int -> int -> term -> (string * term) list option;
+ val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+ val auto: bool ref
+ val auto_time_limit: int ref
end;
structure Quickcheck : QUICKCHECK =
struct
+(* quickcheck configuration -- default parameters, test generators *)
+
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ option };
+fun dest_test_params (Test_Params { size, iterations, default_type}) =
+ ((size, iterations), default_type);
fun mk_test_params ((size, iterations), default_type) =
Test_Params { size = size, iterations = iterations, default_type = default_type };
fun map_test_params f (Test_Params { size, iterations, default_type}) =
@@ -39,6 +45,9 @@
val add_generator = Data.map o apfst o AList.update (op =);
+
+(* generating tests *)
+
fun mk_tester_select name ctxt =
case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name
of NONE => error ("No such quickcheck generator: " ^ name)
@@ -57,6 +66,9 @@
else map_filter Exn.get_result testers
end;
+
+(* testing propositions *)
+
fun prep_test_term t =
let
val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
@@ -66,7 +78,7 @@
val frees = map dest_Free (term_frees t);
in (map fst frees, list_abs_free (frees, t)) end
-fun test_term generator_name ctxt quiet size i t =
+fun test_term ctxt quiet generator_name size i t =
let
val (names, t') = prep_test_term t;
val testers = case generator_name
@@ -96,7 +108,7 @@
let
val T' = AList.lookup (op =) insts v
|> the_default (the_default T default_T)
- in if Sign.of_sort thy (T, S) then T
+ in if Sign.of_sort thy (T, S) then T'
else error ("Type " ^ Syntax.string_of_typ_global thy T ^
" to be substituted for variable " ^
Syntax.string_of_typ_global thy T ^ "\ndoes not have sort " ^
@@ -105,13 +117,7 @@
| subst T = T;
in (map_types o map_atyps) subst end;
-fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
- | pretty_counterex ctxt (SOME cex) =
- Pretty.chunks (Pretty.str "Counterexample found:\n" ::
- map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
-
-fun test_goal generator_name quiet size iterations default_T insts i assms state =
+fun test_goal quiet generator_name size iterations default_T insts i assms state =
let
val ctxt = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -122,7 +128,16 @@
val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
|> monomorphic_term thy insts default_T
|> ObjectLogic.atomize_term thy;
- in test_term generator_name ctxt quiet size iterations gi' end;
+ in test_term ctxt quiet generator_name size iterations gi' end;
+
+fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
+ | pretty_counterex ctxt (SOME cex) =
+ Pretty.chunks (Pretty.str "Counterexample found:\n" ::
+ map (fn (s, t) =>
+ Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
+
+
+(* automatic testing *)
val auto = ref false;
val auto_time_limit = ref 5000;
@@ -136,7 +151,7 @@
fun test () =
let
val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
- (try (test_goal NONE true size iterations default_type [] 1 assms)) state;
+ (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
in
case res of
NONE => state
@@ -150,119 +165,71 @@
else state
end;
-(*val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);*)
+val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
+
+
+(* 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));
+
+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);
+
+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 test_goal_cmd generator_name i state =
- test_goal generator_name false 10 100 NONE [] i [] (Toplevel.proof_of state)
- |> pretty_counterex (Toplevel.context_of state)
- |> Pretty.writeln;
+fun quickcheck_params_cmd pos 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;
+ in
+ thy
+ |> (Data.map o apsnd o map_test_params) (Library.apply fs)
+ end;
+
+fun quickcheck_cmd pos 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 (((size, iterations), default_type), (generator_name, insts)) =
+ Library.apply fs (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
-fun read_nothing x thy = x;
-fun read_typ raw_ty thy = Syntax.read_typ_global thy raw_ty;
-
-val parse_test_param = (P.short_ident --| P.$$$ "=" #->
- (fn "size" => P.nat >> (apfst o apfst o K)
- | "iterations" => P.nat >> (apfst o apsnd o K)
- | "default_type" => P.typ >> (apsnd o K)));
-
-val parse_test_param_inst =
- P.type_ident --| P.$$$ "=" -- P.typ >> (apsnd o AList.update (op =))
- || parse_test_param >> apfst;
-
-(*fun quickcheck_test_params_cmd fs thy =
- (Data.map o apsnd o map_test_params) (Library.apply fs);*)
-
-(*val _ =
- OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
- (P.$$$ "[" |-- P.list1 parse_test_param --| P.$$$ "]" >>
- (Toplevel.theory o quickcheck_test_params_cmd));*)
+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))));
-(*
-val params =
- [("size", P.nat >> (K o set_size)),
- ("iterations", P.nat >> (K o set_iterations)),
- ("default_type", P.typ >> set_default_type)];
-
-val parse_test_params = P.short_ident :|-- (fn s =>
- P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
-
-fun parse_tyinst xs =
- (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
- fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
-
-
-*)
-
-val _ = OuterSyntax.improper_command "test_goal" "try to find counterexample for subgoal" K.diag
- (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- Scan.optional P.nat 1
- >> (fn (some_name, i) => Toplevel.no_timing o Toplevel.keep (test_goal_cmd some_name i)));
+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)));
end; (*local*)
+end;
-(*
-val _ =
- OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
- (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
- (fn fs => Toplevel.theory (fn thy =>
- map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
-
-val _ =
- OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
- (Scan.option (P.$$$ "[" |-- P.list1
- ( parse_test_params >> (fn f => fn thy => apfst (f thy))
- || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
- (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
- test_goal false (Library.apply (the_default []
- (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
- (get_test_params (Toplevel.theory_of st), [])) g [] |>
- pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
-
-val auto_quickcheck = ref false;
-val auto_quickcheck_time_limit = ref 5000;
-
-fun test_goal' int state =
- let
- val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.assms_of ctxt);
- val params = get_test_params (Proof.theory_of state);
- fun test () =
- let
- val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
- (try (test_goal true (params, []) 1 assms)) state;
- in
- case res of
- NONE => state
- | SOME NONE => state
- | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
- end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
- in
- if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
- then test ()
- else state
- end;
-*)
-
-(*
-fun value_cmd some_name modes raw_t state =
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt raw_t;
- val t' = case some_name
- of NONE => value ctxt t
- | SOME name => value_select name ctxt t;
- val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t ctxt;
- val p = PrintMode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;*)
-
-end;
-
-(*val auto_quickcheck = Quickcheck.auto;
-val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;*)
+val auto_quickcheck = Quickcheck.auto;
+val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;
--- a/src/Pure/codegen.ML Mon Sep 22 13:56:03 2008 +0200
+++ b/src/Pure/codegen.ML Mon Sep 22 13:56:04 2008 +0200
@@ -77,10 +77,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> (string * term) list option) ref
- val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
- val test_term': Proof.context -> term -> int -> term list option
- val auto_quickcheck: bool ref
- val auto_quickcheck_time_limit: int ref
+ val test_term: Proof.context -> term -> int -> term list option
val eval_result: (unit -> term) ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -918,7 +915,7 @@
val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
-fun test_term' ctxt t =
+fun test_term ctxt t =
let
val thy = ProofContext.theory_of ctxt;
val (code, gr) = setmp mode ["term_of", "test"]
@@ -950,101 +947,6 @@
val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
in ! test_fn #> (Option.map o map) snd end;
-fun test_term thy quiet sz i t =
- let
- val ctxt = ProofContext.init thy;
- val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
- error "Term to be tested contains type variables";
- val _ = null (term_vars t) orelse
- error "Term to be tested contains schematic variables";
- val frees = map dest_Free (term_frees t);
- val frees' = frees ~~
- map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
- val (code, gr) = setmp mode ["term_of", "test"]
- (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
- val s = "structure TestTerm =\nstruct\n\n" ^
- cat_lines (map snd code) ^
- "\nopen Generated;\n\n" ^ string_of
- (Pretty.block [str "val () = Codegen.test_fn :=",
- Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
- mk_let (map (fn ((s, T), s') =>
- (mk_tuple [str s', str (s' ^ "_t")],
- Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
- str "i"])) frees')
- (Pretty.block [str "if ",
- mk_app false (str "testf") (map (str o snd) frees'),
- Pretty.brk 1, str "then NONE",
- Pretty.brk 1, str "else ",
- Pretty.block [str "SOME ", Pretty.block (str "[" ::
- flat (separate [str ",", Pretty.brk 1]
- (map (fn ((s, T), s') => [Pretty.block
- [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
- str (s' ^ "_t ())")]]) frees')) @
- [str "]"])]]),
- str ");"]) ^
- "\n\nend;\n";
- val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
- fun iter f k = if k > i then NONE
- else (case (f () handle Match =>
- (if quiet then ()
- else warning "Exception Match raised in generated code"; NONE)) of
- NONE => iter f (k+1) | SOME x => SOME x);
- fun test k = if k > sz then NONE
- else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
- case iter (fn () => !test_fn k) 1 of
- NONE => test (k+1) | SOME x => SOME x);
- in test 0 end;
-
-fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state =
- let
- val thy = Proof.theory_of state;
- fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
- | strip t = t;
- val (_, (_, st)) = Proof.get_goal state;
- val (gi, frees) = Logic.goal_params (prop_of st) i;
- val gi' = ObjectLogic.atomize_term thy (map_types
- (map_type_tfree (fn p as (s, S) =>
- let val T = the_default (the_default (TFree p) default_type)
- (AList.lookup (op =) tvinsts s)
- in if Sign.of_sort thy (T, S) then T
- else error ("Type " ^ Syntax.string_of_typ_global thy T ^
- " to be substituted for variable " ^
- Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
- Syntax.string_of_sort_global thy S)
- end))
- (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
- in test_term thy quiet size iterations gi' end;
-
-fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
- | pretty_counterex ctxt (SOME cex) =
- Pretty.chunks (Pretty.str "Counterexample found:\n" ::
- map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
-
-val auto_quickcheck = ref false;
-val auto_quickcheck_time_limit = ref 5000;
-
-fun test_goal' int state =
- let
- val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.assms_of ctxt);
- val params = get_test_params (Proof.theory_of state);
- fun test () =
- let
- val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
- (try (test_goal true (params, []) 1 assms)) state;
- in
- case res of
- NONE => state
- | SOME NONE => state
- | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
- end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
- in
- if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
- then test ()
- else state
- end;
(**** Evaluator for terms ****)
@@ -1165,12 +1067,10 @@
val setup = add_codegen "default" default_codegen
#> add_tycodegen "default" default_tycodegen
#> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
- #> Quickcheck.add_generator ("SML", test_term')
+ #> Quickcheck.add_generator ("SML", test_term)
#> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
(fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
-val _ = Context.>> (Specification.add_theorem_hook test_goal');
-
val _ =
OuterSyntax.command "code_library"
"generates code for terms (one structure for each theory)" K.thy_decl
@@ -1181,37 +1081,4 @@
"generates code for terms (single structure, incremental)" K.thy_decl
(parse_code false);
-val params =
- [("size", P.nat >> (K o set_size)),
- ("iterations", P.nat >> (K o set_iterations)),
- ("default_type", P.typ >> set_default_type)];
-
-val parse_test_params = P.short_ident :|-- (fn s =>
- P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
-
-fun parse_tyinst xs =
- (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
- fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
-
-val _ =
- OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
- (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
- (fn fs => Toplevel.theory (fn thy =>
- map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
-
-val _ =
- OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
- (Scan.option (P.$$$ "[" |-- P.list1
- ( parse_test_params >> (fn f => fn thy => apfst (f thy))
- || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
- (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
- test_goal false (Library.apply (the_default []
- (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
- (get_test_params (Toplevel.theory_of st), [])) g [] |>
- pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
-
end;
-
-val auto_quickcheck = Codegen.auto_quickcheck;
-val auto_quickcheck_time_limit = Codegen.auto_quickcheck_time_limit;
-