# HG changeset patch # User haftmann # Date 1222084564 -7200 # Node ID d3cf88fe77bc14a904679cc353c23e0d189e640b # Parent 053419cefd3cd83a69e9fb64e2a11ba3e12ce166 generic quickcheck framework diff -r 053419cefd3c -r d3cf88fe77bc src/HOL/ex/Quickcheck.thy --- 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 \ 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 "\(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 \ 'a) list \ 'a \ 'a" where + "app [] x = x" + | "app (f # fs) x = app fs (f x)" -ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\(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 \ 'a list \ 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 \ 'a list \ '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 "\(xs\int list) ys. rev (xs @ ys) = rev xs @ rev ys"} *} +lemma "xs ~= [] \ Suc (occurs a (del1 a xs)) = occurs a xs" + quickcheck [generator = code] + -- {* Also wrong.*} + oops + +lemma "0 < occurs a xs \ 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 \ 'a \ 'a list \ '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 \ a=b \ 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 \ 'a list" where + "leaves Twig = []" + | "leaves (Leaf a) = [a]" + | "leaves (Branch l r) = (leaves l) @ (leaves r)" + +primrec plant :: "'a list \ '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 \ '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 "\(s \ string). s \ 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 \ 'a list" where + "inOrder (Tip a)= [a]" + | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" + +primrec root :: "'a ntree \ 'a" where + "root (Tip a) = a" + | "root (Node f x y) = f" -ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\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 diff -r 053419cefd3c -r d3cf88fe77bc src/Pure/ProofGeneral/preferences.ML --- 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] diff -r 053419cefd3c -r d3cf88fe77bc src/Pure/Tools/quickcheck.ML --- 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; diff -r 053419cefd3c -r d3cf88fe77bc src/Pure/codegen.ML --- 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; -