# HG changeset patch # User haftmann # Date 1222063226 -7200 # Node ID c24bc53c815c0699c9cbe8c4b7bb670c5f6ba814 # Parent d4396a28fb29a89beb05555d0e2151ace4bc3f98 some steps towards generic quickcheck framework diff -r d4396a28fb29 -r c24bc53c815c src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Mon Sep 22 08:00:24 2008 +0200 +++ b/src/HOL/ex/Quickcheck.thy Mon Sep 22 08:00:26 2008 +0200 @@ -244,6 +244,8 @@ structure Quickcheck = struct +open Quickcheck; + val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; fun mk_generator_expr thy prop tys = @@ -267,48 +269,30 @@ val t = fold_rev mk_bindclause bounds (return $ check); in Abs ("n", @{typ index}, t) end; -fun compile_generator_expr thy prop tys = - let - val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy - (mk_generator_expr thy prop tys) []; - in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; - -fun VALUE prop tys thy = +fun compile_generator_expr thy t = let - val t = mk_generator_expr thy prop tys; - val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t) - in - thy - |> TheoryTarget.init NONE - |> Specification.definition (NONE, (Attrib.no_binding, eq)) - |> snd - |> LocalTheory.exit - |> ProofContext.theory_of - end; + val tys = (map snd o fst o strip_abs) t; + val t' = mk_generator_expr thy t tys; + val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' []; + in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; end *} +setup {* + Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) +*} + subsection {* Examples *} -(*export_code "random :: index \ seed \ ((_ \ _) \ (unit \ term)) \ seed" - in SML file -*) - -(*setup {* Quickcheck.VALUE - @{term "\f k. int (f k) = k"} [@{typ "int \ nat"}, @{typ int}] *} - -export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML" -use "~~/../../gen_code/quickcheck.ML" -ML {* Random_Engine.run (QuickcheckExample.range 1) *}*) - -(*definition "FOO = (True, Suc 0)" - -code_module (test) QuickcheckExample - file "~~/../../gen_code/quickcheck'.ML" - contains FOO*) +(*lemma + fixes n m :: nat + shows "n + m \ n * m" +;test_goal [code]; +oops*) ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *} + @{term "\(n::nat) (m::nat) (q::nat). n = m + q + 1"} *} ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *} @@ -323,7 +307,7 @@ ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *} + @{term "\(n::int) (m::int) (q::int). n = m + q + 1"} *} ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *} @@ -341,8 +325,7 @@ ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\(xs\int list) ys. rev (xs @ ys) = rev xs @ rev ys"} - [@{typ "int list"}, @{typ "int list"}] *} + @{term "\(xs\int list) ys. rev (xs @ ys) = rev xs @ rev ys"} *} ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *} @@ -373,7 +356,7 @@ ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\(s \ string). s \ rev s"} [@{typ string}] *} + @{term "\(s \ string). s \ rev s"} *} ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *} @@ -388,7 +371,7 @@ ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* val f = Quickcheck.compile_generator_expr @{theory} - @{term "\f k. int (f k) = k"} [@{typ "int \ nat"}, @{typ int}] *} + @{term "\f k. int (f k) = k"} *} ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *} ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *} diff -r d4396a28fb29 -r c24bc53c815c src/Pure/Tools/quickcheck.ML --- a/src/Pure/Tools/quickcheck.ML Mon Sep 22 08:00:24 2008 +0200 +++ b/src/Pure/Tools/quickcheck.ML Mon Sep 22 08:00:26 2008 +0200 @@ -7,38 +7,247 @@ signature QUICKCHECK = sig - (*val test: Proof.context -> int -> int -> term -> (string * term) list option - val test_select: string -> Proof.context -> int -> int -> term -> (string * term) list option - val test_cmd: string option -> string list -> string -> Toplevel.state -> unit*) + val test_term: string option -> Proof.context -> bool -> int -> int -> term -> (string * term) list option; val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory end; structure Quickcheck : QUICKCHECK = struct -structure Generator = TheoryDataFun( - type T = (string * (Proof.context -> term -> int -> term list option)) list; - val empty = []; +datatype test_params = Test_Params of + { size: int, iterations: int, default_type: typ option }; + +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}) = + mk_test_params (f ((size, iterations), default_type)); +fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1}, + Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) = + mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), + case default_type1 of NONE => default_type2 | _ => default_type1); + +structure Data = TheoryDataFun( + type T = (string * (Proof.context -> term -> int -> term list option)) list + * test_params; + val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE }); val copy = I; val extend = I; - fun merge pp = AList.merge (op =) (K true); + fun merge pp ((generators1, params1), (generators2, params2)) = + (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2), + merge_test_params (params1, params2)); ) -val add_generator = Generator.map o AList.update (op =); +val add_generator = Data.map o apfst o AList.update (op =); + +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) + | SOME generator => generator ctxt; + +fun mk_testers ctxt t = + (map snd o fst o Data.get o ProofContext.theory_of) ctxt + |> map_filter (fn generator => try (generator ctxt) t); + +fun mk_testers_strict ctxt t = + let + val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt) + val testers = map (fn generator => Exn.capture (generator ctxt) t) generators; + in if forall (is_none o Exn.get_result) testers + then [(Exn.release o snd o split_last) testers] + else map_filter Exn.get_result testers + end; + +fun prep_test_term t = + let + 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); + in (map fst frees, list_abs_free (frees, t)) end -(*fun value_select name ctxt = - case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name - of NONE => error ("No such evaluator: " ^ name) - | SOME f => f ctxt; +fun test_term generator_name ctxt quiet size i t = + let + val (names, t') = prep_test_term t; + val testers = case generator_name + of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' + | SOME name => [mk_tester_select name ctxt t']; + fun iterate f 0 = NONE + | iterate f k = case f () handle Match => (if quiet then () + else warning "Exception Match raised during quickcheck"; NONE) + of NONE => iterate f (k - 1) | SOME q => SOME q; + fun with_testers k [] = NONE + | with_testers k (tester :: testers) = + case iterate (fn () => tester k) i + of NONE => with_testers k testers + | SOME q => SOME q; + fun with_size k = if k > size then NONE + else (if quiet then () else priority ("Test data size: " ^ string_of_int k); + case with_testers k testers + of NONE => with_size (k + 1) | SOME q => SOME q); + in case with_size 1 + of NONE => NONE + | SOME ts => SOME (names ~~ ts) + end; + +fun monomorphic_term thy insts default_T = + let + fun subst (T as TFree (v, S)) = + 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 + 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 " ^ + Syntax.string_of_sort_global thy S) + end + | 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 = + let + val ctxt = Proof.context_of state; + 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' = 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; + +val auto = ref false; +val auto_time_limit = ref 5000; -fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt) - in if null evaluators then error "No evaluators" - else let val (evaluators, (_, evaluator)) = split_last evaluators - in case get_first (fn (_, f) => try (f ctxt) t) evaluators - of SOME t' => t' - | NONE => evaluator ctxt t - end end; +fun test_goal_auto int state = + let + val ctxt = Proof.context_of state; + val assms = map term_of (Assumption.assms_of ctxt); + val Test_Params { size, iterations, default_type } = + (snd o Data.get o Proof.theory_of) state; + fun test () = + let + val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit)) + (try (test_goal NONE true size iterations default_type [] 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 andalso not (!Toplevel.quiet) + then test () + else state + end; + +(*val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);*) + +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; + +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 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))); + +end; (*local*) + + + +(* +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; @@ -53,15 +262,7 @@ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end;*) -(*local structure P = OuterParse and K = OuterKeyword in - -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; +end; -val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag - (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term - >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep - (value_cmd some_name modes t))); - -end; (*local*)*) - -end; +(*val auto_quickcheck = Quickcheck.auto; +val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;*) diff -r d4396a28fb29 -r c24bc53c815c src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Sep 22 08:00:24 2008 +0200 +++ b/src/Pure/codegen.ML Mon Sep 22 08:00:26 2008 +0200 @@ -78,6 +78,7 @@ 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 eval_result: (unit -> term) ref @@ -917,6 +918,38 @@ val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); +fun test_term' ctxt t = + let + val thy = ProofContext.theory_of ctxt; + val (code, gr) = setmp mode ["term_of", "test"] + (generate_code_i thy [] "Generated") [("testf", t)]; + val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t); + val frees' = frees ~~ + map (fn i => "arg" ^ string_of_int i) (1 upto length frees); + 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 + 1)"])) 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; + in ! test_fn #> (Option.map o map) snd end; + fun test_term thy quiet sz i t = let val ctxt = ProofContext.init thy; @@ -1132,6 +1165,7 @@ 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') #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));